reciprocalInvolution_never_reaches
plain-language theorem explainer
From any nonzero strain coordinate, iterates of the reciprocal involution never converge to the zero-strain carrier; the orbit oscillates forever. Gravity and C2-bridge authors cite this as the structural counterexample showing the recognition kernel fixes cost but not motion. The proof is a short limit argument: even iterates are the identity, so any convergent subsequence would force the seed strain to vanish.
Claim. Let $t_0 \in \mathbb{R}$ with $t_0 \neq 0$. Write $R$ for the reciprocal involution on strain space ($t \mapsto -t$). Then the sequence $k \mapsto R^{\circ k}(t_0)$ does not tend to $\operatorname{arsinh}(0)$ as $k \to \infty$.
background
This module asks how far the recognition kernel reaches: it fixes the cost of a configuration, not how configurations move. The kernel's cost content is the five-premise package that forces the cost functional to be $J$ (reciprocity, normalization, the recognition composition law, unit log-curvature calibration, and continuity on positive ratios). None of those premises quantifies over a dynamical map on the ratio ledger.
The reciprocal involution is the ledger's own map $x \mapsto 1/x$, which in the strain coordinate is $t \mapsto -t$. Its invariance is exactly the reciprocity premise that selects $J$. Sibling results record that the map is continuous and preserves bare recognition cost at every point. The carrier (least-cost state) sits at strain zero, equivalently $\operatorname{arsinh}(0)$.
The local question is whether continuous cost-lowering dynamics toward that carrier is forced by the kernel. The involution is the canonical test motion: it obeys everything the kernel says about cost, yet never settles.
proof idea
Argue by contradiction. Assume the orbit of $t_0$ under the involution tends to $\operatorname{arsinh}(0)$. Rewrite the limit point as $0$. The even-index map $k \mapsto 2k$ tends to infinity at infinity, so the even subsequence also tends to $0$. The even-iterate identity (reciprocalInvolution_iterate_even) collapses that subsequence to the constant sequence $t_0$. Uniqueness of limits in $\mathbb{R}$ forces $t_0 = 0$, contradicting the hypothesis. Hence no such convergent orbit exists.
why it matters
This is the dynamical half of the module's "reach wall": the kernel fixes cost, not motion. Together with cost preservation under the same involution, it feeds the sibling claim that kernel cost content does not entail cost-spending dynamics, and thereby justifies naming an explicit cost-spending substrate postulate for the C2 bridge rather than deriving descent from the kernel alone.
In the broader Recognition framework the result is structural, not accidental. Reciprocity (the $J$-automorphism $x \mapsto 1/x$) is already forced by the T5 uniqueness of $J$ and the recognition composition law; the same map, read as a flow on strain, is continuous, cost-preserving, and non-convergent away from the carrier. So the residue that stationarity and strict cost descent demand is independent of what the kernel says about single-ratio cost. Downstream the module packages that residue as a named postulate rather than a theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.