2.13. The measurement model, licensed distribution, and stated requirements (R26–R28)🔗

R26 — A module's behavior is a checked measurement model. The metrological-modularity chapter's behavior clause, stated as an expressiveness requirement: a declared boundary carries relation edges (Provenance.Relation) whose witnesses are kernel-checked theorems; every relation kind has a conclusion-shape check; a boundedBy edge names a kinded tolerance; named side conditions are checked against the witness statement; and every carrier rung beyond the witness's own is answered for by a named repair or restatement (RelationLicense) — a rung claimed with neither is refused. The checks are the elaborator's (#kind_relation, surveyed by #kind_relations), pinned by acceptance and refusal probes for all four relation kinds.

R27 — A module's distribution is licensed by declared extensivity. The mereology clause as a verifiable requirement: produced ports carry aggregation classes (Provenance.AggregationClass — the §13.5 vocabulary of the extensivity chapter, extended by the count-keyed, parameter-conditioned, and interface-licensed classes, each naming the tolerance, sortal, transport, or law that is the content of its claim), and recarving or sharding a module's batch axis is licensed by theorem from those declarations: Recarving.distribution_license — one map, every declared-extensive output's total preserved — with the quasi-extensive price at most both carvings' joins times the per-join tolerance, tied to the rounding budget where the carrier demands it. The clause's hygiene is the elaborator's (checkAggregations, rendered in every #kind_contract report), pinned by acceptance and refusal probes.

R28 — A module's requirements are stated with their evidence. The requirement clause of the metrological-modularity chapter, stated as an expressiveness requirement: every produced port of a model boundary is governed by a Provenance.Requirement or exempted with a reason (@[kindRequirementFree]); object scopes are compared with the result domain inferred from the member's return type, while missing indices or unresolved object domains are unchecked violations unless exempted; .sort requires an indexed result and a Sorted instance; the census first reduces the actual result bearer's sort inside the member telescope, then falls back to object scopes or is ungoverned on a definite mismatch, while a stuck sort follows the object-domain path and may be unchecked. A .decided scope requires a deciderProof theorem proving that its decider holds for every result of the governed member; otherwise the port is unchecked. A provable requirement's witness is a sorry-free theorem, or a theorem edge to a specification boundary, whose statement names no @[kindReferent]-marked declaration, with Bool spot checks the command evaluates where the model runs; an empirical requirement names marked referents and a gate mentioning one, and no witness; a claimed absence is a license the environment holds no instance of; and an attestation never stands beside a discharge. The checks are the elaborator's (#kind_requirement, surveyed by #kind_requirements, censused by #kind_requirement_coverage and gated by #kind_requirement_clean), pinned by acceptance and refusal probes; what the clause buys is argued in every claim a model makes, with its evidence.