Before any number, name what each quantity is by the examination that produces it. A kind-of-property is the common defining aspect of mutually comparable properties (Dybkær §6.19); two otherwise-comparable kinds are individuated by their examination principle — the defining aspect of the procedure that measures them, so that a different principle forces a different kind. This is the layer a description logic partly has: it can record a class, but not the operator algebra or the laws the later steps add.

In the example this is the catalogue of bare kinds — the radar backscatter \sigma^0, the optical ndvi, the surface reflectivity, and the Mironov dielectric fit-constant kinds — each declared as a def of KindOfProperty, named by the instrument or principle that examines it. That a different examination principle forces a different kind is itself checked there: monostatic and bistatic reflectivity share name, scale, and dimension yet are distinct kinds. A kind is general (a type); this pixel's backscatter is individual (a term, Quantity backscatter α). Fix the kinds first: everything above is indexed by them.

Give each kind its dimension, and let dimension do only what it can. The dimension map is a forgetful functor — it keeps a kind's SI base-quantity exponents and discards the rest — so it answers only the coarse question, are these even commensurable? It respects products, which is ordinary dimensional bookkeeping proved as a law, but it does not decide identity. This step matters precisely because the quantities that carry the retrieval are almost all dimension one — a volume fraction, a reflectivity, an index. Dimension equates them all; the kind layer keeps them apart. Pairing a kind with its dimension here is what lets a later product be checked for dimensional consistency and kind consistency at once.

In the example, volumetric and gravimetric water content (vwc, gwc) are both dimension one yet distinct kinds — a units library alone would silently accept one for the other, which is exactly the failure this layer removes. (The literal dim-functor collapse is the Mathlib-backed dimension layer, shown in the Units and Dimension chapters; here the point is made one level up, at the kind.)

Now write the model's data and forward maps as records of typed quantities, and let the interaction algebra gate the arithmetic: a product is formed only where the kinds sanction it (KMul for products, KDiv for quotients), so a wrong pairing is a compile error, not a wrong number. Same-kind addition is the gate on +; products and quotients change kind by the algebra. Authored over an abstract carrier α, the whole record re-represents at the proof carrier (ℝ), the rounding spec (binary32), and the executable (Float) by one map, preserving every kind.

The example's MiniMironovCoeffs α is the pattern: each Mironov-2009 fit constant is a field of its own kind — a dry refractive index ndA0 : Quantity refractiveIndexKind α, a relaxation time taub0 : Quantity relaxTimeKind α, a conductivity sigbF0 : Quantity conductivityKind α — so the elaborator refuses to pass a relaxation time where a conductivity is expected, even though all three erase to the same carrier. Its MiniMironovCoeffs.map re-represents the whole table at any carrier (the constants moved from Int to executable Float by one map), each constant keeping its kind.

Finally, decide what to do about quantities that share a kind. There are two cases, and they go on different axes.

When two quantities should be different kinds because their measurement target differs — same quantity, different system or component — make them distinct with a dedicated kind: holding the component (or system) apart is enough to force distinct kinds, without inventing identity strings. In the example the bound-water and free-water static permittivities (boundStaticPerm, freeStaticPerm) are one relative-permittivity kind dedicated to two components, hence provably distinct.

When the algebra forces a genuinely shared kind, the leftover distinction is positional, not metrological, and belongs on a second axis carried by named record fields — not arrays. One row of the Cholesky factor — the example's CholRowQ α — is row-homogeneous: three fields l20 l21 l22, all Quantity reflectivity α, because A = L L^{\mathsf T} makes every L_{ik} L_{jk} land at the same kind regardless of the column — a kind that separated them would make the factorization's own row sums ill-typed. The remaining "which slot" distinction is held by the distinct field names and checked off the kind axis by an erasure rfl: the theorem cholRowQ_magnitudes proves the kinded row's .magnitudes are definitionally the bare-Float kernel's outputs, so a same-kind slot swap still type-checks but breaks parity. A Fin 3-indexed array would push that positional bookkeeping onto the type and discard the named slots; the record keeps both axes separable — kind by the elaborator, position by parity-to-reference.

Last, say where the model's numbers come from, where they go, and what the model claims about them. The first four steps fix what each quantity is; this one fixes what the module is. Its interface is a declared boundary of kind-typed ports — the inputs it ingests, the outputs it emits, its parameters, and the conditional outputs with their deciders — and its claim is a relation to its measurement model: that the output equals, inverts, refines, or is bounded by the measurement the module stands for, carried as a named witness theorem with its hypotheses and a license per carrier. The boundary is also what makes Step 4's erasure deployable: the distribution license says that only an extensive output commutes with a re-carving of its input, so sharding and batching — the deployment spectrum below — rest on the boundary's license clause. With the boundary in place the module states each requirement it makes against it: what its quantities must satisfy, and by what evidence, a theorem or an observation (the requirement clause).

MiniWriteOnce stops at Step 4; the step is shown by the tutorial's oscillator exhibit Tutorial.HarmonicOscillatorRequirements. There complianceBoundary takes three stiffnesses in and puts one compliance out, complianceSpec is the specification boundary that bounds it — one member, the wall spring's own compliance — and the requirement hp1 names the boundedBy edge between the two, with its theorem as witness and a Bool spot check evaluated at Float. #kind_contract_decide checks each boundary in the kernel and leaves the theorem behind; #kind_boundary_audit lists every site where a number enters or leaves with its evidence tier, and a site with none is a printed violation, not a review comment.