def
definition
weakIsospin
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.WeakForceEmergence on GitHub at line 210.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
207theorem nine_eq_8_plus_1 : 9 = 8 + 1 := rfl
208
209/-- Weak isospin I = 1/2 for doublets. -/
210def weakIsospin : ℚ := 1 / 2
211
212/-- 2I + 1 = 2 (doublet size for I = 1/2). -/
213theorem doublet_from_isospin : leptonDoublet = 2 := rfl
214
215/-! ## Decay Processes -/
216
217/-- Beta decay: n → p + e⁻ + ν̄e via W⁻. -/
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