Realized as the Carrier / LawfulCarrier classes. Carrier R bundles zero and add; LawfulCarrier R extends it with associativity, commutativity, and the unit laws. Int and (in the Dimension library) ℝ are lawful carriers; Float is a Carrier but deliberately not lawful (floating-point addition is not associative).

Realized as structure Quantity (k : KindOfProperty) (R : Type) carrying a magnitude in R, with same-kind addition Quantity.add : Quantity k R → Quantity k R → Quantity k R (R4: the type forces both summands to share the kind). The algebraic operations come from the carrier typeclass on R; which operators are even admissible is the orthogonal scale gate (the proved operator stratification, operator monotonicity).

Proved in PropertyKindCalculus.Quantity (axiom-free). Each law unfolds Quantity.add to its carrier operation and rewrites by the corresponding LawfulCarrier field; laws_parametric bundles the four. Specializing to Int (core) and ℝ (in the Dimension library) reuses the same proof verbatim, which is the R10 payoff.

Realized as the CarrierRefinement class (core, axiom-free). TorchLean's FP32 gives an unconditional instance over \mathbb{R}, and IEEE32Exec refines \mathbb{R} on the finite path — both in the separately built Torch library.

Proved as Quantity.add_refines (core, axiom-free): the CarrierRefinement bridge law lifted along the kind index. It is instantiated concretely in the separately built Torch library at TorchLean's binary32 — an unconditional CarrierRefinement FP32 ℝ (the rounding spec has no overflow, so the law holds by computation) and a conditional IEEE32Exec refinement on the finite/no-overflow path (Quantity.add_refines_exec), where overflow is an explicit hypothesis rather than a silent failure. This is TorchLean's Bridge/FP32 pattern ("compute in \mathbb{R}, then round").

Realized as the MulRefinement class (core, axiom-free), a Prop class parametrized by a CarrierRefinement rather than extending it, so one carrier has one forgetful map and one rounding. Instantiated at TorchLean's FP32 in the separately built Torch library, where NF multiplication is ofReal (a·b) and the law is therefore rfl.

Realized as the DivRefinement class (core, axiom-free), with the unconditional DivRefinement FP32 ℝ instance in the Torch library. The executable rung's Quantity.div_refines_exec asks that the executable quotient be finite, and the Torch-tier probes discharge that on concrete binary32 values and then refute it at a zero denominator, where the divisor's decoded mantissa is shown to be zero.

Proved as Quantity.mul_refines (core, depending on no axioms at all): the MulRefinement law lifted along the kind product. Specialized at binary32 as Quantity.mul_refines_fp32, and conditionally at the executable carrier as Quantity.mul_refines_exec under decoding and finiteness hypotheses.

Proved as Quantity.div_refines (core, depending on no axioms at all), with Quantity.div_refines_fp32 at the binary32 rounding spec and Quantity.div_refines_exec at the executable carrier. Both are exercised over a genuinely lossy toy carrier in the core probes — where 3 \times 3 reads 9 exactly but forgets to 8 — so neither capstone is satisfied vacuously by an identity rounding.

Realized as the pointwise Carrier (ι → R) / LawfulCarrier (ι → R) instances (core). The fuller structural apparatus — coordinate frames, tensor variance, transforms — remains a separate, owed axis.

Realized as RealUnit k, a Quantity k ℝ chosen as the reference together with the one condition the choice must satisfy: ref_ne_zero. That field is what the phrase "express the ratio of the two quantities as a number" presupposes and the symbolic layer never has to state — a reference of magnitude zero expresses no ratio — and carrying it makes a degenerate unit not a term of the type. Measuring is measure : Quantity k ℝ → RealUnit k → ℝ, division by the reference; ofNumber is the multiplication back; and the §13.3.3 number-and-reference round-trip is then a bijection in both directions (measure_ofNumber, ofNumber_measure) rather than a definitional unfolding. ratio is the §1.22 conversion factor for an arbitrary chosen reference, nonzero from the two licenses and reciprocal in the two directions, of which the power-of-radix factor is the special case. The refinement inherits the §9.13.4 exclusions rather than widening them: WellFormed is the symbolic layer's BearsUnit, so a nominal or ordinal kind bears no real-valued unit either.

Because the conversion factor is a power of ten, its exponent is an Int — an element of an additive group — so the shift u_1\to u_2 (shift, the difference of the prefix exponents) and the shift back sum to zero (shift_add_symm). The round-trip on the decimal exponent is then x + (e_1 - e_2) + (e_2 - e_1) = x, closed by omega with no rounding. The numeric \mathbb{R} companion multiplies by 10^{e_1-e_2} then 10^{e_2-e_1}; zpow_add₀ on 10\neq 0 collapses the exponents to 10^0 = 1. Neither needs a chosen-reference nonzeroness hypothesis; the general real-valued case is where one is needed, and it carries ref_ne_zero as a field so that ratio_ne_zero follows from the two licenses and from nothing else.

Proved in the Dimension library. vwc and gwc are declared as dimensioned kinds with distinct kind ids, so vwc.kind ≠ gwc.kind is by decide; both carry dim = 1, so their dimensions agree by rfl. Together they witness \exists a\ b,\ a.\mathrm{kind} \neq b.\mathrm{kind} \wedge \dim a = \dim b \wedge \dim a = 1.

A structure SIPrefix carrying name, symbol, and an integer exponent (the factor is 10^{\text{exponent}}); the full SI set (quetta … quecto) is enumerated as defs.

A structure BinaryPrefix carrying name, symbol, and an integer exponent (the factor is 2^{\text{exponent}}); the eight prefixes kibi … yobi are enumerated as defs. A PrefixedUnit records the resolved radix (10 or 2) so that a single convertExp_roundtrip serves both families, gated to a common radix.