mH_obs
plain-language theorem explainer
The declaration supplies the numerical value of the observed Higgs boson mass, 125.2 GeV. Researchers verifying the Recognition Science mass predictions against LHC data cite this constant when checking the (120, 130) GeV interval. The entry is a direct definition that carries no proof obligations.
Claim. The observed Higgs boson mass is defined by $m_H^{obs} = 125.2$ GeV.
background
Recognition Science derives the Higgs mass from the phi-ladder in the broken electroweak phase. The physical Higgs scalar remains after three Goldstone bosons are absorbed into the W and Z vector bosons. The module sets lambda equal to one half from the second derivative of the J-cost potential and combines it with the Weinberg angle (3 - phi)/6 to obtain the base value near 118 GeV, then applies the Q3 correction of order 1/16 to approach the observed datum.
proof idea
Direct definition by constant assignment. No lemmas or tactics are invoked.
why it matters
The value anchors the HiggsRungCert and HiggsMassScoreCardCert structures that certify agreement within five percent. It completes the module's hypothesis that the RS prediction falls inside (120, 130) GeV. This step ties the T5 J-uniqueness and T6 phi fixed point to the measured spectrum via the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.