vev_wz_mass_hierarchy
plain-language theorem explainer
The theorem asserts existence of positive reals m_W, m_Z, v satisfying m_Z > m_W, using laboratory values for the W and Z masses and electroweak VEV. Physicists mapping electroweak symmetry breaking onto the Recognition Science phi-ladder cite it to fix the observed hierarchy before deriving rung positions. The proof is a term-mode construction that instantiates the three numbers and discharges the four inequalities via norm_num.
Claim. There exist positive real numbers $m_W$, $m_Z$, $v$ such that $m_Z > m_W$, where $m_W$ and $m_Z$ are the W and Z boson masses and $v$ is the vacuum expectation value.
background
Module C-020 formalizes the RS structural framework for the electroweak VEV. The vacuum expectation value enters the boson masses through $m_W = v/2 g$ and $m_Z = v/2 sqrt(g^2 + g'^2)$, with both couplings themselves phi-ladder quantities. The upstream scale definition supplies the discrete rung structure via noncomputable def scale (k : ℕ) : ℝ := phi ^ k.
proof idea
The term proof instantiates the concrete values 80.4, 91.2, 246.0. It then applies constructor four times to assert positivity of each quantity and the strict inequality m_Z > m_W, with every subgoal closed by norm_num.
why it matters
The result supplies the concrete electroweak hierarchy that sibling hierarchy_problem_dissolution invokes to dissolve the apparent separation between v ≈ 246 GeV and the Planck scale under discrete phi-ladder rungs. It fills the C-020 registry item by exhibiting the entire electroweak scale as a single phi-scaled structure rather than a tuned parameter. The declaration touches the open question of full numeric extraction of the laboratory VEV from ledger rungs, which the module marks as blocked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.