34.2. The template
The rows below are generated from PropertyKindCalculus.Rubrics.modelTemplate, so a
rubric added to the catalogue appears here without this chapter being edited, and one
removed cannot linger in it. The author's part column is the one to read while building
a document; the sections that follow argue why each group asks for what it asks. The
argument is not repeated in the table and the instruction is not repeated in the prose, so
neither can drift from the other.
| Requires | The rubric | The author's part |
|---|---|---|---|
The premise |
|
|
|
| exposition | The measurand and the deliverable are named and kept apart from what a reference measurement reports | Name the measurand and the deliverable in the model's own quantities, and say what a reference measurement reports instead — with the conversion that relates them where they differ, which is the step a validation comparing the two must perform |
| exposition | Why the kind layer is load-bearing in this domain: which quantities are of dimension one, and which confusions survive a unit check | State which of this model's quantities land on dimension one and which of its confusions survive a unit check, and cite the model's own dimensional-coverage table for the census the paragraph summarizes |
| exposition | The typing discipline is cited, not re-argued | Name what the document assumes of the calculus and point at where it is established; do not restate the case for kinds |
| exposition | The measurement chain in the order the physics runs it, and the layer map saying where each claim lives | Give the measurement chain in the order the physics runs it, and a map from each claim the document makes to the library layer that holds it |
The kind vocabulary |
|
|
|
| generated | Every quantity the document names is a declared kind-typed quantity, inventoried rather than surveyed | Declare every quantity the document names as a kind-typed declaration, and render the inventory with the generated index rather than a table written beside it |
| generated | Kinds of dimension one are individuated by their examination principle, with the procedure ⊑ method ⊑ principle refinement recorded | Give every kind of dimension one an examination principle and record the procedure ⊑ method ⊑ principle chain; where such a kind is deliberately principle-free, declare the exception so an audit can read it |
| checked | Dedications to systems and components are declared, and each separation the model relies on is proved rather than assumed | Declare the dedications to systems and components, and prove each separation an argument in the document rests on rather than asserting it |
| generated | The arithmetic surface is closed: the complete list of products, quotients and powers the model is permitted to form | Author every product, quotient and power the model may form, and publish the closed surface as a generated table — the empty cells included, since those are the combinations the model has decided are meaningless |
| checked | Every departure from the algebra is authored, and an audit that gates the build makes the inventory complete rather than a survey | Author every departure from the algebra — a genuine meeting of two kinds, kind-preserving plumbing, a point where a kinded value leaves the calculus — and run the audit that fails the build on an unauthored one |
| generated | Dimensional coverage is audited edge by edge, and inter-derivability the algebra cannot refuse is reported rather than hidden | Pin the dimensional-coverage reading and the inter-derivability report, so a newly undimensioned edge or a newly merged cluster is a change a reader sees in the diff |
The model as modules |
|
|
|
| checked | Each boundary is a declared metrological module of kind-typed ports | Declare each boundary as a contract of kind-typed ports, and sweep the namespace so that a boundary declared anywhere is enrolled without being listed by name |
| checked | A module's behavior is a measurement model carried as a theorem edge, not as prose beside it | Carry each module's behavior as a relation naming a theorem, not as prose beside the module |
| checked | The implementation's relation to the measurement model is named — equals, inverts, refines, or bounded by a kinded tolerance | Name the relation the implementation bears to the measurement model — equals, inverts, refines, or bounded by a kinded tolerance — and let the sweep check that the witness is sorry-free and about those two boundaries |
| checked | Licenses are stated per carrier rung, because laws transfer across the carrier ladder and side conditions do not | List on the edge itself one license per carrier rung the claim is extended to beyond the rung its witness is stated at, each answered for by a named repair or a named per-rung restatement |
| checked | Mereology is declared per output port, and any recarving or sharding is licensed by that declaration | Declare per output port whether it aggregates over parts, and license any recarving or sharding of a batch by that declaration rather than by the fact that it worked |
| generated | One specification sheet per boundary, generated from the checked declaration rather than written beside it | Generate one specification sheet per boundary from the declared contract, so the commit that changes a contract either regenerates the sheet or fails |
Carriers, adequacy and uncertainty |
|
|
|
| checked | The specification carrier and the executable carrier are distinguished, and the refinement bridge between them is named | Register the specification carrier and the executable carrier as distinct, and name the bridge that carries a claim from one to the other |
| checked | The deployed representation is shown numerically adequate at the scale of the input uncertainties | Show that the deployed representation loses no information at the scale of the input uncertainties — a claim about this model's numbers, not a preference for wider floats |
| checked | Uncertainty names the rung of the method ladder it was computed at, and the coverage its recorded variance certifies | Name, for each reported uncertainty, the rung of the method ladder it was computed at and the coverage its recorded variance certifies |
Well-posedness and honest failure |
|
|
|
| checked | Where the model is inverted, existence and uniqueness are proved on a declared domain | Where the model is inverted, prove existence and uniqueness on a domain the document declares — both the proof and the domain it is about |
| checked | Failure outside that domain is detected and reported, and ambiguity is surfaced rather than silently resolved | Detect and report failure outside that domain, and surface ambiguity rather than resolving it silently to whichever root the algorithm reached first |
| checked | The conditioning and quality outputs a consumer must read are part of the declared contract, not a side channel | Put the conditioning and quality outputs a consumer must read into the declared contract as ports, not into a side channel a downstream stage may or may not read |
Assurance |
|
|
|
| generated | Every load-bearing definition and theorem links to the declaration that realizes it and carries that declaration's machine-checked status | Cite each load-bearing definition and theorem by the declaration that realizes it, so the rendered claim carries that declaration's machine-checked status |
| generated | A dependency graph and an assurance ledger are generated from those same nodes, so neither can omit a cited claim | Generate the dependency graph and the assurance ledger from the same nodes the chapters cite, so neither view can omit a claim the other carries |
| exposition | The limits of a green status are stated plainly: which rung each theorem holds at, and which results are measured rather than proved | State plainly what this document's green status does not mean: which rung each theorem holds at, and which of its numbers are measured rather than proved |
| measured | Each reported measurement names the parameter it was swept over, the denominator it is relative to, and the statistic it reports | For each reported measurement, name the parameter it was swept over, the denominator it is relative to, and the statistic it reports |