nonnegFlag_eq_of_balanced
plain-language theorem explainer
Balanced signed orbits share the same computable nonnegative flag. Anyone assembling order, sign, or multiplicative congruence on the PRC integer surface cites this invariance. The proof rewrites balance as equal recovered integers, case-splits the two Boolean flags, and discharges the mismatched cases by omega on the integer inequalities.
Claim. Let $z,w$ be signed orbits. If they are balanced, meaning $z_{\mathrm{pos}}+w_{\mathrm{neg}}=w_{\mathrm{pos}}+z_{\mathrm{neg}}$, then their nonnegative flags agree: the structural comparison $\mathrm{neg}\le\mathrm{pos}$ returns the same Boolean on both.
background
In the Primitive Recognition Calculus, integers are carried as signed orbits: pairs of distinction-nat lengths (pos, neg) recording positive and negative δ-orbit mass. The internal equivalence is balance: two orbits are balanced when a.pos + b.neg = b.pos + a.neg. That relation is defined entirely on orbit positions (K4.9), with no appeal to classical ℤ.
The recovery map toInt sends a signed orbit to an ordinary integer. Upstream, balance is characterized exactly by equal recovered integers: balanced a b ↔ a.toInt = b.toInt. That bridge lets internal PRC statements talk to the conservative ℤ display.
The nonnegative flag is the computable Boolean leq neg pos on the two sides. It is tied to the display by the iff lemmas: the flag is true exactly when 0 ≤ toInt, and false exactly when toInt < 0. This module builds the order surface on those flags.
proof idea
Rewrite the balance hypothesis via balanced_iff_toInt_eq, so z.toInt = w.toInt. Case-split on both Boolean flags.
Matching cases (true/true and false/false) close by reflexivity. The crossed cases are impossible: if one flag is false and the other true, the flag-iff lemmas give z.toInt < 0 and 0 ≤ w.toInt (or the symmetric pair). With equal toInt values, omega finishes the contradiction.
why it matters
This is the basic sign-invariance under the PRC integer relation. Downstream it is the one-line engine for negativeFlag_eq_of_balanced (negativity is just the flipped nonnegative flag), and for the multiplicative flag congruences: nonnegFlag_mul_eq_of_balanced and its left/right variants reduce to this after mul_congr_of_balanced. Scaling lemmas such as nonnegFlag_mul_ofOrbit_left_of_ne_zero likewise transport the flag across balanced multiplications.
Those facts feed the closed order surface certificate integer_order_certificate, which packages the signed nonnegative display and flag display as part of the internal integer-order API. In the foundation stack this is bookkeeping on the integer layer forced from logic, not yet a physics constant, but it is required scaffolding before rung arithmetic and mass formulas can sit on a well-behaved ordered ring of orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.