integral_sq_half_third
plain-language theorem explainer
The definite integral of t ↦ t²/2 from 0 to any real x equals x³/6. Strain-descent and hyperbolic remainder estimates cite it as the elementary FTC identity behind the cubic Taylor gap for sinh. The proof is a direct fundamental-theorem application: differentiate t³/6 and integrate back on the interval.
Claim. For every real number $x$, $\int_0^x \frac{t^2}{2}\,dt = \frac{x^3}{6}$.
background
The StrainDescent module builds a convergent least-cost flow on link strain so the C2 bridge can adopt a sourced stationary carrier. Per-channel cost is $\psi_a(s)=\cosh s-1-a s$, with residual $g=\sinh s-a$ and a self-tuned gradient step whose Lyapunov and contraction bounds need sharp scalar inequalities for $\cosh$ and $\sinh$.
Those inequalities are obtained from single integrals plus monotonicity of $\cosh$ on $\mathbb{R}_{\ge 0}$. The first bound is $\cosh x-1\le(x^2/2)\cosh x$; the second is $|\sinh x-x|\le(|x|^3/6)\cosh x$. Both rest on elementary antiderivatives of polynomials and of $\cosh t-1$.
This declaration records the pure polynomial identity $\int_0^x t^2/2,dt=x^3/6$, the cubic building block for the sinh remainder.
proof idea
Term-mode FTC. Apply intervalIntegral.integral_eq_sub_of_hasDerivAt with antiderivative $f(t)=t^3/6$ and derivative $f'(t)=t^2/2$ on $[0,x]$. The derivative obligation is discharged by the chain (hasDerivAt_id t).pow 3 then div_const 6, converted by ring. Integrability of the continuous integrand $t\mapsto t^2/2$ is immediate. The resulting evaluation $f(x)-f(0)$ simplifies to $x^3/6$.
why it matters
Feeds directly into abs_sinh_sub_self_le_sixth, the second scalar bound $|\sinh x-x|\le(|x|^3/6)\cosh x$. That bound, together with the companion $\cosh x-1\le(x^2/2)\cosh x$, supplies the envelope constants used to choose the step size $\eta=E^{-1}$ so that one-dimensional descent decreases the Lyapunov $\psi$ by at least $(\eta/2)g^2$ and contracts off the stationary point $s^*=\mathrm{arsinh},a$.
Those one-dimensional facts assemble into the multi-channel strain descent that replaces the blocked tick-update wall and discharges the existence half of stationarity adoption on each hinge link. The identity itself is classical calculus; its place in the framework is as a zero-sorry brick under the gravity SevenGaps strain flow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.