recip_recip_crossEq_self
plain-language theorem explainer
Double reciprocal returns every ratio orbit to itself up to cross-multiplication equivalence. Anyone assembling the PRC rational field or order surface cites this involution fact. The proof bridges to ordinary rationals via the toRat display, applies reciprocal twice, and simplifies.
Claim. For every ratio orbit $a$ (signed-orbit numerator over a nonzero distinction-nat denominator), the double reciprocal satisfies $\mathrm{crossEq}(\mathrm{recip}(\mathrm{recip}(a)), a)$: cross-multiplication balances the two sides, equivalently their verifier rationals agree.
background
In the Primitive Recognition Calculus integer layer, a ratio orbit packages a signed-orbit numerator with a nonzero distinction-nat denominator. Cross-equivalence is the internal rational relation: two orbits match when the scaled products of numerator and opposite denominator balance as signed orbits (K4.10). That relation is proved equivalent to equality of the ordinary rational displays toRat.
Reciprocal on ratio orbits is total and mirrors $\mathbb{Q}$: zero maps to zero; otherwise numerator and denominator swap in the nonzero branch. The companion lemma recip_toRat states that the display of a reciprocal is the field inverse of the original display. Upstream, the same reciprocal idea appears as the dual-recognition involution $\iota(x)=x^{-1}$ on positive reals in the universal forcing stack.
This module builds the signed-orbit order surface on those displays; involution of reciprocal under cross-equivalence is a basic algebraic identity needed before order and certificate packing.
proof idea
Short tactic proof. Rewrite the goal with the bridge crossEq_iff_toRat_eq, so the claim becomes equality of rationals. Apply recip_toRat twice to replace each double-reciprocal display by a double field inverse. simp finishes, using that inversion on $\mathbb{Q}$ is an involution (including the zero case already handled by the total reciprocal).
why it matters
Closes the involution half of reciprocal under the PRC rational relation. Downstream, self_crossEq_recip_recip is the symmetric orientation obtained by crossEq_symm, and recip_crossEq_iff uses the involution to show reciprocal preserves and reflects cross-equivalence. Both feed the packed integer_order_certificate, whose doc states the internal signed-orbit order surface is closed.
In the broader Recognition stack this is bookkeeping for the dual-recognition symmetry (reciprocal generator $\iota$), not a forcing-chain step itself. It keeps the integer/rational layer coherent so later cost uniqueness and J-calculus can treat ratio orbits as a field-like display without leaving the $\delta$-orbit vocabulary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.