charged_current_uses_W
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.
claimBeta 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 in Recognition Science
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.
scope and limits
- Does not compute the Fermi constant or weak mixing angle.
- Does not derive the range of the weak force from boson masses.
- Does not address neutral current processes mediated by Z.
- Does not incorporate quark mixing via CKM.
formal statement (Lean)
224theorem charged_current_uses_W : betaDecayViaW ∧ muonDecayViaW := by
proof body
Term-mode proof.
225 simp only [betaDecayViaW, muonDecayViaW, and_self]
226
227/-! ## CKM Matrix -/
228
229/-- CKM matrix is 3×3 unitary. -/