recip_crossEq_iff
plain-language theorem explainer
Reciprocals preserve and reflect cross-equivalence of ratio orbits: a ~ b if and only if 1/a ~ 1/b under the internal PRC cross-multiplication relation. Order and rational-structure proofs cite it when moving inequalities or equalities across inversion. The proof is a short biconditional: one direction is congruence of recip under crossEq; the other routes through double-reciprocal recovery and transitivity.
Claim. For ratio orbits $a,b$ (signed-orbit numerator over nonzero distinction-nat denominator), the cross-multiplication relation holds between $a$ and $b$ if and only if it holds between their reciprocals: $\mathrm{crossEq}(\mathrm{recip}\,a,\,\mathrm{recip}\,b)\leftrightarrow\mathrm{crossEq}(a,b)$.
background
In the Primitive Recognition Calculus, a ratio orbit is an internal rational display: a signed orbit numerator over a nonzero distinction-nat denominator (K4.7). Equality of such displays is not postulated as ℚ-equality; it is the cross-multiplication predicate crossEq (K4.10): $a$ and $b$ are related when $a.num$ scaled by $b.den$ balances $b.num$ scaled by $a.den$ as signed orbits. That relation is already known to be symmetric and transitive on ratio orbits.
Reciprocal swaps numerator and denominator (with the appropriate signed-orbit packaging) and is involutive up to crossEq: applying recip twice recovers the original orbit under cross-equivalence. Congruence of recip under crossEq is the one-way map: if $a\sim b$ then $\mathrm{recip},a\sim\mathrm{recip},b$. The present statement upgrades that to an iff, so inversion is an automorphism of the crossEq relation.
The ambient module builds the integer order surface on these δ-orbit rationals without classical choice on the ℚ bridge; crossEq and its algebraic lemmas are the choice-free backbone.
proof idea
Term-mode constructor on the biconditional.
Forward ($\mathrm{crossEq}(\mathrm{recip},a,\mathrm{recip},b)\Rightarrow\mathrm{crossEq}(a,b)$): apply recip_crossEq_congr to the hypothesis to get equivalence of double reciprocals, then chain with crossEq_trans and crossEq_symm against the two instances of recip_recip_crossEq_self (double recip recovers $a$ and $b$).
Reverse ($\mathrm{crossEq}(a,b)\Rightarrow\mathrm{crossEq}(\mathrm{recip},a,\mathrm{recip},b)$): one-line application of recip_crossEq_congr.
No display bridge or classical choice is used; only the already-proved congruence, involution-up-to-crossEq, and the equivalence-relation lemmas for crossEq.
why it matters
Inversion must be a relation automorphism before order and comparison lemmas on ratio orbits can move freely across reciprocal. Downstream, integer_order_certificate packages the closed internal signed-orbit order surface (truncated subtraction, ≤ display, abs-diff, nonneg flags). This iff is a small but necessary algebraic hinge in that certificate chain: without reflecting crossEq under recip, sign and order facts on inverted displays would not transport back to the original orbits.
In the broader Recognition stack this sits in Foundation PRC integer/rational scaffolding that underwrites later cost and forcing material (J-uniqueness, phi ladder). It does not itself touch T5–T8; it keeps the rational substrate choice-free and internally consistent so those later steps can quote orbit arithmetic without smuggling classical ℚ identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.