recipNonzero_num_zero_lt_iff
plain-language theorem explainer
For a nonzero ratio orbit, the numerator of its reciprocal is strictly positive exactly when the original numerator is. Order and comparison lemmas for ratio orbits cite this when reducing sign questions under inversion. The proof rewrites both sides by the nonnegFlag characterization of zero-lt, then uses that recip preserves the nonnegFlag and nonzeroness of the numerator.
Claim. Let $a$ be a ratio orbit whose numerator is not balanced with zero (i.e., the numerator is nonzero in the signed-orbit sense). Then $0 < (\mathrm{recipNonzero}(a)).\mathrm{num}$ if and only if $0 < a.\mathrm{num}$, where $<$ is the strict order on signed orbits.
background
In the Primitive Recognition Calculus, integers are realized as signed orbits: pairs of $\delta$-orbit lengths with a nonnegativity flag. Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; balance with zero is the internal notion of being zero. Strict order on signed orbits is defined so that $0<z$ holds exactly when $z$ is nonnegative and not balanced with zero (zero_lt_iff_nonnegFlag_and_not_balanced_zero).
Ratio orbits package a signed numerator and denominator. The operation recipNonzero inverts a ratio orbit under the hypothesis that its numerator is not balanced with zero. Upstream facts already record that this reciprocal keeps the numerator's nonnegFlag (recipNonzero_num_nonnegFlag_eq) and keeps the numerator nonzero (recipNonzero_num_not_balanced_zero). The present lemma packages those into a clean order equivalence for $0<\cdot$ on numerators.
proof idea
Term-mode proof by rewriting and a two-way constructor. Rewrite both sides of the biconditional with zero_lt_iff_nonnegFlag_and_not_balanced_zero, so each side becomes "nonnegFlag true and not balanced with zero". Then rewrite the reciprocal's nonnegFlag via recipNonzero_num_nonnegFlag_eq, which equates it to the original numerator's flag.
Left-to-right: from the reciprocal side one already has the shared nonnegFlag; the original nonzeroness hypothesis $h$ supplies the missing "not balanced with zero" conjunct. Right-to-left: the original side supplies the nonnegFlag; recipNonzero_num_not_balanced_zero supplies nonzeroness of the reciprocal numerator.
why it matters
This is a local sign-preservation fact under inversion inside the integer-order surface of PRC. It is used immediately by the comparison lemmas recipNonzero_num_cmp_zero and recipNonzero_num_zero_cmp, which lift the order equivalence to SignedOrbit.cmp against zero, and by recip_num_zero_lt_iff_of_not_balanced_zero, which transfers the same statement to the total reciprocal RatioOrbit.recip once nonzeroness is known.
Those pieces feed the closed certificate integer_order_certificate ("the internal signed-orbit order surface is closed"), which packages display lemmas for truncated subtraction, $\le$, absolute difference, and signed nonnegativity. In the broader Recognition stack this sits in Foundation arithmetic built from logic, before the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$); it is plumbing that keeps rational sign and order coherent on $\delta$-orbits rather than a physics landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.