Cosmology Neutrino Dilution G Star S From Conservation

The entropy bookkeeping

In the early universe, particle species annihilate and the remaining plasma cools. Cosmologists track this with an effective count of entropy-carrying degrees of freedom, written g*s. After electron-positron annihilation, the standard value is g*s = 43/11. A theorem in the framework's machine-checked library of formal theorems, named gStarS_from_conservation, derives this number from two physical assumptions plus a large body of proven statistical mechanics, rather than taking it as an input.

The physical picture is bookkeeping. Before annihilation, the coupled plasma of photons and electron-positron pairs carries a certain entropy. After annihilation, only photons remain in that coupled sector, but the neutrinos, which decoupled earlier, keep their own temperature. The two assumptions are adiabatic expansion, meaning the comoving entropy of the coupled sector stays constant, and free streaming, meaning the neutrino temperature simply redshifts with the expansion. Under those conditions, the theorem proves the neutrino dilution factor (T_ν/T_γ)³ = 4/11, and then proves the total present-day entropy density is exactly (2π²/45)·(43/11)·T_γ³. The 43/11 emerges from the arithmetic of 2 photon polarizations plus 6 neutrino degrees of freedom, each weighted by the derived fermion entropy factor 7/8.

The derivation does not assume the 7/8 factor or the 4/3 law for bosons. Those come from proven integrals of the entropy functional σ(x) = x²[±(1±f)ln(1±f) − f ln f], whose closed forms 4π⁴/45 and 7π⁴/90 are themselves theorems. The structural theorem radiationEntropy_eq collapses the plasma entropy density to (2π²/45)·(gB + (7/8)·gF)·T³, with both coefficients derived. The 11/2 → 2 drop in coupled degrees of freedom is not an input; it is the output of applying that structural theorem to the two species counts.

What the theorem does not claim is just as important. The particle content itself, namely 2 photon polarizations, 4 electron-positron degrees of freedom, and 6 neutrino degrees of freedom, is a model choice, not a theorem. Instantaneous decoupling is likewise a model approximation. The two conservation hypotheses, adiabatic expansion and free streaming, are model assumptions, though the framework's downstream module derives them from the Friedmann equations. All the statistical mechanics, including the 7/8 weight, the 4/11 ratio, and the 43/11 total, is theorem-grade given those hypotheses. The theorem also does not claim to derive the baryon-to-photon ratio η_B itself; it supplies the g*s prefactor that enters that calculation.

For a reader, the consequence is concrete: the number 43/11, which appears in every cosmology textbook as a given, is here forced by entropy conservation plus the derived entropy functional. It is not a free parameter. The framework's contribution is to show that the standard bookkeeping is not arbitrary arithmetic but a consequence of the same entropy integrals that govern the radiation bath.

/-- **THEOREM (neutrino dilution from entropy conservation).**
If comoving entropy of the coupled photon–e± sector is conserved through
annihilation (`radiationEntropy 2 4 T₁ · a₁³ = radiationEntropy 2 0 T_γ · a₂³`)
and decoupled neutrinos redshift freely from the shared pre-annihilation
temperature (`a₂·T_ν = a₁·T₁`), then

  `(T_ν/T_γ)³ = 4/11`.

