Cosmology Number Density Integral Entropy Density Coeff Provenance

The provenance theorem

In the standard physics of the early universe, the entropy density of a photon gas is written as s = (2π²/45) g*ₛ T³, where T is temperature and g*ₛ counts the effective degrees of freedom. The number 2π²/45 is a familiar but often unexplained factor. The Recognition Science library, a machine-checked collection of formal theorems, contains a result called entropy_density_coeff_provenance that shows this factor is not arbitrary. It proves that (4/3) times the integral of t³/(eᵗ−1) from zero to infinity, divided by 2π², equals exactly 2π²/45. In plain terms, the theorem derives the entropy density coefficient from a single definite integral, the kind that appears in the statistical mechanics of a gas of massless particles.

The proof rests on a known integral: the integral of t³/(eᵗ−1) from 0 to ∞ equals π⁴/15. This is a standard result, and the theorem uses it to rewrite the coefficient. The library's contribution is to verify the chain of reasoning in a formal proof system, so that the equality is not taken on faith but checked step by step. The declaration is part of a larger module that also handles the number density of photons, where the integral of t²/(eᵗ−1) from 0 to ∞ equals 2ζ(3), with ζ(3) the Apéry constant. The number density coefficient is then 2ζ(3)/π², and the ratio of fermion to boson number densities is 3/4, a companion to the 7/8 factor familiar from entropy.

The theorem is a statement about a mathematical identity, not about the physical universe. It does not claim that the entropy density of the actual cosmos is given by this formula, nor that the particle census used in the standard model is correct. The proof takes the statistical mechanics identifications, such as the phase-space measure and the relation s = (4/3)ρ/T, as given. What the theorem establishes is that, once those identifications are accepted, the numerical coefficient 2π²/45 follows from a single integral with no further input. The library's own documentation notes that the only model content left in the entropy-per-photon chain is the particle census and the statistical mechanics identifications; every analytic constant is a theorem.

/-- **THEOREM (entropy-density coefficient provenance).** The `2π²/45`
coefficient of `s = (2π²/45)·g*s·T³` is `(4/3)·(∫t³/(eᵗ−1))/(2π²)`: the
radiation relation `s = (4/3)ρ/T` applied to the Bose energy integral over
the phase-space normalization. -/
theorem entropy_density_coeff_provenance :
    4 / 3 * ((∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1)) / (2 * π ^ 2))
      = 2 * π ^ 2 / 45 := by
  rw [FermionWeightIntegral.bose_integral_value]
  have hpi : (π : ℝ) ≠ 0 := Real.pi_ne_zero
  field_simp
  ring

/-- **THEOREM (Bose number integral).** `∫_{0}^{∞} t²/(eᵗ−1) dt = 2·ζ(3)`.
This is the analytic content of the photon number density
`n_γ = (2ζ(3)/π²)·T³`. -/
theorem bose_number_integral_value :
    (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t - 1)) = 2 * zeta3 := by
  have h := mellin_bose3_value
  rw [mellin_bose3_eq_integral] at h
  exact Complex.ofReal_inj.mp h

/-- **THEOREM (3/4 number-density fermion weight).** The Fermi–Dirac number
integral is exactly 3/4 of the Bose–Einstein one: `η(3)/ζ(3) = 1 − 2⁻² = 3/4`
(the companion of the 7/8 entropy weight). -/
theorem fermi_div_bose_number_integral :
    (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t + 1))
      / (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t - 1)) = 3 / 4 := by
  rw [bose_number_integral_value, fermi_number_integral_value]
  have hz : zeta3 ≠ 0 := zeta3_pos.ne'
  field_simp
  ring

What this page does not claim

The theorem does not claim that the actual entropy density of the universe is given by this formula. The theorem does not claim that the particle census (g*ₛ values) is correct; that is a model assumption. The theorem does not claim that the statistical mechanics identifications, such as s = (4/3)ρ/T, are derived within the framework.

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