`doublet_from_isospin`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.WeakForceEmergence
domain: Physics
line: 213 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.WeakForceEmergence on GitHub at line 213.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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
 241end Physics
 242end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.