half_sq_le_cosh_sub_one_of_nonneg
plain-language theorem explainer
For every nonnegative real s, s squared over two is at most cosh(s) minus one. Continuum-layer arguments in the forced recognition measure cite this elementary hyperbolic bound when comparing quadratic cost to the J-cost shape cosh − 1. The proof reduces the claim to sinh(u) ≥ u via the double-angle identity for cosh, then closes by nonlinear arithmetic.
Claim. For every real number $s \geq 0$, one has $\frac{s^{2}}{2} \leq \cosh s - 1$.
background
Module T9 (MeasureForcing) closes the missing weighting rule on recognition states after the T0–T8 shape chain. Lattice premises force geometric weights $w(n)=\varphi^{-n}$; the continuum layer treats weight as a function of a real additive cost and needs elementary comparisons between that cost and the unique J-cost.
By T5, the unique cost is $J(x)=(x+x^{-1})/2-1$, equivalently $J(e^{s})=\cosh s-1$. The inequality $\frac{s^{2}}{2}\leq\cosh s-1$ is therefore a direct lower bound of J-cost by a pure quadratic, valid on the nonnegative ray.
The standard comparison $\sinh u\geq u$ for $u\geq 0$ (Mathlib Real.self_le_sinh_iff) is the only external analytic input; double-angle and the Pythagorean identity for hyperbolic functions convert it into the claimed cosh bound.
proof idea
From $s\geq 0$ obtain $s/2\geq 0$. Apply Real.self_le_sinh_iff to get $s/2\leq\sinh(s/2)$. Rewrite $\cosh s$ by the double-angle formula: $\cosh s=\cosh(2\cdot(s/2))=\cosh^{2}(s/2)+\sinh^{2}(s/2)$, then replace $\cosh^{2}$ by $\sinh^{2}+1$ and rearrange to $\cosh s=2\sinh^{2}(s/2)+1$. Nonlinear arithmetic on the two inequalities finishes: $\cosh s-1=2\sinh^{2}(s/2)\geq 2(s/2)^{2}=s^{2}/2$.
why it matters
Immediate parent is half_sq_le_cosh_sub_one, which drops the sign hypothesis by evenness of cosh and the same bound on $-t$. That full-line inequality is the continuum comparison between quadratic cost and $J(e^{t})=\cosh t-1$ inside T9 MeasureForcing.
T9 supplies the missing weighting primitive after T0–T8 forced the shape of the law (unique J, $\varphi$, eight-tick period, $D=3$). Every instance-selection problem listed in the module header (Born weights, chirality, $\delta w_{0}$, $\eta_{B}$, rung occupancy) projects onto this measure. The present lemma is pure analysis scaffolding for that continuum step; it does not itself force $\varphi$ or the Gibbs rate, but it licenses quadratic-versus-J comparisons once the cost variable is real.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.