strainEnvelope_continuous
plain-language theorem explainer
For each fixed source load $a$, the strain envelope map on hinge strain is continuous. Anyone assembling continuous self-tuned step sizes or banked gradient steps in the SevenGaps descent pipeline cites this. The proof unfolds the max-of-two-bounds definition, imports residual continuity, and closes by the standard continuous-function calculus.
Claim. For every real source parameter $a$, the strain envelope $E_a:\mathbb{R}\to\mathbb{R}$ is continuous, where $E_a(s)$ is the pointwise maximum of the Lyapunov assembly bound $2\bigl(\cosh s/2+|\sinh s|\,|r_a(s)|/6\bigr)\cosh|r_a(s)|$ and the contraction bound $\cosh(|s|+|r_a(s)|)$, with $r_a$ the strain residual.
background
This module studies the descent principle for sourced hinge strain: the carrier follows steepest descent of total recognition cost, but "steepest" is metric-relative. The main theorem shows that any continuous strictly cost-decreasing map on strain space converges to the least-cost point $t^*=\mathrm{arsinh},a$, so the metric choice cannot matter.
The strain envelope is the larger of two explicit positive bounds built from $\cosh$, $\sinh$, and the residual $r_a(s)$: one bound feeds the Lyapunov assembly, the other the contraction estimate. The residual itself is continuous in strain for each fixed $a$ (proved by unfolding and fun_prop). Continuity of the envelope is the next link before the reciprocal step size can be shown continuous.
proof idea
Unfold the envelope definition (a pointwise max of compositions of continuous elementary functions of $s$ and of the residual). Invoke residual continuity at the same $a$. Close with fun_prop, which discharges continuity of absolute value, multiplication, division by constants, cosh, and max.
why it matters
Feeds strainStepSize_continuous: the self-tuned step size is the reciprocal of the envelope, so envelope continuity plus strict positivity yields a continuous positive step map, and thence continuity of the banked gradient step. That continuity is load-bearing in the module's universality argument: without it, one can build strictly cost-decreasing maps that abandon the least-cost rest state and oscillate forever. The result sits inside the gravity SevenGaps descent stack that reduces C2 stationarity to a single dynamical principle (cost-decreasing continuous dynamics on strain).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.