step_fixed_iff_arsinh
plain-language theorem explainer
Fixed points of the one-dimensional strain descent step are exactly the sourced stationary point $s^*=\operatorname{arsinh} a$. Hinge-stationarity and convergence arguments in the gravity bridge cite this to identify equilibria of the flow. Both directions are elementary: a fixed step forces the residual to vanish (step size is strictly positive), and at $\operatorname{arsinh} a$ the residual is zero so the step is the identity.
Claim. For all real $a$ and $s$, writing $g=\sinh s-a$ and $\eta$ for the reciprocal envelope step size, the update $s'=s-\eta\,g$ satisfies $s'=s$ if and only if $s=\operatorname{arsinh} a$.
background
This module builds a convergent least-cost flow on link strain space. The C2 bridge needs the substrate to attain the sourced least-cost carrier on each hinge link; the canonical tick update cannot supply that premise (it is eventually 8-periodic). The per-channel cost is $\psi_a(s)=\cosh s-1-a\cdot s$, strictly convex with unique critical point $s^*=\operatorname{arsinh} a$.
The residual (gradient) is $g=\sinh s-a$. The self-tuned step size $\eta$ is the reciprocal of an envelope $E$ large enough for both the Lyapunov and contraction bounds. One descent step is $s'=s-\eta,g$. The theorem characterizes when that map is stationary.
Upstream facts used here: positivity of the step size, and the residual definition. The zero-product fact applied in the proof is the ordinary real fact that a product vanishing forces a factor to vanish (the named dependency is the LogicInt form of the same principle).
proof idea
Bidirectional constructor.
Forward: assume $s'=s$. Unfolding the step gives $\eta\cdot g=0$. Since $\eta>0$ (strainStepSize_pos), the residual $g$ vanishes, so $\sinh s=a$. Rewrite via $\sinh(\operatorname{arsinh} a)=a$ and apply injectivity of $\sinh$.
Reverse: substitute $s=\operatorname{arsinh} a$, unfold step and residual, use $\sinh(\operatorname{arsinh} a)=a$, and simplify to the identity.
why it matters
Closes the fixed-point half of the one-dimensional descent package stated in the module doc (paired with strict Lyapunov decrease off stationarity). Downstream, the vector fixed-point theorem reduces componentwise to this scalar statement, identifying fixed points of the multi-channel step with the sourced minimizer. Universality of cost-decreasing dynamics uses the reverse direction to seed the unique limit $\operatorname{arsinh} a$. The cost-spending substrate inhabitation theorem uses the same residual-vanishing logic to show the banked gradient step is a legitimate substrate, so adopting it is consistent.
In the broader RS gravity bridge this supplies the existence half of stationarity adoption on each hinge link: the dynamics actually reaches the sourced least-cost carrier rather than merely descending a formal Lyapunov function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.