fermi_entropy_pointwise
plain-language theorem explainer
For every positive dimensionless energy t, the Fermi–Dirac entropy integrand equals the Fermi energy kernel plus a logarithmic kernel: σ_F(t) = t³/(eᵗ+1) + t² ln(1+e⁻ᵗ). Cosmology and statistical-mechanics arguments that integrate σ_F cite this identity to split the integral into known pieces. The proof is elementary real analysis: expand the definition, rewrite three logarithms, and cancel algebraically.
Claim. For every real $t > 0$, if $f = 1/(e^{t}+1)$ and $\sigma_F(t) = t^{2}\bigl[-f\ln f - (1-f)\ln(1-f)\bigr]$, then $\sigma_F(t) = \dfrac{t^{3}}{e^{t}+1} + t^{2}\ln\bigl(1+e^{-t}\bigr)$.
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 the $4/3$ factor as a thermodynamic assumption. The Fermi–Dirac occupation is $f = 1/(e^{t}+1)$ with dimensionless energy $t = E/T$. The entropy integrand is defined by
$$\sigma_F(t) = t^{2}\bigl[-f\ln f - (1-f)\ln(1-f)\bigr].$$
The companion Bose identity splits $\sigma_B$ into the Bose energy kernel plus $-t^{2}\ln(1-e^{-t})$. The Fermi case is the parallel decomposition: energy kernel $t^{3}/(e^{t}+1)$ plus logarithmic kernel $t^{2}\ln(1+e^{-t})$. Once the pointwise split is available, the improper integral of $\sigma_F$ reduces to two standard Mellin-type integrals already controlled in the sibling number-density and fermion-weight modules.
proof idea
Tactic proof by direct expansion. First record positivity of $e^{t}$ and $e^{t}+1 \neq 0$. Three logarithmic rewrites follow:
- $\ln(1/(e^{t}+1)) = -\ln(e^{t}+1)$ via $\ln$ of the inverse;
- $\ln(1 - 1/(e^{t}+1)) = t - \ln(e^{t}+1)$ after simplifying the argument to $e^{t}/(e^{t}+1)$ and applying $\ln$ of a quotient;
- $\ln(1+e^{-t}) = \ln(e^{t}+1) - t$ by writing $1+e^{-t} = (e^{t}+1)/e^{t}$.
Unfold the definition of the entropy integrand, substitute the three identities, and finish with ring. No external lemmas beyond Mathlib real-analysis facts are required.
why it matters
This is the Fermi half of the module's method section: the pointwise split that lets the entropy integral be evaluated without assuming $s=(4/3)\rho/T$. Downstream, fermi_entropy_integral_value applies set-integral congruence with this identity to obtain
$$\int_{0}^{\infty}\sigma_F = 7\pi^{4}/90,$$
which is exactly $(4/3)$ times the Fermi energy integral. That value feeds fermi_entropy_eq_four_thirds_energy, the $7/8$ entropy weight relative to Bose, and ultimately the coefficient $2\pi^{2}/45$ in $s_{\gamma}$. In the broader $\eta_B$ chain this closes a MODEL gap: the entropy-per-photon and number-density layers no longer treat $4/3$ as an external thermodynamic input. The result is pure classical analysis; it does not itself invoke the forcing chain T0–T8, but it supplies a certified statistical-mechanics brick those cosmological arguments rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.