strainStepSize_pos
plain-language theorem explainer
The self-tuned strain descent step size η(a,s) is strictly positive for every real source weight a and strain s. Anyone citing the one-dimensional Lyapunov decrease, contraction, or fixed-point characterization needs this positivity. The proof is a one-line reciprocal of the already-proved envelope positivity.
Claim. For all real $a$ and $s$, the self-tuned step size $\eta(a,s) := E(a,s)^{-1}$ satisfies $0 < \eta(a,s)$, where $E(a,s)$ is the strain envelope used to control the gradient step on the per-channel cost $\psi_a(s) = \cosh s - 1 - a\cdot s$.
background
This module builds a convergent least-cost flow on link strain space, needed because the canonical tick update cannot supply the C2 bridge's stationarity-adoption premise (it is eventually 8-periodic). The sourced action decomposes per channel as $\Phi_c(t) = \sum_i(\cosh t_i - 1) - (c/n)\sum_i t_i$, so the scalar cost is $\psi_a(s) = \cosh s - 1 - a\cdot s$ with residual $g = \sinh s - a$ and unique stationary point $s^* = \mathrm{arsinh}, a$.
The descent step is $s' = s - \eta\cdot g$ with self-tuned size $\eta = E^{-1}$. The envelope $E$ is the max of two explicit hyperbolic bounds chosen so Lyapunov decrease and contraction hold simultaneously. The definition strainStepSize is exactly that reciprocal; the sibling theorem strainEnvelope_pos already records $0 < E(a,s)$ via $E \ge 1$.
proof idea
One-line term proof. Unfold the definition $\eta = E^{-1}$, then apply Mathlib's inv_pos to the already-established strainEnvelope_pos a s (itself $E \ge 1 > 0$). No case splits or hyperbolic identities.
why it matters
Positivity of $\eta$ is the gate for every quantitative one-step estimate in the strain descent. Downstream it feeds: the contraction $|s' - s^| \le (1-\eta)|s-s^|$; the correction bound that keeps the Lyapunov remainder at most half the tangent term; the comparison $\cosh(\eta g) \le \cosh|g|$; strict decrease of $\psi_a$ off stationarity; the multi-channel sourced-action decrease; and the fixed-point characterization $s' = s \Leftrightarrow s = \mathrm{arsinh}, a$.
Together those close the existence half of stationarity adoption on each hinge link, the physical premise the eight-tick update cannot carry. The construction sits in the Gravity/SevenGaps layer that supplies the C2 bridge, not in the T0–T8 forcing chain itself, but it is the dynamics that makes the sourced least-cost carrier attainable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.