A Property Kind Calculus for Measurement Metrology

34.1. What a template is, and what it is not🔗

A rubric is an obligation to answer, not a section to write. Two documents that discharge the same rubric may look nothing alike: one may answer M2 in a paragraph of its introduction and another in the closing page of a chapter, and both conform. What the template fixes is the question and the kind of evidence that settles it.

Of those two, it is the evidence that is worth stating carefully: a checklist that names its questions but not what settles them can be checked off by asserting the answers. Four kinds of evidence appear, and they are not interchangeable:

  • Exposition. A tagged section of the document states the answer. There is nothing to prove — the obligation is that a reader can find it — so the evidence is a cross-reference, and a cross-reference to a section that does not exist is a render error.

  • Generated. A view read off the compiled environment: an index, a specification sheet, a graph. The obligation is specifically that it is generated. A table transcribed by hand sits on the page looking identical and satisfies the letter of the rubric, so the evidence required is not the table but the declaration that produces or gates it — which only the generated one has.

  • Checked. A kernel-checked declaration: a theorem edge, a proof, an audit that fails the build when the property it checks does not hold.

  • Measured. A reported measurement. This is weaker evidence than a proof and the template keeps it weaker on purpose: a measured result is discharged by naming the parameter it was swept over, the denominator it is relative to, and the statistic it reports.

Reporting all four as a single "done" would let a cross-reference pass for a proof. Reported separately, a document's own matrix says which of its answers are proved and which are merely written down.

Each rubric therefore carries two texts, written for different moments. The rubric is a property of a finished document — what a reader can check by reading it. The author's part is an instruction: the artifact to produce, in the imperative. Neither is derivable from the other by someone who has not built such a document before, which is why the template carries both rather than leaving the second to be inferred from the first.

The template has 26 rubrics: 5 discharged by a section that states the answer, 7 by a view generated from the compiled environment, 13 by a kernel-checked declaration, and 1 by a labeled measurement.