recip_num_negativeFlag_eq_of_not_balanced_zero
plain-language theorem explainer
For a ratio orbit with nonzero numerator, the reciprocal keeps the same numerator negative-flag. Anyone wiring sign bookkeeping into the internal integer-order certificate cites this. The proof rewrites the total reciprocal onto the nonzero branch and applies the already-proved flag identity there.
Claim. Let $a$ be a ratio orbit (signed-orbit numerator over a nonzero distinction-nat denominator). If the numerator of $a$ is not balanced with zero, then the negative flag of the numerator of the reciprocal $a^{-1}$ equals the negative flag of the numerator of $a$.
background
Primitive Recognition Calculus builds integers and rationals from signed orbits rather than from $\mathbb{Z}$ as a primitive. A SignedOrbit carries nonnegative and negative orbit lengths; two orbits are balanced when $a.pos + b.neg = b.pos + a.neg$ (the internal equality relation K4.9). The negative flag is the Boolean dual of the structural nonnegative flag: strict negativity as failure of nonnegativity.
A ratio orbit is the rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Reciprocal is total on ratio orbits, but on the nonzero-numerator locus it coincides with an explicit nonzero reciprocal constructor that rearranges numerator and denominator with sign bookkeeping.
The local module develops the internal order surface on these displays (reflexivity, totality, trichotomy, flag characterizations of $\le 0$ and $< 0$). Upstream, the nonzero reciprocal already preserves the numerator negative flag; a separate lemma identifies the total reciprocal with that nonzero branch under the same hypothesis.
proof idea
Two-step term proof. First rewrite the total reciprocal via recip_eq_recipNonzero_of_not_balanced_zero, which unfolds the reciprocal definition and simplifies under the nonzero-numerator hypothesis, replacing recip a by recipNonzero a h. Then apply recipNonzero_num_negativeFlag_eq, which already proves the flag equality on the nonzero branch (by case split on the original negative flag and the negate-of-orbit identities). No new case analysis is introduced here.
why it matters
This is a small but necessary sign-invariance lemma on the path to 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, so downstream order and comparison proofs can stay inside PRC data rather than escaping to classical $\mathbb{Z}$.
In the Recognition Science stack this sits in Foundation, beneath the forcing chain (T0–T8) and the Recognition Composition Law: before J-cost uniqueness, $\varphi$, the eight-tick octave, or $D=3$ can be stated on ledger quantities, the integer/rational order surface must be certified. The lemma closes one reciprocal-sign obligation that the certificate assembly uses when comparing inverted ratio displays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.