33. Using the library: annotations and generated indexes🔗

The preceding chapters develop the calculus. This one is about working in it: the annotations an author writes, what each one changes, and the indexes the library generates from them.

Four things cannot be inferred from a definition and so must be stated by its author. Each is a family of annotations, and each has its own section below.

Where the calculus is left — each site at which a value already carrying one kind is re-typed as another, the plumbing that must drop to the carrier, the point at which a kinded value becomes a naked one. The boundary family: @[kindCrossing], @[kindIngest], @[kindConst], @[carrierVocab] and @[kindEmission] each name the tier that sanctions a boundary site; @[kindCarrier] is what brings a downstream carrier under the audit at all, @[kindAttest] registers a wrapper through which authored mints go on the record, and @[kindCounterexample] exempts a deliberate falsification probe from the provenance sweeps.
What a vocabulary answers for — whether every dimension-one kind is individuated, every boundary carries a measurement model, every inversion says where it fails. The census marks: @[kindPrincipleFree], @[kindRelationFree] and @[kindInversionTotal] record an honest negative with its reason, and @[kindDiagnostic] enrolls a conditioning output.
How a definition should read — the notation, the constants, the intermediate bindings a rendered equation should keep. The rendering family: @[pkc_math], steered by @[pkc_math_symbol], @[pkc_math_config] and @[pkc_math_transparent].
What an external document says — which requirement a theorem discharges, which clause of Dybkær or VIM a definition formalizes. The metadata family: @[requirement], @[dybkaer] and @[vim4].

The distinction that matters most is between the first two families and the other two, and it is a distinction about what happens when an annotation is absent. A boundary site that carries no tier is reported as a violation by #kind_boundary_audit, and that report is pinned, so omitting @[kindCrossing] fails the build, and a dimension-one kind with neither a principle nor a @[kindPrincipleFree] mark fails #kind_examination_clean the same way: the annotation discharges an obligation about the code, in the way a proof discharges one about a proposition. Omitting a rendering or metadata annotation fails nothing — @[pkc_math_symbol] changes only how something reads. Read the Enforcement column below with that asymmetry in mind: it says checked for @[pkc_math] and @[pkc_math_config] too, but what those checks reject is a misuse of the annotation — an argument naming a binding the definition does not have, an attribute attached to something that is not a structure — never its absence.

Everything in the Generated indexes section at the end is computed from the environment when this chapter is built, scoped to this package's own worked examples. No row is maintained by hand, so a renamed declaration is a build error rather than a stale table.