RSFDNStructural010Cert
plain-language theorem explainer
Certificate structure packaging three structural facts for RS foundation module 10: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Calibration theorists cite it to witness that the E_coh-by-electron-mass layer is well-posed and parameter-free. It is a pure field bundle; inhabitance is discharged downstream by the concrete cert value.
Claim. A structural certificate for module 10 is a triple of facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 10 is the RS calibration layer: the coherence energy $E_{\mathrm{coh}}$ is fixed once by the electron mass, after which all predictions are parameter-free. The local status claim is a structural theorem with zero sorry and zero axiom.
Domain cost is the real-valued cost assigned to a measure/expectation pair $(m,e)$. Its diagonal vanishing says matched pairs carry zero cost; nonnegativity is the cost axiom for positive arguments. The canonical threshold is the positive cutoff used in the calibration comparison.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity (Cost.Jcost_nonneg). The present structure lifts that cost discipline into an explicit three-field certificate type for the structural module.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity of domain cost on positive reals, positivity of the canonical threshold). Inhabitance is not claimed here; the sibling definition cert fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and cert_inhabited wraps that value as Nonempty.
why it matters
Gives the typed witness that module 10's calibration layer is structurally sound before any numerical prediction is emitted. Downstream, cert inhabits the structure and cert_inhabited records Nonempty RSFDNStructural010Cert, closing the module's structural theorem claim (0 sorry, 0 axiom).
In the broader RS chain this sits under foundation forcing: cost nonnegativity traces to the $J$-cost minimum at identity (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), and the parameter-free calibration slogan matches the RS-native constants program ($c=1$, $\hbar=\varphi^{-5}$, etc.). It does not itself force $\varphi$ or $D=3$; it only certifies the cost/threshold side of the electron-mass calibration step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.