HiggsBosonCert
plain-language theorem explainer
The HiggsBosonCert structure packages three properties of the J-cost function: it vanishes at unity, is strictly positive for all other positive arguments, and is invariant under inversion. Researchers modeling the Higgs sector within Recognition Science would reference this to establish the vacuum as the recognition minimum. The declaration is a bare structure definition with no internal proof steps, relying on sibling lemmas to populate its fields in the downstream instance.
Claim. A structure consisting of three properties of the J-cost function $J$: $J(1)=0$, for all $r>0$ with $r≠1$ one has $J(r)>0$, and for all $r>0$ one has $J(r)=J(r^{-1})$.
background
The J-cost function is imported from the Cost module and measures recognition cost for a scale factor $r$. The module develops the Higgs boson mass in RS terms, where the electroweak vacuum expectation value $v=246$ GeV fixes the scale and the Higgs mass satisfies $J(m_H/v)=J(phi^{-2})$. The structure encodes the claim that the Higgs vacuum corresponds to the unique J-cost minimum at $r=1$, with mass arising from the second derivative $J''(1)=1$ (the calibration condition). It depends on the upstream theorem from the HiggsMechanism module stating that particle mass is positive for positive Yukawa coupling.
proof idea
This is a structure definition that declares three fields encoding the vacuum zero, positivity, and symmetry properties of the J-cost function. There is no proof body. The instance is constructed downstream by supplying proofs from the sibling definitions higgs_vacuum, higgs_mass_positive, and higgs_symmetry.
why it matters
This structure provides the interface for certifying Higgs boson properties in the J-cost formulation and is instantiated by higgsBosonCert in the same module. It realizes the structural claim in the module documentation that the Higgs vacuum at $v$ corresponds to the unique J-cost minimum at $r=1$. In the framework it connects to T5 J-uniqueness and the phi-ladder mass formula, supporting the prediction $m_H^2 = v^2 (1 - J(phi^{-2}))$ while touching the open question of deriving the precise numerical Higgs mass from J-cost calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.