number_integrand_bose
plain-language theorem explainer
The boson number-density integrand t²/(eᵗ−1) equals t² times the mean Bose occupation of a mode. Cosmologists tying photon number density to the grand partition function cite this identity. The proof rewrites occupation by the Bose–Einstein closed form and finishes by ring cancellation.
Claim. For every real $t>0$, $t^2\cdot\langle n\rangle_B(t)=t^2/(e^t-1)$, where $\langle n\rangle_B(t)$ is the ensemble-mean occupation of a single bosonic mode at dimensionless energy $t=E/T$.
background
The StatisticsKernels module rebuilds the Bose/Fermi pressure and energy kernels from the single-mode grand partition function at $\mu=0$. Inputs are only Gibbs weights $e^{-n t}$ and the occupancy sets: unrestricted $n\in\mathbb{N}$ for bosons, ${0,1}$ for fermions.
Mean Bose occupation is defined as $\langle n\rangle_B=(\sum_n n,w_n)/Z_B$. Upstream, the Bose–Einstein theorem evaluates the weighted geometric series to the closed form $\langle n\rangle_B=1/(e^t-1)$ for $t>0$.
In the number-density integral, modes are weighted by a phase-space factor $t^2$. The classical photon integrand is therefore $t^2/(e^t-1)$, whose integral is $2\zeta(3)$. This lemma records that the integrand is exactly $t^2$ times occupation.
proof idea
One-line wrapper: rewrite the left-hand side by the upstream Bose–Einstein identity $\langle n\rangle_B(t)=1/(e^t-1)$, then cancel the common factor $t^2$ with ring. No series work is repeated here.
why it matters
Places the standard photon number integrand on the same footing as the energy kernels already derived from $\ln Z$: number density counts occupation over modes, not an independent MODEL input. The module doc frames this as step 3–4 of the partition-function program (occupation closed forms, then kernels as $t\cdot\langle n\rangle$ or mode measures times $\langle n\rangle$). No recorded downstream users yet; the natural landing site is a NumberDensityIntegral construction in the cosmology chain. No T0–T8 forcing landmark is involved; this is thermodynamic bookkeeping for the photon/plasma sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.