one_crossEq_mul_recip_of_not_crossEq_zero
plain-language theorem explainer
For any nonzero ratio orbit a, the unit orbit is cross-equivalent to a times its reciprocal. Order and field-structure work in the Primitive Recognition Calculus cites this when the inverse identity is needed oriented as 1 ~ a·a⁻¹ rather than a·a⁻¹ ~ 1. The proof is a one-line symmetry flip of the reverse-orientation lemma.
Claim. If $a$ is a ratio orbit not cross-equivalent to zero, then the unit ratio orbit is cross-equivalent to the product of $a$ with its reciprocal: $1 \sim a \cdot a^{-1}$.
background
Ratio orbits are the internal PRC display of rationals: a signed-orbit numerator over a nonzero distinction-nat denominator (K4.7). Cross-equivalence is the native rational equality: two ratio orbits match when the cross-scaled numerator-denominator products balance as signed orbits, defined entirely on δ-orbit positions (K4.10).
The reciprocal on ratio orbits is total and sends zero to zero, matching the convention on ℚ (K4.12). Its continuum counterpart is the dual-recognition involution ι(x) = x⁻¹ on the positive reals. This module assembles the integer order surface on those orbit displays.
The upstream result already proves a · recip(a) ~ 1 for nonzero a. The present statement is the swapped orientation of that same identity.
proof idea
One-line term proof. Apply cross-equivalence symmetry to the conclusion of the upstream lemma that a · recip(a) is cross-equivalent to one (under the nonzero hypothesis). Because signed-orbit balance is symmetric, swapping the two sides yields one cross-equivalent to a · recip(a).
why it matters
Used by the integer-order certificate, which asserts that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, order flags, absolute difference, and signed nonnegativity. Both orientations of the multiplicative inverse identity keep rational field steps available without manual symmetry when assembling order and arithmetic certificates in the PRC foundation.
In the Recognition Science stack this lives in the pre-physics arithmetic layer that underwrites later forcing-chain uniqueness (J-cost, φ, eight-tick octave, D = 3). It is a small orientation lemma needed for a closed integer-order surface, not a physics claim on its own.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.