recipNonzero_num_negativeFlag_eq
plain-language theorem explainer
For a nonzero ratio orbit, the reciprocal keeps the same numerator sign flag as the original. Anyone proving that reciprocal preserves negativity (or building the integer-order certificate) cites this. The proof splits on the numerator sign flag and rewrites with the two reciprocal-numerator normal forms plus the sign of ofOrbit and its negation.
Claim. Let $a$ be a ratio orbit whose numerator is not balanced with zero. Then the negative-sign flag of the numerator of the nonzero reciprocal of $a$ equals the negative-sign flag of the numerator of $a$.
background
In the Primitive Recognition Calculus, integers are carried as signed orbits: a nonnegative flag and a derived negative flag on a distinction-nat payload. A ratio orbit is a pair of signed orbits (numerator, denominator) with nonzero denominator. Balance against zero is the internal equality test; the hypothesis here is that the numerator is not the zero orbit.
The nonzero reciprocal swaps roles of numerator and denominator, inserting a negation when the original numerator is negative so that the represented rational is inverted correctly. Two companion lemmas give the exact numerator after reciprocal: if the numerator is nonnegative, the reciprocal numerator is ofOrbit of the denominator; if negative, it is the negation of that orbit.
Sign flags are exclusive and exhaustive: negative-flag false if and only if nonnegative-flag true. Upstream, ofOrbit always has negative flag false, and negation of a nonzero ofOrbit has negative flag true.
proof idea
Case split on whether the numerator negative flag is true.
If true, rewrite the reciprocal numerator via the negative-flag normal form to negate(ofOrbit den), then apply negativeFlag_negate_ofOrbit_of_ne_zero (denominator nonzero) to get true, matching the hypothesis flag.
If not true, force the flag to false by cases, convert to nonnegative flag true via negativeFlag_eq_false_iff_nonnegFlag_eq_true, rewrite the reciprocal numerator via the nonnegative normal form to ofOrbit den, and apply negativeFlag_ofOrbit to get false.
why it matters
This is a sign-preservation lemma for inversion on the internal rational surface. It feeds directly into recipNonzero_num_lt_zero_iff, which upgrades flag equality to the order relation "reciprocal numerator is negative iff original numerator is," and into the unrestricted reciprocal version recip_num_negativeFlag_eq_of_not_balanced_zero.
Both sit under integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. Closing order under reciprocal is part of making the ledger rationals a usable ordered field fragment before the forcing chain (T5 J-uniqueness, T6 phi) is attached. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.