weak_range_short
plain-language theorem explainer
The weak interaction range computed from the ratio of ħc to the W boson mass is shown to lie below 0.01 fm. Researchers modeling emergent gauge forces in Recognition Science would cite this bound to confirm the scale set by massive mediators. The proof is a direct numerical reduction that unfolds the range definition and evaluates the inequality.
Claim. Let $r = (0.197327)/80.3692$ denote the weak interaction range in fm. Then $r < 0.01$.
background
The Weak Force Emergence module derives the weak nuclear force from the 3D ledger geometry of Recognition Science. Massive gauge bosons arise from the J-cost minimum at phi, producing the short range via the standard Compton wavelength formula. The module states that this range is approximately 2 times 10 to the minus 3 fm.
proof idea
The term proof is a one-line wrapper. It applies simp to unfold weakRange_fm, hbar_c_GeV_fm, and wBosonMass_GeV, then invokes norm_num to verify the numerical inequality 0.00245 < 0.01.
why it matters
This theorem supplies a concrete numerical check for the short-range prediction of the weak force in the RS framework. It supports the module's account of SU(2) emergence from 3D rotations and massive carriers from the phi fixed point. The result aligns with the eight-tick octave and D = 3 in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.