balanced_of_nonnegFlag
plain-language theorem explainer
When a signed orbit is flagged nonnegative, it is balanced (integer-equivalent) with the canonical pure-nonnegative orbit built from its absolute value. Order and certificate lemmas cite this to pin the positive half of sign-canonical form. The proof is a short rewrite through the toInt bridge plus the absolute-value identity for nonnegative flags.
Claim. Let $z$ be a signed orbit. If the structural nonnegative flag of $z$ holds (negative side $\le$ positive side), then $z$ is balanced with the signed orbit obtained by embedding $|z|$ as a pure nonnegative orbit: equivalently, their integer displays agree.
background
In Primitive Recognition Calculus, integers are carried by signed orbits: pairs of $\delta$-orbit positions (pos, neg). Two signed orbits are balanced when a.pos + b.neg = b.pos + a.neg; this is the internal PRC integer relation (K4.9), defined entirely on orbit positions. The bridge theorem balanced_iff_toInt_eq states that balance is equivalent to equality of the conservative $\mathbb{Z}$ displays toInt.
The computable flag nonnegFlag is structural comparison leq neg pos. Absolute value abs is the orbit-position difference absDiff pos neg. The constructor ofOrbit embeds a bare orbit as a nonnegative signed orbit. Upstream, abs_toInt_of_nonnegFlag already shows that under the nonnegative flag, the natural absolute value coerces to the same integer as z.toInt.
This module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, sign-flag exclusivity) before packaging a closed certificate.
proof idea
Term-mode, three steps. Rewrite the goal with balanced_iff_toInt_eq, turning balance into toInt equality, then with ofOrbit_toInt so the right-hand side is the integer display of the absolute orbit. The remaining equality is the symmetric form of abs_toInt_of_nonnegFlag h, which already equates (z.abs.toNat : ℤ) with z.toInt under the nonnegative flag. No case split or omega is needed here.
why it matters
This lemma is the nonnegative half of sign-canonical form. Downstream, balanced_sign_canonical packages the dichotomy: either the nonnegative flag holds and $z$ balances with ofOrbit z.abs, or the negative flag holds and $z$ balances with the negation of that canonical orbit. That dichotomy is part of closing the internal signed-orbit order surface.
The larger consumer is integer_order_certificate, whose doc-comment states "The internal signed-orbit order surface is closed." The certificate records display lemmas for truncated subtraction, leq, absolute difference, and both the Prop-level and flag-level nonnegative characterizations. Without the nonnegative balance identity, the positive canonical representative would not be tied back to the internal balance relation.
In the broader Recognition stack this sits in Foundation PRC integer construction, upstream of ledger forcing and the T0–T8 chain; it is bookkeeping that makes the integer order choice-free and display-faithful, not a physics forcing step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.