fermi_div_bose_integral
plain-language theorem explainer
The Fermi–Dirac energy integral ∫₀^∞ t³/(eᵗ+1) dt equals exactly 7/8 of the Bose–Einstein integral ∫₀^∞ t³/(eᵗ−1) dt. Cosmologists and statistical-mechanics workers tracking the fermionic entropy weight in the photon–electron plasma cite this. The proof substitutes the closed forms π⁴/15 and 7π⁴/120, clears the positive denominator, and finishes by ring.
Claim. The ratio of the Fermi–Dirac and Bose–Einstein energy integrals on $(0,\infty)$ is exactly $7/8$: $$\frac{\displaystyle\int_{0}^{\infty}\frac{t^{3}}{e^{t}+1}\,dt}{\displaystyle\int_{0}^{\infty}\frac{t^{3}}{e^{t}-1}\,dt}=\frac{7}{8}.$$
background
This module sits at the thermodynamic (integral) layer of the 7/8 fermion weight. The series layer already proves η(4)=(7/8)·ζ(4). Here both energy integrals are identified as Mellin transforms at s=4 of the geometric expansions 1/(eᵗ−1)=∑ e^{−(n+1)t} and 1/(eᵗ+1)=∑ (−1)ⁿ e^{−(n+1)t}, yielding Bose = Γ(4)·ζ(4)=π⁴/15 and Fermi = Γ(4)·η(4)=7π⁴/120.
Upstream, bose_integral_value states ∫ t³/(eᵗ−1) dt = π⁴/15 and fermi_integral_value states ∫ t³/(eᵗ+1) dt = 7π⁴/120. The rational constant fermionWeight := 7/8 in EntropyPerPhoton is the bookkeeping factor for fermionic entropy degrees of freedom; its series provenance is fermionWeight_eq_eta_zeta_ratio.
The local claim is the ratio form of those two closed evaluations: the Fermi integral is exactly the weight times the Bose integral.
proof idea
One-line algebraic reduction from the two closed-form evaluations. Rewrite the numerator by fermi_integral_value (7π⁴/120) and the denominator by bose_integral_value (π⁴/15). Clear the division via div_eq_iff after a positivity check on the Bose integral, then finish with ring to obtain 7/8.
why it matters
Closes the integral layer of the 7/8 factor: together with the series identity η(4)=(7/8)·ζ(4), the full mathematical content of fermionWeight = 7/8 is theorem, not model. The only remaining model content in the entropy-per-photon chain is the relativistic-species census g*, not the statistics factor.
Downstream, energy_ratio_seven_eighths restates the same 7/8 ratio at the partition-function level, writing each integrand as t³ times an occupation number drawn from the derived Bose/Fermi partition functions. That occupation-energy theorem cites this integral ratio as the bridge from Mellin/Dirichlet evaluations to thermal energy bookkeeping.
In the broader RS cosmology stack this pins the fermionic weight used before e± annihilation (dof 2+(7/8)·4 = 11/2), so entropy-per-photon numerics rest on proved analysis rather than an imported constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.