Cosmology Entropy Per Photon Entropy Per Photon Eq Formula

Entropy per photon

In cosmology, the entropy per photon is a standard measure of the universe's disorder per particle of light. It is conventionally written as s/n_γ and its value is about 7.04. This number appears in calculations of how matter came to outnumber antimatter in the early universe.

The standard derivation is a textbook exercise. The entropy density of a gas of photons and other relativistic particles is set by their temperature and the number of ways each particle can be arranged. The photon density is set by the same temperature. The ratio of the two is π⁴ g_*s / (45 ζ(3)), where g_*s counts the effective degrees of freedom and ζ(3) is the Riemann zeta function evaluated at 3, approximately 1.2020569. The number 7.04 is what this ratio becomes using the known particle content of the Standard Model.

The Recognition Science library has now turned that textbook calculation into a machine-checked theorem. The declaration entropyPerPhoton_eq_formula proves that the ratio equals π⁴ (43/11) / (45 ζ(3)). The factor 43/11 is the present-day value of g_*s, and it is derived, not assumed. The photon contributes 2 degrees of freedom. The electron and positron contribute 4, each weighted by 7/8 because they are fermions. The three neutrino generations contribute 6, also weighted by 7/8, and then diluted by the cube of the neutrino-to-photon temperature ratio, (4/11), after electron-positron annihilation heats the photons but not the neutrinos. The library proves the fermion weight 7/8 from a series identity, and it proves the temperature ratio from entropy conservation. What remains as an input is only the particle content itself.

The theorem does not claim that the universe's actual entropy per photon is exactly 7.04. It proves a window: the value lies between 7.0393 and 7.0396. The familiar 7.04 is that window rounded to three significant figures. The proof bounds ζ(3) by summing its first 40 terms exactly and trapping the infinite tail between two telescoping series, and it bounds π⁴ using standard estimates. The result is a derived constant with a precise range, not a fitted parameter.

Within the framework, this matters because the entropy per photon feeds directly into the dynamical prefactor for baryogenesis, the process that sets the matter-antimatter imbalance. A constant that was previously inserted by hand is now a proved consequence of the Standard Model's particle content and of entropy conservation. The framework's library, a machine-checked collection of formal theorems, propagates the derived window into that prefactor and re-proves the rung-selection theorems that use it.

/-- 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.** `g*s = 43/11 ≈ 3.909`. -/
theorem gStarS_eq : gStarS = 43 / 11 := by
  unfold gStarS gPhoton fermionWeight gNeutrino
  rw [dilutionCubed_eq]
  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

/-- **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 dilutionCubed_eq : dilutionCubed = 4 / 11 := by
  unfold dilutionCubed gAfter gBefore gPhoton fermionWeight gElectron
  norm_num

What this page does not claim

The theorem does not prove the universe's actual entropy per photon equals 7.04 exactly. The theorem does not derive the Standard Model particle content; it takes that content as an input. The theorem does not prove that the entropy per photon is constant throughout cosmic history.

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: