occupationEnergyCert
plain-language theorem explainer
Packages two identities into a single audit certificate: the Bose energy integrand equals dimensionless energy times the occupation number from the grand partition function, and the Fermi-to-Bose thermal energy integral ratio is exactly 7/8 when both integrands are written as t³⟨n⟩. Cosmology auditors tracing 7/8 back to Z cite this. Proof is a term-mode pair of the two component theorems.
Claim. For every $t>0$, $\frac{t^3}{e^t-1}=t^3\cdot\frac{\sum_{n=1}^\infty n\,e^{-nt}}{\sum_{n=0}^\infty e^{-nt}}$, and the ratio of $\int_0^\infty t^3\langle n\rangle_{\mathrm{F}}\,dt$ to $\int_0^\infty t^3\langle n\rangle_{\mathrm{B}}\,dt$ equals $7/8$, where the Fermi occupation uses the two-term sum over $\{0,1\}$ and the Bose occupation uses the full geometric series.
background
The module links occupation numbers from the per-mode grand partition function to the classical energy integrands $t^3/(e^t\mp 1)$. The chain is: partition function $Z$ yields mean occupation $\langle n\rangle=1/(e^t\mp 1)$, the energy density integrand is $t^3\langle n\rangle$, and the integrals of those kernels recover $\pi^4/15$ (Bose) and $7\pi^4/120$ (Fermi), hence the ratio $7/8$.
Upstream, bose_energy_kernel_eq states that the Bose energy integrand equals $t^3$ times the occupation number derived from the partition function (via the geometric-series formula for $\langle n\rangle$). Upstream energy_ratio_seven_eighths restates the $7/8$ ratio with both integrands written explicitly as $t^3\times\langle n\rangle$ from those partition-function occupations, rather than as the closed forms $t^3/(e^t\mp 1)$ alone.
The Fermi side uses a finite sum over $\mathrm{Fin},2$ (occupation $0$ or $1$); the Bose side uses the full series over $\mathbb{N}$.
proof idea
One-line term proof: the certificate is the ordered pair of the two already-proved component theorems. The first conjunct is bose_energy_kernel_eq (rewrite by the Bose occupation identity from PartitionKernels, then ring). The second conjunct is energy_ratio_seven_eighths (the $7/8$ ratio at the $t^3\langle n\rangle$ level). No extra algebra is performed here.
why it matters
Closes the end-to-end audit path advertised in the module: partition function $\to$ occupation number $\to$ energy integrand $\to$ integral values and $7/8$. Without this packaging, the $7/8$ factor in thermal cosmology could be read as an ad-hoc choice of integrand; with it, $7/8$ is derived from $Z$. The module status line marks these as THEOREM targets under loop management. No downstream consumers are wired yet (used_by is empty); the declaration exists as the named certificate for axiom-audit pages rather than as a lemma inside a larger proof tree. In the broader RS cosmology stack it anchors the fermionic thermal weight relative to the bosonic one once the eight-tick and ladder structure fix the mode counting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.