recip_num_nonnegFlag_eq_of_not_balanced_zero
plain-language theorem explainer
When a ratio orbit has nonzero numerator, the reciprocal keeps the same nonnegativity flag on its numerator. Order work in the primitive recognition calculus cites this to track signs under inversion of rational displays. The proof rewrites the total reciprocal onto the nonzero branch and applies the flag-preservation lemma already proved there.
Claim. Let $a$ be a ratio orbit (signed-orbit numerator over a nonzero distinction-natural denominator). If the numerator of $a$ is not balanced with zero, then the nonnegativity flag of the numerator of the reciprocal of $a$ equals the nonnegativity flag of the numerator of $a$.
background
In the Primitive Recognition Calculus, integers appear as signed orbits: pairs of distinction-natural positions (pos, neg). Two signed orbits are balanced when their lengths match crosswise, $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. Balance of a numerator with zero is the internal zero test. The computable nonnegativity flag is the structural comparison neg ≤ pos on that pair.
A ratio orbit packages a signed-orbit numerator with a nonzero distinction-natural denominator. Reciprocal is defined on every ratio orbit; under the nonzero-numerator hypothesis it coincides with a specialized nonzero branch. This module develops the internal order surface on those integer and rational displays, including sign and flag lemmas used by the order certificate.
proof idea
Short term proof in two steps. Rewrite the total reciprocal along the equality that identifies it with the nonzero reciprocal whenever the numerator is not balanced with zero. Then apply the already-proved lemma that the nonzero reciprocal preserves the numerator nonnegativity flag under that same hypothesis.
why it matters
Used by the integer-order certificate, which closes the internal signed-orbit order surface (display lemmas for truncated subtraction, order, absolute difference, and signed nonnegativity flags). Sign preservation under reciprocal keeps those flag displays coherent when rational orbits are inverted. The result lives in the foundation layer that underwrites ledger balance and integer displays feeding later forcing structure; it is not itself a named T0–T8 step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.