fermi_div_bose_entropy
plain-language theorem explainer
The Fermi–Dirac entropy integral on (0,∞) equals exactly 7/8 of the Bose–Einstein entropy integral. Anyone tracking the η_B / entropy-per-photon chain cites this to lift the fermionic statistics weight from energy to the entropy functional. Proof rewrites both sides to closed forms 7π⁴/90 and 4π⁴/45, clears the positive denominator, and rings.
Claim. Let $\sigma_F(t)=t^2[-f\ln f-(1-f)\ln(1-f)]$ with $f=1/(e^t+1)$ and $\sigma_B(t)=t^2[(1+g)\ln(1+g)-g\ln g]$ with $g=1/(e^t-1)$. Then $\bigl(\int_0^\infty\sigma_F\bigr)/\bigl(\int_0^\infty\sigma_B\bigr)=7/8$.
background
This module derives the radiation identity $s=(4/3),\rho/T$ from the microscopic entropy functional of a massless quantum gas, rather than importing 4/3 as a thermodynamic axiom. The Bose integrand is $\sigma_B(t)=t^2[(1+f)\ln(1+f)-f\ln f]$ with $f=1/(e^t-1)$; the Fermi integrand is $\sigma_F(t)=t^2[-f\ln f-(1-f)\ln(1-f)]$ with $f=1/(e^t+1)$.
Upstream, bose_entropy_integral_value evaluates $\int_0^\infty\sigma_B=4\pi^4/45$, and fermi_entropy_integral_value evaluates $\int_0^\infty\sigma_F=7\pi^4/90$. Both rest on a pointwise split of each entropy kernel into the energy density piece plus a logarithmic kernel, then Mellin/series evaluation.
The rational constant $7/8$ is the same fermionic weight already recorded as fermionWeight in EntropyPerPhoton: the energy-layer ratio $\int t^3/(e^t+1),/,\int t^3/(e^t-1)=\eta(4)/\zeta(4)=1-2^{-3}=7/8$. The present result lifts that weight to the entropy-functional layer.
proof idea
One short tactic proof. Rewrite the numerator by fermi_entropy_integral_value ($7\pi^4/90$) and the denominator by bose_entropy_integral_value ($4\pi^4/45$). Apply div_eq_iff after a positivity check on the Bose integral, then ring to obtain $7/8$. No new analytic work: the closed forms already carry the $\pi^4$ factors that cancel in the ratio.
why it matters
Closes the third bullet of the module's theorem list: the fermionic statistics factor now holds at the entropy-functional layer, not only at the energy layer. That is the content of the doc-comment: "$\int\sigma_F=\mathrm{fermionWeight}\cdot\int\sigma_B$ with the $7/8$ MODEL constant of EntropyPerPhoton.fermionWeight."
Together with the companion identities $\int\sigma_B=(4/3)\int x^3/(e^x-1)$ and $\int\sigma_F=(4/3)\int x^3/(e^x+1)$, it discharges the last MODEL input that the entropy-per-photon and number-density chain had been assuming. Downstream the module extracts the coefficient $2\pi^2/45$ of $s_\gamma=(2\pi^2/45),g,T^3$ without ever positing 4/3. No external used_by edges yet; the declaration is the terminal ratio step inside this module's η_B closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.