IndisputableMonolith.StandardModel.RelativisticDOF

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Foundation.GaugeFromCube
   4import IndisputableMonolith.Foundation.ParticleGenerations
   5
   6/-!
   7# g_star = 106.75: Standard Model Bookkeeping with RS-Sourced Inputs
   8
   9STATUS TAG: **BOOKKEEPING over adopted SM content** (not a novel RS prediction).
  10
  11This module computes the standard high-temperature Standard Model
  12relativistic degree count
  13
  14  g_star = g_b + (7/8) g_f = 28 + (7/8)·90 = 427/4 = 106.75
  15
  16as exact rational arithmetic in Lean. Honest scope (per the 2026-06-25
  17external review): this is the textbook count, valid ONLY in the
  18high-temperature regime T ≳ T_EW where all listed species are relativistic
  19and thermally populated. It is correct bookkeeping, not a new calculation.
  20
  21## What RS supplies vs. what is imported
  22
  23RS-DERIVED inputs (each proved upstream, cited by name):
  24- The gauge group SU(3)×SU(2)×U(1) from Q₃ automorphisms (GaugeFromCube).
  25- The generation count 3 = face_pairs(3) from D = 3 (ParticleGenerations).
  26- The sign choice Fermi–Dirac vs. Bose–Einstein from the 8-tick
  27  spin-statistics theorem (Foundation.SpinStatistics and QFT.SpinStatistics
  28  in the full `reality` repository; those modules are not included in this
  29  curated repository).
  30
  31IMPORTED (standard physics, NOT derived by RS):
  32- The Standard Model matter representations (which reps the fermions sit
  33  in: quark doublets/singlets, lepton doublets, colors per quark).
  34- The minimal-neutrino convention (left-handed only, 2 DOF per generation).
  35  See Part 5 for the Dirac-neutrino branch (g_f = 96, g_star = 112).
  36- The 7/8 thermal weight, i.e. the value of the Fermi–Dirac vs.
  37  Bose–Einstein energy-density integral ratio
  38  ∫x³/(eˣ+1)dx / ∫x³/(eˣ−1)dx = 7/8. RS fixes the SIGN via
  39  spin-statistics; the integral value is standard statistical mechanics.
  40- The high-temperature scope. g_star is temperature dependent; the single
  41  number 106.75 applies above T_EW only. The temperature dependence
  42  (threshold decoupling steps) is implemented in
  43  Cosmology.GStarThresholds as g_star(T).
  44
  45## Assembly
  46
  471. Gauge boson content fixed by the gauge group dimensions (RS-sourced group).
  482. Fermion content = 3 generations × 30 DOF/gen (RS-sourced count; SM reps).
  493. g_star = bosonic_dof + (7/8) × fermionic_dof = 106.75.
  50
  51## Bosonic Degrees of Freedom (28)
  52
  53| Particle | Count | Polarizations | DOF |
  54|----------|-------|---------------|-----|
  55| Gluons   | 8     | 2             | 16  |
  56| W±       | 2     | 3             | 6   |
  57| Z        | 1     | 3             | 3   |
  58| γ        | 1     | 2             | 2   |
  59| Higgs (T > T_EW) | 1 | 4 (complex doublet) | 4 |
  60| **Total** |      |               | **28** (at T_EW: W/Z massive → 3 pol each) |
  61
  62The 28 comes from: at the EW scale and above, the Higgs doublet contributes
  63all 4 real DOF (before Goldstone absorption). The W/Z are massive with
  643 polarization states each. Below T_EW, the Goldstones are eaten but the
  65count is the same either way — rearranged, not changed.
  66
  67Correction: at T > T_EW (symmetric phase), all gauge bosons are massless
  68with 2 polarizations each: 12 × 2 = 24, plus 4 Higgs DOF = 28.
  69
  70## Fermionic Degrees of Freedom (90)
  71
  72Per generation:
  73- Quarks: 2 flavors × 3 colors × 2 chiralities × 2 (particle + antiparticle) = 24
  74- Leptons: 1 charged lepton × 2 chiralities × 2 (p + ap) + 1 neutrino × 1 chirality × 2 = 6
  75
  76Per generation DOF = 24 + 6 = 30
  773 generations × 30 = 90
  78
  79## The 7/8 Factor
  80
  81Fermi-Dirac statistics gives ⟨n⟩ = 1/(e^{E/T}+1) vs Bose-Einstein
  82⟨n⟩ = 1/(e^{E/T}-1). The energy density ratio for fermions vs bosons
  83in thermal equilibrium is 7/8. Division of labor: the SIGN (+1 fermions,
  84−1 bosons) follows from spin-statistics, which IS proved from the 8-tick
  85structure (IndisputableMonolith.Foundation.SpinStatistics and
  86IndisputableMonolith.QFT.SpinStatistics in the full `reality` repository;
  87not included in this curated repository). The VALUE 7/8 of the resulting
  88thermal integral ratio is standard statistical mechanics, imported here
  89as a rational constant, not re-derived in Lean.
  90
  91## Result
  92
  93g_star = 28 + (7/8) × 90 = 28 + 78.75 = 106.75  (high-T SM regime only)
  94
  95For the temperature-dependent g_star(T) step function (threshold
  96decoupling), see Cosmology.GStarThresholds.
  97
  98## Status: 0 sorry, 0 axiom (arithmetic verified; scope tags above bind)
  99-/
 100
 101namespace IndisputableMonolith
 102namespace StandardModel
 103namespace RelativisticDOF
 104
 105open Foundation.GaugeFromCube Foundation.ParticleGenerations
 106
 107/-! ## Part 1: Gauge Boson Counting -/
 108
 109/-- Adjoint dimension of SU(n): n² − 1. -/
 110def adjoint_dim (n : ℕ) : ℕ := n ^ 2 - 1
 111
 112theorem su3_adjoint : adjoint_dim 3 = 8 := by native_decide
 113theorem su2_adjoint : adjoint_dim 2 = 3 := by native_decide
 114
 115/-- Gluon DOF: 8 gluons × 2 polarizations (massless at T > T_EW). -/
 116def gluon_dof : ℕ := adjoint_dim 3 * 2
 117
 118theorem gluon_dof_eq : gluon_dof = 16 := by native_decide
 119
 120/-- Weak boson DOF at T > T_EW (symmetric phase):
 121    W₁, W₂, W₃ (3 SU(2) generators) × 2 polarizations = 6.
 122    B (1 U(1) generator) × 2 polarizations = 2.
 123    Total: 8. -/
 124def weak_boson_dof_symmetric : ℕ := adjoint_dim 2 * 2 + 1 * 2
 125
 126theorem weak_boson_dof_symmetric_eq : weak_boson_dof_symmetric = 8 := by native_decide
 127
 128/-- Higgs doublet DOF: complex SU(2) doublet = 4 real DOF. -/
 129def higgs_dof : ℕ := 4
 130
 131/-- Total bosonic DOF at T > T_EW. -/
 132def bosonic_dof : ℕ := gluon_dof + weak_boson_dof_symmetric + higgs_dof
 133
 134theorem bosonic_dof_eq : bosonic_dof = 28 := by native_decide
 135
 136/-! ## Part 2: Fermion Counting -/
 137
 138/-- Number of quark flavors per generation (up-type + down-type). -/
 139def quark_flavors_per_gen : ℕ := 2
 140
 141/-- Number of colors from Q₃ (SU(3) fundamental rep dimension). -/
 142def n_colors : ℕ := color_layer.fund_rep_dim
 143
 144theorem n_colors_eq : n_colors = 3 := rfl
 145
 146/-- Number of chiralities (left + right). -/
 147def chiralities : ℕ := 2
 148
 149/-- Particle + antiparticle factor. -/
 150def particle_antiparticle : ℕ := 2
 151
 152/-- Quark DOF per generation:
 153    2 flavors × 3 colors × 2 chiralities × 2 (p + ap) = 24. -/
 154def quark_dof_per_gen : ℕ :=
 155  quark_flavors_per_gen * n_colors * chiralities * particle_antiparticle
 156
 157theorem quark_dof_per_gen_eq : quark_dof_per_gen = 24 := by native_decide
 158
 159/-- Charged lepton DOF per generation:
 160    1 flavor × 2 chiralities × 2 (p + ap) = 4. -/
 161def charged_lepton_dof_per_gen : ℕ := 1 * chiralities * particle_antiparticle
 162
 163theorem charged_lepton_dof_per_gen_eq : charged_lepton_dof_per_gen = 4 := by
 164  native_decide
 165
 166/-- Neutrino DOF per generation (SM: left-handed only):
 167    1 flavor × 1 chirality × 2 (p + ap) = 2. -/
 168def neutrino_dof_per_gen : ℕ := 1 * 1 * particle_antiparticle
 169
 170theorem neutrino_dof_per_gen_eq : neutrino_dof_per_gen = 2 := by native_decide
 171
 172/-- Total fermion DOF per generation. -/
 173def fermion_dof_per_gen : ℕ :=
 174  quark_dof_per_gen + charged_lepton_dof_per_gen + neutrino_dof_per_gen
 175
 176theorem fermion_dof_per_gen_eq : fermion_dof_per_gen = 30 := by native_decide
 177
 178/-- Number of generations from Q₃ face-pairs. -/
 179def n_generations : ℕ := face_pairs 3
 180
 181theorem n_generations_eq : n_generations = 3 := rfl
 182
 183/-- Total fermion DOF: 3 generations × 30 = 90. -/
 184def fermionic_dof : ℕ := n_generations * fermion_dof_per_gen
 185
 186theorem fermionic_dof_eq : fermionic_dof = 90 := by native_decide
 187
 188/-! ## Part 3: The 7/8 Weighting and g_star -/
 189
 190noncomputable section
 191
 192/-- The Fermi-Dirac weighting factor: 7/8.
 193    Fermions contribute 7/8 as much energy density per DOF as bosons
 194    in thermal equilibrium: ∫₀^∞ x³/(eˣ+1) dx = (7/8) × ∫₀^∞ x³/(eˣ-1) dx.
 195    IMPORTED CONSTANT: the integral value 7/8 is standard statistical
 196    mechanics and is NOT re-derived here (the integrals are not formalized
 197    in this module). What RS supplies is the sign difference (Fermi-Dirac
 198    +1 vs Bose-Einstein −1), a consequence of the 8-tick spin-statistics
 199    theorem (Foundation.SpinStatistics / QFT.SpinStatistics in the full
 200    `reality` repository; not included in this curated repository). -/
 201def fermi_dirac_weight : ℝ := 7 / 8
 202
 203theorem fermi_dirac_weight_pos : 0 < fermi_dirac_weight := by
 204  norm_num [fermi_dirac_weight]
 205
 206/-- g_star = 106.75, assembled from the counts above.
 207
 208    g_star = bosonic_dof + (7/8) × fermionic_dof
 209           = 28 + (7/8) × 90
 210           = 28 + 78.75
 211           = 106.75
 212
 213    Honest ingredient list (see module header for the full split):
 214    - gauge GROUP from Q₃ automorphisms (RS-derived); gauge boson DOF then
 215      follow from the group dimensions plus standard polarization counting.
 216    - generation COUNT 3 from Q₃ face-pairs (RS-derived); the per-generation
 217      30 DOF uses the imported SM representation content and the
 218      minimal-neutrino convention.
 219    - 7/8: sign from spin-statistics (RS-derived); integral value imported.
 220
 221    Valid in the high-T SM regime (T ≳ T_EW) only. This is verified SM
 222    bookkeeping with RS-sourced group/generation inputs, not an
 223    independent RS prediction of a new number. -/
 224def g_star_derived : ℝ :=
 225  (bosonic_dof : ℝ) + fermi_dirac_weight * (fermionic_dof : ℝ)
 226
 227theorem g_star_derived_eq : g_star_derived = 106.75 := by
 228  unfold g_star_derived fermi_dirac_weight
 229  rw [bosonic_dof_eq, fermionic_dof_eq]
 230  norm_num
 231
 232theorem g_star_derived_pos : 0 < g_star_derived := by
 233  rw [g_star_derived_eq]; norm_num
 234
 235/-- Bridge: the derived g_star matches the hand-entered value in
 236    BaryonAsymmetryDerivation and EWPhaseTransition. -/
 237theorem g_star_matches_cosmology :
 238    g_star_derived = 106.75 := g_star_derived_eq
 239
 240end
 241
 242/-! ## Part 4: Component Traceability -/
 243
 244/-- Each bosonic DOF traces to Q₃ structure. -/
 245theorem bosonic_traces_to_Q3 :
 246    gluon_dof = adjoint_dim color_layer.fund_rep_dim * 2 ∧
 247    adjoint_dim color_layer.fund_rep_dim = 8 ∧
 248    bosonic_dof = 28 :=
 249  ⟨rfl, su3_adjoint, bosonic_dof_eq⟩
 250
 251/-- Each fermionic DOF traces to Q₃ structure. -/
 252theorem fermionic_traces_to_Q3 :
 253    n_generations = face_pairs 3 ∧
 254    n_colors = color_layer.fund_rep_dim ∧
 255    fermionic_dof = 90 :=
 256  ⟨rfl, rfl, fermionic_dof_eq⟩
 257
 258/-! ## Part 5: Model-Dependent Branch — Thermalized Dirac Neutrinos
 259
 260The 106.75 value uses the minimal-SM convention: neutrinos are left-handed
 261only (2 DOF per generation). If neutrinos are Dirac AND the right-handed
 262components are thermally populated, each generation gains 2 more DOF:
 263
 264  g_f = 96,  g_star = 28 + (7/8)·96 = 112.
 265
 266This branch is carried explicitly so the convention is a named input,
 267not a hidden assumption. Which branch reality takes is a MODEL choice
 268(and for the right-handed states, a thermalization question) that this
 269module does not decide. -/
 270
 271/-- Neutrino DOF per generation with thermalized Dirac (right-handed)
 272    components: 1 flavor × 2 chiralities × 2 (p + ap) = 4. -/
 273def neutrino_dof_per_gen_dirac : ℕ := 1 * chiralities * particle_antiparticle
 274
 275theorem neutrino_dof_per_gen_dirac_eq : neutrino_dof_per_gen_dirac = 4 := by
 276  native_decide
 277
 278/-- Fermion DOF per generation in the thermalized-Dirac-neutrino branch: 32. -/
 279def fermion_dof_per_gen_dirac : ℕ :=
 280  quark_dof_per_gen + charged_lepton_dof_per_gen + neutrino_dof_per_gen_dirac
 281
 282theorem fermion_dof_per_gen_dirac_eq : fermion_dof_per_gen_dirac = 32 := by
 283  native_decide
 284
 285/-- Total fermion DOF in the thermalized-Dirac-neutrino branch: 96. -/
 286def fermionic_dof_dirac : ℕ := n_generations * fermion_dof_per_gen_dirac
 287
 288theorem fermionic_dof_dirac_eq : fermionic_dof_dirac = 96 := by native_decide
 289
 290noncomputable section
 291
 292/-- g_star in the thermalized-Dirac-neutrino branch. -/
 293def g_star_dirac : ℝ :=
 294  (bosonic_dof : ℝ) + fermi_dirac_weight * (fermionic_dof_dirac : ℝ)
 295
 296/-- g_star = 112 with thermalized right-handed Dirac neutrinos. -/
 297theorem g_star_dirac_eq : g_star_dirac = 112 := by
 298  unfold g_star_dirac fermi_dirac_weight
 299  rw [bosonic_dof_eq, fermionic_dof_dirac_eq]
 300  norm_num
 301
 302/-- The two branches differ by (7/8)·6 = 5.25: the neutrino convention is
 303    a real model input that moves the answer, not notation. -/
 304theorem g_star_branch_gap : g_star_dirac - g_star_derived = 5.25 := by
 305  rw [g_star_dirac_eq, g_star_derived_eq]
 306  norm_num
 307
 308end
 309
 310/-! ## Part 6: Master Certificate -/
 311
 312structure GStarCert where
 313  bosonic : bosonic_dof = 28
 314  fermionic : fermionic_dof = 90
 315  n_gen : n_generations = 3
 316  n_col : n_colors = 3
 317  gluons : gluon_dof = 16
 318  higgs : higgs_dof = 4
 319  g_star : g_star_derived = 106.75
 320  g_star_positive : 0 < g_star_derived
 321
 322def gStarCert : GStarCert where
 323  bosonic := bosonic_dof_eq
 324  fermionic := fermionic_dof_eq
 325  n_gen := n_generations_eq
 326  n_col := n_colors_eq
 327  gluons := gluon_dof_eq
 328  higgs := rfl
 329  g_star := g_star_derived_eq
 330  g_star_positive := g_star_derived_pos
 331
 332end RelativisticDOF
 333end StandardModel
 334end IndisputableMonolith
 335