Cosmology Neutrino Dilution Total Entropy Eq G Star S

The entropy ledger

In the standard cosmology of the early universe, a plasma of photons, electrons, and positrons cooled until the electrons and positrons annihilated, leaving photons and neutrinos. That event set a permanent ratio between the neutrino and photon temperatures, and it set the total entropy carried by the radiation. The declaration total_entropy_eq_gStarS is a machine-checked theorem stating that, under two named physical assumptions, the present-day entropy density of photons plus neutrinos is exactly (2π²/45)·(43/11)·T_γ³, where T_γ is the photon temperature. The number 43/11 is the effective number of entropy degrees of freedom, usually written g*s.

The two assumptions are both physical models, not mathematical axioms. First, the comoving entropy of the coupled photon-electron-positron sector is conserved through annihilation. Second, neutrinos decouple before annihilation and then redshift freely, so their temperature falls as the inverse scale factor. Given those two hypotheses, the theorem derives the dilution factor (T_ν/T_γ)³ = 4/11 and then the total entropy with g*s = 43/11. The 7/8 fermion entropy weight and the 2π²/45 coefficient come from derived integrals of the entropy functional, not from fitted inputs.

The declaration does not claim that the particle content is derived. The two photon polarizations, four electron-positron degrees of freedom, and six neutrino degrees of freedom are model inputs. Instantaneous decoupling is also a model input. The theorem proves the entropy arithmetic given those inputs. It also does not claim that the baryon-to-photon ratio η_B is derived; g*s enters that prefactor, but the ratio itself is not established here.

What the declaration changes is the status of a standard number. Cosmology textbooks quote g*s = 43/11 as a known result; in this framework it is a proved consequence of entropy conservation plus free streaming, with the statistical mechanics made explicit. The reader can now see the exact chain: plasma entropy density, dilution, total entropy, and the effective degree count, each step checked by the machine.

/-- **THEOREM (provenance).** The present-day total equals
`(2π²/45)·gStarS·T_γ³` with `EntropyPerPhoton.gStarS`: the `43/11` upstream
is the value forced by the diluted neutrino sector. -/
theorem total_entropy_eq_gStarS
    {Tγ Tν : ℝ} (hTγ : Tγ ≠ 0) (hdil : (Tν / Tγ) ^ 3 = 4 / 11) :
    radiationEntropy 2 0 Tγ + radiationEntropy 0 6 Tν
      = 2 * π ^ 2 / 45 * ((EntropyPerPhoton.gStarS : ℚ) : ℝ) * Tγ ^ 3 := by
  have h : ((EntropyPerPhoton.gStarS : ℚ) : ℝ) = 43 / 11 := by
    rw [EntropyPerPhoton.gStarS_eq]
    norm_num
  rw [h]
  exact total_entropy_today hTγ hdil

/-- **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 (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 particle content (2 photon polarizations, 4 electron-positron dof, 6 neutrino dof) is not derived, it is a model input. Instantaneous neutrino decoupling is a model input, not a proved fact. The baryon-to-photon ratio η_B itself is not derived by this declaration.

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: