18.2. The payoff🔗

Authored in this order, the model is one source. The kinds make every operation in the forward physics and the normal-equations solve a checked equation; the dimension layer certifies commensurability without conflating dimension-one quantities; the interaction algebra gates the arithmetic; dedication plus named fields carry the distinctions the kind axis cannot; and the boundary says what enters, what leaves, and what the module claims about it. Then .magnitude erases the whole overlay and the compiled kernel is the bare Float program — proved, by a definitional rfl for every input, to be the same numbers. Write once correctly, go fast automatically.

The worked example is PropertyKindCalculus.Examples.MiniWriteOnce, build-gated by the project's own CI, so every illustration above is a checked fact rather than a claim. The recipe scales to a full retrieval: the same five steps, composed in the same order, carry a complete SMAP–NISAR soil-moisture model — and because each step's facts are real declarations, a downstream verifiable ATBD can cite them by name with their proved-or-sorry status, keeping the document and the code in lockstep. PropertyKindCalculus supplies the five primitives this chapter names; a model composes them in this order.