self_crossEq_recip_recipNonzero
plain-language theorem explainer
Double reciprocal returns a nonzero ratio orbit to itself under cross-multiplication equivalence. Anyone assembling the PRC rational order, or checking that reciprocal is an involution on nonzero orbits, would cite this. The proof is a one-line symmetry flip of the reverse-direction lemma.
Claim. Let $a$ be a ratio orbit whose numerator is not balanced against the zero signed orbit. Then $a$ is cross-equivalent to the reciprocal of its reciprocal (the inner reciprocal taken under the nonzero-numerator hypothesis).
background
In the Primitive Recognition Calculus, integers are signed orbits and rationals are ratio orbits: a numerator signed orbit over a nonzero distinction-nat denominator. Two signed orbits are balanced when their positive and negative lengths match by swap, $a.pos + b.neg = b.pos + a.neg$. That is the internal integer equality.
Two ratio orbits are related by cross-equivalence when the scaled products of numerator and denominator balance as signed orbits. The module doc and K4.10 pin this as the internal PRC rational relation, defined entirely on $\delta$-orbit positions, and it agrees with ordinary rational equality of the verifier displays.
Reciprocal on a nonzero ratio orbit swaps and inverts the display in the orbit language. The companion lemma already shows that applying reciprocal twice lands back on $a$ up to cross-equivalence in one order; the present statement is the opposite order.
proof idea
One-line term proof. Apply symmetry of cross-equivalence (crossEq_symm, which reduces to symmetry of signed-orbit balance) to the reverse-direction result recip_recipNonzero_crossEq_self. That companion lemma rewrites through the toRat display and the reciprocal/recipNonzero display lemmas to get equality of rationals, hence cross-equivalence. No new arithmetic is done here.
why it matters
Closes the involution half of reciprocal on nonzero ratio orbits inside the integer-order layer. Downstream it is consumed by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed: the certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags.
In the Recognition foundation this sits under the Primitive Recognition Calculus that feeds the forcing chain (ledger balance, J-cost uniqueness, and the later T5–T8 landmarks). Without double-reciprocal recovery, the rational order surface would not be algebraically closed under inversion, and the certificate could not honestly claim closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.