recip_respects_cross
plain-language theorem explainer
Cross-equality of ratio orbits is preserved by taking reciprocals (zero maps to zero). Anyone constructing the total reciprocal on the ratio-orbit display cites this lemma. The proof never opens classical rationals: it rewrites to integer cross-multiplication, then cases on zero numerators and matching sign flags, finishing by linear combination or contradiction on sign mismatch.
Claim. Let $a,b$ be ratio orbits (signed-orbit numerator over a nonzero distinction-nat denominator). If they are cross-equal, i.e. the integer products of numerator with the other denominator agree, then the reciprocals of $a$ and $b$ are likewise cross-equal.
background
In the primitive recognition calculus, rationals are not imported from classical $\mathbb{Q}$. A ratio orbit packages a signed orbit numerator with a nonzero distinction-nat denominator (K4.7). Equality of two such displays is the cross-multiplication relation: the integer images satisfy $n_a d_b = n_b d_a$, not a quotient construction.
The reciprocal of a ratio orbit is total in the style of $\mathbb{Q}$: a zero numerator is sent to the zero ratio orbit; otherwise numerator and denominator swap after taking absolute value and restoring sign (K4.12). Signed-orbit balance against zero detects the zero numerator without classical cancellation.
The module builds integer and rational arithmetic from recognition orbits and orbit arithmetic, staying choice-free by routing identities through the integer cross-multiplication hub rather than a classical rational display.
proof idea
Rewrite the hypothesis via the integer cross-equality characterization. Denominators are strictly positive as integers (from the nonzero-denominator invariant).
Case on whether $a$'s numerator is balanced with signed zero. If so, cross-equality forces $b$'s numerator to zero as well; both reciprocals collapse to the zero ratio orbit, and reflexivity closes the goal.
If not, $b$'s numerator is likewise nonzero. Unfold the nonzero branch of reciprocal and return to integer cross-equality. Subcases on the nonneg flags: matching positive signs reduce the swapped cross identity to a linear combination of the hypothesis (absolute values recover the original integers). Opposite signs yield an immediate positivity contradiction against the cross product. The remaining sign patterns are symmetric.
why it matters
This private lemma is the well-definedness engine for the total reciprocal on ratio orbits (K4.12): without it, recip would not respect the cross-equality that stands in for rational equality. Downstream, that reciprocal is the orbit-level stand-in for the reciprocal automorphism used elsewhere in the cost algebra.
In the Recognition foundation stack, integers and rationals are forced from distinction and orbit structure before continuum or measure structure appears. Preserving cross-equality under reciprocal is a necessary algebraic checkpoint on that path: it keeps the rational display closed under inversion while remaining choice-free and independent of classical $\mathbb{Q}$.
The result sits inside the primitive recognition calculus layer that underwrites later forcing-chain arithmetic (phi-ladder bookkeeping, eight-tick counting), even though it does not itself mention $J$, $\varphi$, or T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.