muonDecayViaW
Muon decay proceeds via the W boson in the Recognition Science ledger model of weak interactions. Physicists building charged-current processes cite this flag when verifying that all such decays route through W±. The declaration is a direct boolean constant assignment confirming the channel.
claimThe muon decay process satisfies $muonDecayViaW$, i.e., the channel $μ^- → e^- + ν̄_e + ν_μ$ occurs via $W^-$ exchange.
background
The Weak Force Emergence module derives the weak force from 3D ledger geometry that produces SU(2)_L with three generators, chiral couplings from the 8-tick cycle orientation, and massive bosons from the J-cost minimum at φ. Upstream results in Masses.Anchor, LeptonGenerations.TauStepDerivation, and MassTopology each define W as the wallpaper group count (17), supplying the topological basis that links mass ladders to symmetry generators. The module states that short range follows from the massive mediators with range ≈ ℏc / m_W c².
proof idea
The declaration is a direct boolean assignment set to true, serving as a one-line flag that the muon channel uses W.
why it matters in Recognition Science
This definition is referenced by the downstream theorem charged_current_uses_W, which asserts betaDecayViaW ∧ muonDecayViaW to confirm all charged-current processes route through W±. It fills the P-019 weak force emergence derivation, connecting the 3D spatial dimensions (T8) and eight-tick octave (T7) to the SU(2) structure and parity violation in the Recognition Science chain.
scope and limits
- Does not compute decay rates or branching fractions.
- Does not derive the numerical value of the Fermi constant.
- Does not address neutral-current Z-mediated processes.
- Does not specify the W boson mass from the phi-ladder.
Lean usage
theorem charged_current_uses_W : betaDecayViaW ∧ muonDecayViaW := by simp only [betaDecayViaW, muonDecayViaW, and_self]formal statement (Lean)
221def muonDecayViaW : Bool := true
proof body
Definition body.
222
223/-- All charged-current weak processes use W±. -/