Cosmology Number Density Integral Bose Number Integral Value

The photon count integral

In the standard physics of the early universe, the number of photons in a hot bath is not a guess but a definite integral. For a gas of particles that obey Bose-Einstein statistics, the number density nᵧ is proportional to ∫₀^∞ t²/(eᵗ−1) dt, where t is a scaled energy. The integral itself has a known exact value: it equals 2 times ζ(3), where ζ(3) ≈ 1.2020569 is Apéry's constant, the value of the Riemann zeta function at 3. This is a classical result, derived by expanding the integrand as a geometric series and integrating term by term.

The Recognition Science framework's machine-checked library of formal theorems contains a proof of this identity, named bose_number_integral_value. The theorem states, in the framework's own notation, that the integral from 0 to infinity of t²/(eᵗ−1) with respect to t equals 2 * zeta3. Here zeta3 is the framework's formal name for Apéry's constant. The proof follows the classical two-step Mellin transform argument: first, the geometric series for the kernel 1/(eᵗ−1) is converted into a Dirichlet series, and second, the resulting sum is evaluated using the known value of the zeta function at s=3. The framework's proof is axiom-clean, meaning it relies only on the standard axioms of its logical foundation and no framework-specific assumptions.

This integral is not an isolated curiosity; it is the last analytic piece in the framework's derivation of the entropy per photon in the early universe. The framework proves that the photon number density coefficient, gᵧ times the integral divided by 2π², equals 2ζ(3)/π². It also proves a companion result for fermions: the same integral with a plus sign in the denominator equals (3/2)ζ(3). Taking the ratio of the fermion to boson integrals gives exactly 3/4, a number that appears in cosmology as the dilution factor for neutrino number densities relative to photons. These results are tagged as theorems in the framework, meaning they are formally proved.

What the declaration does not claim is just as important as what it proves. It does not claim that the integral equals a closed-form expression involving π; ζ(3) is known to be irrational but no simple closed form is known, and none is needed. It does not claim that the physical universe actually contains this many photons; that requires additional model choices, such as the values of the statistical weights gᵧ, gₑ, and gᵥ, and the identification of the phase-space measure. The theorem is about the mathematics of the integral, not about the empirical content of cosmology. It also does not claim that the framework derives the fine-structure constant or any other coupling constant; that remains an open target.

The practical consequence is that a central quantity in early-universe physics, the photon number density, is now anchored to a formally verified mathematical identity. Anyone reading a cosmology textbook can see the same integral, but the framework's contribution is to have its value checked by a machine, with no hidden assumptions in the analytic steps. The remaining choices in the entropy-per-photon chain are explicit model choices, not unproved mathematical leaps.

/-- **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 (photon number-density coefficient provenance).** The `2ζ(3)/π²`
coefficient of `n_γ = (2ζ(3)/π²)·T³` is `g_γ·(∫t²/(eᵗ−1))/(2π²)` with
`g_γ = 2`: the Bose number integral over the phase-space normalization. -/
theorem number_density_coeff_provenance :
    ((EntropyPerPhoton.gPhoton : ℚ) : ℝ)
        * (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t - 1)) / (2 * π ^ 2)
      = 2 * zeta3 / π ^ 2 := by
  rw [bose_number_integral_value]
  unfold EntropyPerPhoton.gPhoton
  have hpi : (π : ℝ) ≠ 0 := Real.pi_ne_zero
  push_cast
  field_simp

/-- **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 ζ(3) has a closed form in terms of π or any other elementary constant. The theorem does not claim that the physical universe contains exactly this many photons; that requires additional model choices for statistical weights. The theorem does not claim to derive the fine-structure constant or any other coupling constant from first principles.

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: