bose_entropy_pointwise
plain-language theorem explainer
For every positive dimensionless energy t, the Bose–Einstein entropy integrand equals the energy kernel t³/(eᵗ−1) plus the logarithmic kernel t²(−ln(1−e^{−t})). Cosmologists deriving s=(4/3)ρ/T from the microscopic entropy functional cite this identity. The proof is elementary real analysis: rewrite the three logarithms in the expanded σ_B definition and cancel by ring.
Claim. For every real $t>0$, the Bose–Einstein entropy integrand $\sigma_B(t)=t^2\bigl[(1+f)\ln(1+f)-f\ln f\bigr]$ with $f=1/(e^t-1)$ equals $$\sigma_B(t)=\frac{t^3}{e^t-1}+t^2\bigl(-\ln(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 Bose entropy integrand is
$$\sigma_B(t)=t^2\bigl[(1+f)\ln(1+f)-f\ln f\bigr],\qquad f=\frac{1}{e^t-1}.$$
The module method is to split $\sigma_B$ pointwise into the Bose energy kernel $t^3/(e^t-1)$ plus a pure logarithmic kernel $t^2(-\ln(1-e^{-t}))$. Once that split is available, the definite integral of $\sigma_B$ reduces to known Mellin/energy integrals already developed in the sibling number-density and fermion-weight modules.
The same pattern is stated for Fermi–Dirac statistics in the companion pointwise lemma immediately below.
proof idea
Fix $t>0$. First record $e^t>1$ (so $e^t-1\neq 0$) from monotonicity of $\exp$. Three logarithmic rewrites are proved by field simplification and the log-quotient rule:
- $\ln\bigl(1+1/(e^t-1)\bigr)=t-\ln(e^t-1)$,
- $\ln\bigl(1/(e^t-1)\bigr)=-\ln(e^t-1)$,
- $\ln(1-e^{-t})=\ln(e^t-1)-t$.
Unfold the definition of the entropy integrand, substitute the three identities, and finish with ring. No external lemmas beyond Mathlib real-analysis primitives are required.
why it matters
This is the algebraic hinge of the Bose half of the radiation-entropy relation. Downstream, bose_entropy_integral_value integrates the split form over $(0,\infty)$ and obtains $\int\sigma_B=4\pi^4/45$, which is exactly $(4/3)$ times the Bose energy integral. That equality is what closes the MODEL step in the $\eta_B$ chain: the factor $4/3$ and the coefficient $2\pi^2/45$ in $s_\gamma=(2\pi^2/45)gT^3$ emerge from the entropy functional rather than being postulated.
The Fermi twin and the ratio $\int\sigma_F/\int\sigma_B=7/8$ sit on the same foundation. Within Recognition Science cosmology this supplies the statistical-mechanics layer that earlier entropy-per-photon arguments had treated as an external input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.