34.5. The model as modules🔗

Rubrics M11 through M16 are the Metrological modularity chapter's paradigm read as an obligation on a document.

• M11 — Boundaries as declared modules. Each boundary is a declared metrological module of kind-typed ports.

• M12 — Behavior as a theorem edge. A module's behavior is a measurement model carried as a theorem edge rather than as prose beside it.

• M13 — The implementation relation, named. The implementation's relation to that model is named: equals, inverts, refines, or bounded by a kinded tolerance.

• M14 — Licenses per carrier rung. The rubric this project has been bitten by, and it generalizes past metrology: laws transfer across the carrier ladder and side conditions do not. A theorem proved over the reals is a statement about the reals; the licenses under which it survives to the executable carrier are separate, per rung, and must be stated there. A document that proves at one rung and deploys at another without saying so has published a claim about something other than the thing it ships.

• M15 — Mereology per output port. Mereology is declared per output port — which outputs aggregate over parts and which do not — and any recarving or sharding of a batch is licensed by that declaration rather than by the fact that it happened to work.

• M16 — A specification sheet per boundary. One specification sheet per boundary, generated from the checked declaration: the page one hands a prospective consumer, which the same commit that changes a contract either regenerates or fails on.