RSFDNStructural009Cert
plain-language theorem explainer
Certificate record bundling three structural facts: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is strictly positive. Downstream code cites it to inhabit the module-9 structural certificate and prove Nonempty. Pure structure definition; no proof body.
Claim. A structural certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals $0$; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 9 sits in the RS foundation forcing chain (T5 J-uniqueness through T8 forcing $D=3$). It packages structural facts about a domain-level cost and a canonical threshold used as a recognition cutoff.
Domain cost is the real-valued cost assigned to a pair of positive scale parameters (measured versus expected, or two ladder coordinates). The diagonal identity domainCost r r = 0 for $r \neq 0$ says matched scales incur zero cost. Nonnegativity for positive arguments is the continuous analogue of the upstream fact that every recognition event has nonnegative cost (via Jcost_nonneg on the event state).
The canonical threshold is the fixed positive cutoff against which domain costs are compared in later structural steps. The module status line records a structural theorem layer with zero sorry and zero axioms once the certificate is inhabited.
proof idea
Definition only: a structure with three propositional fields and no constructors beyond the record. Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No tactics or term-mode proof appear on this declaration.
why it matters
Gives the typed interface for RS structural module 9 so the forcing-chain layer can export a single inhabited certificate rather than three loose lemmas. Downstream, cert builds a concrete value and cert_inhabited proves Nonempty of the certificate type, closing the module's structural export.
In the broader chain this sits after T5 (J-uniqueness, $J(x)=\cosh(\log x)-1$) and the Recognition Composition Law, and before or alongside the T6--T8 steps that force $\varphi$, the eight-tick octave, and $D=3$. The packaged nonnegativity and diagonal vanishing are the minimal cost axioms needed for threshold comparisons later in foundation modules. No open scaffold remains on this declaration itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.