17.6. What the requirement clause adds — every claim a model makes, with its evidence🔗

The five clauses before it answer the reviewer's question about a module's computation: the declared boundary says what it reads and produces, the theorem edge says how that relates to its measurement model and the license clause at which carriers, and the mereology clause says how it distributes. Together they are evidence that the module computes what it is specified to compute. They leave open the question a model is asked when it is put to use — do the quantities it produces satisfy what that use demands of them? — and that question has a different shape: its answer names a bound, a band, a tolerance, and sometimes a number the model does not define. The sixth clause answers it the way the other five answer theirs, as data beside the boundary, checked by the elaborator, surveyed and censused by commands whose reports are pinned, and gated. What follows is what that buys, point by point, against the mechanisms the definitions above name.

The demarcation is read off the statement, not granted to the author. A requirement is provable or empirical according to the constants its evidence mentions, and the @[kindReferent] mark is what the check reads: a provable requirement's witness statement may name no referent, and an empirical requirement's gate must name one. The consequence is a symmetry no prose ledger enforces. A claim about the world cannot be presented as a theorem, since a witness whose statement names a datasheet value is refused as provable; and a claim about the model cannot shelter behind a test, since an empirical requirement that names a witness is refused as empirical. The two categories are kinds of evidence, not degrees of confidence: a reader who meets provable in the survey knows the discharge is a theorem the command checked for sorry, and empirical names the referent only observation closes. Metrology draws a neighboring distinction, between verification against a specification and validation for an intended use; the clause cuts along a different line — how a claim is discharged, not what it is about — because that is the line the elaborator can decide. That an output never exceeds a physical bound is an intended-use demand and provable; a rounding budget over the operational input distribution is a design demand and empirical, its referent the distribution.

Non-vacuity, carried from the capstones down to each requirement. The capstone chapter owes every theorem three witnesses — an instance the kernel decides, a mutant that fails, a pinned axiom profile — so that a proved statement is shown to carry weight. A provable requirement owes the same, and the command collects it. Its witness is a theorem edge, checked as the license clause checks one, or a bare theorem whose axioms the report prints; on either route a witness that depends on sorryAx is refused. Its spot checks are the instance: Bool declarations evaluated where the model runs, on the operational inputs. And the construct's own test pins a refusal for each clause of the check beside the acceptances, which is the mutant discipline applied to the checker itself. The spot check is where the carrier ladder bites. The theorem is proved at ℝ; the license clause above records that a side condition does not transfer across carriers on its own; so the Bool the command evaluates at Float is the evidence that the proof reaches the carrier the model runs on and the inputs it meets there — evidence of reach, not a second discharge. The asymmetry with the empirical category is exactly that there the test is the discharge, and its oracle is the referent rather than the requirement's own statement.

A negative claim becomes a discharge. What a module must never do — sum an angular frequency over the pair, distribute a whole-proper quantity over its parts — is as much a requirement as what it must do. The kind algebra can refute such a sum as a theorem, and the oscillator case study does; but the fact a reviewer needs is about the registry: that the environment the model is built in holds no license for the sum. A provable requirement may name that license as the one that must be absent, and the command discharges it by asking the environment for an instance and finding none. The refusals the calculus is built around are thereby citable as the evidence for a stated claim, rather than visible only as a probe that fails to elaborate.

The referent is the constant mint of the validation side. An empirical requirement's gate decides against a threshold, and a threshold that is a bare carrier value with a docstring is the docstring problem in a new place: invisible to every census, its provenance a comment. The referent is a kinded quantity carrying @[kindReferent "where it comes from"], so a datasheet band, a prior, a reference measurement enters the model through a declared tier with its provenance on the record, as a constant mint enters the computation; the mark is what the demarcation reads and what the survey prints beside the requirement. A gate whose threshold is the model's own is refused: a decision against nothing the world supplied is not an observation.

Scope, through the ontological square. "Every spring", "body A", "the objects a decider selects" are quantifiers over particulars, and a requirement scope states them through the Sorted edge of the object type: a sort, named objects, or a decider. Over a boundary whose objects are nominal none of the three is statable. This is where the object layer pays for itself a second time: besides keeping one object's quantity from standing in for another's, it makes a demand about particular objects statable at all — a bound that holds of the coupling spring and not of the wall springs, a band every spring of one sort must lie in — and it is why a requirement is declared beside a boundary whose objects have sorts, not beside a bare function.

What the capstones do not claim becomes what the model states and counts. The capstone chapter closes with what no theorem there asserts — the truth of an attestation, accuracy against nature — and leaves them to the uncertainty chapter and the reader. The requirement clause is where those become data: each an empirical requirement with its referent and gate, or deferred by an attestation whose reason the survey prints. The coverage census then asks of every produced port of every model boundary whether some requirement governs it or a @[kindRequirementFree "reason"] mark says why none does, in the shape of the other coverage censuses, and counts the attested ones. That count is a ratchet: it moves only by a conscious edit, and it is meant to fall as the apparatus supplies its numbers. A model's remaining dependence on the world is then a number in a pinned report, with a reason per entry, rather than a sentence in a limitations section.

What a reader gets. For each output of each module, the survey and the census answer in one pinned report: what must hold of it, in the author's words; over which objects; whether the evidence is a theorem or an observation; where a theorem's proof reaches, by its spot checks; which referent an observation is decided against and where that referent comes from; and what is still attested, with the reason. That is the per-output form of the question the mereology clause closes with — where does this module's guarantee actually come from? — answered from data the elaborator checked rather than from a reading of the source.

The tutorial's harmonic oscillator carries the clause in both categories over the ForPhysLib case study, and its reports are pinned in Tutorial.HarmonicOscillatorRequirements:

The census over the module reads 3 governed, 2 exempted — clean and 4 provable, 3 empirical, 3 attested: the two specification boundaries are listed as the subject of no requirement, and the three attestations are the ratchet's opening count. The node below is the clause's witness in this document, in the form the capstones set.