higgsMass_GeV
plain-language theorem explainer
The declaration sets the Higgs boson mass to the constant 125.25 GeV for use in electroweak derivations. Mass-ratio modelers in the Recognition Science framework cite this value when testing proximity to phi or positioning the electroweak scale on the phi-ladder. The definition is a direct numerical assignment with no lemmas or reductions.
Claim. The Higgs boson mass is defined as $m_H = 125.25$ GeV.
background
The Electroweak Boson Masses Derivation module (P-015, P-016, C-004) treats the Higgs mechanism as the J-cost minimum that breaks SU(2)_L × U(1)_Y to U(1)_EM, with the vacuum expectation value v ≈ 246 GeV placed at a specific rung on the phi-ladder. The module also introduces the weak mixing angle whose cosine yields the W/Z mass ratio. Upstream results supply W as the wallpaper-groups count that anchors topological fractions in the mass-topology ledger.
proof idea
Direct definition that performs a constant assignment. No tactics or lemmas are invoked; the value serves as an input parameter for ratio and inequality theorems that follow.
why it matters
This definition supplies the observed Higgs mass for the downstream theorems higgs_w_ratio and higgs_w_near_phi, which compare the ratio to phi, and for vev_determines_scale, which places the electroweak scale below the VEV. It implements the mass-formula placement on the phi-ladder and connects to the eight-tick octave and T5 J-uniqueness steps of the forcing chain. It leaves open the exact rung assignment for the Higgs in the full RS mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.