33.7. What a vocabulary answers for — the coverage censuses🔗

The audits so far ask about one declaration, one namespace's boundary, or one boundary's agreement with itself. The censuses ask the question the model template's rubrics put to a whole vocabulary: over a population the environment can enumerate — every dimension-one kind, every declared boundary, every produced port, every inversion edge — does each member declare what the rubric obliges it to? Six censuses share one shape, set by #kind_examination_coverage: a record command whose sorted info message is pinned, a _clean gate that throws and pins nothing, a declared exception where the population has honest negatives, and an audit receipt at each success point — which is what lets a document's conformance table read a rubric as green only in a build where its census ran over the document's scope.

• #kind_examination_coverage ns … (M6) walks every dimension-one DimensionedKind in scope and reports it [individuated] by its examination principle, ⊘ exempted by a @[kindPrincipleFree] mark, or ⚠ UNINDIVIDUATED. Inside the dimension-one fiber the principle is the only defining aspect that separates two kinds, so a kind declared without one is named, not individuated. A KindOfProperty that no DimensionedKind wraps is reported ⚠ UNDIMENSIONED rather than decided: "dimension one" is a fact about a dimension the vocabulary never declared, and a gate that passed over such kinds would pass over nothing.

• #kind_relation_coverage ns … (M12) walks every Provenance.Contract in scope and reports it [witnessed] by the theorem edges naming it, ⊘ exempted by a @[kindRelationFree] mark, or ⚠ UNWITNESSED. Relations are walked unscoped, since a theorem edge may live beside a deployment rather than beside the boundary it is about, and a @[kindCounterexample] relation is not a witness. Whether a named edge is valid is #kind_relations' question; this census asks only whether one exists.

• #kind_mereology_coverage ns … (M15) walks every produced port — output or conditional — of every contract in scope and reports it [classed] by its aggregation class or ⚠ UNDECLARED. There is no exception mark: the AggregationClass vocabulary is total over the honest negatives — a port that must never be summed declares .intensive, one its parts do not determine declares .wholeProper — so declaring nothing is exactly the finding.

• #kind_inversion_coverage ns … (M21, the domain half) walks every contract that an inverts edge names as its left side — the boundary that recovers what another consumed — and reports it [guarded] by a conditional port, with its decider where one is named, ⊘ exempted by a @[kindInversionTotal] mark, or ⚠ UNGUARDED.

• #kind_wellposedness_coverage ns … (M20, and M21's ambiguity half) walks every inverts edge in scope and reports it [well-posed] by a wellPosed witness on its declared domain, [surfaced] by an ambiguity witness, or ⚠ UNDECIDED. No exception mark: an inversion either has exactly one answer on a declared domain or it does not, and either answer is a declaration.

• #kind_diagnostic_coverage ns … (M22) walks every @[kindDiagnostic]-marked kind in scope and reports it [exported] by a produced port carrying it or ⚠ SIDECHANNELED. Enrollment is the mark, so a scope with no marks records that visibly rather than passing in silence.

Each has its _clean sibling — #kind_examination_clean, #kind_relation_clean, #kind_mereology_clean, #kind_inversion_clean, #kind_wellposedness_clean, #kind_diagnostic_clean — which throws while any member of its population is a ⚠ row, and records the audit receipt exactly when it does not fire. A @[kindCounterexample] contract is a subject of none of them and is listed as exempted, so a census says what it skipped; a mark on a member that satisfies the predicate anyway is inert, so a stale exemption cannot hide a declaration made later; and a contract declared at node or kind types the census cannot read is reported ⚠ UNREADABLE rather than walked past. Every census is import-closure sensitive in the direction the other environment walks are: an exemption declared in a module the probe does not reach is a loud false alarm, never a silent pass.

The pinned form of the first, from the validation suite — the namespace prefix and two further [individuated] rows elided:

examination coverage:
[individuated] …probeIndividuated (probe individuated) — principle: probe-principle
⊘ exempted …probeGeometry (probe geometry) — the wave calculus's own geometry, the product of no phenomenon
⚠ UNDIMENSIONED …probeBareKind (probe bare kind) — no DimensionedKind wraps it
⚠ UNINDIVIDUATED …probeBare (probe bare)
5 dimension-one kind(s): 3 individuated, 1 exempted, 1 UNINDIVIDUATED; 1 kind(s) UNDIMENSIONED — examination-coverage violation

/-- Dimension one, no principle, exempted with a reason. -/
@[kindPrincipleFree "the wave calculus's own geometry, the product of no phenomenon"]
def probeGeometry : DimensionedKind :=
  { kind := { id := "probe geometry", scale := .ratio }, dim := 1 }

`@[kindPrincipleFree]` expects a 'DimensionedKind' — '…notAKind' is not one. The mark exempts a
dimension-one kind from the examination-coverage sweep, and dimension is a fact about the
DimensionedKind, so that is where the mark goes.

/-- No edge, on purpose. Its port is classed. -/
@[kindRelationFree "a data-movement boundary: its behavior is the identity on kinds, and \
  there is no measurement model to carry"]
def dataMove : Provenance.Contract NodeId KindRef where …

/-- Inverted, no conditional port, exempted as total. -/
@[kindInversionTotal "total on its input type: every integer is the forward's image of one, \
  so there is no outside to detect"]
def totalInverse : Provenance.Contract NodeId KindRef where …

/-- A quality kind the retrieval exports: marked diagnostic, and carried by a produced
port of `Good.invBoundary` below. -/
@[kindDiagnostic "whether the retrieval's answer was decided inside its domain"]
def qcK : KindOfProperty := { id := "contract coverage probe quality", scale := .ordinal }