1.3. In plain terms — the requirements🔗

In plain terms, rigorous metrology here means:

Telling apart quantities that look identical. Two measurements in the same units can still be different in nature — volumetric and gravimetric soil moisture are both "just a ratio", yet confusing them corrupts a result. The calculus keeps such quantities distinct types, so the mix-up is impossible rather than merely discouraged; agreeing units (or dimensions) are treated as necessary but never sufficient (R1, R7).
Rejecting nonsense arithmetic before it runs. Adding a length to a mass — or even a torque to an energy, which share the same dimension — is a compile-time error, not something caught (or missed) at run time. Quantities that genuinely combine, such as a torque times an angle giving an energy, are sanctioned explicitly; everything else is refused (R4, R5).
Knowing which operations even make sense. What you may do to a measurement depends on its scale: you can rank mineral hardness but not average it; you can subtract Celsius temperatures but only take ratios of thermodynamic ones. These rules are enforced automatically (R6).
A faithful hierarchy of kinds. Width and height are special cases of length — usable where a length is wanted, never the reverse — while a general kind (length) is never confused with one individual measurement (the length of this pencil). A kind can even be tied to the system and component it is dedicated to, so "water content of soil" is named in its own right, and a value carries the object it characterizes in its own type, so one soil column's water content cannot stand in for another's (R2, R3, R19, R22).
Units that convert safely and never silently. A unit is a chosen reference of one specific kind; a conversion round-trips exactly, and there is simply no conversion between units of different kinds (R8, R16, R17).
Summing only what may be summed. The masses of the parts add up to the mass of the whole; the volumes of mixed liquids do not. The calculus tracks which quantities aggregate and refuses to assume it of the rest (R9).
Classifications you can trust because they are earned. Labeling a value "an area" requires a proof that it really is a width times a height; an arbitrary number cannot wear the label (R12).
The same model from proof to running code. One quantity can carry exact real numbers for proving properties and IEEE floating-point for execution — with a theorem guaranteeing the running code matches the proven specification, rounding and all — and a vector quantity is a list of numbers under a single shared unit, not a bag of separately-united components (R10, R11).
Components that remember the frame they were read in. A vector quantity's numbers are coefficients in some chosen set of axes, and that choice is no part of the physics: turn the axes and every component changes, while the scalar product of two vectors does not. Readings taken in different frames do not combine, a change of frame acts on them through the law their kind of index obeys, and the combinations that are genuinely frame-independent are the ones proved to be (R20).
Honest unit classification. The SI sorts units into base and derived, but not even the seven base units are alike: the mole is dimensionally a pure number and the candela a power, and each stays a base unit only because it carries a human-chosen coefficient sized to keep everyday values readable. Units like these get a category of their own — scale-spanning — instead of being forced into a base/derived split that does not fit them (R13).
Uncertainty propagated, with the cheap method licensed by the expensive one. An input carries a spread as well as a magnitude, and the calculus carries it through the model by one of three methods of rising cost and fidelity: a linearization, a cumulant method that keeps the shape of the tails, and a sampling method that keeps the full non-linearity. The three are proved to nest — each coarser one is a projection of the finer one — so reaching for the cheap method is an approximation with a stated relationship to the expensive one rather than an act of faith. The variance that comes out then certifies a coverage interval: a conservative one that assumes nothing about the distribution's shape, an exact one where the shape is known (R14, R18).
Knowing when single precision is enough. Because one model runs at exact reals and at floating point alike, the two can be compared where it matters. An input whose contribution falls below half a unit in the last place of the running sum is numerically invisible — its uncertainty was silently dropped — and its dual is a subtraction that is exact yet magnifies the relative uncertainty of what remains. Both are flagged, so "enough precision" is a checkable property of a model at its inputs rather than a habit (R15).
Rigor that costs nothing at run time, and reads back as mathematics. The kinded expression compiles to exactly the term a hand-written bare-number kernel would — same operations, same rounding, nothing added — so what the kinds buy is checking, paid at compile time and not at run time. In the other direction, a definition is rendered back out of its own elaborated form as a typeset equation with the kind bookkeeping suppressed, so what a reviewer reads is generated from what the machine checked, not written alongside it (R21, R25).
Where a number came from, and how much of a program is answered for. A value can carry an auditable record of the graph that produced it — which inputs, through which steps, and where values left the calculus for bare numbers — against a boundary the author declares and the machine checks against the boundary the code actually has. Such an audit is always a claim about one named scope, never about the library, and a scope once blessed may only grow: a regression fails the check instead of quietly passing it (R23, R24).
Modules that state what they compute, and what may be split. A module's declared boundary carries the relations its outputs stand in to its inputs — each backed by a theorem the kernel checks, each numerical bound naming a kinded tolerance. The same declaration says which outputs aggregate over a carving of the data, and that is what licenses running the computation in tiles or shards: a theorem says the total is preserved, rather than the schedule being trusted to preserve it (R26, R27).
What a module's quantities must satisfy, and by what evidence. A requirement is stated beside the boundary it governs, in the author's words, with its evidence: a theorem, where the statement closes over the model, spot-checked where the model runs; or a gate against a named referent the model does not define — a datasheet value, a prior, a reference measurement — where it does not. Which of the two it is, the machine reads off the statement rather than taking the author's word, and every output either carries a requirement or says why it needs none (R28).

Between them these bullets name all twenty-eight requirements, each of which is stated precisely below; the status table at the end of that section maps every requirement to the checked declarations that address it.