recipNonzero_num_not_balanced_ofOrbit_den_iff_negativeFlag
plain-language theorem explainer
For a nonzero ratio orbit, the reciprocal's numerator fails to balance against the denominator orbit exactly when the original numerator is strictly negative. Order and sign bookkeeping for reciprocal ratios cite this. The proof rewrites through the dual nonnegativity equivalence and flips the Boolean sign flags.
Claim. Let $a$ be a ratio orbit whose numerator is not balanced with zero. Then the numerator of the nonzero reciprocal of $a$ is not balanced with the signed orbit of $a$'s denominator if and only if the numerator of $a$ carries the strict-negativity flag.
background
In the Primitive Recognition Calculus, integers are coded as signed orbits: pairs of distinction-nat counts (pos, neg). Two signed orbits are balanced when a.pos + b.neg = b.pos + a.neg, the internal equality relation on $\delta$-orbit positions. Nonnegativity is the computable flag nonnegFlag z := (z.neg \le z.pos); strict negativity is its Boolean negation negativeFlag z := !z.nonnegFlag.
Ratio orbits package a numerator and denominator signed orbit. The nonzero reciprocal recipNonzero a h is defined only when the numerator is not balanced with zero. Comparing that reciprocal's numerator against ofOrbit a.den is the structural test for the sign of the inverted ratio.
The dual fact already proved is that the same balance holds exactly when a.num.nonnegFlag = true. The Boolean identity negativeFlag = true \leftrightarrow nonnegFlag = false converts nonnegativity statements into negativity statements.
proof idea
One rewrite plus a two-direction Boolean flip. First rewrite the goal by the dual theorem recipNonzero_num_balanced_ofOrbit_den_iff_nonnegFlag, turning "not balanced" into "not (nonnegFlag = true)".
Forward: assume not-nonneg; apply negativeFlag_eq_true_iff_nonnegFlag_eq_false and case on a.num.nonnegFlag. The false branch is definitional; the true branch contradicts the assumption.
Backward: assume negativeFlag = true and nonnegFlag = true; the flag equivalence forces nonnegFlag = false, contradicting the second hypothesis.
why it matters
This is a sign-flip companion to the nonnegativity balance lemma for reciprocal numerators. It feeds recip_num_not_balanced_ofOrbit_den_iff_negativeFlag_of_not_balanced_zero, which drops the recipNonzero packaging and works with plain recip, and sits in the cluster that closes the internal signed-orbit order surface via integer_order_certificate.
In the Recognition foundation, ordered integers and rationals are not imported from classical $\mathbb{Z}$; they are forced from balanced $\delta$-orbits. Correct reciprocal sign behavior is required before the phi-ladder mass formula and the forcing chain can treat rational comparisons as native ledger facts. The certificate's claim that "the internal signed-orbit order surface is closed" depends on this family of flag equivalences being complete for both signs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.