def
definition
muonDecayViaW
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.WeakForceEmergence on GitHub at line 221.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
218def betaDecayViaW : Bool := true
219
220/-- Muon decay: μ⁻ → e⁻ + ν̄e + νμ via W⁻. -/
221def muonDecayViaW : Bool := true
222
223/-- All charged-current weak processes use W±. -/
224theorem charged_current_uses_W : betaDecayViaW ∧ muonDecayViaW := by
225 simp only [betaDecayViaW, muonDecayViaW, and_self]
226
227/-! ## CKM Matrix -/
228
229/-- CKM matrix is 3×3 unitary. -/
230def ckmDimension : ℕ := 3
231
232/-- CKM has 4 independent parameters (3 angles + 1 phase). -/
233def ckmParameters : ℕ := 4
234
235/-- 4 = 3 + 1 (angles + CP phase). -/
236theorem ckm_params_3_plus_1 : ckmParameters = 3 + 1 := rfl
237
238end
239
240end WeakForceEmergence
241end Physics
242end IndisputableMonolith