strainStepSize_continuous
plain-language theorem explainer
For each fixed source amplitude, the self-tuned strain step size (reciprocal of the strain envelope) is a continuous function of the strain coordinate. Anyone proving continuity of the banked gradient step, or feeding the metric-free descent universality theorem, cites this. The proof unfolds the reciprocal definition and applies reciprocal-continuity to a strictly positive continuous envelope.
Claim. For every real source amplitude $a$, the map $s \mapsto \bigl(\mathrm{Env}_a(s)\bigr)^{-1}$ is continuous on $\mathbb{R}$, where $\mathrm{Env}_a$ denotes the strain envelope at amplitude $a$.
background
This module studies the descent principle for hinge-link strain: carrier dynamics is steepest descent of total recognition cost, but "steepest" is metric-relative. The main claim is that any continuous strictly cost-decreasing map on strain space still converges to the sourced least-cost point $t^*=\mathrm{arsinh},a$, so the metric choice cannot matter.
In the concrete banked gradient flow from StrainDescent, the self-tuned step size is the reciprocal of the strain envelope: $\eta_a(s)=(\mathrm{Env}_a(s))^{-1}$. The envelope is built from the residual of the sourced cost and is known to be at least one, hence strictly positive (strainEnvelope_pos). Continuity of the envelope itself is already established in this file (strainEnvelope_continuous).
Continuity of $\eta_a$ is the remaining scalar ingredient before the full one-step map $s\mapsto s-\eta_a(s),g_a(s)$ can be shown continuous.
proof idea
Term-mode, two steps. Unfold the definition of the step size to the pointwise reciprocal of the envelope. Apply Mathlib's Continuous.inv₀ to the already-proved continuity of the envelope at amplitude $a$, discharging the nowhere-zero side condition with the strict positivity lemma strainEnvelope_pos (via .ne'). No further analysis is required.
why it matters
This lemma is the continuity half of the banked gradient step. Its sole direct consumer is strainStep1_continuous, which assembles identity, this step-size map, and residual continuity into continuity of one full descent update. That continuity is exactly the hypothesis the module's main universality theorem needs: every continuous strictly cost-decreasing dynamics converges to the least-cost strain, with no metric, no fixed step size, and no convexity of the update. In the broader SevenGaps gravity stack, this closes the analytic gap between the constructive banked flow and the metric-free Lyapunov argument that reduces C2 stationarity to pure descent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.