@[kindCrossing]

a definition

Two kinds can meet in two ways. Under a law — an authored edge such as ProductKind k₁ k₂ k or a KindMul entry — the calculus derives a third kind from two, and the use site needs no annotation, because the edge already licenses it. 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, which is why it must be declared and why the audit counts it. Both kinds are stated in the signature, on the argument side as much as the result; the mint or erasure inside is the crossing's mechanism, reviewed once.

checked — rejected at elaboration if no argument carries a registered carrier; #kind_boundary_audit also reports an untagged boundary site as a violation

@[kindIngest]

a definition

Declares a checked ingest mint: raw external/host data enters the calculus for the first time, admitted through some check. The dual of @[kindCrossing] — no argument need carry a kind, because none has been established yet.

checked — #kind_boundary_audit reports an untagged boundary site as a violation

@[kindConst]

a definition

Declares a constant mint: an adjudicated value enters the calculus as data — a cited table, a configuration bound, a seed, a threshold, or a structural constant.

checked — #kind_boundary_audit reports an untagged boundary site as a violation

@[carrierVocab]

a definition

Registers kind-preserving representation plumbing — an operation the kind algebra does not name (a branchless min, a map over a coefficient table) that must drop to the carrier.

checked — #kind_boundary_audit reports an untagged boundary site as a violation

@[kindEmission]

a definition

Marks a genuine emission boundary: a kinded value becomes a naked one for a consumer outside the calculus (a deploy driver, a tape recorder).

checked — #kind_boundary_audit reports an untagged boundary site as a violation

@[kindCarrier]

a structure

Registers a downstream single-field quantity-like carrier, so the boundary audit recognizes its mints and erasures — and so its records and operations are indexed.

checked — rejected at elaboration if the declaration is not a structure

@[kindCounterexample]

a Provenance.Contract or Provenance.Relation definition

Marks a deliberate provenance counterexample — a falsification probe kept because its checker refuses it. The by-type sweeps (#kind_contracts, #kind_contracts_decide, #kind_relations) list it as exempted instead of gating on it, and the contracts and provenance-coverage tables neither count it as a witness nor as a coverage subject.

checked — rejected at elaboration if the declaration is not a Provenance.Contract or Provenance.Relation

@[kindAttest]

a definition taking a `KindOfProperty` and a `String` argument

Registers an authored-mint attestor (Quantity.attest is built in): the boundary audit reports each of its call sites with the reason string harvested from the argument, and skips the attestor's own body, so the wrapper's one raw mint is reviewed once, at registration, instead of hiding every site behind the wrapper's name.

checked — rejected at elaboration unless the declaration takes both a KindOfProperty argument (the attested kind) and a String argument (the reason)

@[pkc_math]

a Quantity-valued definition

Renders the definition as typeset LaTeX into its own docstring, so doc-gen4 and the InfoView display the equation. Clauses keeping and substituting control let-bindings and derivations; a literal string argument overrides the rendering entirely.

checked — rejected if keeping names an unbound let, if substituting names a recursive definition, or if a literal override is combined with either clause

@[pkc_math_symbol "…"]

any declaration

Fixes the LaTeX a token renders as, overriding every naming heuristic. The optional operator modifier prints a one-argument application as juxtaposition rather than a call.

advisory

@[pkc_math_config]

a structure

Declares a configuration type: its field projections render as the qualified constant Struct.field rather than as a function applied to the configuration value.

checked — rejected at elaboration if the declaration is not a structure

@[pkc_math_transparent]

a definition

Marks a notational wrapper the renderer should see through, so the wrapped term is rendered in place of a call to the wrapper.

advisory

@[requirement "…" role]

any declaration

Records that the declaration specifies, proves, implements or exemplifies a numbered requirement.

advisory

@[dybkaer "…" "…"]

any declaration

Records the Dybkær Ontology on Property section and term this declaration formalizes.

advisory

@[vim4 "…" "…"]

any declaration

Records the VIM 4 2CD entry and term this declaration corresponds to.

advisory

@[kindPrincipleFree "…"]

a `DimensionedKind` definition

Declares that a dimension-one kind is legitimately without an examination principle, with the reason: #kind_examination_coverage lists it as exempted and #kind_examination_clean does not fire on it. Inert on a kind that carries a principle.

checked — rejected at elaboration unless the declaration is a DimensionedKind and the reason is non-empty

@[kindRelationFree "…"]

a `Provenance.Contract` definition

Declares that a boundary legitimately has no theorem edge — its behavior is not a measurement model — with the reason: #kind_relation_coverage lists it as exempted and #kind_relation_clean does not fire on it. Inert on a boundary an edge names.

checked — rejected at elaboration unless the declaration is a Provenance.Contract and the reason is non-empty

@[kindInversionTotal "…"]

a `Provenance.Contract` definition

Declares that an inverted boundary legitimately has no conditional port — the inversion is total on its input type — with the reason: #kind_inversion_coverage lists it as exempted and #kind_inversion_clean does not fire on it. Inert on a boundary that declares a conditional port.

checked — rejected at elaboration unless the declaration is a Provenance.Contract and the reason is non-empty

@[kindDiagnostic "…"]

a `KindOfProperty` definition

Declares a kind to be a quality or conditioning output a consumer must read, with what it diagnoses: #kind_diagnostic_coverage then asks the declared boundaries in scope for a produced port carrying it. The mark is the census's enrollment — an unmarked kind is not walked, and removing a mark is the exemption.

checked — rejected at elaboration unless the declaration is a KindOfProperty and the description is non-empty