Cosmology Number Density Integral Fermi Div Bose Number Integral

The fermion number weight

The number density of a particle species in the early universe is computed from an integral over its momentum states. For massless particles in thermal equilibrium, the integral takes the form ∫ t²/(eᵗ − 1) dt for bosons and ∫ t²/(eᵗ + 1) dt for fermions, where t is a dimensionless measure of energy divided by temperature. The minus sign in the boson kernel and the plus sign in the fermion kernel encode the different statistical behavior of the two families.

The framework's machine-checked library of formal theorems proves that the boson integral equals 2ζ(3) and the fermion integral equals (3/2)ζ(3), where ζ(3) is Apéry's constant, approximately 1.202. The ratio of the fermion integral to the boson integral is therefore exactly 3/4. This is the content of the declaration fermi_div_bose_number_integral: it establishes the ratio of the two number-density integrals, not the individual values, and it does so as a proved theorem.

The 3/4 weight has a direct physical meaning. In the standard cosmological model, the number density of neutrinos relative to photons per species is set by this ratio before any dilution effects. The framework's theorem shows that this 3/4 factor is not an input but a consequence of the integral definitions. It is the number-density companion to the better-known 7/8 factor that appears in the entropy density of fermions; the two factors differ because entropy and number density weight the momentum distribution differently.

The proof follows a two-step Mellin transform argument. First, the zeta function ζ(3) is split into even and odd parts, giving the Dirichlet eta function η(3) = 3/4 ζ(3). Second, the Mellin transform of each kernel at s = 3 evaluates the integral, using the fact that Γ(3) = 2. The theorem is axiom-clean, meaning it relies only on the standard axioms of the underlying type theory, with no additional assumptions.

What the theorem does not claim is equally important. It does not derive the particle census of the standard model, such as the number of neutrino species or the values of the degeneracy factors g. Those remain model choices. It also does not claim that the 3/4 ratio is a prediction of the Recognition Science framework; it is a mathematical identity that holds for the standard integrals. The framework's contribution is to prove the identity rigorously, not to introduce a new physical law.

/-- **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

/-- **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 (Fermi number integral).** `∫_{0}^{∞} t²/(eᵗ+1) dt = (3/2)·ζ(3)`. -/
theorem fermi_number_integral_value :
    (∫ t in Ioi (0 : ℝ), t ^ 2 / (Real.exp t + 1)) = 3 / 2 * zeta3 := by
  have h := mellin_fermi3_value
  rw [mellin_fermi3_eq_integral] at h
  exact Complex.ofReal_inj.mp h

/-- `Γ(3) = 2! = 2`. -/
lemma gamma_three : Complex.Gamma 3 = 2 := by
  have h := Complex.Gamma_ofNat_eq_factorial 2
  norm_num [Nat.factorial] at h
  convert h using 2
  norm_num

/-- `mellin (1/(eᵗ−1)) 3 = 2·ζ(3)` (i.e. `Γ(3)·ζ(3)`). -/
lemma mellin_bose3_value : mellin boseKernel 3 = ((2 * zeta3 : ℝ) : ℂ) := by
  refine hasSum_mellin_bose3.unique ?_
  have hre : HasSum (fun n : ℕ => (2 : ℝ) * ((1 : ℝ) / ((n : ℝ) + 1) ^ 3))
      (2 * zeta3) := hasSum_zeta3_shift.mul_left 2
  have hC := Complex.hasSum_ofReal.mpr hre
  refine hC.congr_fun fun n => ?_
  rw [gamma_three, cpow_shift3 n]
  push_cast
  ring

/-- `mellin (1/(eᵗ+1)) 3 = (3/2)·ζ(3)` (i.e. `Γ(3)·η(3)`). -/
lemma mellin_fermi3_value : mellin fermiKernel 3 = ((3 / 2 * zeta3 : ℝ) : ℂ) := by
  refine hasSum_mellin_fermi3.unique ?_
  have hre : HasSum (fun n : ℕ => (2 : ℝ) * ((-1 : ℝ) ^ n / ((n : ℝ) + 1) ^ 3))
      (3 / 2 * zeta3) := by
    have h := hasSum_eta3_shift.mul_left 2
    convert h using 1
    ring
  have hC := Complex.hasSum_ofReal.mpr hre
  refine hC.congr_fun fun n => ?_
  rw [gamma_three, cpow_shift3 n]
  push_cast
  ring

What this page does not claim

The theorem does not derive the number of neutrino species or any other particle census. The theorem does not claim the 3/4 ratio is a new prediction of the framework. The theorem does not address the physical conditions under which the integrals apply.

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: