fermiEnergyKernel_eq_occupation
plain-language theorem explainer
The Fermi energy kernel equals dimensionless energy times mean fermionic occupation: $t/(e^t+1)=t\cdot\langle n\rangle_F(t)$. Workers on the RS plasma pressure/energy chain cite it to replace the MODEL energy kernel by an occupation-derived expression from the two-state partition function. The proof rewrites occupation to the Fermi–Dirac closed form, unfolds the kernel, and finishes by ring.
Claim. For every real $t$, the Fermi energy kernel equals dimensionless energy times mean fermionic occupation: $\frac{t}{e^{t}+1}=t\cdot\langle n\rangle_F(t)$, where $\langle n\rangle_F$ is the ensemble mean over the Pauli-allowed occupancies $\{0,1\}$.
background
This module rebuilds the Bose/Fermi pressure kernels $\mp\ln(1\mp e^{-t})$ and energy kernels $t/(e^t\mp 1)$ from a single-mode grand partition at $\mu=0$. The only inputs are Gibbs weights $e^{-n t}$ and the occupancy sets: unrestricted $n\in\mathbb{N}$ for bosons, ${0,1}$ for fermions.
Upstream, PhaseSpaceReduction defined the Fermi energy kernel as the MODEL expression $t/(e^t+1)$. In this module the mean occupation $\langle n\rangle_F$ is the two-state ensemble average $(\sum_{n<2} n,w_n)/Z_F$, and the Fermi–Dirac theorem evaluates it to $1/(e^t+1)$ with no convergence hypothesis. The present identity is the fermionic half of the module claim that energy kernels are exactly $t\cdot\langle n\rangle$.
proof idea
Three-step tactic proof. First rewrite the right-hand side with the Fermi–Dirac closed form $\langle n\rangle_F(t)=1/(e^t+1)$. Then unfold the energy-kernel definition $t/(e^t+1)$. The two sides match by ring arithmetic on the common denominator.
why it matters
Closes item 4 of the module ledger: energy kernels are $t\cdot\langle n\rangle$, not independent MODEL inputs. Downstream, the thermodynamic-consistency theorem rewrites the kernel as $-t,(\mathrm{d}/\mathrm{d}t)\ln Z_F$ by applying this identity after the log-kernel derivative. The plasma-energy capstone then substitutes $t\cdot\langle n\rangle_F$ into the $D=3$ phase-space density and matches GrandPotential.plasmaEnergy, so the $\eta_B$ energy chain starts from $\sum e^{-nE/T}$ rather than a postulated kernel. Parallel to the Bose occupation identity; together they make pressure and energy derivative-related as grand-canonical formalism requires.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.