balanced_negate_ofOrbit_abs_iff_negate_nonnegFlag
plain-language theorem explainer
A signed orbit z balances against the negation of its absolute-value orbit exactly when the negated orbit is flagged non-negative. Authors of the internal integer-order certificate cite this bridge between balance and the sign flag under flip. The proof rewrites both sides through the toInt display and closes each direction by omega on integer inequalities.
Claim. For every signed orbit $z$, the internal balance relation $z \sim -\lvert z\rvert$ holds if and only if the non-negativity flag of $-z$ equals true (equivalently, $z\le 0$ in the verifier integer display).
background
In the Primitive Recognition Calculus, integers are carried as signed orbits: pairs of distinction-orbit positions (pos, neg). The internal equivalence is balance: a balances b when a.pos + b.neg = b.pos + a.neg (K4.9). Absolute value projects to a non-negative orbit length via absDiff of the two legs; ofOrbit re-embeds that length as a non-negative signed orbit; negate swaps the legs.
The verifier display toInt recovers an ordinary ℤ value. Upstream, balanced_iff_toInt_eq states that balance agrees exactly with equality of these displays, and abs_toNat identifies the internal absolute value with Int.natAbs. The non-negativity flag is the boolean surface of toInt ≥ 0.
This module builds the order surface on those primitives: reflexivity, totality, trichotomy, and the flag characterizations of z ≥ 0 and z < 0. The present lemma sits among the sign-flag identities that feed the closed certificate.
proof idea
Rewrite the balance claim by balanced_iff_toInt_eq, then push negate and ofOrbit through toInt, so the left side becomes an equality of ordinary integers involving -|z.toInt|.
Forward: assume that equality, rewrite the nonnegativity flag of -z via nonnegFlag_eq_true_iff and negate_toInt, and finish with omega.
Reverse: assume the flag of -z is true, obtain z.toInt ≤ 0 by omega, invoke Int.ofNat_natAbs_of_nonpos to replace the absolute value by -z.toInt, transport via abs_toNat, and close again with omega.
why it matters
The sole downstream consumer is integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas for truncated subtraction, ≤, absolute difference, and both the Prop and flag forms of signed non-negativity. This lemma supplies the missing link that the balance of z against -|z| is exactly the nonnegativity flag of -z, so the certificate can treat sign flip and absolute value as coherent with the order flags.
In the broader Foundation stack this is bookkeeping for integers-from-logic: once signed orbits carry a closed order, later forcing steps can treat discrete comparison as already internal to the recognition calculus rather than imported from classical ℤ. It does not itself touch T5–T8 (J-uniqueness, φ, eight-tick, D=3), but it hardens the integer substrate those landmarks sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.