Cosmology Entropy Per Photon

Entropy per photon

In cosmology, entropy per photon is the ratio of the universe's total entropy to the number of photons in it, a number that stays nearly constant as the universe expands. It appears in calculations of how matter came to outnumber antimatter, and in the standard model of particle physics it is treated as a fixed input, usually given as 7.04. The ratio is defined by the formula s / n_γ = π⁴ g_*s / (45 ζ(3)), where g_*s counts the effective degrees of freedom for entropy, and ζ(3) is the Riemann zeta function evaluated at 3, approximately 1.2020569.

The standard derivation, found in textbooks like Kolb and Turner's The Early Universe, builds the ratio from two ingredients: the statistical mechanics of a hot gas of particles, and the particle content of the Standard Model. The photon contributes 2 degrees of freedom from its two polarizations; electrons and positrons add 4 fermionic degrees of freedom; and three neutrino generations add 6. Fermions get a statistical weight of 7/8 relative to bosons, and after electron-positron annihilation the neutrino temperature drops relative to the photon temperature by a factor (4/11)^1/3, because the entropy released heats the photons but not the decoupled neutrinos. Combining these gives g_*s = 43/11, and the formula yields 7.0393 to 7.0396.

In Recognition Science, the framework's machine-checked library of formal theorems re-derives this number instead of assuming it. The library proves the value of ζ(3) lies between 1.202042 and 1.202065 by splitting the infinite sum at 40 terms and bounding the tail with telescoping series. It proves π⁴ lies between 97.40900 and 97.40914 using standard bounds on π. It also proves the 7/8 fermion weight and the thermodynamic integrals themselves, such as ∫x³/(e^x+1) dx = 7π⁴/120, instead of taking them as inputs. The only assumptions left are the Standard Model particle content and two named conservation hypotheses: comoving entropy conservation and free neutrino streaming.

The main result is a theorem: entropy per photon = π⁴ (43/11) / (45 ζ(3)), which lies strictly between 7.0393 and 7.0396, and is within 0.0007 of the rounded value 7.04. This derived window replaces the bare constant used in earlier staging modules, and it propagates into the dynamical prefactor P = (28/79) · s/n_γ, so the framework's rung-selection theorems now rest on a fully derived prefactor instead of a fitted number. What this establishes in plain language is that a standard cosmological input, usually taken from observation or convention, can be computed from the particle content and the laws of thermodynamics alone, with the arithmetic checked by a machine.

/-- **THEOREM.** `ζ(3) > 1.202042`. -/
theorem zeta3_gt : (1.202042 : ℝ) < zeta3 := by
  rw [zeta3_split]
  have h1 := S40_gt
  have h2 := tail_ge
  linarith

/-- **THEOREM.** `ζ(3) < 1.202065`. -/
theorem zeta3_lt : zeta3 < (1.202065 : ℝ) := by
  rw [zeta3_split]
  have h1 := S40_lt
  have h2 := tail_le
  linarith

/-- **THEOREM.** `π⁴ > 97.40900`. -/
theorem pi4_gt : (97.40900 : ℝ) < Real.pi ^ 4 := by
  have h := Real.pi_gt_d6
  calc (97.40900 : ℝ) < (3.141592 : ℝ) ^ 4 := by norm_num
    _ < Real.pi ^ 4 := by
        apply pow_lt_pow_left₀ h (by norm_num)
        norm_num

/-- **THEOREM.** `π⁴ < 97.40914`. -/
theorem pi4_lt : Real.pi ^ 4 < (97.40914 : ℝ) := by
  have h := Real.pi_lt_d6
  calc Real.pi ^ 4 < (3.141593 : ℝ) ^ 4 := by
        apply pow_lt_pow_left₀ h (le_of_lt Real.pi_pos)
        norm_num
    _ < (97.40914 : ℝ) := by norm_num

/-- Fermionic entropy weight `7/8`: the ratio of the Fermi–Dirac to
Bose–Einstein thermodynamic integrals, `∫x³/(eˣ+1) / ∫x³/(eˣ−1) = η(4)/ζ(4)
= 1 − 2⁻³ = 7/8`.

**THEOREM-backed** (upgraded from MODEL 2026-07-01): the series layer is
`FermionWeight.fermionWeight_eq_eta_zeta_ratio` (`η(4) = (7/8)·ζ(4)`), and
the integral layer is `FermionWeightIntegral.fermi_integral_eq_weight_mul_bose`
(`∫ t³/(eᵗ+1) = (7/8)·∫ t³/(eᵗ−1)`, with both integrals in closed form:
`π⁴/15` and `7π⁴/120`). Both are axiom-clean. The modules import this
definition (not vice versa), so the value stays a plain rational here. -/
def fermionWeight : ℚ := 7 / 8

/-- The ratio in terms of the derived `gStarS` (the `43/11` in the definition
is not bare: it is `gStarS`). -/
theorem entropyPerPhoton_eq_formula :
    entropyPerPhoton = Real.pi ^ 4 * (gStarS : ℝ) / (45 * zeta3) := by
  rw [gStarS_eq]
  norm_num [entropyPerPhoton]

/-- **THEOREM.** `s/n_γ > 7.0393`. -/
theorem entropyPerPhoton_gt : (7.0393 : ℝ) < entropyPerPhoton := by
  have hz := zeta3_lt
  have hp := pi4_gt
  have hzpos := zeta3_pos
  unfold entropyPerPhoton
  rw [lt_div_iff₀ (by linarith : (0 : ℝ) < 45 * zeta3)]
  nlinarith

/-- **THEOREM.** `s/n_γ < 7.0396`. -/
theorem entropyPerPhoton_lt : entropyPerPhoton < (7.0396 : ℝ) := by
  have hz := zeta3_gt
  have hp := pi4_lt
  have hzpos := zeta3_pos
  unfold entropyPerPhoton
  rw [div_lt_iff₀ (by linarith : (0 : ℝ) < 45 * zeta3)]
  nlinarith

/-- **THEOREM (the staged constant is the derived value to 3 s.f.).**
`|s/n_γ − 7.04| < 0.0007`: the bare `7.04` in the staging modules is the
derived ratio rounded to three significant figures. -/
theorem entropyPerPhoton_near_704 : |entropyPerPhoton - 7.04| < 0.0007 := by
  rw [abs_sub_lt_iff]
  constructor
  · linarith [entropyPerPhoton_lt]
  · linarith [entropyPerPhoton_gt]

What this page does not claim

The module does not derive the particle content of the Standard Model; it takes the photon, electron, and neutrino degrees of freedom as MODEL inputs. The theorem does not establish that the universe's entropy is exactly this value; it derives the ratio from the specified statistical mechanics and conservation assumptions. The framework does not claim to have measured entropy per photon; the 7.04 value is a standard cosmological input, and this module derives it from theory rather than observation.

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/EntropyPerPhoton.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: