one_lt_exp
plain-language theorem explainer
For every positive real t, exp(t) is strictly larger than 1. Cosmology and statistical-mechanics proofs cite it to guarantee that Bose denominators e^t−1 are positive. The argument rewrites 1 as exp(0) and applies strict monotonicity of the real exponential.
Claim. If $t \in \mathbb{R}$ satisfies $t > 0$, then $1 < e^{t}$.
background
The StatisticsKernels module rebuilds the Bose and Fermi pressure and energy kernels from a single-mode grand partition function at vanishing chemical potential. The only dimensionless input is $t = E/T > 0$, and the Gibbs weight of an $n$-quanta microstate is $e^{-n t}$.
Bosonic occupancy runs over all natural numbers, so the partition function is the geometric series $Z_B = (1 - e^{-t})^{-1}$. Mean occupation is then $\langle n \rangle_B = 1/(e^t - 1)$. Any positivity or closed-form argument for that expression needs $e^t > 1$ as soon as $t > 0$; the present lemma isolates that elementary comparison.
A sibling fact exp_neg_lt_one handles the dual inequality $e^{-t} < 1$. Together they keep every Bose denominator and every geometric-series remainder strictly positive on the physical half-line.
proof idea
Two-step tactic proof. First rewrite the constant 1 as $\mathrm{Real.exp}, 0$ via Real.exp_zero. The goal becomes $\exp 0 < \exp t$. Discharge it by Real.exp_lt_exp.mpr applied to the hypothesis $0 < t$, i.e. strict monotonicity of the real exponential. No Recognition-specific lemmas are required; the argument is pure Mathlib analysis.
why it matters
Local support lemma inside the Bose half of StatisticsKernels. Downstream, boseOccupation_eq obtains the closed form $1/(e^t-1)$, and boseOccupation_pos quotes this lemma to conclude $\langle n \rangle_B > 0$ by div_pos and linarith. The same positivity underwrites the derivative identity boseLogKernel_hasDerivAt, which states that mean occupation is minus the $t$-derivative of the log partition function, so pressure and energy kernels are not independent inputs.
In the broader Recognition cosmology stack those kernels feed the plasma pressure and energy identities that close the $\eta_B$ chain. The lemma itself is not a forcing-chain step (T0–T8); it is bookkeeping that keeps the Bose geometric series on solid analytic ground once $t = E/T > 0$ is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.