m_H_exp
plain-language theorem explainer
The definition supplies the experimental Higgs boson mass value of 125200 for use in electroweak mass verification within the Recognition Science framework. Particle physicists comparing RS predictions to collider data would reference this constant. It is implemented as a direct numerical definition without further computation or lemmas.
Claim. The experimental Higgs boson mass is defined by the constant assignment $m_{H,exp} := 125200$ (in MeV).
background
The ElectroweakMasses module differentiates the Higgs from the Z and W bosons. Z sits at rung 1 giving mass $2 phi^{51}/10^6$ MeV. The W mass follows from the Weinberg angle with $sin^2 theta_W = (3 - phi)/6$, and the Higgs is approximated as $m_W times phi$. This definition supplies the observed value 125200 for verification. It rests on the PrimitiveDistinction theorem that reduces seven independent axioms to four substantive structural conditions plus three definitional facts.
proof idea
The declaration is a direct definition that assigns the constant 125200 to m_H_exp. No tactics or lemmas are invoked; it functions as a fixed experimental input for the BosonVerification module.
why it matters
This constant feeds the m_H_exp definition in BosonVerification, enabling checks against the RS mass predictions from the phi-ladder. It supports the electroweak sector predictions derived from the gauge embedding geometry and the forcing chain up to T8. The value aligns with the approximate relation to the W mass scaled by phi, closing the comparison between theory and the observed Higgs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.