recipNonzero_num_lt_zero_iff
plain-language theorem explainer
For a ratio orbit with nonzero numerator, the reciprocal's numerator is strictly negative exactly when the original numerator is. Order-theory and rational-arithmetic developments cite this when tracking sign under inversion. The proof is a three-rewrite chain through the negative-flag characterization of strict negativity and the fact that reciprocal preserves that flag.
Claim. Let $a$ be a ratio orbit whose numerator is not balanced with zero (i.e., nonzero). Then the numerator of the nonzero reciprocal of $a$ is strictly less than zero if and only if the numerator of $a$ is strictly less than zero.
background
In the Primitive Recognition Calculus, integers are signed orbits: pairs of nonnegative orbit lengths with a sign flag. Two signed orbits are balanced when $a.pos + b.neg = b.pos + a.neg$; balance with zero is the internal zero test. Strict order is nonnegative difference with nonzero (unbalanced) difference.
Ratio orbits package a numerator and denominator signed orbit. The nonzero reciprocal recipNonzero is defined only when the numerator is unbalanced with zero, swapping and renormalizing so the result stays a well-formed ratio.
Upstream, lt_zero_iff_negativeFlag equates strict negativity with the negative flag being true. The companion lemma recipNonzero_num_negativeFlag_eq states that the reciprocal's numerator carries exactly the same negative flag as the original numerator.
proof idea
Term-mode rewrite proof. Rewrite both sides of the biconditional with lt_zero_iff_negativeFlag, turning each strict-less-than-zero claim into an equality of the corresponding negative flag with true. The remaining goal is flag equality, discharged by recipNonzero_num_negativeFlag_eq.
why it matters
Sign preservation under reciprocal is a basic sanity check for the internal rational order. Downstream it feeds recipNonzero_num_cmp_zero and recipNonzero_num_zero_cmp, which lift the same fact to the three-way comparison function, and recip_num_lt_zero_iff_of_not_balanced_zero, which transfers the statement to the total reciprocal operation. Those lemmas sit on the path to integer_order_certificate, the closure certificate that the signed-orbit order surface is fully displayed. Within Recognition Science this is foundation scaffolding for ordered arithmetic on the ledger, not a forcing-chain landmark (T5–T8), but without it the rational layer cannot talk about signs of inverted quantities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.