strainStep1_continuous
plain-language theorem explainer
For every source amplitude a, the banked one-dimensional gradient step on hinge strain is a continuous self-map of the reals. Anyone invoking the metric-free descent universality theorem for this concrete dynamics needs that continuity hypothesis. The proof is a short composition: the step is identity minus continuous step-size times continuous residual.
Claim. For every real source amplitude $a$, the banked gradient step map $S_a:\mathbb{R}\to\mathbb{R}$ (identity minus step size times strain residual) is continuous.
background
This module treats steepest descent of sourced recognition cost on a hinge link's strain coordinate as a family of maps, not a single metric-forced flow. The per-channel cost $\Phi_a$ has unique minimizer $t^=\mathrm{arsinh},a$. Any continuous self-map $S$ that strictly lowers $\Phi_a$ off $t^$ has every orbit converging to $t^*$, with no metric, step-size law, or convexity of $S$ required.
The banked gradient step is the concrete dynamics already studied in StrainDescent: it subtracts a positive step size times the strain residual from the current strain. Continuity of that map is load-bearing for the universality argument: without it, one can build a cost-spending map that never settles at the least-cost state.
Upstream, continuity of the residual and of the step-size factor are already proved (strainResidual_continuous, strainStepSize_continuous), typically by unfolding and fun_prop.
proof idea
Unfold the definition of the banked step. It is the pointwise difference of the identity map and the product of the step-size map with the residual map. Apply continuity of the identity, multiply the two continuous factors via the already-proved residual and step-size continuity lemmas, then subtract. The whole argument is a single exact term built from Mathlib continuity combinators.
why it matters
Continuity is one of the three hypotheses fed to the module's main Lyapunov theorem when specializing to the banked step. Downstream, strainStep1_converges_by_universality applies cost-decreasing dynamics convergence with this continuity fact, recovering the direct StrainDescent convergence as an instance of the metric-free principle. The same fact witnesses that a cost-spending substrate exists (costSpendingSubstrate_nonempty), so the dynamical postulate is inhabited rather than contradictory.
In the broader gravity stack this closes a gap between the reduced C2 stationarity premise (carrier follows steepest descent of recognition cost) and the claim that the metric on strain space need not be forced: any continuous cost-spending map, including the banked gradient step, converges to the sourced least-cost carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.