fermi_energy_kernel_eq
plain-language theorem explainer
The Fermi–Dirac energy integrand t³/(e^t+1) equals t³ times the two-state Pauli occupation number from the fermionic partition function. Cosmology and thermal-radiation arguments cite it to rewrite energy kernels as occupation-weighted moments. The proof is a one-line rewrite by the Fermi occupation identity, followed by ring.
Claim. For every real $t>0$, $$\frac{t^3}{e^{t}+1}=t^3\cdot\frac{\sum_{n=0}^{1} n\,e^{-nt}}{\sum_{n=0}^{1} e^{-nt}}.$$ The right-hand factor is the mean occupancy of a two-state fermionic mode.
background
This module sits between partition kernels and thermal weight integrals. The chain is: grand partition function $Z$ per mode $\to$ mean occupation $\langle n\rangle=1/(e^{t}\mp 1)$ $\to$ energy integrand $t^{3}\langle n\rangle$ $\to$ integrals $\pi^{4}/15$ and $7\pi^{4}/120$, hence the classical $7/8$ photon-to-fermion energy ratio.
Upstream, fermi_occupation proves that the Pauli-restricted two-state average
$(\sum_{n\in{0,1}} n,x^{n})/(\sum_{n\in{0,1}} x^{n})$ with $x=e^{-t}$ equals $1/(e^{t}+1)$. That is exactly the Fermi–Dirac factor appearing in blackbody and neutrino energy densities.
The hypothesis $t>0$ matches the positive temperature (or frequency) regime of the thermal integrals over $(0,\infty)$ used downstream.
proof idea
Term-mode proof in two steps. First rewrite the occupation quotient by the upstream identity PartitionKernels.fermi_occupation t, which replaces
$(\sum_{n:Fin 2} n,e^{-nt})/(\sum_{n:Fin 2} e^{-nt})$
by $1/(e^{t}+1)$. Then ring multiplies through by $t^{3}$ and rearranges to the left-hand energy kernel. No analysis or integral estimates are needed; the equality is purely algebraic once the occupation identity is in hand.
why it matters
Closes the middle link of the module chain: occupation numbers from partition functions become the energy integrands whose integrals are already known. Downstream, energy_ratio_seven_eighths integrates $t^{3}\langle n\rangle_{\mathrm{F}}$ over $(0,\infty)$ against the Bose counterpart and obtains exactly $7/8$ at the partition-function level, not by postulating the integrands.
In Recognition Science cosmology this underwrites the thermal-weight step that feeds radiation and neutrino energy densities without an ad hoc choice of kernel. It is local bookkeeping rather than a forcing-chain (T0–T8) step, but it makes the $7/8$ ratio a derived consequence of the two-state fermionic ledger rather than an imported continuum formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.