weakRange_fm
plain-language theorem explainer
The definition supplies the weak interaction range in femtometers obtained by dividing the ħc conversion factor in GeV fm units by the W boson mass in GeV. Particle physicists studying electroweak processes or nuclear beta decay would reference this scale when converting energy units to length. The definition is realized as a direct quotient of two pre-defined real constants.
Claim. The weak force range in femtometers is $ r = (ħc) / m_W $ where the numerator is the conversion constant ħc expressed in GeV fm and the denominator is the W boson mass in GeV.
background
Recognition Science derives the weak force from ledger geometry in three dimensions. The SU(2) generators arise from rotations in the 3D space while the eight-tick cycle produces the chiral asymmetry. Massive gauge bosons result from J-cost minimization with the J function J(x) = (x + 1/x)/2 - 1 whose minimum at x = 1 sets the mass scale. The module imports the W boson mass from the electroweak bosons section and the unit conversion factor. Upstream results on spectral emergence establish the full gauge group content and the origin of three generations from the Q3 structure. Ledger factorization provides the convex J-cost whose global minimum fixes the boson masses. This definition converts the mass into a length scale via the Compton relation yielding the short range characteristic of weak interactions.
proof idea
This is a one-line definition that divides the imported ħc conversion constant in GeV fm by the W boson mass in GeV to produce the range in fm.
why it matters
This definition provides the numerical value required by the downstream theorem weak_range_short which proves the range is less than 0.01 fm and thereby confirms the short-range nature of the weak force. It fills the gap between the massive mediator mechanism and observable length scales in the RS framework. The result is consistent with the T7 eight-tick octave and D = 3 dimensions from the forcing chain and it supports the predicted Fermi constant relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.