one_crossEq_recip_one
plain-language theorem explainer
The unit ratio orbit is cross-equivalent to its reciprocal: one and recip(one) agree under internal cross-multiplication. Anyone assembling the signed-orbit order surface or rational displays in Primitive Recognition Calculus cites this. The proof is a one-line symmetry wrapper on the already-proved reverse direction.
Claim. If $1$ denotes the unit ratio orbit and $\mathrm{recip}$ its total reciprocal (sending zero to zero), then $1$ is cross-equivalent to $\mathrm{recip}(1)$: the scaled numerator–denominator products balance as signed orbits.
background
In Primitive Recognition Calculus, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator. Cross-equivalence is the internal rational relation: two ratio orbits $a,b$ satisfy crossEq when $a.\mathrm{num}$ scaled by $b.\mathrm{den}$ balances $b.\mathrm{num}$ scaled by $a.\mathrm{den}$ as signed orbits (K4.10). This is equality of rationals, stated entirely on $\delta$-orbit positions.
The reciprocal on ratio orbits is total: balanced-to-zero numerators map to zero, otherwise numerator and denominator swap in the nonzero case (K4.12). The dual-recognition reciprocal on positive reals is the same involution $\iota(x)=x^{-1}$ used in Universal Forcing.
The reverse fact already holds: $\mathrm{recip}(1)$ is cross-equivalent to $1$, proved by reducing both sides to rational displays and a numeric check. Symmetry of crossEq then flips the order.
proof idea
One-line wrapper. Apply crossEq_symm to the prior theorem recip_one_crossEq_one, which states the opposite orientation. Symmetry itself unfolds crossEq and invokes signed-orbit balance symmetry, so no further arithmetic is needed here.
why it matters
Feeds integer_order_certificate, which closes the internal signed-orbit order surface (truncated subtraction, $\le$ display, absolute difference, nonnegativity flags). Having both orientations of $1\sim\mathrm{recip}(1)$ keeps the unit fixed under the reciprocal involution inside the rational display layer, so order and sign flags on ratio orbits stay consistent with the dual-recognition symmetry the framework is built on.
This is bookkeeping inside the foundation stack rather than a forcing-chain landmark (T5–T8), but the reciprocal generator and cross-equivalence are the discrete substrate on which J-cost comparisons and later ladder arithmetic sit. Without unit–reciprocal agreement, the order certificate could not treat the identity ratio as self-dual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.