recip_num_balanced_ofOrbit_den_iff_nonnegFlag_of_not_balanced_zero
plain-language theorem explainer
For a nonzero ratio orbit, the numerator of its reciprocal balances against the nonnegative lift of the denominator exactly when the original numerator carries the nonnegative flag. Authors of the integer-order certificate cite this when closing signed-orbit comparison under inversion. The proof rewrites the total reciprocal to the nonzero branch and applies the matching nonzero lemma.
Claim. Let $a$ be a ratio orbit whose numerator is not balanced with zero. Then the numerator of the reciprocal of $a$ is balanced with the nonnegative signed orbit built from the denominator of $a$ if and only if the nonnegative flag of the numerator of $a$ equals true.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of $\delta$-orbit positions (positive and negative sides). Two signed orbits are balanced when $a.pos + b.neg = b.pos + a.neg$; that is the internal PRC integer relation, defined entirely on orbit lengths. The computable nonnegative flag on a signed orbit is the structural comparison leq of its negative side against its positive side. The constructor ofOrbit builds a nonnegative signed orbit from a bare $\delta$-orbit by pairing it with zero on the negative side.
Ratio orbits package a signed numerator with a denominator orbit. Reciprocal is total on ratio orbits, but under the hypothesis that the numerator is not balanced with zero it coincides with the nonzero reciprocal branch. The local module builds the order surface on these signed and ratio orbits; the present statement is one of the inversion lemmas that relate balance of the reciprocal numerator against ofOrbit(den) to the sign flag of the original numerator.
proof idea
One-line wrapper. First rewrite the total reciprocal to the nonzero reciprocal via recip_eq_recipNonzero_of_not_balanced_zero under the given non-balance hypothesis. Then apply recipNonzero_num_balanced_ofOrbit_den_iff_nonnegFlag, which already states the same biconditional for the nonzero branch.
why it matters
Feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, leq, absolute difference, and signed nonnegativity flags; the present biconditional is part of the inversion bookkeeping that makes those displays consistent under reciprocal.
In the Recognition foundation stack this sits inside Primitive Recognition Calculus integer order, upstream of ledger forcing and the T0–T8 chain. It does not itself force $\phi$ or dimension; it keeps the discrete order surface coherent so later forcing steps can treat integer comparison as closed data rather than an open interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.