fermiLog_series

The module derives the radiation identity $s = (4/3),\rho/T$ from the microscopic entropy functional of a massless quantum gas, rather than assuming the thermodynamic factor. Pointwise, the Fermi entropy integrand splits as $\sigma_F(x) = x^3/(e^x+1) + x^2\ln(1+e^{-x})$. The second summand is the Fermi logarithmic kernel.

To evaluate Mellin transforms of that kernel one needs a power-series handle on $\ln(1+e^{-t})$ for $t>0$. The classical Mercator expansion of $\ln(1-z)$ at $z = -e^{-t}$ supplies it: because $t>0$ forces $|e^{-t}|<1$, the geometric-log series converges absolutely and yields the alternating form stated here.

Sibling lemmas treat the Bose counterpart $\ln(1-e^{-t})$ and the summability/Mellin packaging used later in the entropy integrals.

First prove $|-e^{-t}|<1$ from $t>0$ via positivity of the exponential and $\mathrm{exp_lt_one_iff}$. Apply Mathlib's Real.hasSum_pow_div_log_of_abs_lt_one at that radius and negate the resulting HasSum. Rewrite the summed value $-\ln(1-(-e^{-t}))$ into $\ln(1+e^{-t})$ by double negation and $a-(-b)=a+b$. Finally congruence the general term: $(-1)^{n+1}(-e^{-t})^{n+1}/(n+1)$ rearranges by neg_pow, pow_succ, and ring into $(-1)^n e^{-t(n+1)}/(n+1)$.

This lemma is the series engine behind hasSum_mellin_fermiLog, which packages the Mellin/Dirichlet identity for the Fermi logarithmic kernel at $s=3$. That identity feeds the evaluation of $\int_0^\infty x^2\ln(1+e^{-x}),dx$ and, with the pointwise split of $\sigma_F$, closes fermi_entropy_eq_four_thirds_energy.

In the broader $\eta_B$ chain the module upgrades the $4/3$ factor and the $7/8$ fermionic weight from thermodynamic inputs to theorems about the entropy functional. Without a controlled expansion of $\ln(1+e^{-t})$, the Fermi half of that derivation has no series path into Gamma/zeta values. The result is pure classical analysis; its Recognition role is infrastructural inside Cosmology rather than a T0–T8 forcing step.