strainStepVecOrbit
plain-language theorem explainer
Defines the discrete orbit of the componentwise strain step on an n-channel link: start from strain vector t and iterate the per-channel gradient step with source strength c. Convergence theorems cite this sequence as the dynamical object whose components each tend to arsinh(c/n). The body is plain recursion on ℕ, applying the vector step at each successor.
Claim. For $n\in\mathbb{N}$, source parameter $c\in\mathbb{R}$, and initial strain $t:\{0,\ldots,n-1\}\to\mathbb{R}$, the strain-step orbit is the sequence $t^{(k)}$ in $\mathbb{R}^n$ with $t^{(0)}=t$ and $t^{(k+1)}=S_{n,c}(t^{(k)})$, where $S_{n,c}$ applies the one-dimensional strain step with parameter $a=c/n$ independently on each channel.
background
This module builds a convergent least-cost flow on hinge-link strain space. The C2 bridge needs the substrate to attain the sourced least-cost carrier on each link; the canonical tick update cannot supply that premise (it is eventually 8-periodic). The sourced action on a link splits per channel as $\Phi_c(t)=\sum_i(\cosh t_i-1)-(c/n)\sum_i t_i$. Each channel has cost $\psi_a(s)=\cosh s-1-a s$ with $a=c/n$, strictly convex, unique minimizer $s^*=\mathrm{arsinh},a$.
The scalar step uses residual $g=\sinh s-a$ and a self-tuned envelope step size $\eta=E^{-1}$ so that a Lyapunov decrease and a contraction bound hold together. The vector step strainStepVec applies that scalar step channelwise: $(S_{n,c}t)_i=\mathrm{step}_1(c/n,t_i)$. The present definition iterates that map from an arbitrary initial $t$.
proof idea
Definition by recursion on the step index, not a proved theorem. Base case $k=0$ returns the initial strain vector $t$. Successor case applies the componentwise strain step strainStepVec n c to the previous orbit value. No lemmas are invoked in the body; downstream results prove by induction that the $i$-th component equals the scalar orbit with parameter $c/n$.
why it matters
This is the dynamical object for the multi-channel strain descent that replaces the blocked tick-update route to stationarity adoption. Downstream, strainStepVecOrbit_apply identifies each component with the scalar orbit, and strainStepVec_tendsto_minimizer concludes that every channel tends to $\mathrm{arsinh}(c/n)$ as $k\to\infty$. That channelwise convergence is the existence half of sourced least-cost attainment on the link, feeding the C2 bridge premise the eight-tick wall cannot carry. In the broader RS gravity stack it sits under the SevenGaps strain analysis that supports hinge-aware Regge/TT structure, not under the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.