nonneg_iff_of_balanced
plain-language theorem explainer
Balanced signed orbits share nonnegativity: if two signed orbits have equal integer displays, one is nonnegative exactly when the other is. Authors of the PRC integer-order surface cite this when transporting the internal order across the balanced congruence. The proof rewrites both sides through the toInt display and applies the balanced-to-integer bridge in each direction.
Claim. If two signed orbits $z$ and $w$ are balanced, meaning $z_{\mathrm{pos}}+w_{\mathrm{neg}}=w_{\mathrm{pos}}+z_{\mathrm{neg}}$, then $z$ is nonnegative if and only if $w$ is nonnegative.
background
In the Primitive Recognition Calculus, integers are represented internally by signed orbits: pairs of distinction-nat orbit lengths (positive and negative sides). Two signed orbits are balanced when their lengths satisfy $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$. That relation is the internal PRC integer equivalence; the bridge theorem states it holds exactly when the conservative integer displays agree, $a.{\mathrm{toInt}}=b.{\mathrm{toInt}}$.
Internal nonnegativity is defined without external $\mathbb{Z}$: a signed orbit is nonnegative when it balances with some purely positive orbit. A companion theorem equates that predicate with the display inequality $0\le z.{\mathrm{toInt}}$. The present module builds the order surface on these internal predicates, so congruence lemmas that move nonnegativity across balanced pairs are needed before antisymmetry and trichotomy can close.
proof idea
Term-mode, two rewrites then a constructed iff. Both sides of the goal are rewritten by the display characterization of nonnegativity, reducing the claim to $0\le z.{\mathrm{toInt}}\leftrightarrow 0\le w.{\mathrm{toInt}}$. The balanced hypothesis is converted via the balanced-to-integer bridge into $z.{\mathrm{toInt}}=w.{\mathrm{toInt}}$, and that equality is substituted in each direction of the iff. No case splits or omega calls appear at this layer.
why it matters
This lemma is one of the congruence facts that let the internal signed-orbit order treat balanced pairs as interchangeable for the nonnegative cone. It is consumed by the integer-order certificate, whose doc-comment states that "the internal signed-orbit order surface is closed" and which packages the signed nonnegativity display among other order-surface witnesses. Without transport of nonnegativity across balance, the certificate could not treat the internal order as well-defined on the PRC integer quotient. In the broader foundation stack this sits under the ledger and forcing layers that eventually feed the T0--T8 chain; it is pure integer-order infrastructure rather than a direct forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.