higgs_w_near_phi
plain-language theorem explainer
The declaration shows that the Higgs-to-W boson mass ratio lies within 0.1 of the golden ratio phi. Electroweak model builders in the Recognition Science program cite it to locate the Higgs scale near the phi-ladder rung. The proof reduces the claim to numerical bounds on phi and direct computation of the ratio from the stated GeV values.
Claim. Let $m_H = 125.25$ GeV and $m_W$ denote the Higgs and W boson masses. Then $|(m_H / m_W) - phi| < 0.1$, where $1.61 < phi < 1.62$.
background
In the electroweak sector the Higgs mechanism generates the W and Z masses after symmetry breaking, with the vacuum expectation value placed on the phi-ladder. The ratio is defined as higgsMass_GeV divided by wBosonMass_GeV. Upstream lemmas supply the tight bounds phi_gt_onePointSixOne and phi_lt_onePointSixTwo that bracket the golden ratio: even tighter lower bound phi > 1.61 and phi < 1.62 since sqrt(5) < 2.24.
proof idea
The tactic proof first simplifies the ratio to the explicit quotient 125.25 / 80.3692. It then introduces the phi bounds from the Constants module and establishes that the quotient lies between 1.55 and 1.56 by norm_num. Finally it rewrites the absolute-value inequality and solves the resulting system with linarith.
why it matters
This result anchors the Higgs mass near the phi fixed point in the electroweak sector, consistent with the phi-ladder mass formula and the eight-tick octave structure. It supports the placement of the electroweak scale in the Recognition framework (P-015, P-016). No immediate downstream theorems depend on it yet, leaving open the question of deriving the precise mass values from the forcing chain rather than inserting them numerically.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.