balanced_of_negativeFlag
plain-language theorem explainer
If a signed orbit is flagged negative, it is balanced with the pointwise negation of the orbit built from its absolute value: z ~ -|z|. Order and sign-canonicalization lemmas cite this to pin the negative branch of the internal integer display. The proof rewrites balance to integer equality, applies the absolute-value identity for negative flags, and finishes by omega.
Claim. Let $z$ be a signed orbit. If its negative flag is true, then $z$ is balanced with the negation of the orbit of its absolute value: $\mathrm{balanced}(z,\,-|z|)$, equivalently $z^{\mathbb{Z}} = -|z|^{\mathbb{Z}}$.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of distinction-nat positions (pos, neg) with an integer display toInt. Balance is the internal equivalence a.pos + b.neg = b.pos + a.neg (K4.9); it is proved equivalent to equality of the conservative ℤ displays via balanced_iff_toInt_eq.
Negation swaps the two legs. Absolute value is the orbit position absDiff pos neg. The negative flag is the discrete sign bit tied to toInt < 0. Upstream, abs_toInt_of_negativeFlag states that a negative flag forces (z.abs.toNat : ℤ) = -z.toInt, so the absolute orbit recovers the magnitude on the negative ray.
This module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, flag characterizations of nonnegativity and negativity) without classical choice on bare iff goals.
proof idea
Rewrite the goal with balanced_iff_toInt_eq, then negate_toInt and ofOrbit_toInt, so the claim becomes an equality of integer displays. Invoke abs_toInt_of_negativeFlag on the negative-flag hypothesis to obtain (z.abs.toNat : ℤ) = -z.toInt. Close the resulting linear arithmetic goal with omega.
why it matters
This is the negative half of sign canonicalization: every negative signed orbit is balanced with -|z|. It feeds balanced_sign_canonical, which asserts that either the nonnegative flag holds and z ~ |z|, or the negative flag holds and z ~ -|z|. It also supplies one direction of balanced_negate_ofOrbit_abs_iff_negativeFlag_or_balanced_zero.
Downstream, integer_order_certificate packages the closed internal signed-orbit order surface (nonnegativity displays, truncated subtraction, abs-diff). In the Recognition foundation this keeps the ledger integer layer choice-free and internal to δ-orbit positions before the forcing chain (T5–T8) and the Recognition Composition Law are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.