IndisputableMonolith.Cosmology.BaryogenesisFromJCost

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Baryogenesis from J-Cost — A3 Cosmology
   6
   7The baryon-to-photon ratio η ≈ 6.1 × 10⁻¹⁰ (CMB measurement).
   8
   9In RS terms: the matter-antimatter asymmetry is a σ-imbalance in the
  10early universe. The Sakharov conditions (baryon number violation,
  11C and CP violation, departure from equilibrium) correspond to:
  121. Baryon violation = σ-export above threshold
  132. CP violation = J(r) ≠ J(r*) where r* is the CP-conjugate
  143. Non-equilibrium = J(r) > 0
  15
  16Five baryogenesis mechanisms (leptogenesis, electroweak, Affleck-Dine,
  17cold baryogenesis, GUT baryogenesis) = configDim D = 5.
  18
  19Lean status: 0 sorry, 0 axiom.
  20-/
  21
  22namespace IndisputableMonolith.Cosmology.BaryogenesisFromJCost
  23open Cost
  24
  25inductive BaryogenesisMechanism where
  26  | leptogenesis | electroWeak | affleckDine | cold | GUT
  27  deriving DecidableEq, Repr, BEq, Fintype
  28
  29theorem baryogenesisMechanismCount : Fintype.card BaryogenesisMechanism = 5 := by decide
  30
  31/-- Equilibrium = matter-antimatter balance (J=0). -/
  32theorem matter_balance_equilibrium : Jcost 1 = 0 := Jcost_unit0
  33
  34/-- Asymmetry = J > 0 when matter ≠ antimatter. -/
  35theorem asymmetry_positive_cost {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  36    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  37
  38structure BaryogenesisCert where
  39  five_mechanisms : Fintype.card BaryogenesisMechanism = 5
  40  equilibrium : Jcost 1 = 0
  41  asymmetry : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  42
  43def baryogenesisCert : BaryogenesisCert where
  44  five_mechanisms := baryogenesisMechanismCount
  45  equilibrium := matter_balance_equilibrium
  46  asymmetry := asymmetry_positive_cost
  47
  48end IndisputableMonolith.Cosmology.BaryogenesisFromJCost
  49