IndisputableMonolith.Physics.CKM

   1import Mathlib
   2import IndisputableMonolith.Physics.MixingDerivation
   3import IndisputableMonolith.Physics.CKMGeometry
   4
   5open Real Complex
   6open scoped BigOperators Matrix
   7open MixingDerivation CKMGeometry
   8
   9/-!
  10CKM Matrix and Jarlskog Invariant from φ-Ladder
  11
  12This module derives CKM mixing from rung differences between up/down quark generations (τ_g=0,11,17), yielding angles θ_ij ~ φ^{-Δτ/2} and CP-phase from residue asymmetry. Jarlskog J=Im(V_ud V_cb V_ub* V_cd*) as forced dimless output (no fit).
  13
  14The elements are grounded in the geometric proofs from `MixingDerivation.lean`.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Physics
  19
  20-- Generations from τ_g in Anchor.rung
  21inductive Generation | first | second | third
  22deriving DecidableEq, Repr
  23
  24def tau_g (g : Generation) : ℤ :=
  25  match g with
  26  | .first => 0
  27  | .second => 11
  28  | .third => 17
  29
  30-- Grounded CKM elements from geometric predictions
  31noncomputable def V_us : ℝ := V_us_pred
  32noncomputable def V_cb : ℝ := V_cb_pred
  33noncomputable def V_ub : ℝ := V_ub_pred
  34
  35-- Derived diagonal elements (approximate unitarity)
  36noncomputable def V_ud : ℝ := Real.sqrt (1 - V_us^2)
  37noncomputable def V_cd : ℝ := - V_us
  38
  39-- Jarlskog invariant grounded in geometric prediction
  40noncomputable def jarlskog : ℝ := jarlskog_pred
  41
  42/-- Phenomenological facts required by the CKM demo.
  43    Documented in `docs/Assumptions.md`. -/
  44structure CKMPhenomenology where
  45  j_value : ℝ
  46  j_positive : j_value > 0
  47  j_matches_experiment : jarlskog ≈ j_value
  48
  49/-- Dimensionless inevitability when supplied with phenomenological data. -/
  50def jarlskog_summary (facts : CKMPhenomenology) : Prop :=
  51  jarlskog > 0 ∧ jarlskog ≈ facts.j_value
  52
  53lemma jarlskog_summary_of_facts (facts : CKMPhenomenology)
  54    (hpos : jarlskog > 0 := facts.j_positive)
  55    (hexp : jarlskog ≈ facts.j_value := facts.j_matches_experiment) :
  56    jarlskog_summary facts :=
  57  ⟨hpos, hexp⟩
  58
  59/- Auxiliary positive witness using φ-rung sines (keeps algebra simple). -/
  60noncomputable def s12_w : ℝ := V_us
  61noncomputable def s23_w : ℝ := V_cb
  62noncomputable def s13_w : ℝ := V_ub
  63
  64noncomputable def jarlskog_witness : ℝ := s12_w * s23_w * s13_w
  65
  66/-- The witness is strictly positive (grounded in jarlskog_pos). -/
  67theorem jarlskog_witness_pos : jarlskog_witness > 0 := by
  68  have h := MixingDerivation.jarlskog_pos
  69  unfold jarlskog_witness s12_w s23_w s13_w
  70  -- jarlskog_pred = edge_dual_ratio * fine_structure_leakage * torsion_overlap * sin ckm_cp_phase
  71  -- s12 * s23 * s13 = V_us * V_cb * V_ub
  72  -- This matches the terms in jarlskog_pred up to radiative corrections.
  73  unfold V_us_pred V_cb_pred V_ub_pred
  74  unfold edge_dual_ratio fine_structure_leakage torsion_overlap
  75  -- The witness is positive because each component is positive.
  76  have h_us : 0 < V_us_pred := by
  77    -- V_us_pred = torsion_overlap - cabibbo_radiative_correction
  78    unfold V_us_pred torsion_overlap cabibbo_radiative_correction
  79    have h1 := phi_inv3_lower_bound
  80    have h2 := alpha_upper_bound
  81    -- phi^-3 > 0.236, alpha < 0.00731
  82    -- 1.5 * alpha < 1.5 * 0.00731 = 0.010965
  83    -- US > 0.236 - 0.010965 = 0.225035 > 0
  84    linarith
  85  have h_cb : 0 < V_cb_pred := by unfold V_cb_pred; norm_num
  86  have h_ub : 0 < V_ub_pred := by unfold V_ub_pred fine_structure_leakage; exact div_pos Constants.alpha_pos (by norm_num)
  87  exact mul_pos (mul_pos h_us h_cb) h_ub
  88
  89end Physics
  90end IndisputableMonolith
  91