Move Float16 Prelude off the Double primitive

[isomorphisms]

Historical stack tip above #48. Its GitHub base is still fix/float16-bootstrap-totality; #48 is closed as superseded, so this PR is not yet based on current Idriç.

This removes the inherited wide floating primitive from Prelude.Float16 itself rather than merely wrapping its division operations in assert_total.

Boundary

• restore the compiler's existing internal primitive Float path as implementation substrate;
• carry Float16 values in primitive Float, not Double;
• perform the binary16 quantizer and +, -, *, / through prim__*_Float;
• avoid introducing a new Float→Integer primitive during bootstrap: round-to-nearest-even uses a fixed-depth binary search with the already-supported Integer→Float cast;
• avoid decimal constants inside Prelude.Float16, so that module does not need the inherited double-literal conversion path internally;
• format Float16 for Show directly from the primitive-Float carrier instead of casting back to Double;
• keep the explicit binary16 rounding boundary after construction and basic arithmetic.

The CI guard fails if Prelude.Float16 contains the token Double, regresses to a Float→Integer primitive, or loses the primitive-Float/Float16 path. edric007 also executes primitive Float arithmetic without decimal/Double literals before checking the binary16 rounding regression.

Ordinary .idr compatibility with inherited Double is deliberately unchanged. This does not yet claim that Float16 is a native core primitive or that every backend has native half-precision instructions; the current primitive Float substrate is the intermediate representation below the Prelude, while source-visible Float16 arithmetic still rounds to binary16.

Downstream Wegert evidence

The hosted Wegert probe already exercised an earlier #49 head, 9cfc0ae20f2367b1359d47f4fa3b19b00284b064, against shader backend a855d89ab0f25025d825afdc194f492e4c00ecff with mediump.

That exact tuple passed:

• hosted x86_64 prerequisites;
• existing handwritten Wegert GLSL validation;
• Wegert x86 C fallback;
• Edric bootstrap;
• Edric compiler API installation;
• GLSL backend build against Edric;
• full ordinary .idr 64-zero/64-pole Wegert compilation;
• generated GLSL validation/link.

Its first real failure came later in the actual .idric path: Float16 versus Double in Shader.Source, followed by unsupported shader entry type Float16 in the GLSL signature layer. That is useful separation: removing Double from this Prelude does not break the compiler/API bridge; it exposes the next shader-source/type boundary.

ICK remains outside this hosted path.

Current-head receipt

Exact head 3aa3a84d07856aab098582d13dec3841efc68b4c has a green bootstrap + edric007 receipt in Edric wrapper run 33315887705, job source-profile:

• the no-Double source guard passed;
• make bootstrap SCHEME=scheme reached bootstrap stage 2 complete;
• make test only=idris2/basic/edric007 reported idris2/basic/edric007: success and 1/1 tests successful.

An independent pinned-Chez reproduction of this exact head also completed the two-stage bootstrap and all focused handoff tests edric001 through edric007.

The separate Bootstrap run 33315887702 did not reject the Float changes. Its initialise job requested retired ubuntu-20.04, acquired no runner, produced no steps or logs, and was cancelled after 24 hours; the dependent bootstrap job was consequently skipped.

Remaining boundaries

• RefC successfully compiles and executes the Float16 rounding and decimal probes.
• Node code generation is not yet a valid Float target: compiling the primitive-Float probe reaches INTERNAL ERROR: invalid cast: Integer -> Float. That portability boundary is not covered by the Chez receipt above.
• The PR remains stacked on the closed Fix Float16 bootstrap totality through carrier division #48 base rather than current Idriç; retarget/reconciliation is still required before merge.

[isomorphisms]

Classification: NEEDS_REBASE_OR_RETARGET.

Receipt correction: exact head 3aa3a84d07856aab098582d13dec3841efc68b4c is PASS for the PR's Chez bootstrap + edric007 contract. Edric wrapper run 33315887705, job source-profile, passed the no-Double guard, reached bootstrap stage 2 complete, then reported idris2/basic/edric007: success and 1/1 tests successful. A separate pinned-Chez reproduction also passed edric001–edric007.

The cancelled Bootstrap run 33315887702 is infrastructure-only: initialise requested retired ubuntu-20.04, acquired no runner, has no steps/logs, and was cancelled at 24 hours; GitHub then skipped its dependent bootstrap job.

The Float16 implementation is coherent on the exercised Chez path, and the same rounding/decimal probes compile and run under RefC. The uncovered code boundary is Node: its code generator rejects Integer -> Float with an internal error. That is not a failure of the recorded Chez receipt, but it prevents claiming backend-wide Float support.

Merge is still blocked independently because this PR's base is fix/float16-bootstrap-totality (closed #48 stack), not current Idriç.