bose_energy_kernel_eq
plain-language theorem explainer
For positive dimensionless temperature t, the Bose energy integrand t³/(e^t−1) equals t³ times the mean bosonic occupation written as a ratio of geometric series. Cosmology and thermal-weight arguments cite it to ground the classical Bose kernel in the partition-function occupation number. The proof is a one-line rewrite by the Bose occupation identity followed by ring algebra.
Claim. For every real $t>0$, $$\frac{t^3}{e^t-1}=t^3\cdot\frac{\sum_{n=0}^\infty n\,e^{-nt}}{\sum_{n=0}^\infty e^{-nt}}.$$
background
This module sits in the cosmology energy-kernel chain: grand partition function Z per mode yields an occupation number ⟨n⟩, which is then multiplied by the dimensionless mode energy t³ to produce the energy integrand whose integrals are already known.
Upstream, bose_occupation states that the Bose–Einstein mean occupancy equals both the series ratio (Σ n x^n)/(Σ x^n) with x=e^{-t} and the closed form 1/(e^t−1), for t>0. The classical Bose energy density integrand is t³/(e^t−1); the present result simply factors that closed form as t³·⟨n⟩.
The module goal is to derive the thermal 7/8 ratio from partition functions rather than from ad-hoc integrands. Sibling results do the same for Fermi–Dirac statistics and then form the ratio of the two energy integrals.
proof idea
Term-mode proof in two steps. First rewrite the right-hand occupation ratio by the upstream theorem that equates (Σ n e^{-nt})/(Σ e^{-nt}) with 1/(e^t−1) for t>0. After that substitution the two sides differ only by the common factor t³, and ring finishes the equality.
why it matters
Closes the Bose half of the occupation-to-energy step in the module chain: Z → ⟨n⟩ → t³·⟨n⟩ → integrated thermal weights. Downstream, energy_ratio_seven_eighths quotes this identity (and its Fermi twin) so that the ratio of energy integrals is stated entirely at the partition-function level and equals 7/8. The certificate occupationEnergyCert packages the same equality for the axiom audit.
In the broader Recognition Science cosmology layer this justifies treating the standard Bose kernel as derived from the per-mode grand partition function, not postulated. It does not itself invoke the forcing chain (T5–T8) or the J-cost; those enter only if one later ties the thermal weights to ledger or recognition structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.