boseOccupation_pos
plain-language theorem explainer
For any positive dimensionless energy t = E/T, the bosonic mean occupation is strictly positive. Cosmology and statistical-mechanics arguments that need a strictly positive Bose–Einstein factor cite this. The proof rewrites to the closed form 1/(e^t − 1) and uses e^t > 1 to get a positive denominator.
Claim. If $t > 0$, then the bosonic mean occupation $\langle n\rangle_B(t)$ satisfies $0 < \langle n\rangle_B(t)$. Equivalently, $0 < 1/(e^{t}-1)$.
background
This module rebuilds the Bose/Fermi pressure and energy kernels from a single-mode grand partition function at $\mu = 0$, with dimensionless energy $t = E/T$. The only inputs are Gibbs weights $e^{-n t}$ and the occupancy sets ($n \in \mathbb{N}$ for bosons).
The bosonic mean occupation is defined as the ensemble average $\langle n\rangle_B = (\sum_n n, w_n)/Z_B$. Upstream, boseOccupation_eq identifies this with the Bose–Einstein law $\langle n\rangle_B = 1/(e^{t}-1)$ for $t > 0$, via the geometric series $\sum n x^n = x/(1-x)^2$ and $Z_B = (1-x)^{-1}$ with $x = e^{-t}$. The elementary comparison $1 < e^{t}$ for $t > 0$ is recorded as one_lt_exp.
Positivity of $\langle n\rangle_B$ is the elementary sign fact needed before treating energy kernels as $t\cdot\langle n\rangle$ and before thermodynamic derivative identities.
proof idea
Rewrite the goal with boseOccupation_eq under $t > 0$, replacing the series definition by $1/(e^{t}-1)$. Invoke one_lt_exp to get $1 < e^{t}$, hence $e^{t}-1 > 0$ by linarith. Conclude with div_pos on the positive numerator $1$ and that positive denominator.
why it matters
In the StatisticsKernels ledger this is the sign lemma for bosonic occupation: once $\langle n\rangle_B = 1/(e^{t}-1)$ is known, positivity is immediate and licenses treating the Bose energy integrand as $t\cdot\langle n\rangle_B$ with a strictly positive mean occupation at $t > 0$. The module’s next block states that energy kernels are exactly $t\cdot\langle n\rangle$; this fact is the elementary positivity half of that story.
No downstream uses are recorded yet in the graph, so the lemma is presently a local hygiene result inside the Bose/Fermi kernel derivation chain that feeds plasma pressure and energy from $\sum e^{-nE/T}$. It does not touch the forcing chain (T0–T8) or the RCL; it sits in the cosmology statistics layer that makes the $\eta_B$ plasma kernels theorem-shaped rather than MODEL inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.