1.1. The paradigm: metrological provenance as taint tracking🔗

The calculus is easiest to see through an analogy with taint analysis in software security. A taint analyzer marks what a program reads from outside as tainted, follows it through the code, and reports where tainted data reaches a sink that must only ever see trusted data. Read metrologically:

• A raw number is tainted. It could be a value of any kind — a velocity, an acceleration, a reflectivity — so nothing downstream may rely on what it means.

• A kinded quantity, Quantity k R, is clean. Its kind k is in its type, so everything downstream may rely on it, and the kind is what every operation on it is checked against.

Taint analysis tracks untrusted data through source code; the calculus tracks kinded quantities through the kind algebra. Here the analogy breaks in the calculus's favor. A taint analyzer has to approximate how data flows through a program, whereas here the kind rides in the type and the elaborator propagates it exactly, with nothing to approximate. What a taint analyzer must still be told — where data enters, where it leaves, and where trust is granted by hand — is exactly what an author still declares, and each declaration is an annotation the machine checks:

• Sources. Raw data enters through @[kindIngest], a checked ingest — a mint admitted by a check; an adjudicated constant — a cited coefficient, a threshold — enters as a constant mint through @[kindConst].

• Sinks. A kinded value leaves the calculus as a bare number at an emission, through @[kindEmission]: a deploy driver, a serializer, the parity apparatus the erasure theorems are stated over.

• Trust granted by hand. A value that already carries one kind and is re-typed as another, with no law of the algebra to derive it, is a crossing, tagged @[kindCrossing]; representation plumbing that drops to the carrier without changing the kind is a @[carrierVocab].

Between the sources and the sinks nothing is declared, because nothing needs to be: a kind reached through a law of the algebra is derived, at a site the elaborator checked. That leaves three ways a value comes to carry a kind — its evidence tier — and the provenance layer names them (Provenance.IntroTier):

• derived — through a law, such as ProductKind massK velocityK momentumK. No judgment is made at the use site; it was made once, when the edge was registered, and the edge audits enumerate the edges.

• gated — through a check. A KindAdmissible instance gives a predicate on the raw value, Quantity.certify runs it, and the check is the declaration's evidence. It is necessary, not sufficient: no predicate on bits can establish that a number is a velocity rather than an acceleration.

• attested — through no check at all. Quantity.attest "why" m is definitionally the raw value ⟨m⟩; the author states the classification claim, and the reason string, harvested into the audit, is the only content.

An attestation is a hypothesis of the model, not an axiom of the calculus. The distinction is the one Lean draws. An axiom is global — stated once, available to every proof, and a single false one makes everything provable — whereas a hypothesis is local to the statement that carries it, and a theorem with thirty of them is unremarkable. A model of any size carries dozens of attestations, because every place a number's kind rests on the author's knowledge rather than on a law or a check is one: an identification of a retrieved variable with the forward model's own, a convention such as NaN for no value, a re-entry from a table fetch the calculus cannot see, an operation the algebra has no edge for. Like a hypothesis, an attestation does no work in the computation — Quantity.attest "why" m is ⟨m⟩ — it licenses an interpretation, and the reason is its whole content.

The axiom's part is not played by the calculus. The core postulates nothing about any particular kind: its foundation is Dybkær's ontology of property (Foundations), and what it fixes — which operators a scale admits, that two kinds meet only under a witnessed law, that dimension is forgetful — is designed and proved. The system of quantities the calculus is instantiated with is ISO 80000's (the standards catalogue): a width is a kind of length, speed is path length per duration, each entry cited to its item. That is an axiomatization in the mathematician's sense — a system adopted by the consensus of the community whose subject it is, not a list of assumptions — and the calculus checks each transcribed relation: its scale preconditions close by rfl, and the catalogued dimensions are confirmed against it by computation. A domain model extends that system with kinds and relations of its own, and those are the postulates the trust model prices: authored, reviewed, and refutable wherever their kinds carry a dimension. Its attestations are its hypotheses.

For a theorem, the hypotheses stand gathered in its statement. A model scatters them over its source, and the boundary audit (the boundary family) gathers them back: #kind_boundary_audit ns … lists every boundary site in a namespace — each entry, exit and crossing, with its tier and, for an attestation, its harvested reason — so the pinned report is the model's statement, the list of what it assumes. Pinned under #guard_msgs, an entry point nobody declared fails the build — not as a type error, since a raw ⟨x⟩ typechecks, but because the audit refuses it. The discipline is a referee's, not a no-axiom rule: derive what a law derives, check what a check can establish, and state everything else. Its end state is not zero attestations but zero unstated ones. And the honest limit is a hypothesis's: a false one leaves every downstream step valid and the conclusion worthless. It typechecks, appears as one line in the pinned report, and is exactly as good as the reading of that line — the reader is the caller who discharges it.