A Property Kind Calculus for Measurement Metrology

1.4. What an author writes, and what the machine checks🔗

The Using the library chapter explains each annotation in turn. This section is the summary to have before reading it: what a model written in the calculus asks of its author, and what the author gets back. Since the kind propagates in the type (the paradigm), an author states three things, and the machine checks all three.

First, the equations are written over kinded variables. Where a physics text writes T = \tfrac{1}{2} m v^2 over bare reals, the model writes it over a Quantity massK ℝ and a Quantity velocityK ℝ, and every operation between them has to be licensed:

  • Addition and comparison are gated by the kind index itself. Two quantities of the same kind add; a velocity added to an angular velocity is a type error (R4).

  • Products and quotients go through the operator table. A KindMul k₁ k₂ k or KindDiv k₁ k₂ k entry is registered per sanctioned pair of kinds, each wrapping the ProductKind or QuotientKind law the ISO 80000 defining relations are stated as: the entry KindMul massK velocityK momentumK encodes ISO 80000-4 item 4-8, p = m\,v. A file opts in with open scoped PropertyKindCalculus.OperatorTable, after which m * v elaborates at the momentum kind. Where no entry exists, the product does not elaborate at all (R5, the interaction algebra).

  • Functions go through the function table (the function calculus), which sorts them into six families by kind signature: kind-preserving (abs, min, max), powers and roots, the dimensionless transcendentals, the trigonometric functions, logarithmic levels, and re-expression against another reference. The trigonometric family is the showcase: a plane angle is dimension one but a distinct kind, so sin of an angle is fine while sin of a reflectivity is a category error a dimension-only system cannot forbid.

What the switch buys is the two things a bare equation cannot say. A kinded expression combines only where the algebra licenses it. And the kind separates what the dimension cannot: the ForPhysLib classical-mechanics benchmark alone has six distinct kinds at the joule (kinetic, potential, mechanical, the Lagrangian, and König's translational and rotational pair), two at \mathrm{T^{-1}} (angular frequency and angular velocity, the same letter \omega in two subtrees), and two at \mathrm{T} (duration and period), and the distinctions are decidable (angularFrequency_ne_angularVelocity is closed by decide). The kinds are paid for at compile time, not at run time (R21): the kinetic energy authored through the table, \tfrac{1}{2}\langle p, v\rangle built from the edges m \cdot v \to p and p \cdot v \to 2T, erases to PhysLib's \tfrac{1}{2} m \langle \dot{x}, \dot{x}\rangle by the theorem kineticFromTableQ_erases.

Second, the boundary is declared. Each source, sink and hand-granted crossing of the paradigm carries its annotation from the boundary family. Inside such a declaration, where no check applies, the mint itself is written as an attestation:

@[inline, expose] def attest (_why : String) (m : R) : Quantity k R := ⟨m⟩

It is definitionally the raw value: the physics context is in the type, Quantity velocityK ℝ say, not in the string. What the string does is put the judgment on the record. The boundary audit harvests it and prints it beside the site, so each authored mint is a one-line review artifact rather than an anonymous ⟨m⟩. The discipline is that attest is the last resort, for a classification with no machine-checkable evidence, and the reason should say why no check applies; where a KindAdmissible check exists, Quantity.certify runs it and keeps the receipt in the type.

One command enumerates all of it: #kind_boundary_audit ForPhysLib.ClassicalMechanics, the boundary audit, prints one line per boundary site in that namespace — its tier and, for an attestation, its harvested reason — and ends 42 boundary site(s), all tagged — clean. The report is pinned with #guard_msgs, so an entry point nobody declared fails the build. That is not a type error, to be clear: a raw ⟨x⟩ typechecks. The audit is what refuses it (R23, R24).

Third, the requirements are stated. What a module's quantities must satisfy — a bound, a band, a tolerance — is a Provenance.Requirement beside the boundary that produces them, and it says by what evidence it is met. A provable requirement's statement closes over the model, so a theorem discharges it, with Bool spot checks the command evaluates where the model runs; an empirical requirement names a referent the model does not define — a datasheet value, a prior, a reference measurement, marked @[kindReferent "where it comes from"] — so a gate against that referent discharges it, or an attestation with its reason defers it. The category is read off the statement's constants, not chosen: a witness that names a referent is refused as provable, and a gate that names none is refused as empirical. #kind_requirements surveys a namespace's requirements as one pinned report, and #kind_requirement_coverage asks of every produced port whether a boundary/port-matching requirement governs it. For object scopes, the result member's type supplies the inferred object domain; a missing index or unresolved bearer is an unchecked violation unless the boundary is exempted. A .sort scope requires an indexed result and a Sorted instance; the census first reduces the actual result bearer's sort inside the member telescope. A definite match governs, a definite mismatch falls back to object scopes or is ungoverned, and a stuck sort follows the object-domain path and may be unchecked. .decided governs only when its deciderProof proves the decider holds for every result of the member; otherwise the census marks it unchecked. .all remains broad (every claim a model makes, with its evidence).