gf_from_mw
plain-language theorem explainer
The definition supplies the Fermi constant as √2 g² / (8 m_W²) using the SU(2) coupling and measured W-boson mass. Electroweak model builders cite it when linking gauge parameters to the observed beta-decay rate. It is realized as a direct one-line algebraic substitution with no lemmas or tactics.
Claim. The Fermi constant is defined by $G_F = √2 g² / (8 m_W²)$, where $g$ is the SU(2) weak coupling and $m_W$ the W-boson mass.
background
The weak-force module derives SU(2)_L from three-dimensional ledger geometry and obtains boson masses from the J-cost minimum at φ. The upstream definition wBosonMass_GeV fixes the numerical value at 80.3692 GeV. The companion definition weak_coupling_g sets g = 2 m_W / v with v the vacuum expectation value, yielding the standard relation between coupling, mass, and Fermi constant.
proof idea
The declaration is a one-line definition that directly encodes the electroweak formula by substituting the expressions for weak_coupling_g and wBosonMass_GeV.
why it matters
This definition supplies the numerical input to the downstream check gf_matches, which verifies agreement with the empirical Fermi constant to within 10 percent. It completes the P-019 step that converts the ledger-derived SU(2) structure into the observed weak-interaction strength, anchoring the eight-tick and D=3 predictions against PDG data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.