half_sq_le_cosh_sub_one
plain-language theorem explainer
The elementary inequality $\cosh t-1\ge t^2/2$ holds for every real $t$. Analysts cite it when converting J-cost bounds into Gaussian tails in log-coordinates. The proof splits on the sign of $t$ and reduces the negative case to the nonnegative lemma via evenness of $\cosh$.
Claim. For every real number $t$, $\dfrac{t^{2}}{2}\le\cosh t-1$.
background
Module MeasureForcing closes T9: after T0–T8 force the shape of the law (unique cost $J$, scale $\varphi$, eight-tick period, $D=3$), one still needs the weighting on recognition states. The forced rule is the geometric $\varphi$-measure, equivalently a Gibbs weight $\propto\exp(-(\ln\varphi)\cdot\mathrm{cost})$.
The cost $J$ is the unique RS cost from T5: $J(x)=(x+x^{-1})/2-1$, so along the exponential chart $x=e^{t}$ one has $J(e^{t})=\cosh t-1$. Sub-Gaussian control of the forced measure in the $J$-coordinate therefore reduces to comparing $\cosh t-1$ with the quadratic $t^{2}/2$.
The nonnegative half of the comparison is already proved as a private lemma in this module (via $\sinh$ self-bounds and the double-angle identity for $\cosh$). The present theorem removes the sign restriction.
proof idea
Case on $t\ge 0$ versus $t<0$.
If $t\ge 0$, apply the private lemma half_sq_le_cosh_sub_one_of_nonneg directly.
If $t<0$, instantiate that same lemma at $-t\ge 0$, rewrite with $\cosh(-t)=\cosh t$, and transport the left-hand side by $t^{2}=(-t)^{2}$ (ring). The two cases cover $\mathbb{R}$.
why it matters
Immediate consumer is sub_gaussian_in_J: the forced measure at rate $\lambda\ge 0$ satisfies $\exp(-\lambda,J(e^{t}))\le\exp(-\lambda t^{2}/2)$. That theorem rewrites $J(e^{t})$ as $\cosh t-1$, then feeds this inequality into monotonicity of $\exp$.
In the T9 story this is the L² seed: once the continuum weight is Gibbs in $J$, the quadratic lower bound on $\cosh t-1$ gives Gaussian domination in log-deviation, which underwrites concentration and tail estimates for rung occupancy, Born-type projections, and related instance-selection problems listed in the module header. It does not itself force the measure; it converts the already-forced $J$-Gibbs form into a usable analytic bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.