strainStepVecOrbit_apply
plain-language theorem explainer
Componentwise evaluation of the vector strain orbit equals the scalar strain orbit on that channel with step parameter a = c/n. Anyone proving per-channel convergence of the multi-channel descent cites this identity. The proof is induction on the iterate index, with the successor step a rewrite by the inductive hypothesis.
Claim. For every dimension $n\in\mathbb{N}$, source strength $c\in\mathbb{R}$, initial strain vector $t:\mathrm{Fin}\,n\to\mathbb{R}$, iterate index $k\in\mathbb{N}$, and channel $i$, the $i$-th component of the vector strain orbit after $k$ steps equals the scalar strain orbit of the $i$-th initial value under the one-dimensional step with parameter $a=c/n$.
background
The module builds a convergent least-cost flow on link strain, needed because the C2 bridge's stationarity-adoption premise cannot be carried by the canonical tick update (that update is eventually 8-periodic on its image). 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$, so each channel has cost $\psi_a(s)=\cosh s-1-a s$ with $a=c/n$, unique minimizer $s^*=\mathrm{arsinh},a$.
The scalar dynamics is the self-tuned gradient step strainStep1 with residual $g=\sinh s-a$ and envelope-derived step size $\eta$. The scalar orbit strainOrbit a s₀ iterates that step from $s₀$. The vector orbit applies the same step componentwise to an $n$-tuple of strains. This lemma identifies the two views channel by channel.
proof idea
Induction on the iterate index $k$. At $k=0$ both sides are the initial component $t_i$, so reflexivity. In the successor case both sides apply the same one-dimensional step strainStep1 (c/n) to the previous iterate; the inductive hypothesis rewrites the vector-orbit component into the scalar orbit, and the goals match.
why it matters
Feeds directly into strainStepVec_tendsto_minimizer, whose doc-comment states each channel converges to the minimizer: that theorem rewrites the vector-orbit component as the scalar orbit via this identity, then invokes scalar geometric convergence to $\mathrm{arsinh}(c/n)$. Without the componentwise reduction, multi-channel descent would not inherit the one-dimensional Lyapunov and contraction bounds already proved for $\psi_a$.
In the broader Recognition picture this closes the existence half of stationarity adoption on each hinge link: the substrate can attain the sourced least-cost carrier by a convergent strain flow rather than by the blocked eight-tick update. It sits inside the Gravity/SevenGaps strain-descent wall that supports the C2 bridge, not inside the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.