Cosmology Neutrino Dilution Radiation Entropy

The entropy ledger

In the standard picture of the early universe, the cosmos was a hot plasma of photons, electrons, positrons, and neutrinos. When the temperature fell enough, electrons and positrons annihilated, dumping their energy into the photon gas. The neutrinos, already decoupled, did not share in that heat. The result is a lasting temperature difference: the neutrino background today is cooler than the photon background. Cosmology has long computed this ratio as (T_ν/T_γ)³ = 4/11, a number that appears in every textbook on the early universe.

The Recognition Science framework's machine-checked library of formal theorems addresses this in a module called NeutrinoDilution. Its central object, radiationEntropy (a discrete record of the entropy density of a relativistic plasma), is defined as a sum over bosonic and fermionic species. Each species contributes (g/2π²)·T³·∫σ, where g counts internal degrees of freedom and σ is the entropy functional. The library proves, as a theorem, that this expression collapses to the compact form (2π²/45)·(gB + (7/8)·gF)·T³. The coefficient 2π²/45 and the fermion weight 7/8 are not assumed; they emerge from integrals of the entropy functional that the library derives from the Mercator and Mellin machinery.

The physical derivation then proceeds from two model hypotheses. First, adiabatic expansion: the comoving entropy of the coupled photon-electron sector is conserved through annihilation. Second, free streaming: the decoupled neutrinos redshift their temperature as 1/a, meaning a·T_ν stays constant. Given these two hypotheses, the library proves the dilution theorem: (T_ν/T_γ)³ = 4/11. The drop in effective degrees of freedom from 11/2 to 2 is not an input; it is produced by the derived entropy-functional integrals. A further theorem shows that the present-day total entropy, photons at T_γ plus six fermionic neutrino degrees of freedom at T_ν, equals (2π²/45)·(43/11)·T_γ³. The effective degrees of freedom g*s = 43/11, which enters the baryon-to-photon ratio η_B, is thus derived from entropy conservation rather than assumed.

What the declaration does not claim is as important as what it proves. The particle content (two photon polarizations, four electron-positron degrees of freedom, six neutrino degrees of freedom) and the assumption of instantaneous decoupling remain model hypotheses. The framework does not derive these from first principles; it takes them as inputs. The statistical mechanics, including the 7/8 entropy weight and the 4/11 and 43/11 ratios given those hypotheses, is theorem-grade. The two hypotheses themselves are also discharged downstream in a later module, where comoving entropy conservation and the 1/a redshift law are derived from the Friedmann equations. But the framework does not claim to derive the particle content of the standard model from its own axioms.

/-- 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)

/-- **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

/-- **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

/-- **THEOREM (present-day entropy).** Photons at `T_γ` plus 6 fermionic
neutrino dof at `T_ν` with `(T_ν/T_γ)³ = 4/11` carry total entropy
`(2π²/45)·(43/11)·T_γ³`. -/
theorem total_entropy_today
    {Tγ Tν : ℝ} (hTγ : Tγ ≠ 0) (hdil : (Tν / Tγ) ^ 3 = 4 / 11) :
    radiationEntropy 2 0 Tγ + radiationEntropy 0 6 Tν
      = 2 * π ^ 2 / 45 * (43 / 11) * Tγ ^ 3 := by
  rw [radiationEntropy_eq, radiationEntropy_eq]
  have hTν3 : Tν ^ 3 = 4 / 11 * Tγ ^ 3 := by
    rw [div_pow, div_eq_iff (pow_ne_zero 3 hTγ)] at hdil
    linarith
  rw [hTν3]
  ring

What this page does not claim

The framework does not derive the particle content (photon polarizations, electron-positron degrees of freedom, neutrino degrees of freedom) from its axioms; these are model inputs. The framework does not claim instantaneous decoupling is derived; it is a model hypothesis, though downstream modules derive the two main hypotheses from the Friedmann equations. The declaration does not claim to compute the absolute entropy of the universe, only the entropy density of a relativistic plasma.

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: