34.4. The kind vocabulary — and the audits that close it
A model's kind vocabulary is only as good as its closure. Two things can escape it: a quantity the document names but the code carries as a bare number, and an operation on kinded values the declared algebra never licensed — a product formed outside the arithmetic surface, or a crossing between two kinds performed without being authored. The difference between a model that has declared some kinds and a model whose kind discipline is load-bearing is whether anything checks for either, and rubrics M5 through M10 are all variations on that question. The closure asked for is over the document's own vocabulary and not over its domain: it makes no claim that the model covers the physics, only that every quantity the model does name is inside the discipline, and every step out of the discipline is authored.
-
M5 — The kind inventory. Every quantity the document names is a declared kind-typed quantity, reported as an inventory rather than a survey — a table generated by walking the compiled environment, which cannot omit a declaration the way a grep can.
-
M6 — Individuating dimension one. Kinds of dimension one are individuated by their examination principle, with the procedure ⊑ method ⊑ principle refinement recorded: inside the dimension-one fiber the principle is the only thing that separates two kinds, so a model that declares such kinds without recording what examines them has named them, not individuated them.
-
M7 — Dedications, and the separations proved. Dedications to systems and components are declared, and — the part that makes it a
checkedrubric rather than ageneratedone — each separation the model relies on is proved. A dedication nothing depends on separating is inventory; a dedication a chapter's argument rests on is a theorem. -
M8 — The arithmetic surface. The complete list of products, quotients and powers the model is permitted to form. Read the other way, it is the list of combinations the model has decided are meaningless, which is the more useful reading and the one a generated table gives for free.
-
M9 — Authored departures, gated by an audit. The rubric the group exists for. Every departure from the algebra — a genuine meeting of two kinds, kind-preserving plumbing the algebra does not name, a point where a kinded value leaves the calculus — must be authored, and an audit that fails the build on an unauthored one is what turns the resulting list from a survey into an inventory. Without that audit the list means "the crossings someone thought to write down"; with it, the list is closed.
-
M10 — Dimensional coverage and inter-derivability. Two audits that report rather than gate. Dimensional coverage checks each authored edge against the dimension functor — the one layer that can mechanically refute an authored axiom, since an edge over genuinely dimensioned kinds whose exponents fail to balance is wrong, not merely undeclared — and its value is the inventory it produces: where the dimensioned content actually lives, and how much of the model is dimension one and therefore the kind layer's problem alone. And where kinds are inter-derivable — where each can be manufactured from the others by licensed steps, so the algebra cannot refuse a substitution between them — the template asks that this be drawn and pinned rather than left implicit. A model with such clusters is not defective; a model that has them and does not say so is.