A Property Kind Calculus for Measurement Metrology

2.5. Representation parametricity (R10)🔗

R10 — A quantity value is parametric in its numeric representation type. The magnitude of a scalar quantity is carried at a representation type R, a type parameter bounded by whatever algebraic structure a given task demands, so the same kind-indexed value can be instantiated at whichever R the task needs — without changing the kind, scale, dimension, interaction, or extensivity layers above it. This is the axis dependent types make not just possible but necessary: the carrier the kind sits over is exactly where proof and execution diverge, and a single quantity must serve both. Three real representations matter, and they are not interchangeable — and a fourth complexifies any of them:

  • Lean's \mathbb{R} — for proofs. A complete ordered field: the continuous specification against which laws (monotonicity, conversion round-trips, extensivity) are stated and proved.

  • A finite floating-point rounding model — for numerical-accuracy reasoning. TorchLean's FP32 (NeuralFloat at binary32 precision: round-to-nearest, ties-to-even over \mathbb{R}, finite-only, with toReal : FP32 → ℝ). It is non-computable — it exists to bound rounding error against the \mathbb{R} spec, not to run.

  • An executable IEEE-754 type — for exact-execution reasoning and code generation. TorchLean's IEEE32Exec (a bit-level UInt32 binary32 kernel) that models NaN, infinities, signed zeros, and subnormals, with toFloat/ofFloat and isNaN. This is the representation that actually runs and the one in which exceptional values (NaN) can be reasoned about — what one might call the "exec" float, distinct from the FP32 rounding spec.

  • The complexification \mathrm{Complex}\ R of any of the above — for complex-valued quantities. Many physical quantities take a complex value (the relative permittivity of a lossy dielectric \varepsilon = \varepsilon' + j\varepsilon'', an impedance, an AC phasor); complex-ness is a property of the carrier, not the kind, so \mathrm{Quantity}\ k\ (\mathrm{Complex}\ R) is the same kind layer over a complexified carrier. As a functor R \mapsto \mathrm{Complex}\ R it lifts each of the three above — \mathrm{Complex}\ \mathbb{R} to prove, complex binary32 to certify rounding, \mathrm{Complex}\ \mathrm{Float} to run. It is a Carrier — and a LawfulCarrier whenever R is, since complex addition is componentwise so the additivity laws lift for free — carrying the full field +\,-\,\times\,\div; but it is unordered (there is no \le on \mathbb{C}), so unlike the real carriers it sits outside the ordinal/interval/ratio carrier tower: complex magnitudes are compared by modulus, not ranked.

Soundness across representations is itself a theorem, not an assumption: an exec/spec refinement (the executable float result is the rounding of the real result) lets a law proved over \mathbb{R} transfer to the executable run. In plain engineering terms: choose the number type to fit the job — reals to prove, the rounding model to bound error, the IEEE kernel to run and to catch NaN — while the kind, dimension, and unit machinery above is written once and is identical for all three. This refines R1/R3/R4's kind-indexed value into a doubly-indexed Quantity (k : KindOfProperty) (R : Type) whose arithmetic is bounded by a Carrier typeclass on R. The value layer and its additivity laws are realized (sorry-free): Quantity k R with same-kind addition, the additivity laws proved once over any lawful carrier, and three carriers — Int and ℝ (lawful, for proof) and Float (executable, deliberately not lawful). The exec/spec refinement across representations is now also realized (sorry-free): the abstract bridge CarrierRefinement and its kind-indexed capstone Quantity.add_refines — a law over the lawful spec carrier descends to the exec carrier as one rounding step — instantiated in the separately-built Torch library at TorchLean's binary32: FP32 (the rounding spec, an unconditional refinement of \mathbb{R}) and IEEE32Exec (the executable kernel, refining \mathbb{R} on the finite/no-overflow path, with overflow surfaced as an explicit side condition rather than silently dropped).

The bridge spans the whole arithmetic surface, not the additive part alone: MulRefinement and DivRefinement carry the same forgetful map and rounding to \times and \div, and Quantity.mul_refines / Quantity.div_refines lift them across a licensed kind change — the exec product of a k₁ and a k₂ quantity, viewed in the spec carrier, is the rounding of the spec product at the product kind k. The rounding obligation and the kind license are independent and compose, so a rounding step cannot launder a product the kind calculus refuses. This is what lets a weighted mean, a ratio, or a sensitivity coefficient cross at all — none of them is an addition. The division law is unconditional at the specification rung only because \mathbb{R} totalizes x/0; the executable rung's Quantity.div_refines_exec asks that the executable quotient be finite, which is where a zero denominator is actually caught: a finite dividend over zero is an infinity or a NaN.

The real representations above and their complexifications, ordered from proof to execution, are the carrier ladder: each representation is a rung, and a definition written once over an abstract carrier is instantiated at every rung by one map. Laws transfer across the ladder; side conditions do not. That asymmetry is the counterpoint to everything above, and it is worth stating as a rule rather than as a property of one theorem. The bridge carries a law from the lawful carrier to the executable one at the cost of a single rounding step. It carries a side condition — a hypothesis a definition holds as a field, so that the degenerate case is not a term to be handled — not at all. The reason is visible in the statement: a condition phrased in the carrier's own arithmetic says a different thing at each carrier, and the different things are logically independent. A field that is one line of Lean, quantified over the carrier, is not thereby carrier-generic; it is carrier-relative.

The weighted mean is the worked instance, because it is the first aggregation mode with a side condition at all. A carving's license says its total weight is not the carrier's zero. At binary32 that is a claim about the rounded fold; the bound relating the computed mean to the exact one also needs a claim about the exact fold; and neither implies the other, in either direction:

  • three weights 2^{24}, 1, -2^{24} sum exactly to 1 and total exactly +0 on the grid — a mean that exists, refused;

  • four weights 2^{24}, 1, 1, -(2^{24}+2) sum exactly to 0 and total exactly -2 on the grid — a mean that does not exist, computed, with a finite and plausible value and no exceptional flag anywhere to catch it.

So testing a computed denominator against zero is a guard on the number the machine formed, not on the quantity being defined. Two arrangements put the two conditions back together, and they rank. Do not round the denominator: where the refinement's rounding is the identity — a count folded in \mathbb{N}, converted once — forgetting the total is the total of the forgotten weights, so there is one condition rather than two. This is the strongest fix and it is available whenever the weights are counts or indicators, which is the ordinary case for a validity-masked average. Or keep the weights nonnegative: both failures above are built from cancellation, and ruling it out restores the equivalence for weights that are genuinely real-valued — masses, areas, durations, coverage fractions.

The reading generalizes to every \mathrm{Prop} field phrased in carrier operations. The other instance already in the library is a real-valued unit's nonzero-magnitude license.