RSPhysics010Cert
plain-language theorem explainer
Certificate structure packaging three elementary cost/threshold facts for the Higgs-mass physics module: diagonal domain cost vanishes, domain cost is nonnegative on positive mass and energy, and the canonical threshold is strictly positive. Downstream code cites it to build a concrete witness and prove the certificate type is inhabited. Pure definitional packaging of Prop fields; no proof body.
Claim. A certificate is a triple of assertions: (1) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (2) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (3) the canonical threshold is strictly positive.
background
Physics RS Module 10 records the structural claim that the Higgs mass sits on the $\phi$-ladder: $m_H \approx 125.25,\mathrm{GeV}$ matches $\phi^{13}$ scaled into GeV units (module status: structural theorem, zero sorry, zero axiom).
The local cost object is domainCost, a real-valued functional of two positive scale parameters (mass and energy in the module's convention). The first certificate field asks that this cost vanish on the diagonal away from zero; the second asks nonnegativity off the axes. The third field is positivity of canonicalThreshold, the module's fixed comparison scale.
Upstream, nonnegativity of recognition cost is already known in ObserverForcing: every recognition event has cost $\ge 0$, via nonnegativity of the $J$-cost on positive states. The present structure lifts that style of cost inequality into the Higgs-module domain language.
proof idea
No proof: this is a structure whose three fields are propositions. Inhabitation is discharged later by the concrete term cert, which fills the fields with the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The structure itself only names the interface.
why it matters
Gives the typed interface that Module 10 uses to assert its cost and threshold package is coherent. The definition cert builds an instance field-by-field from the sibling lemmas; cert_inhabited then records Nonempty RSPhysics010Cert by packaging that instance.
In the broader Recognition chain this sits under the physics layer that places particle masses on the $\phi$-ladder (yardstick times $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). The module headline is the Higgs match $\phi^{13}\sim 125,\mathrm{GeV}$. The certificate does not itself derive the rung or the GeV conversion; it only locks the elementary cost/threshold side conditions the module treats as structural.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.