IndisputableMonolith.Cosmology.SakharovFromLedger

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Foundation.ParticleGenerations
   4import IndisputableMonolith.Foundation.GrayCodeChirality
   5import IndisputableMonolith.Foundation.GaugeFromCube
   6import IndisputableMonolith.StandardModel.JarlskogInvariant
   7
   8/-!
   9# Sakharov Conditions from the RS Ledger
  10
  11Baryogenesis (the creation of the matter-antimatter asymmetry) requires
  12three conditions (Sakharov, 1967):
  13
  141. **Baryon number violation** (B violation)
  152. **C and CP violation**
  163. **Departure from thermal equilibrium**
  17
  18This module proves TWO structural facts (a ΔB bookkeeping identity and
  19J_CP ≠ 0) and carries the THIRD condition (departure from equilibrium) as an
  20explicit, underived hypothesis parameter. An earlier revision claimed all
  21three were derived "with zero imported physics"; that was false (the
  22out-of-equilibrium condition was a `True` placeholder) and is corrected
  23below. Baryon number as a ledger winding charge is itself an
  24interpretation, not a derived anomaly structure (audit FQ4).
  25
  26## Derivation
  27
  28### Condition 1: Baryon Number Violation
  29On the Z³ ledger, baryon number is a winding charge along one axis
  30(WindingCharges). Sphaleron-like processes correspond to collective
  318-tick phase rotations that change all three winding numbers
  32simultaneously. The ledger allows this because the double-entry
  33structure permits balanced multi-axis rotations.
  34
  35The B-violation rate scales with the weak coupling:
  36  Γ_sph ∝ α_W⁵ T⁴
  37(standard sphaleron-rate scaling, imported from the SM literature; α_W is
  38NOT derived here).
  39
  40### Condition 2: CP Violation
  41PROVED in CPPhaseDerivation: the Berry phase of the chiral Gray code
  42cycle gives δ_CKM ≠ 0, hence J_CP > 0 (JarlskogInvariant).
  43
  44### Condition 3: Out of Equilibrium — HYPOTHESIS, NOT DERIVED
  45Whether the electroweak transition is first order is an open
  46thermal-field-theory question; in the minimal SM with m_H ≈ 125 GeV it is a
  47crossover. No RS derivation exists. The condition is carried below as an
  48explicit hypothesis parameter on every downstream statement.
  49
  50## Main Results
  51
  521. `SakharovConditions EWFirstOrder`: structure packaging the two proved
  53   pieces plus the named out-of-equilibrium hypothesis
  542. `sakharov_from_RS (hEW)`: CONDITIONAL assembly given the hypothesis
  553. `sphaleron_changes_B_by_3`, `sphaleron_preserves_b_minus_l`: ΔB bookkeeping
  564. `cp_source_positive`: CP violation from J_CP > 0 (structural)
  57-/
  58
  59namespace IndisputableMonolith
  60namespace Cosmology
  61namespace SakharovFromLedger
  62
  63open Constants
  64open Foundation.ParticleGenerations
  65open Foundation.GrayCodeChirality
  66open StandardModel.JarlskogInvariant
  67
  68/-! ## Part 1: Baryon Number as Winding Charge
  69
  70Baryon number B is one of three independent topological charges on Z³.
  71It is conserved under local deformations but can change under global
  72(sphaleron) processes that rotate all three axes simultaneously. -/
  73
  74/-- The three independent conservation laws in D = 3. -/
  75theorem three_conservation_laws : face_pairs 3 = 3 := rfl
  76
  77/-- Sphaleron processes change baryon number by ΔB = N_gen = 3 per event.
  78    This is because each generation contributes one unit of B-violation,
  79    and there are exactly 3 generations (from D = 3). -/
  80def deltaB_per_sphaleron : ℕ := face_pairs 3
  81
  82theorem sphaleron_changes_B_by_3 : deltaB_per_sphaleron = 3 := rfl
  83
  84/-- Sphaleron events change lepton number by the same amount as baryon
  85    number (one unit per generation, 3 generations). This is imported SM
  86    anomaly bookkeeping, not a ledger derivation (audit FQ4). -/
  87def deltaL_per_sphaleron : ℕ := face_pairs 3
  88
  89/-- B − L is unchanged per sphaleron event: ΔB = ΔL, so Δ(B−L) = 0.
  90    (An earlier revision stated this as the tautology `ΔB = ΔB`, which
  91    carried no content; corrected to the actual invariant.) -/
  92theorem sphaleron_preserves_b_minus_l :
  93    (deltaB_per_sphaleron : ℤ) - (deltaL_per_sphaleron : ℤ) = 0 := by
  94  simp [deltaB_per_sphaleron, deltaL_per_sphaleron]
  95
  96/-! ## Part 2: CP Violation Source Term
  97
  98The Jarlskog invariant J_CP provides the CP-violating source term for
  99baryogenesis. It enters the baryon production rate as:
 100
 101  ε_CP ∝ J_CP × (mass factors)
 102
 103where the mass factors involve the torsion-induced mass hierarchy. -/
 104
 105/-- CP violation source: J_CP > 0 from JarlskogInvariant. -/
 106theorem cp_source_positive : jarlskog_structural > 0 := jarlskog_positive
 107
 108/-- The CP asymmetry parameter ε is proportional to J_CP. -/
 109noncomputable def cp_asymmetry_parameter : ℝ := jarlskog_structural
 110
 111theorem cp_asymmetry_nonzero : cp_asymmetry_parameter ≠ 0 :=
 112  ne_of_gt jarlskog_positive
 113
 114/-! ## Part 3: Electroweak Phase Transition
 115
 116The EW phase transition temperature T_EW lies on the φ-ladder. Above T_EW,
 117the Higgs VEV is zero (symmetric phase); below, it acquires a nonzero value.
 118
 119In RS, the Higgs field is not fundamental — it emerges from the ε⁴ term
 120of J(e^ε) = cosh(ε) − 1. The VEV v = 246 GeV sits on a specific φ-rung. -/
 121
 122/-! **PHYSICAL HYPOTHESIS (NOT DERIVED — corrected 2026-07-06).**
 123
 124An earlier revision defined `ew_transition_is_first_order : Prop := True` and
 125"proved" it with `trivial`. The 2026 internal audit correctly identified this
 126as a vacuous placeholder wearing a physics name. It is retracted.
 127
 128The honest status: whether the electroweak phase transition is first order is
 129a hard thermal-field-theory question. In the minimal Standard Model with
 130m_H ≈ 125 GeV the transition is in fact a CROSSOVER (Kajantie–Laine–
 131Rummukainen–Shaposhnikov 1996), so a first-order transition requires
 132beyond-SM dynamics. No RS derivation of this exists, and this repository has
 133no finite-temperature effective potential with which even to STATE it
 134faithfully.
 135
 136Rather than fake content, everything downstream is PARAMETERIZED over an
 137abstract proposition `EWFirstOrder : Prop`. The dependence is therefore
 138visible in every type signature, and no theorem in this repository
 139discharges it. -/
 140
 141/-! ## Part 4: Sakharov Conditions Assembled (conditionally) -/
 142
 143/-- The three Sakharov conditions, parameterized over the UNDERIVED
 144    out-of-equilibrium proposition. `EWFirstOrder` is an abstract Prop:
 145    this repository cannot state it faithfully, let alone prove it. -/
 146structure SakharovConditions (EWFirstOrder : Prop) where
 147  b_violation : deltaB_per_sphaleron = 3
 148  cp_violation : cp_asymmetry_parameter ≠ 0
 149  out_of_eq : EWFirstOrder
 150
 151/-- **CONDITIONAL assembly**: given the out-of-equilibrium hypothesis
 152    (NOT derived here; a crossover in the minimal SM), the two structural
 153    conditions (ΔB per sphaleron event, J_CP ≠ 0) combine with it into the
 154    Sakharov package. This is bookkeeping of the two proved pieces plus one
 155    named hypothesis — NOT a derivation of baryogenesis. -/
 156def sakharov_from_RS {EWFirstOrder : Prop} (hEW : EWFirstOrder) :
 157    SakharovConditions EWFirstOrder where
 158  b_violation := rfl
 159  cp_violation := cp_asymmetry_nonzero
 160  out_of_eq := hEW
 161
 162/-- Conditional statement: two structural facts hold unconditionally; the
 163    third (out-of-equilibrium) is carried as an explicit hypothesis. The
 164    earlier claim that all three were "derived (not postulated)" is
 165    retracted. -/
 166theorem baryogenesis_possible {EWFirstOrder : Prop} (hEW : EWFirstOrder) :
 167    deltaB_per_sphaleron = 3 ∧ cp_asymmetry_parameter ≠ 0 ∧ EWFirstOrder :=
 168  ⟨rfl, cp_asymmetry_nonzero, hEW⟩
 169
 170end SakharovFromLedger
 171end Cosmology
 172end IndisputableMonolith
 173