Cosmology Neutrino Dilution Dilution From Entropy Conservation

Neutrino dilution from entropy conservation

In the standard cosmology of the early universe, a well-known consequence of entropy conservation is the neutrino-to-photon temperature ratio. The physics: around one second after the Big Bang, neutrinos decouple from the rest of the plasma and stream freely. Shortly after, electron-positron pairs annihilate, dumping their energy into photons but not into the decoupled neutrinos. Because the comoving entropy of the coupled photon-electron sector is conserved during this annihilation, the photons end up hotter than the neutrinos. The classic result, found in textbooks such as Kolb and Turner's The Early Universe, is that the ratio of neutrino temperature to photon temperature cubed equals 4/11.

The Recognition Science framework's machine-checked library of formal theorems proves this dilution factor from two stated physical assumptions. The first is adiabatic expansion: the comoving entropy of the electromagnetically coupled sector is conserved through electron-positron annihilation. The second is free streaming: neutrinos decouple before annihilation sharing the plasma temperature, and their temperature then redshifts with the scale factor as 1/a. Given these two hypotheses, the theorem dilution_from_entropy_conservation (a discrete record of recognition events, in framework terms) derives that (Tν/Tγ)³ = 4/11. The drop in effective degrees of freedom from 11/2 to 2 is not an input; it emerges from the derived entropy integrals for bosons and fermions.

The same derivation also produces the present-day effective number of entropy degrees of freedom, g*s = 43/11. This is the value that enters the baryon-to-photon ratio prefactor in the framework's cosmology chain. The theorem gStarS_from_conservation shows that photons at temperature Tγ plus six fermionic neutrino degrees of freedom at the diluted temperature Tν carry total entropy density (2π²/45)·(43/11)·Tγ³. Both the 4/11 and the 43/11 are thus derived from entropy conservation rather than assumed as bare rational arithmetic.

What the declaration does not claim is broader. The particle content (two photon polarizations, four electron-positron degrees of freedom, six neutrino degrees of freedom), instantaneous decoupling, and the two physical hypotheses themselves remain model assumptions. The framework proves the statistical mechanics: the 7/8 entropy weight for fermions, the 4/3 law, the 2π²/45 coefficient, and the 4/11 and 43/11 ratios given those hypotheses. The framework does not derive the particle content or the decoupling approximation from first principles; those are chosen inputs. The theorem's force is conditional: if the two physical assumptions hold, the dilution ratio and the effective degrees of freedom follow exactly.

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

What this page does not claim

The framework does not derive the particle content (2 photon polarizations, 4 electron-positron dof, 6 neutrino dof) from first principles. The framework does not prove instantaneous decoupling as a physical process. The theorem is conditional: without the two stated physical hypotheses, the 4/11 ratio does not follow.

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: