fermi_div_bose_number_integral
plain-language theorem explainer
The Fermi–Dirac number-density integral equals three-quarters of the Bose–Einstein one on the positive half-line. Cosmologists cite this for the fermion number weight η(3)/ζ(3)=3/4 that sets n_ν/n_γ per species before dilution. Proof substitutes the closed values (3/2)ζ(3) and 2ζ(3), then clears the ratio by field arithmetic.
Claim. The ratio of improper integrals $\bigl(\int_{0}^{\infty} t^{2}/(e^{t}+1)\,dt\bigr)\big/\bigl(\int_{0}^{\infty} t^{2}/(e^{t}-1)\,dt\bigr)$ equals $3/4$.
background
This module closes the number-density layer (Mellin transforms at $s=3$) for thermal integrals in early-universe cosmology. The Bose kernel $\int_{0}^{\infty}t^{2}/(e^{t}-1),dt$ equals $\Gamma(3)\zeta(3)=2\zeta(3)$; the Fermi kernel equals $\Gamma(3)\eta(3)=(3/2)\zeta(3)$. Here $\zeta(3)$ is Apéry's constant, the series $\sum 1/(n+1)^{3}$, and the Dirichlet eta identity $\eta(3)=(1-2^{1-3})\zeta(3)=(3/4)\zeta(3)$ supplies the weight.
The companion energy-density module at $s=4$ already produced the $7/8$ fermion entropy weight. Number densities dilute with the $3/4$ factor instead. Upstream theorems evaluate the two integrals separately: the Bose value is $2\zeta(3)$ and the Fermi value is $(3/2)\zeta(3)$, each obtained by Mellin–Dirichlet uniqueness from the geometric series of the kernels.
proof idea
Algebraic one-step reduction after substitution. Rewrite both sides by the upstream value theorems (Bose integral $=2\zeta(3)$, Fermi integral $=(3/2)\zeta(3)$). Non-vanishing of $\zeta(3)$ (from the positivity lemma) lets field_simp clear the common factor; ring finishes $(3/2)/2=3/4$.
why it matters
Number-density companion of the classic $7/8$ fermionic entropy weight. Module documentation calls it the last analytic ingredient of the photon number-density formula $n_{\gamma}=(2\zeta(3)/\pi^{2})T^{3}$ and of the rewrite of entropy-per-photon as a pure ratio of thermodynamic integrals. Cosmology uses the $3/4$ factor for species number ratios such as $n_{\nu}/n_{\gamma}$ before $e^{+}e^{-}$ dilution. Inside the Recognition cosmology stack it pins the $s=3$ integral layer that supports the entropy-per-photon constant with $g_{*s}=43/11$. No further downstream dependents are recorded yet; the result is a leaf that closes the number-density bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.