33.3.1. @[kindCrossing] — an authored crossing🔗

Two kinds can meet in two ways, and only one of them is a crossing. Under a law — an authored edge, ProductKind k₁ k₂ k or a KindMul entry — the calculus derives a third kind from two, and the use site needs no annotation at all, because the edge already licenses it. Those are the edge audits' subject, not this family's.

A crossing is the case no law covers: a value already carrying one kind is re-typed as another on the author's signature rather than on a derivation. An edge is a rule the calculus applies; a crossing is a place the calculus is left. That asymmetry is why one is inferred at every use and the other must be declared once and counted.

Both kinds are stated in the signature — on the argument side as much as the result: add rejects a @[kindCrossing] declaration none of whose arguments carries a registered carrier, because a crossing goes FROM an already-kinded value, and a declaration with no kinded argument has nothing to cross from. The mint or erasure inside is the crossing's mechanism, reviewed once.

/-- A tagged crossing minting the probe output kind from an already-kinded gain value. -/
@[kindCrossing]
def probeCrossing (g : Quantity gainKind Float) : Quantity outputKind Float := ⟨g.magnitude⟩

A declaration with no kinded argument at all — probeCrossing (x : Float) : Quantity outputKind Float := ⟨x⟩ — is rejected at the @[kindCrossing] line itself, with a message pointing at the two tiers below it is actually one of: @[kindIngest] if something is checked on the way in, @[kindConst] if it is a fixed literal.

In the InfoView. Nothing else changes on the declaration itself. The effect is on the audit: #kind_boundary_audit prints one line per boundary-active declaration, and the tier tag is what distinguishes a sanctioned site from a violation.

boundary audit:
[kindCrossing] …probeCrossing — mints: outputKind
[carrierVocab] …probeVocab — mints: gainKind
[kindEmission] …probeEmission — erases (emission-only)
[kindIngest] …probeIngest — mints: outputKind
⚠ UNTAGGED …violationSite — mints: outputKind

The last line is the point. An untagged mint is reported as a violation, and because the report is pinned with #guard_msgs in an indexed probe, a new interior boundary fails the build — the same discipline by which a pinned axiom profile catches a proof silently relocated behind a sorry.

And the two gates beside it. #kind_boundary_clean ns… states the same invariant without a message: it throws when any boundary-active declaration in scope carries no tier. The audit says what the boundary is; this says every one of its sites has been adjudicated, and re-blessing the first cannot silence the second because there is nothing here to re-bless. #kind_mint_ratchet ns… tightens the granularity. A tier tag sanctions a whole declaration, so a @[kindCrossing] body can hold any number of interior ⟨…⟩ under one sanction; the ratchet requires that at the crossing and carrier-vocabulary tiers every mint be a licensed derivation or a Quantity.attest whose reason is harvested — the raw column stays empty, so a new anonymous mint fails the build instead of joining a list nobody re-reads. @[kindConst] and @[kindIngest] keep raw mints legal at the declaration granularity, because there the declaration's own evidence is the sanction.

In the generated indexes. Every tagged site appears in the kind-crossing table with the kinds it mints, taken from the audit's own walk so the two cannot disagree. #kind_crossings [ns…] is the same registry from the InfoView — every sanctioned site with the first line of its docstring, grouped by tier. It reads the registry where the audit walks the environment, which is why the audit can report a site the registry does not contain: that site is the violation.

33.3.2. @[kindIngest] — a checked ingest mint🔗

The dual of @[kindCrossing]: raw, external data — a host column, a JSON blob, an env-var's text — enters the calculus for the first time, admitted through some check (a KindAdmissible/ BatchAdmissible instance, an inline range test, a fallible parse). No argument carries a kind, because none has been established yet — that is the entire point of an ingest boundary, and the reason @[kindCrossing]'s own check must not reject it: the check performed is this declaration's evidence, stated once, rather than presupposed.

/-- A checked ingest mint: a raw carrier value enters the calculus as the probe output kind. -/
@[kindIngest]
def probeIngest (x : Float) : Quantity outputKind Float := ⟨x⟩

33.3.3. @[kindConst] — a constant mint🔗

The third mint tier, and the one a nullary crossing candidate turns out to be. Where @[kindCrossing] goes from an already-kinded value and @[kindIngest] admits external data through a check, @[kindConst] mints from neither: the value is adjudicated data — a cited coefficient table, a configuration bound or box, a seed, a threshold, or a structural constant of the model such as a zero accumulator or the vacuum index 1.

/-- The probe's adjudicated threshold, cited to the table it is read from. -/
@[kindConst]
def probeThreshold : Quantity outputKind Float := ⟨0.02⟩

The mint's value is data rather than dataflow, so its provenance is the declaration's docstring rather than its signature — there is no argument to trace it to. That is why the tier exists as its own tag instead of collapsing into @[kindCrossing]: a declaration with no kinded argument is definitionally this tier, having nothing to cross from, and the crossing attribute's rejection message names it for exactly that reason.

33.3.4. @[carrierVocab] — a carrier-vocabulary exception🔗

Representation plumbing for an operation the kind algebra does not name: a branchless minimum, a square root on the complex carrier, a map over a coefficient table. Kind-preserving by construction, which is what distinguishes it from a crossing.

/-- A carrier-vocabulary exception on the probe kinds. -/
@[carrierVocab]
def probeVocab (a b : Quantity gainKind Float) : Quantity gainKind Float :=
  ⟨min a.magnitude b.magnitude⟩

33.3.5. @[kindEmission] — a genuine emission boundary🔗

Where a kinded value legitimately becomes a naked one for a consumer outside the calculus: a deploy driver, a tape recorder, a serializer.

/-- An emission boundary out of the probe world. -/
@[kindEmission]
def probeEmission (x : Quantity outputKind Float) : Float := x.magnitude

33.3.6. @[kindCarrier] — teaching the audit a new carrier🔗

The audit recognizes a boundary as an application of a carrier structure's constructor or first-field projection. Quantity and CertifiedQuantity are built in; a downstream layer registers its own — soil-moisture-model registers its DedicatedQuantity, which carries a DedicatedKind rather than a KindOfProperty.

/-- A toy single-field carrier, standing in for the model's `DedicatedQuantity`. -/
@[kindCarrier]
structure Tagged (k : KindOfProperty) (R : Type) where
  magnitude : R

Registering a carrier is the single opt-in that also earns a layer the two structural indexes: the kinded-record and kinded-operation tables recognize a structure or definition by whether a registered carrier appears in its fields or its result type. A layer therefore cannot register for the audit and be missed by the indexes, or the reverse.

Why the crossing table is not here. The core spine has no kind crossings, and that is a fact about what the spine is rather than an omission: a crossing is where a model meets a measurement, so crossings live downstream. The populated table — twenty-three sites, with the kinds each one crosses — is in soil-moisture-model's technical reference. This chapter's boundary examples come from the validation probe that pins the audit's behaviour.

33.3.7. @[kindAttest] — a registered attestor🔗

An attested mint is an authored ⟨…⟩ written through a registered attestor that names its reason at the call site; Quantity.attest is the built-in one. The audit cannot see through a named wrapper — a helper's body is walked once, under the helper's own name, so a declaration that mints through an unregistered wrapper shows nothing at its own site. Registration turns that hiding into accountability: the audit recognizes a registered attestor's applications, reports each site with the reason string harvested from the argument, and skips the attestor's own body, whose one raw mint is the sanctioned mechanism, reviewed at registration — the same reason a carrier's own constructor is not a site. The attribute derives the attestor's footprint from its signature, and refuses a declaration that does not carry both arguments it needs:

`@[kindAttest]` expects a declaration taking a `KindOfProperty` argument (the attested kind) and
a `String` argument (the reason) — '…' has neither or only one. Without both, attested sites
could not be harvested, and the wrapper would HIDE its mint from the walk instead of putting it
on the record.

The discipline the registry serves: raw mints are the suspect column — a declaration-level tier covers however many its body holds, multiplicity unseen — and attested mints the reviewed one, each surviving site carrying its own one-line justification into the pinned report. An attestation is a claim with no machine-checkable evidence; where evidence exists, the licensed route — a KindAdmissible check at ingest, a ProductKind or QuotientKind witness edge — is what to write instead, and the reason should say why no check applies.