RSPhysics012Cert
plain-language theorem explainer
Certificate structure for RS Physics Module 12 (W-boson mass rung). It packages three obligations: domain cost vanishes on the diagonal, domain cost is nonnegative for positive mass and energy, and the canonical threshold is positive. Downstream code builds a concrete inhabitant and proves the type is nonempty. Pure definitional packaging; proofs live in the field witnesses.
Claim. A Module-12 certificate is a triple of facts: (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 12 is the structural W-boson mass claim: $M_W\approx 80.4,\mathrm{GeV}$ is matched by a $\varphi$-ladder evaluation $\varphi^{13}\cdot 0.154\approx 80.3,\mathrm{GeV}$, reported as MATCH with zero sorry and zero axiom.
The certificate does not compute that number. It packages cost and threshold side-conditions used by the module. Domain cost is the local comparison of a mass scale to an energy scale; the diagonal vanishing clause says equal arguments carry zero cost. Nonnegativity for positive arguments is the module-level shadow of the global fact that recognition cost is nonnegative.
Upstream, ObserverForcing records that every recognition event has nonnegative cost, via nonnegativity of the J-cost $J(x)=(x+x^{-1})/2-1$ (the unique cost forced by the Recognition Composition Law, T5). The canonical threshold is the module's positive cutoff for the ladder comparison.
proof idea
No proof body: this is a structure declaration. Any inhabitant must supply three proofs matching the field types. The concrete assembly is the sibling definition cert, which fills the fields from domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Nonemptiness is then immediate from that witness.
why it matters
Gives the typed bundle that cert and cert_inhabited close, so Module 12 can claim a structural theorem with an inhabited certificate rather than ad-hoc lemmas. In the RS mass ladder, W sits near rung 13 with the yardstick formula $\mathrm{yardstick}\cdot\varphi^{(\mathrm{rung}-8+\mathrm{gap}(Z))}$; the certificate's cost and threshold fields are the local hygiene that makes that MATCH claim machine-checkable. It does not itself derive $M_W$ from T0–T8, but it is the module's formal gate that those cost axioms hold before the numerical comparison is trusted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.