fermiKernel
plain-language theorem explainer
The Fermi–Dirac occupation factor $1/(e^t+1)$, cast from reals to complexes for Mellin analysis. Anyone equating the Fermi energy or number integral to $\Gamma(s)\eta(s)$ cites this kernel. The body is a pure real-to-complex coercion of the reciprocal of $\exp t+1$; no proof content.
Claim. For each real $t$, define the complex Fermi–Dirac kernel by $F(t) := 1/(e^{t}+1) \in \mathbb{C}$.
background
The module sits at the thermodynamic (integral) layer of the fermion-weight story. Cosmology.FermionWeight already gives the Dirichlet identity $\eta(4)=(7/8)\zeta(4)$. What remains is to identify the physical energy integrals
$$\int_0^\infty t^3/(e^t\pm 1),dt$$
with Mellin transforms of the Bose and Fermi kernels at $s=4$, so the $7/8$ ratio becomes a theorem about those integrals, not only about series.
Both kernels admit geometric expansions for $t>0$: $1/(e^t-1)=\sum_{n\ge 0}e^{-(n+1)t}$ and $1/(e^t+1)=\sum_{n\ge 0}(-1)^n e^{-(n+1)t}$. Mathlib’s Mellin-of-power-series lemma turns those into shifted zeta and eta values times $\Gamma(s)$. The present definition supplies the Fermi side of that bridge, complex-valued so it matches the Mellin API.
proof idea
Pure definition: evaluate the real reciprocal $1/(\mathrm{Real.exp}, t+1)$ and coerce the result into $\mathbb{C}$. No lemmas, no tactics; the noncomputable flag is inherited from real exponentiation and division.
why it matters
This kernel is the Fermi input to the whole integral-layer chain. Downstream, hasSum_mellin_fermi feeds it to Mathlib’s Mellin/Dirichlet identity at $s=4$; mellin_fermi_eq_integral identifies that Mellin value with the complexified thermodynamic integral $\int_{t>0}t^3/(e^t+1),dt$; and mellin_fermi_value evaluates it as $7\pi^4/120=\Gamma(4)\eta(4)$. The same kernel is reused at $s=3$ in NumberDensityIntegral for the Fermi number-density integral.
Together with the Bose twin, these results discharge the mathematical content of EntropyPerPhoton.fermionWeight=7/8: only the $g^*$ species census remains model-level physics. The module status is THEOREM at the integral layer, axiom-clean on Lean’s base axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.