weak_coupling_g
plain-language theorem explainer
The definition sets the weak SU(2) coupling g to twice the W-boson mass divided by the Higgs vacuum expectation value. Electroweak model builders cite this relation when deriving the Fermi constant from measured boson masses. It is realized as a direct algebraic rearrangement of the tree-level mass formula m_W = g v / 2 using the fixed numerical inputs for m_W and v.
Claim. $g = 2 m_W / v$, where $m_W$ is the W-boson mass and $v$ the Higgs vacuum expectation value.
background
The ElectroweakBosons module derives W and Z masses from the Higgs mechanism after SU(2)_L × U(1)_Y breaking to U(1)_EM, with the vacuum expectation value placed on the phi-ladder. Upstream supplies vev_GeV as the constant 246.22 GeV and wBosonMass_GeV as 80.3692 GeV; the scalar constant definition anchors the uniform background field whose minimum yields these scales. The local setting treats the weak mixing angle and mass ratio as geometric consequences of the gauge embedding, with g obtained by solving the standard mass relation.
proof idea
One-line definition that rearranges the relation m_W = g v / 2 to isolate g, substituting the numerical values of wBosonMass_GeV and vev_GeV.
why it matters
This supplies the numerical value of g used in weak_coupling_approx to confirm g ≈ 0.653 and in gf_from_mw to obtain G_F ≈ 1.167 × 10^{-5} GeV^{-2}, which gf_matches verifies against the experimental Fermi constant. It closes the electroweak sector loop from RS-derived boson masses to the observed weak strength, consistent with the symmetry-breaking step after the eight-tick octave and phi-ladder placement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.