18. Write Once, Correctly
The chapters so far catalogue what PropertyKindCalculus provides. This one is about method:
the order in which an application author reaches for those pieces when specifying a real model,
and why the order is forced rather than a matter of taste. The running example is
PropertyKindCalculus.Examples.MiniWriteOnce — a small, self-contained soil-moisture retrieval in
the project's own Examples library — read here only to infer the recipe. It is a deliberately
simplified subset, keeping just the salient structure each step needs (a few kinds, a typed
constant table, a dedicated kind, one row of a Cholesky factor) and omitting the full retrieval.
Every line of it is a checked fact, built in the Examples library under CI, so the
illustrations below are machine-verified; PropertyKindCalculus supplies the five primitives named
below; the example composes the first four in this order, and the fifth, the boundary, is shown
on the tutorial's oscillator exhibit.
The discipline has a slogan: write once correctly, go fast
automatically. A quantity is authored once, carrying its kind, over an abstract numeric carrier;
the kind layer is checked by the elaborator and then erases — projected away by .magnitude —
to a bare floating-point kernel, bit for bit. Correctness lives in the types and is paid for at
compile time, while the number that runs is the same one a hand-written kernel would compute.
Getting the authoring order right is what makes that erasure sound: each layer must be in place
before the one above it can type-check.
This carrier-parametric discipline is inherited from TorchLean
(George et al., 2026)Robert Joseph George, Jennifer Cruden, Will Adkisson, Xiangru Zhong, Huan Zhang, and Anima Anandkumar (2026). “TorchLean: Formalizing Neural Networks in Lean”. arXiv preprint arXiv:2602.22631 (cs.MS). ., where a tensor is generic over its
scalar carrier so that one network runs at ℝ for proof and at Float for execution — and the
executable carrier here is, in fact, a TorchLean tensor. PropertyKindCalculus lifts the discipline
up the metrology tower: the same numeric carrier is varied over a kind-typed scalar quantity, a
tensor-valued quantity, and — across the lawful-to-executable refinement — a numerically adequate
one; the same parametric-indexing idea then carries onto an additive uncertainty descriptor,
yielding an uncertain quantity, and onto the measured object as a further type index, yielding an
object-indexed individual quantity. What TorchLean provides for one carrier of one tensor,
PropertyKindCalculus provides for the whole tower of quantity notions.