IndisputableMonolith.Cosmology.GStarThresholds

   1import Mathlib
   2import IndisputableMonolith.StandardModel.RelativisticDOF
   3
   4/-!
   5# g_star(T): Temperature-Dependent Relativistic Degrees of Freedom
   6
   7STATUS TAG: **MODEL (instantaneous-threshold step function) over adopted
   8SM content**. Built 2026-07-02 in response to the external review point
   9"g_star is temperature dependent, but RS fixes one number ... the
  10repository does not implement a function g_star(T), threshold decoupling,
  11finite-temperature equations of state, or epoch-dependent particle
  12content."
  13
  14This module implements the standard threshold-decoupling step function
  15g_star(T): each species contributes its full relativistic degree count
  16while T exceeds its mass threshold and drops out below it, with the QCD
  17confinement transition at T_QCD ≈ 0.15 GeV switching the strong sector
  18from quark–gluon plasma content (gluons + u,d,s) to hadronic content
  19(pions). All arithmetic is exact over ℚ and machine-checked.
  20
  21## Honest scope
  22
  23- The step function is the standard leading approximation. It does NOT
  24  implement Boltzmann-suppressed tails near thresholds, the lattice QCD
  25  equation of state through the crossover, or the neutrino-decoupling
  26  reheating factor (4/11)^(4/3) below e⁺e⁻ annihilation. Valid domain:
  27  T ≳ 1 MeV (above neutrino decoupling).
  28- Mass thresholds are IMPORTED (PDG rounded values, rational
  29  approximations). RS's φ-ladder mass modules (IndisputableMonolith.Masses)
  30  predict these masses independently; this module does not re-derive them,
  31  it uses them as ordering thresholds only (only the relative order of
  32  T vs. m matters for the step counts, so rounding is harmless).
  33- Particle content per species is the same imported SM bookkeeping as
  34  StandardModel.RelativisticDOF (see its header for the RS-derived vs.
  35  imported split: gauge group and generation count RS-derived; matter
  36  representations, neutrino convention, and the 7/8 integral imported).
  37- Below T_EW the bosonic sector is counted in the broken phase (massive
  38  W/Z with 3 polarizations, 1 physical Higgs); above T_EW the symmetric
  39  phase (massless W/Z with 2 polarizations, 4 Higgs-doublet DOF) has the
  40  SAME total (28), so the high-T evaluation matches
  41  RelativisticDOF.g_star_derived exactly (bridge theorem below).
  42
  43## Spot checks proved below (standard textbook values)
  44
  45| T          | epoch                        | g_star  |
  46|------------|------------------------------|---------|
  47| 200 GeV    | all SM relativistic          | 106.75  |
  48| 10 GeV     | after t, H, Z, W decouple    | 86.25   |
  49| 1 GeV      | after b, τ, c decouple       | 61.75   |
  50| 0.14 GeV   | below T_QCD (π, μ, e, ν, γ)  | 17.25   |
  51| 2 MeV      | after π, μ annihilate        | 10.75   |
  52
  53## Main results
  54
  55- `g_star (T : ℚ) : ℚ` — the step function.
  56- `g_star_high_matches_derived` — at high T it equals the fixed 106.75
  57  of StandardModel.RelativisticDOF (so the old fixed number is now the
  58  high-T evaluation of a real function, not a free-standing constant).
  59- `g_star_steps_antitone_chain` — the sampled epochs decrease as the
  60  universe cools.
  61- `g_star_dirac_high` — the thermalized-Dirac-neutrino branch gives 112
  62  at high T (the neutrino convention carried as an explicit input).
  63
  64## Status: 0 sorry, 0 axiom
  65-/
  66
  67namespace IndisputableMonolith
  68namespace Cosmology
  69namespace GStarThresholds
  70
  71/-- A thermal species: name, mass threshold (GeV, rational approximation;
  72    only its order relative to T matters), internal degrees of freedom,
  73    and quantum statistics. -/
  74structure Species where
  75  name : String
  76  mass : ℚ
  77  dof : ℕ
  78  fermion : Bool
  79deriving Repr
  80
  81/-! ## Species tables (imported SM content; masses PDG-rounded) -/
  82
  83/-- Photon: massless, 2 polarizations. -/
  84def photon : Species := ⟨"photon", 0, 2, false⟩
  85
  86/-- Neutrinos, minimal-SM convention: 3 generations × (LH ν + RH ν̄) = 6. -/
  87def neutrinos : Species := ⟨"neutrinos (3 gen, minimal)", 0, 6, true⟩
  88
  89/-- Neutrinos, thermalized-Dirac branch: 3 generations × 4 = 12. -/
  90def neutrinos_dirac : Species := ⟨"neutrinos (3 gen, Dirac, RH thermalized)", 0, 12, true⟩
  91
  92/-- Top quark: m ≈ 173 GeV, 12 DOF (3 color × 2 spin × 2 p/ap). -/
  93def top : Species := ⟨"top", 173, 12, true⟩
  94
  95/-- Higgs boson (broken phase): m ≈ 125 GeV, 1 DOF. -/
  96def higgs : Species := ⟨"Higgs", 125, 1, false⟩
  97
  98/-- Z boson (broken phase): m ≈ 91.2 GeV, 3 polarizations. -/
  99def zboson : Species := ⟨"Z", 456/5, 3, false⟩
 100
 101/-- W± bosons (broken phase): m ≈ 80.4 GeV, 2 × 3 polarizations = 6. -/
 102def wboson : Species := ⟨"W±", 402/5, 6, false⟩
 103
 104/-- Bottom quark: m ≈ 4.2 GeV, 12 DOF. -/
 105def bottom : Species := ⟨"bottom", 21/5, 12, true⟩
 106
 107/-- Tau lepton: m ≈ 1.777 GeV, 4 DOF. -/
 108def tau : Species := ⟨"tau", 1777/1000, 4, true⟩
 109
 110/-- Charm quark: m ≈ 1.27 GeV, 12 DOF. -/
 111def charm : Species := ⟨"charm", 127/100, 12, true⟩
 112
 113/-- Muon: m ≈ 0.1057 GeV, 4 DOF. -/
 114def muon : Species := ⟨"muon", 1057/10000, 4, true⟩
 115
 116/-- Electron: m ≈ 0.000511 GeV, 4 DOF. -/
 117def electron : Species := ⟨"electron", 511/1000000, 4, true⟩
 118
 119/-- Gluons (deconfined, T > T_QCD): 8 × 2 = 16 DOF. -/
 120def gluons : Species := ⟨"gluons", 0, 16, false⟩
 121
 122/-- Up quark (deconfined; current mass ≪ T_QCD): 12 DOF. -/
 123def up : Species := ⟨"up", 0, 12, true⟩
 124
 125/-- Down quark (deconfined): 12 DOF. -/
 126def down : Species := ⟨"down", 0, 12, true⟩
 127
 128/-- Strange quark (deconfined; m_s ≈ 95 MeV < T_QCD): 12 DOF. -/
 129def strange : Species := ⟨"strange", 0, 12, true⟩
 130
 131/-- Pions π⁺, π⁻, π⁰ (confined phase): m ≈ 0.135–0.140 GeV, 3 DOF. -/
 132def pions : Species := ⟨"pions", 27/200, 3, false⟩
 133
 134/-- QCD confinement threshold: T_QCD ≈ 0.15 GeV. Above it the strong
 135    sector is quark–gluon plasma; below it, hadrons. IMPORTED (lattice
 136    QCD crossover scale, rounded); the instantaneous switch is the step
 137    approximation, not the real crossover equation of state. -/
 138def T_qcd : ℚ := 3/20
 139
 140/-- Electroweak-sector species with mass thresholds (decouple as T falls). -/
 141def ew_species : List Species :=
 142  [top, higgs, zboson, wboson, bottom, tau, charm, muon, electron]
 143
 144/-- Strong-sector species above T_QCD (quark–gluon plasma). -/
 145def qgp_species : List Species := [gluons, up, down, strange]
 146
 147/-- Strong-sector species below T_QCD (hadronic phase). -/
 148def hadron_species : List Species := [pions]
 149
 150/-! ## The step function -/
 151
 152/-- Energy-density weight of one species: DOF, times 7/8 for fermions
 153    (sign from spin-statistics, RS-derived; integral value 7/8 imported —
 154    see StandardModel.RelativisticDOF.fermi_dirac_weight). -/
 155def species_g (s : Species) : ℚ :=
 156  if s.fermion then (7 : ℚ) / 8 * s.dof else s.dof
 157
 158/-- Species relativistic and populated at temperature T (GeV), with the
 159    neutrino sector supplied as an explicit input (minimal vs. Dirac). -/
 160def activeWith (nu : Species) (T : ℚ) : List Species :=
 161  [photon, nu]
 162    ++ ew_species.filter (fun s => s.mass < T)
 163    ++ (if T_qcd < T then qgp_species
 164        else hadron_species.filter (fun s => s.mass < T))
 165
 166/-- g_star(T) with an explicit neutrino-sector input. -/
 167def g_starWith (nu : Species) (T : ℚ) : ℚ :=
 168  ((activeWith nu T).map species_g).sum
 169
 170/-- **g_star(T)**: the temperature-dependent relativistic degree count,
 171    minimal-SM neutrino convention. Instantaneous-threshold step model;
 172    valid for T ≳ 1 MeV. -/
 173def g_star (T : ℚ) : ℚ := g_starWith neutrinos T
 174
 175/-! ## Evaluation theorems (exact rational arithmetic) -/
 176
 177/-- T = 200 GeV: all SM species relativistic → 427/4 = 106.75. -/
 178theorem g_star_high : g_star 200 = 427/4 := by native_decide
 179
 180/-- T = 10 GeV: t, H, Z, W decoupled → 345/4 = 86.25. -/
 181theorem g_star_10GeV : g_star 10 = 345/4 := by native_decide
 182
 183/-- T = 1 GeV: b, τ, c also decoupled → 247/4 = 61.75. -/
 184theorem g_star_1GeV : g_star 1 = 247/4 := by native_decide
 185
 186/-- T = 0.14 GeV (just below T_QCD): γ, π, μ, e, ν → 69/4 = 17.25. -/
 187theorem g_star_140MeV : g_star (7/50) = 69/4 := by native_decide
 188
 189/-- T = 2 MeV (above neutrino decoupling; π, μ gone): γ, e, ν
 190    → 43/4 = 10.75. -/
 191theorem g_star_2MeV : g_star (1/500) = 43/4 := by native_decide
 192
 193/-- The sampled epochs decrease monotonically as the universe cools:
 194    10.75 < 17.25 < 61.75 < 86.25 < 106.75. -/
 195theorem g_star_steps_antitone_chain :
 196    g_star (1/500) < g_star (7/50) ∧
 197    g_star (7/50) < g_star 1 ∧
 198    g_star 1 < g_star 10 ∧
 199    g_star 10 < g_star 200 := by native_decide
 200
 201/-! ## Bridge to the fixed high-T constant -/
 202
 203/-- The fixed 106.75 used across the cosmology modules is the high-T
 204    evaluation of g_star(T): the old constant is now a function value,
 205    not a free-standing number. -/
 206theorem g_star_high_matches_derived :
 207    ((g_star 200 : ℚ) : ℝ) = StandardModel.RelativisticDOF.g_star_derived := by
 208  rw [g_star_high, StandardModel.RelativisticDOF.g_star_derived_eq]
 209  norm_num
 210
 211/-! ## The Dirac-neutrino branch (explicit model input) -/
 212
 213/-- With thermalized right-handed Dirac neutrinos, the high-T count is
 214    112, not 106.75 (matches RelativisticDOF.g_star_dirac_eq). The
 215    neutrino convention is a real input that moves the answer. -/
 216theorem g_star_dirac_high : g_starWith neutrinos_dirac 200 = 112 := by
 217  native_decide
 218
 219/-- The two neutrino conventions agree everywhere except through the
 220    neutrino term: the branch gap at high T is (7/8)·6 = 21/4 = 5.25. -/
 221theorem g_star_branch_gap_high :
 222    g_starWith neutrinos_dirac 200 - g_star 200 = 21/4 := by native_decide
 223
 224end GStarThresholds
 225end Cosmology
 226end IndisputableMonolith
 227