recipNonzero_num_zero_cmp
plain-language theorem explainer
For a ratio orbit with nonzero numerator, comparing zero to the numerator of its nonzero reciprocal yields the same ordering as comparing zero to the original numerator. Order and ratio-arithmetic developers in the primitive recognition calculus cite this when closing signed comparison under inversion. The proof cases on the three-way comparison, kills the equal branch by the nonzero hypothesis, and transports the two strict branches through reciprocal numerator order iff lemmas.
Claim. Let $a$ be a ratio orbit whose numerator is not balanced with zero. Writing $a^{-1}$ for the nonzero reciprocal of $a$, the internal signed-orbit comparison satisfies $\mathrm{cmp}(0,\,\mathrm{num}(a^{-1}))=\mathrm{cmp}(0,\,\mathrm{num}(a))$.
background
In the primitive recognition calculus, signed orbits are the internal integer carriers. Two signed orbits are balanced when they represent the same value; the internal selector cmp returns equality exactly on the balanced case, and otherwise reads the nonnegativity flag of the difference to decide less-than or greater-than. Strict order on the underlying logic naturals is the usual successor witness ($n<m$ means $n+\mathrm{succ},k=m$ for some $k$).
Ratio orbits package a signed numerator and denominator. The nonzero reciprocal is the inversion map defined only when the numerator is not balanced with zero. The local module builds the full integer-order surface (reflexivity, totality, trichotomy, sign flags) from these primitives, without appealing to a verifier integer display.
Upstream comparison characterizations equate cmp outcomes with balanced equality and with the strict order in each direction, which is what lets a case split on cmp become a clean transport of inequalities.
proof idea
Term-mode proof by cases on $c=\mathrm{cmp}(0,\mathrm{num}(a))$.
- If $c=\mathrm{lt}$: convert via the lt characterization to $0<\mathrm{num}(a)$, push across the reciprocal by the nonzero-reciprocal numerator lt-iff, then reassemble
cmpwith the of-lt constructor. - If $c=\mathrm{eq}$: the eq characterization yields balanced zero and numerator; symmetry of balanced contradicts the nonzero hypothesis, so
False.elim. - If $c=\mathrm{gt}$: convert to $\mathrm{num}(a)<0$, transport by the reciprocal numerator lt-zero iff, and reassemble with the of-gt constructor.
why it matters
This lemma is a sign-preservation step under ratio inversion: the numerator's comparison against zero is invariant when passing to the nonzero reciprocal. Downstream it is applied by the wrapper that lifts the same identity to the total reciprocal (after rewriting recip to recipNonzero on the nonzero branch), and it contributes to the integer-order certificate that declares the internal signed-orbit order surface closed (display lemmas for truncated subtraction, absolute difference, nonnegativity flags, and related order facts).
In the Recognition Science foundation this sits under arithmetic-from-logic and ledger forcing: before the forcing chain forces $J$, $\varphi$, the eight-tick octave, and $D=3$, the calculus needs a self-contained integer and ratio order that does not smuggle classical $\mathbb{Z}$ comparisons. Closing comparison under reciprocal is a necessary brick in that certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.