34.9. What the machine can hold, and what it cannot🔗

Everything above is about what a document must contain. This section is about something else: whether anything can check that it contains all of it.

Of the 26 rubrics, 5 have no census and can have none — their population is what the document says. Of the other 21, 16 are walked today (10 by an audit that fails the build, the rest by a generated view or a pinned reading), and 5 have a population a sweep could enumerate and no sweep walking it: for those, the template is reporting exemplars, and is only as complete as the author's memory.

The two are easy to confuse, because a conformance matrix reports them in one word. A status is computed from whether the document offers a site — one declaration, one section — in each channel the rubric's evidence kind requires. A site is never a claim about the rest, so two annotated theorems and two hundred read identically. Where a rubric's population can be walked by the machine, that gap can be closed; where it cannot, the rubric is reporting an exemplar and has to be read as one.

A census needs three things, and each of them either exists or does not.

A population that is a type. #kind_contracts sweeps every declared contract under a namespace — membership is by type, so declaring a boundary enrolls it. That is the whole difference between a census and a list: enrolment has to be a side effect of doing the work, never a second act of remembering. Where the population is what the document says — the measurand, the case for kinds in this domain, the limits of a green status — no such type exists, and no census can.
A decidable per-member predicate. M6 has one: a kind of dimension one either carries an examination principle or it does not. M7 does not — "each separation the model relies on" is not a machine notion, and the nearest mechanical proxy, every pair of dedicated kinds that meet in one signature, is a different claim. Choosing that proxy is a design decision to be made and written down, not a formality to be skipped on the way to an audit.
Declarable exceptions. A census with honest negatives and no way to record them is a census someone will switch off. Kinds of dimension one that are principle-free on purpose — a geometry vocabulary, a nominal designation — are the ordinary case, and an audit that cannot be told so is an audit that gets deleted. @[kindCounterexample] and the declared clusters #kind_scc_clean takes are the library's two idioms for it: the legitimate gap becomes data rather than a sentence in a docstring no audit can read.

Where all three hold, the population can be held at one of three strengths, and the library names them. A reading answers a question. A record is a reading pinned with #guard_msgs: the whole answer is reviewable in the diff and a changed answer fails the build. A gate is the _clean form, which throws and carries no message to re-bless — kept separate from the record for the reason every violation-capable pin needs a gate beside it, that pinning a violation is how it stops being noticed.

The table below says where each rubric of this template stands. The rows to watch are the ones reading census possible: their population could be enumerated and nothing enumerates it, so the rubric is discharged by whichever instances the author remembered, and a green cell on such a row is a statement about those instances and not about the model.

	Closure	What holds the population, or what a sweep would walk
The premise
`M1`	no census	—
`M2`	no census	—
`M3`	no census	—
`M4`	no census	—
The kind vocabulary
`M5`	pinned	the generated kind, record and operation index, walked from the compiled environment
`M6`	gated	`#kind_examination_clean ns …`, with `#kind_examination_coverage` as the record and `@[kindPrincipleFree]` the declared exception; a bare `KindOfProperty` no `DimensionedKind` wraps is reported, not skipped
`M7`	census possible	the pairs of dedicated kinds a signature makes meet — the mechanical proxy for `relied on`, which has to be chosen before it can be swept
`M8`	pinned	`#kind_edges k`, and the Algebra column of the generated kinds table
`M9`	gated	`#kind_boundary_clean ns …` and `#kind_mint_ratchet ns …`
`M10`	pinned	`#kind_dimensional_coverage ns …` and `#kind_scc ns …`, pinned with `#guard_msgs`; the `_clean` forms gate where a model can afford it
The model as modules
`M11`	gated	`#kind_contracts ns …`, or `#kind_contracts_decide ns …` for kernel receipts
`M12`	gated	`#kind_relation_clean ns …`, with `#kind_relation_coverage` as the record and `@[kindRelationFree]` the declared exception
`M13`	gated	`#kind_relations ns …`
`M14`	gated	`#kind_relations ns …`, which fails on a license clause not answered for by name
`M15`	gated	`#kind_mereology_clean ns …`, with `#kind_mereology_coverage` as the record; no exception mark, since the aggregation vocabulary names every honest negative
`M16`	pinned	the module card, generated from the declared contract
Carriers, adequacy and uncertainty
`M17`	census possible	registered carriers with no declared bridge — the carriers are enumerable (the `Carrier`/`NumCarrier` instance vocabulary, specification from executable by `LawfulCarrier`), but a bridge that is a theorem rather than a `CarrierRefinement` instance has no declaration form, so a sweep today would report every real bridge as missing; the form comes first
`M18`	census possible	deployed output ports carrying no adequacy claim
`M19`	census possible	reported uncertainties that name neither a rung nor a coverage
Well-posedness and honest failure
`M20`	gated	`#kind_wellposedness_clean ns …` — every `inverts` edge declares its well-posedness (`wellPosed`, an `∃!`-concluding sorry-free theorem, with the `domain` its statement mentions) or surfaces its ambiguity — with `#kind_wellposedness_coverage` as the record; no exception mark, the two fields are total over the honest negatives; the fields themselves are validated by `#kind_relation`
`M21`	gated	`#kind_inversion_clean ns …` for the domain half — every inverted boundary declares a `conditional` port — with `#kind_inversion_coverage` as the record and `@[kindInversionTotal]` the declared exception; `#kind_wellposedness_clean ns …` for the ambiguity half — an inverts edge that does not prove well-posedness surfaces its `ambiguity` as a declaration
`M22`	gated	`#kind_diagnostic_clean ns …` — every `@[kindDiagnostic]`-marked kind is carried by a produced port of some declared boundary — with `#kind_diagnostic_coverage` as the record; enrollment is the mark itself, so removing a mark is the exemption, and a scope with no marks records that visibly rather than passing in silence
Assurance
`M23`	pinned	the document's own harvest of cited declarations, which cannot omit a node it renders
`M24`	pinned	the graph and ledger directives, generated from the cited nodes
`M25`	no census	—
`M26`	census possible	reported measurements, once each is declared as data rather than written as a number in a sentence