vev_determines_scale
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the boson masses from the phi-ladder or J-cost functional.
- Does not prove the weak mixing angle or the W/Z mass ratio.
- Does not address the origin of the VEV within the T0-T8 forcing chain.
- Does not extend the inequalities to other particles or energy scales.
Lean usage
have hscale := vev_determines_scaleformal statement (Lean)
213theorem vev_determines_scale :
214 wBosonMass_GeV < vev_GeV ∧
215 zBosonMass_GeV < vev_GeV ∧
216 higgsMass_GeV < vev_GeV * 0.6 := by
proof body
Term-mode proof.
217 simp only [wBosonMass_GeV, zBosonMass_GeV, higgsMass_GeV, vev_GeV]
218 norm_num
219
220/-- The Higgs and electroweak VEV scales are non-degenerate. -/