self_crossEq_recip_recip
plain-language theorem explainer
Any ratio orbit is cross-equivalent to the double reciprocal of itself: applying reciprocal twice returns an orbit in the same rational class. Order and rational-structure proofs in the primitive recognition calculus cite this to treat double reciprocal as identity up to cross-multiplication. The proof is a one-line symmetry flip of the companion double-reciprocal lemma.
Claim. For every ratio orbit $a$ (signed-orbit numerator over a nonzero distinction-nat denominator), $a$ is cross-equivalent to $\mathrm{recip}(\mathrm{recip}(a))$: the two orbits agree under the internal cross-multiplication relation on $\delta$-orbit positions.
background
In the primitive recognition calculus, a ratio orbit packages a signed orbit numerator with a nonzero distinction-nat denominator. Cross-equivalence is the internal rational equality: two ratio orbits $a,b$ satisfy it when the scaled products $a.num\cdot b.den$ and $b.num\cdot a.den$ are balanced as signed orbits (K4.10). It is the PRC stand-in for ordinary rational equality, defined entirely on $\delta$-orbit positions rather than on $\mathbb{Q}$.
Reciprocal on ratio orbits is total: zero maps to zero, and nonzero orbits invert numerator and denominator in the usual way (K4.12). The companion lemma already shows that double reciprocal is cross-equivalent back to the original orbit in the opposite order. Symmetry of cross-equivalence (inherited from balance symmetry of signed orbits) is the only extra ingredient needed here.
The local module builds the integer order surface on these orbit displays: flags, truncated subtraction, and comparison predicates that must close under the rational operations.
proof idea
One-line wrapper. Apply symmetry of cross-equivalence to the companion theorem that already proves $\mathrm{crossEq}(\mathrm{recip}(\mathrm{recip}(a)), a)$. That companion reduces via the display equality $\mathrm{crossEq}\Leftrightarrow$ equal rational images, then rewrites both reciprocal displays and simplifies. No new arithmetic is done here.
why it matters
Feeds the integer-order certificate, which asserts that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags). Double-reciprocal identity up to cross-equivalence is part of making reciprocal a well-behaved involution on the rational orbit layer, so order and comparison proofs can move freely past inversion.
In the broader Recognition stack this sits under the foundation forcing material that later yields the J-cost uniqueness (T5), the self-similar fixed point $\phi$ (T6), and the reciprocal generator $\iota(x)=x^{-1}$ as dual-recognition symmetry. Closing rational-orbit algebra is scaffolding for those later uniqueness and dimension results, not a physics claim by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.