gf_matches
plain-language theorem explainer
The theorem shows that the Fermi constant computed from the W boson mass and vacuum expectation value in the Recognition Science ledger model agrees with the measured value to within 10 percent. Electroweak model builders would cite it to confirm consistency between the derived coupling and PDG data. The proof first algebraically reduces the expression for the derived constant to sqrt(2) over twice the vev squared, then applies explicit numerical bounds on sqrt(2) and the vev squared term followed by inequality chaining.
Claim. Let $G_F$ be the Fermi constant and let $g_{F, m_W}$ be the value obtained from the W-boson mass via $G_F = sqrt(2) / (2 v^2)$ with $v = 246.22$ GeV. Then $|G_F - g_{F, m_W}| / G_F < 0.1$.
background
The module derives the weak force from the Recognition Science ledger geometry. SU(2)_L arises from the three generators of spatial rotations in three dimensions, while the eight-tick cycle supplies the chiral orientation that produces parity violation. The vacuum expectation value $v$ enters as the scale at which the J-cost minimum occurs, fixing the W and Z masses through the relation $m_W = g v / 2$ with $g$ the weak coupling. Upstream results supply the discrete Tick as the atomic time unit and the identity event at unit state with zero J-cost; these underwrite the discrete ledger steps that generate the effective four-fermion interaction whose strength is $G_F$.
proof idea
The tactic proof begins by unfolding the definitions of $g_{F, m_W}$ and the weak coupling, then applies field_simp and ring to obtain the identity $g_{F, m_W} = sqrt(2) / (2 v^2)$. Separate lemmas bound sqrt(2) between 1.41 and 1.42 and $v^2$ between 60624 and 60625. These bounds are propagated through division inequalities to sandwich $g_{F, m_W}$ between 1.162e-5 and 1.172e-5. The absolute difference from the constant 1.1663787e-5 is shown less than 0.01e-5 by lt_trans on the chained inequalities, after which division by the positive Fermi constant yields the relative error bound below 0.1.
why it matters
This declaration closes the numerical consistency check for the weak sector in proposition P-019 of the Weak Force Emergence derivation. It links the three-dimensional ledger geometry and eight-tick octave directly to the observed Fermi constant without additional free parameters beyond the vev scale. The result sits inside the broader forcing chain that produces D = 3 and the phi-ladder mass formula, confirming that the short-range weak interaction strength emerges at the expected magnitude once the J-cost minimum is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.