balanced_zero_of_both_abs_representatives
plain-language theorem explainer
If a signed orbit is equivalent both to the nonnegative lift of its absolute value and to the negation of that lift, then it is equivalent to zero. Order and integer-structure proofs in the primitive recognition calculus cite this to collapse the only case where both absolute representatives match. The argument is a one-line application of the corresponding biconditional.
Claim. Let $z$ be a signed orbit. If $z$ is balanced with the nonnegative signed orbit built from $|z|$ and also balanced with the negation of that orbit, then $z$ is balanced with zero.
background
In the primitive recognition calculus, integers are represented as signed orbits: pairs of $\delta$-orbit positions (pos, neg). Two signed orbits $a$ and $b$ are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; this is the internal equality relation on the PRC integers, defined entirely on orbit positions.
Absolute value sends a signed orbit to a bare orbit position via absolute difference of its components. The map ofOrbit embeds a nonnegative orbit position as $\langle n,0\rangle$, and negation swaps the two components. Zero is the balanced identity for this relation.
The local module builds the order surface on these signed orbits (reflexivity, transitivity, antisymmetry under balance, trichotomy, sign flags). The immediate upstream fact is the biconditional that both absolute representatives balance with $z$ if and only if $z$ balances with zero.
proof idea
One-line term proof. Apply the forward direction of balanced_both_abs_representatives_iff_balanced_zero at $z$, packing the two hypotheses into the left-hand conjunction. No further case analysis or arithmetic is performed here.
why it matters
Feeds integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags). Without collapsing the double-absolute-representative case to zero, antisymmetry and the zero characterizations on the order surface would leave a gap.
In the Recognition foundation stack this sits under ledger forcing and the integer layer that later supports the forcing chain (T0–T8). It is pure structural bookkeeping on signed orbits, not a physical claim, but the certificate it supports is part of making the PRC integer order machine-checkable end to end.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.