not_both_abs_representatives_of_not_balanced_zero
plain-language theorem explainer
If a signed orbit is not balanced with zero, it cannot be balanced with both its absolute-value representative and that representative's negation. Order theorists assembling the PRC integer order cite this exclusivity lemma. The proof is a one-line contrappositive via the matching biconditional on absolute representatives.
Claim. Let $z$ be a signed orbit. Write $\mathrm{bal}(a,b)$ for the orbit-length balance $a_{+} + b_{-} = b_{+} + a_{-}$. If $\neg\,\mathrm{bal}(z,0)$, then it is not the case that both $\mathrm{bal}(z,\mathrm{ofOrbit}(|z|))$ and $\mathrm{bal}(z,-\mathrm{ofOrbit}(|z|))$ hold.
background
In the Primitive Recognition Calculus, integers are realized as signed orbits: pairs of $\delta$-orbit positions with a positive and a negative leg. Two signed orbits $a,b$ are balanced when their lengths match crosswise, $a_{+} + b_{-} = b_{+} + a_{-}$. That relation is the internal PRC integer equality (K4.9), defined entirely on orbit positions.
The absolute value of a signed orbit is the distinction-nat $\mathrm{absDiff}$ of its two legs; ofOrbit lifts that back to a (nonnegative) signed orbit, and negate flips sign. Zero is the zero signed orbit. The sibling biconditional balanced_both_abs_representatives_iff_balanced_zero states that $z$ balances both the absolute representative and its negation if and only if $z$ balances zero.
This module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags). The present lemma is the exclusive half of the absolute-representative characterization of zero.
proof idea
One-line contrappositive wrapper. Assume both absolute representatives balance with $z$. Apply the forward direction (.mp) of balanced_both_abs_representatives_iff_balanced_zero to conclude that $z$ balances zero, contradicting the hypothesis. No case split or arithmetic is needed beyond that iff.
why it matters
Feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags on signed orbits. Without exclusivity of the two absolute representatives away from zero, the order surface could not cleanly separate the zero class from nonzero classes under balance.
In the broader Recognition stack this sits inside the foundation layer that forces discrete integer structure before the forcing chain (T0–T8) and the Recognition Composition Law are applied. It is a local algebraic hygiene fact, not a physics claim, but the certificate it supports is part of the closed PRC integer interface used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.