1.2. The calculus at a glance🔗

The chapters that follow develop each piece in full, every node linked to the declaration that discharges it. This is the map, in the order the pieces rest on one another.

• A kind is a type-level index. Quantity k R is a magnitude in the carrier R at the kind k. Two quantities are comparable, addable, or given a common unit exactly when their kinds agree, and a kind of dimension one is as distinct from its neighbors as a length is from a mass. Which operators a kind admits at all — order, difference, ratio — is fixed by its scale; specialization (a radius is a length) is a lattice on kinds, and instantiation (this pencil's length) is term-of-type, never subtyping (The proved spine).

• A kind is a kind of something. The sort of system a kind is dedicated to and the object an individual quantity characterizes are the two sides of Lowe's square (Foundations, Dedicated kinds-of-property), and a value can carry the object it characterizes in its type, so one soil column's water content cannot stand in for another's (The object type).

• Two kinds meet only under a law. ProductKind k₁ k₂ k and QuotientKind k₁ k₂ k are the authored edges of the interaction algebra — the ISO 80000 defining relations are stated as them — and the operator table registers KindMul and KindDiv notation over those laws, so m * v elaborates at the momentum kind and a pair with no entry has no product. Functions go through the function calculus, six families sorted by kind signature. What is checked is explicitness and propagation, not truth: an edge is an authored claim, enumerable like an axiom (the trust model).

• Dimension certifies; it does not decide. \dim : \mathrm{Kind} \to \mathrm{Dimension} is a forgetful functor: every edge the algebra admits is proved dimensionally coherent, and agreeing dimensions are necessary, never sufficient. A unit is a distinguished quantity of one kind, converted by proved round trips and never across kinds (Units and the dimension-1 problem); the units the base/derived split does not fit get a category of their own (Scale-spanning units).

• Aggregation is a claim about the kind. Which kinds sum over a carving of a system into parts, and under what law or tolerance, is declared and proved rather than assumed (Extensivity).

• One model, several carriers. A model is written once over a carrier typeclass and instantiated at ℝ to prove, at binary32 to bound rounding, at Float or a GPU tape to run; the kinded term erases to the bare-number kernel, so the checking is paid at compile time (Write once, correctly). The same parametricity carries measurement uncertainty through the model and flags where floating point loses information at the scale of the input uncertainties (Uncertainty quantification and numerical adequacy).

• A module declares its boundary, what it computes, and what its quantities must satisfy. A Provenance.Contract states a module's kind-typed ports and exits, a Provenance.Relation its measurement model as a theorem edge, and the aggregation classes on its outputs are what license sharding it (Metrological modularity). A Provenance.Requirement per produced port states what that port's quantity must satisfy and by what evidence — provable by a theorem, or empirical by a gate against a referent the model does not define — surveyed and censused, with the deferred ones counted (every claim a model makes, with its evidence).

• The standard is the test. Eleven parts of ISO/IEC 80000, item by item, with checked dimensions and proved defining relations (The standards catalogue); Dybkær's and the VIM's clauses are cross-referenced to the declarations that formalize them (External cross-references).

• Annotations declare; commands ask. The annotations an author writes and the commands that audit them are catalogued in Using the library, and the model and deployment templates fix what a domain document conforming to the calculus states.