The dof drop `11/2 → 2` is not an input: it is produced by the derived
entropy-functional integrals inside `radiationEntropy_eq`. -/
theorem dilution_from_entropy_conservation
    {a₁ a₂ T₁ Tγ Tν : ℝ} (ha₂ : a₂ ≠ 0) (hTγ : Tγ ≠ 0)
    (hcons : radiationEntropy 2 4 T₁ * a₁ ^ 3 = radiationEntropy 2 0 Tγ * a₂ ^ 3)
    (hfree : a₂ * Tν = a₁ * T₁) :
    (Tν / Tγ) ^ 3 = 4 / 11 := by
  rw [radiationEntropy_eq, radiationEntropy_eq] at hcons
  have hC : (2 * π ^ 2 / 45 : ℝ) ≠ 0 := by positivity
  have hkey : (11 / 2 : ℝ) * (a₁ * T₁) ^ 3 = 2 * (a₂ * Tγ) ^ 3 := by
    have h : (2 * π ^ 2 / 45 : ℝ) * ((11 / 2) * (a₁ * T₁) ^ 3)
        = (2 * π ^ 2 / 45) * (2 * (a₂ * Tγ) ^ 3) := by
      linear_combination hcons
    exact mul_left_cancel₀ hC h
  rw [← hfree] at hkey
  have ha₂3 : (a₂ : ℝ) ^ 3 ≠ 0 := pow_ne_zero 3 ha₂
  have hTT : (11 / 2 : ℝ) * Tν ^ 3 = 2 * Tγ ^ 3 := by
    have h : a₂ ^ 3 * ((11 / 2 : ℝ) * Tν ^ 3) = a₂ ^ 3 * (2 * Tγ ^ 3) := by
      linear_combination hkey
    exact mul_left_cancel₀ ha₂3 h
  rw [div_pow, div_eq_iff (pow_ne_zero 3 hTγ)]
  linarith

/-- **CAPSTONE.** Entropy conservation through e± annihilation plus free
neutrino streaming force the present-day entropy density to be
`(2π²/45)·(43/11)·T_γ³`: the effective dof `g*s = 43/11` entering
`entropyPerPhoton = π⁴·g*s/(45·ζ(3))` (and hence the η_B dynamical
prefactor) is **derived** from the entropy functional, not assumed. -/
theorem gStarS_from_conservation
    {a₁ a₂ T₁ Tγ Tν : ℝ} (ha₂ : a₂ ≠ 0) (hTγ : Tγ ≠ 0)
    (hcons : radiationEntropy 2 4 T₁ * a₁ ^ 3 = radiationEntropy 2 0 Tγ * a₂ ^ 3)
    (hfree : a₂ * Tν = a₁ * T₁) :
    radiationEntropy 2 0 Tγ + radiationEntropy 0 6 Tν
      = 2 * π ^ 2 / 45 * ((EntropyPerPhoton.gStarS : ℚ) : ℝ) * Tγ ^ 3 :=
  total_entropy_eq_gStarS hTγ
    (dilution_from_entropy_conservation ha₂ hTγ hcons hfree)

/-- **THEOREM (structural form).** The plasma entropy density collapses to
`(2π²/45)·(gB + (7/8)·gF)·T³`, with the `2π²/45` coefficient and the `7/8`
entropy weight both coming from the derived integrals `∫σ_B = 4π⁴/45`,
`∫σ_F = 7π⁴/90` — neither is assumed. -/
theorem radiationEntropy_eq (gB gF T : ℝ) :
    radiationEntropy gB gF T = 2 * π ^ 2 / 45 * (gB + 7 / 8 * gF) * T ^ 3 := by
  unfold radiationEntropy
  rw [RadiationEntropyRelation.bose_entropy_integral_value,
    RadiationEntropyRelation.fermi_entropy_integral_value]
  have hpi : (π : ℝ) ≠ 0 := Real.pi_ne_zero
  field_simp
  ring

/-- Entropy density of a relativistic plasma with `gB` bosonic and `gF`
fermionic internal degrees of freedom at temperature `T`, built directly
from the entropy-functional integrals of `RadiationEntropyRelation`:
each species contributes `(g/2π²)·T³·∫σ`. -/
noncomputable def radiationEntropy (gB gF T : ℝ) : ℝ :=
  gB / (2 * π ^ 2) * T ^ 3
      * (∫ t in Ioi (0 : ℝ), RadiationEntropyRelation.boseEntropyIntegrand t)
    + gF / (2 * π ^ 2) * T ^ 3
      * (∫ t in Ioi (0 : ℝ), RadiationEntropyRelation.fermiEntropyIntegrand t)

What this page does not claim

The theorem does not derive the particle content of the standard model, which is a model input. The theorem does not prove the baryon-to-photon ratio η_B itself, only the g*s prefactor entering it. The theorem does not claim instantaneous decoupling is exact; it is a model approximation.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/NeutrinoDilution.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: