fermiLogKernel
plain-language theorem explainer
The Fermi logarithmic kernel sends a real scaled energy t to the complex value ln(1+e^{-t}). Radiation-entropy and phase-space pressure developments cite it as the fermionic log-partition integrand inside Mellin and 3D reductions. The body is a direct real logarithm coerced to ℂ; no further proof content.
Claim. For each real $t$, the Fermi logarithmic kernel is the complex number $\ln(1+e^{-t})$, obtained by evaluating the real logarithm and coercing $\mathbb{R}\to\mathbb{C}$.
background
The module derives the radiation identity $s=(4/3)\rho/T$ for a massless quantum gas from the microscopic entropy functional, rather than assuming the thermodynamic factor. For Fermi–Dirac statistics the entropy integrand splits pointwise as $\sigma_F(x)=x^3/(e^x+1)+x^2\ln(1+e^{-x})$, so the logarithmic piece $\ln(1+e^{-x})$ is an independent kernel that must be integrated against $x^2$ (and later Mellin-transformed).
A real-valued twin already lives in the phase-space reduction layer as the Fermi pressure kernel $\ln(1+e^{-t})$. The present definition re-exports the same elementary expression at type $\mathbb{C}$ so that the Mellin machinery (complex contour and series arguments) can consume it without repeated coercions.
Upstream, the two-state Fermi partition $Z_F(t)=1+e^{-t}$ is known; its logarithm is exactly this kernel. The complex packaging is bookkeeping for the entropy and pressure chains, not a change of physics.
proof idea
Pure definition. Evaluate $\mathrm{Real.log}(1+\mathrm{Real.exp}(-t))$ on $\mathbb{R}$ and coerce the result to $\mathbb{C}$. No lemmas, no tactics, no analytic continuation is performed at this site.
why it matters
This kernel is the fermionic half of the log-partition layer that closes the radiation-entropy MODEL element in the $\eta_B$ chain. Downstream, hasSum_mellin_fermiLog and the Mellin-value theorems feed on the complex form; fermiLogKernel_from_partition and partitionKernelsCert identify it with $\log Z_F$ from the two-state Pauli sum; the phase-space pressure closed form and potential theorems insert it into the 3D integral that yields Stefan–Boltzmann with the fermionic $7/8$ weight and the thermodynamic relation $s=dP/dT$.
Together with the Bose twin, it lets the module prove $\int\sigma_F=(4/3)\int x^3/(e^x+1)$ and $\int\sigma_F/\int\sigma_B=7/8$ at the entropy-functional layer, so the classical $4/3$ factor and the $2\pi^2/45$ photon coefficient are derived rather than assumed. It is scaffolding-free definitional glue between partition functions, Mellin transforms, and the pressure-to-entropy derivative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.