vev_determines_scale
plain-language theorem explainer
The theorem establishes that the W boson mass, Z boson mass, and Higgs boson mass each lie strictly below the electroweak vacuum expectation value of 246.22 GeV, with the Higgs mass further bounded by 0.6 times that value. Model builders working on electroweak symmetry breaking in the Recognition Science setting would cite it to confirm the required mass hierarchy before deriving mixing angles or couplings. The proof is a term-mode reduction that unfolds the four constant definitions and discharges the inequalities by direct numerical check.
Claim. Let $m_W = 80.3692$ GeV, $m_Z = 91.1876$ GeV, $m_H = 125.25$ GeV, and $v = 246.22$ GeV. Then $m_W < v$, $m_Z < v$, and $m_H < 0.6 v$.
background
The Electroweak Bosons module derives W and Z masses from the Higgs mechanism in the Recognition Science framework, where electroweak symmetry breaking corresponds to a J-cost minimum and the vacuum expectation value sits at a specific rung on the phi-ladder. The relevant constants are defined directly as wBosonMass_GeV := 80.3692, zBosonMass_GeV := 91.1876, higgsMass_GeV := 125.25, and vev_GeV := 246.22. These numerical assignments encode the experimental inputs that the module then relates through the weak mixing angle and mass ratio relations. The upstream CirclePhaseLift.and result supplies a log-derivative bound used elsewhere in the module but is not invoked in the present numerical check.
proof idea
The term proof applies simp only to the four constant definitions, exposing the concrete real numbers, then invokes norm_num to verify the three strict inequalities by arithmetic comparison.
why it matters
The declaration fills the module-level claim that the electroweak scale v sets the mass scale and is invoked directly by the downstream theorem vev_not_equal_higgs_mass to establish non-degeneracy between the Higgs mass and the VEV. It aligns with the RS mechanism of symmetry breaking at the J-cost minimum and with the phi-ladder placement of v near 246 GeV, consistent with the eight-tick octave and D = 3 spatial dimensions in the forcing chain. No open scaffolding remains for this numerical hierarchy step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.