cert
plain-language theorem explainer
Packages the three structural obligations of the Higgs-mass physics module into one certificate: domain cost vanishes on the diagonal, stays nonnegative off it, and the canonical threshold is positive. Anyone citing Module 10's structural status uses this bundle. Construction is a pure field assembly of three sibling lemmas; no new argument.
Claim. There is a certificate for RS Physics Module 10 consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module 10 treats the Higgs mass match $m_H\approx 125.25,\mathrm{GeV}$ against the $\varphi$-ladder identity $\varphi^{13}\approx 521,\mathrm{GeV}\times 0.240\approx 125,\mathrm{GeV}$. The module is marked structural (zero sorry, zero axiom).
The certificate structure demands three facts about the module's domain cost and threshold. Domain cost is the local cost functional on mass/energy pairs; it must vanish when the two arguments coincide (nonzero) and stay nonnegative for positive arguments. The canonical threshold is the positive cutoff used by the module's matching criterion.
Upstream, nonnegativity of recognition cost is already known from ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity on positive states. The sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos specialize that infrastructure to this module's domain cost and threshold.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No tactic proof and no new calculation; pure packaging of already-proved local facts into RSPhysics010Cert.
why it matters
Gives Module 10 a single named certificate object so downstream physics code can assume the three structural hypotheses at once rather than re-importing each lemma. The module doc frames the content as the Higgs rung match on the $\varphi$-ladder (T6 fixed point, mass formula yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). No used_by edges are recorded yet; the companion cert_inhabited is the natural consumer. Closes the structural side of the Higgs match without touching the numerical GeV identification itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.