`CKMElement`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.ThreeGenerations
domain: Physics
line: 148 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.ThreeGenerations on GitHub at line 148.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 145
 146/-- The CKM matrix elements encode how generations "talk" to each other.
 147    In RS, this comes from the overlap of 8-tick phases. -/
 148structure CKMElement where
 149  /-- From generation (1, 2, or 3). -/
 150  fromGen : Fin 3
 151  /-- To generation (1, 2, or 3). -/
 152  toGen : Fin 3
 153  /-- Mixing amplitude (complex). -/
 154  amplitude : ℂ
 155
 156/-- **THEOREM (CKM from Phase Overlap)**: The CKM matrix elements come from
 157    the overlap of 8-tick phase patterns between generations. -/
 158theorem ckm_from_phase_overlap :
 159    Fintype.card (Fin 3 × Fin 3) = 9 := by decide
 160
 161/-- The Cabibbo angle θ_C ≈ 13° emerges from φ-structure. -/
 162noncomputable def cabibboAngle : ℝ := Real.arcsin (1/phi^2)  -- Approximately correct
 163
 164/-! ## Neutrino Generations -/
 165
 166/-- Neutrinos also come in 3 generations (flavors).
 167    The PMNS matrix is the leptonic analog of CKM. -/
 168structure PMNSElement where
 169  /-- From flavor (e, μ, τ). -/
 170  fromFlavor : Fin 3
 171  /-- To mass eigenstate (1, 2, 3). -/
 172  toMass : Fin 3
 173  /-- Mixing amplitude. -/
 174  amplitude : ℂ
 175
 176/-- **THEOREM (Neutrino Generations = Charged Lepton Generations)**:
 177    Both are 3 because both arise from the same 8-tick × 3D structure. -/
 178theorem neutrino_generations_match :

papers checked against this theorem

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