17.5. The requirement clause — what the model must satisfy🔗

The five clauses above say what a module computes, how that relates to its measurement model, at which carriers, and how it distributes. None says what the module's quantities must satisfy — the input/output ratio that may not exceed a bound, the output that must lie in a band, the idealization whose error must stay below a tolerance — nor by what evidence each demand is met. A requirement is that statement, as data beside the declared boundary it governs, in the shape the theorem edge set: declaration names the environment resolves, the author's words where the calculus cannot read them, and nothing the commands do not check.

Two categories, told apart by the statement and not by the effort. A provable requirement closes over the model's own declarations and kinded quantities — every constant its statement mentions is the model's or the library's — so a theorem about the model discharges it: a theorem edge from the governed boundary to a specification boundary, a declared boundary whose one member computes the bound and whose role says so, or a bare theorem; a negative one — "this is never summed over the pair" — by the absence of a license the elaborator asks the environment for and must not find. Where the model also runs, the requirement names its spot checks: Bool declarations the requirement command evaluates and requires true, the way an inhabitation check spot-checks a proof — evidence that the proof reaches the carrier the model runs on and the operational inputs, not a discharge. An empirical requirement names a referent the model does not define — a datasheet value, a prior, a reference measurement, a population — so no theorem about the model alone can discharge it, however much proof is spent: the referent is a free variable only observation closes, which makes this the falsifiable category and testing its correct instrument rather than a fallback. It is discharged by a gate, a decider whose threshold is the referent, or deferred. The referent is a kinded quantity carrying @[kindReferent "where it comes from"], and the mark is what makes the demarcation mechanical: a provable requirement's statement may name no referent, and an empirical requirement's gate must name one. Either category may be attested, in the sense of attestation: deferred with a reason in the author's words. That is not a third category but a ratchet, counted by the census and meant to fall.

A requirement has a requirement scope: the objects it quantifies over — every object the boundary is evaluated for, every object of a named sort, reached through the Sorted edge of the ontological square, named objects, or the objects a named decider selects. "Every spring" is a sort, "the coupling spring" is an object, and neither is statable over a boundary whose objects are nominal.