R3 gate #67: numeric construction demonstration

dsl/std/float.dag

@@ -1,9 +1,9 @@
 // std/float.dag -- Floating-point types as algebraic compositions.
 //
-// Fixed-width floats are width refinements of a single approximate-float
-// algebra axis (`Ieee754Float`) composed with `MachineWidth<Word*>` (R3 §1.8
-// gate #19 `numeric_aliases_align_to_refinements`). IEEE 754 rounding still
-// breaks pure field laws — approximate semantics remain Grounding's concern.
+// Fixed-width floats are compatibility aliases for fixed-width reals:
+// `Float<N> = Real<N> = Compose<Real, MachineWidth<Word*>>` (R3 §1.8 gate #67
+// `numeric_construction_demonstration`). IEEE 754 rounding still breaks pure
+// field laws — approximate semantics remain Grounding's concern.
 //
 // T-Numeric-Construction / R3 gate #17 — abstract `Real` (construction-chain
 // layer 5). Spelling per
@@ -21,17 +21,24 @@ import std.integer { Int }
 import std.machine_constraints { Compose, MachineWidth }
 import v3.std.approximate_field { ApproximateField }
 
-// Opaque substrate carrier for the IEEE-754 approximate-float algebra axis
-// (width-independent at this layer; specialization via Compose).
+// Opaque compatibility carrier for older Float<N> receipts. The construction
+// chain authority below is `Real`; fixed-width public aliases route through
+// Real<N>-shaped Compose rows.
 type Ieee754Float
 
-type Float32 = Compose<Ieee754Float, MachineWidth<Word32>>
-type Float64 = Compose<Ieee754Float, MachineWidth<Word64>>
-
-// Default alias
-type Float = Float64
-
 // Abstract reals: approximate field over the exact rational **carrier**
 // `FieldOfFractions<Int>` (see `dsl/std/rational.dag` for `Rational =
 // Field<FieldOfFractions<Int>>`).
 type Real = ApproximateField<FieldOfFractions<Int>>
+
+// Fixed-width reals: abstract `Real` × machine width (refinement-shaped Compose).
+// These are the R3 gate #67 `numeric_construction_demonstration` Real<N>
+// construction entries; Rust Grounding maps Real64 to `f64`.
+type Real32 = Compose<Real, MachineWidth<Word32>>
+type Real64 = Compose<Real, MachineWidth<Word64>>
+
+type Float32 = Real32
+type Float64 = Real64
+
+// Default alias
+type Float = Float64