charged_current_uses_W
plain-language theorem explainer
The theorem establishes that beta decay and muon decay both proceed exclusively through charged-current interactions mediated by the W boson. Researchers modeling weak decays in the Recognition Science framework would reference this result when linking ledger-based SU(2) symmetry to observed processes. The proof reduces directly to the definitions of the two decay modes via simplification and conjunction introduction.
Claim. Beta decay proceeds via the $W^-$ boson and muon decay proceeds via the $W^-$ boson.
background
The WeakForceEmergence module derives the weak force from the 3D ledger geometry in Recognition Science, where SU(2)_L emerges from the three generators of rotations and chirality from the 8-tick cycle orientation. Beta decay is defined as the process $n$ to $p + e^- +$ anti-nu_e mediated by $W^-$, and muon decay as mu^- to $e^- +$ anti-nu_e + nu_mu via $W^-$, each set to true as a Boolean flag. Upstream results include structural definitions from SimplicialLedger and GameTheory that ensure collision-free ledger operations and mechanism design consistency.
proof idea
The proof applies the simp tactic to unfold the definitions of betaDecayViaW and muonDecayViaW, both of which evaluate to true, then uses and_self to conclude the conjunction.
why it matters
This result anchors the charged-current sector within the weak force emergence derivation (P-019), confirming that the W boson mediates the observed decays as required by the RS ledger structure. It supports the broader claim that the weak force arises from the phi-ladder and eight-tick octave, feeding into subsequent discussions of the CKM matrix and parity violation. No open questions are directly addressed here, but it closes the basic verification for charged currents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.