reciprocalInvolution_iterate_even
plain-language theorem explainer
Even iterates of the reciprocal involution fix every real strain: applying t ↦ −t exactly 2k times returns the starting value. Gravity and C2-bridge arguments cite this to control the orbit of the ledger's canonical cost-preserving motion. The proof is induction on k, reducing to the two-step identity via iterate additivity.
Claim. For every real strain $t_0$ and every natural number $k$, the $2k$-fold iterate of the reciprocal involution (strain map $t \mapsto -t$) satisfies $\iota^{2k}(t_0) = t_0$.
background
This module asks how far the recognition kernel reaches into strain dynamics. The kernel's cost content is the premise package that forces the cost functional $J$ (reciprocity, normalization, the recognition composition law, unit log curvature, continuity on positive ratios). Those premises fix what a configuration costs; none constrain how configurations move.
The reciprocal involution is the ledger's own map $x \mapsto 1/x$, written in strain coordinates as $t \mapsto -t$. Reciprocity of $J$ is exactly invariance under this map, so the motion is continuous and preserves bare recognition cost. The present lemma records the elementary period-2 fact needed to describe its orbit: even iterates are the identity on every starting strain.
Local setting is the "reach wall": if the kernel forced cost-spending descent to the carrier, this canonical motion would be ruled out. It is not.
proof idea
Induction on $k$. The zero case is immediate (simp on the 0-fold iterate). In the successor step, rewrite $2(m+1) = 2m+2$ and split the iterate by Function.iterate_add_apply. The two-step block collapses by unfolding the definition: $\iota(\iota(t_0)) = -(-t_0) = t_0$. The inductive hypothesis then finishes. No external lemmas beyond iterate algebra and the definition of the involution.
why it matters
Feeds reciprocalInvolution_never_reaches, which states that from any nonzero strain the involution's orbit never reaches the carrier and oscillates forever. That non-convergence is the structural counterexample showing kernel cost content does not entail cost-spending dynamics (kernel_cost_content_does_not_entail_cost_spending).
In the Seven Gaps gravity stack this separates what the recognition kernel forces (the cost $J$, via the RCL and reciprocity) from the C2 bridge's stationarity/descent postulate, which must be named explicitly rather than derived from the kernel. The even-iterate identity is the algebraic hinge: along the subsequence of even times the orbit is constantly $t_0 \neq 0$, so it cannot tend to the zero-strain carrier. Framework landmark: reciprocity premise of $J$-uniqueness (T5), used here as a dynamical obstruction rather than a uniqueness input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.