zero_not_crossEq_mul_recip_pair_of_not_crossEq_zero
plain-language theorem explainer
If two rational orbits are nonzero under cross-equality, the product of their reciprocals is likewise nonzero. Authors of the integer-order certificate cite this when sealing the signed-orbit order surface. The proof is a one-line transfer of the product-nonzero lemma through the reciprocal-nonzero equivalence.
Claim. For rational orbits $a$ and $b$, if $a$ is not cross-equal to zero and $b$ is not cross-equal to zero, then zero is not cross-equal to $\mathrm{recip}(a)\cdot\mathrm{recip}(b)$.
background
In the Primitive Recognition Calculus, a rational orbit is an integer numerator over a nonzero distinction-nat denominator (K4.7). Cross-equality is the internal rational relation: two orbits match when the scaled numerators balance under cross-multiplication of denominators (K4.10), i.e. the PRC stand-in for ordinary rational equality on $\delta$-orbit positions.
The total reciprocal on rational orbits sends the zero orbit to itself and otherwise swaps numerator and denominator (K4.12), mirroring the dual-recognition involution $\iota(x)=x^{-1}$ on the positive reals. The local module builds the signed-orbit order surface from these displays: nonnegativity flags, truncated subtraction, and absolute difference, all stated entirely in orbit language rather than classical $\mathbb{Z}$ or $\mathbb{Q}$.
Upstream, nonzeroness is preserved by reciprocal ($\neg\mathrm{crossEq}(\mathrm{recip},a,0)\leftrightarrow\neg\mathrm{crossEq}(a,0)$), and the product of two nonzero orbits is nonzero. Those two facts are the only inputs needed here.
proof idea
One-line term proof. Apply the product-nonzero lemma to the pair $(\mathrm{recip},a,\mathrm{recip},b)$. Discharge the two nonzeroness hypotheses by the right-to-left direction of the reciprocal-nonzero equivalence on $a$ and on $b$. No further case splits or arithmetic.
why it matters
Feeds the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and signed nonnegativity flags; product-of-reciprocals nonzeroness is one of the algebraic hygiene facts required so that order comparisons never collapse a nonzero reciprocal product onto zero.
Within Recognition Science this sits in the foundation layer that reconstructs rational arithmetic from distinction orbits before the forcing chain (T5 J-uniqueness through T8 dimension) is applied. It does not itself force $\phi$ or the eight-tick octave; it keeps the rational display consistent so later cost and ladder constructions can quote a closed order surface without classical $\mathbb{Q}$ axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.