abs_eq_zero_iff_balanced_zero
plain-language theorem explainer
Absolute value of a signed orbit vanishes exactly when that orbit is balanced against zero. Anyone building the internal integer order or reciprocal-nonzero lemmas cites this bridge. The proof is a three-rewrite chain through the toInt display.
Claim. For every signed orbit $z$, $|z| = 0$ if and only if $z$ is balanced with the zero signed orbit (i.e., $z.\mathrm{pos} + 0 = 0 + z.\mathrm{neg}$).
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction-nat positions (pos, neg), read as the formal difference pos - neg. Absolute value is the orbit-position absDiff pos neg. Two signed orbits are balanced when their lengths match: a.pos + b.neg = b.pos + a.neg. That is the internal PRC integer equality (K4.9), defined only on δ-orbit positions.
The verifier integer display toInt is the conservative bridge to ordinary ℤ. Upstream, abs_eq_zero_iff_toInt_eq_zero says |z| = 0 iff z.toInt = 0, and balanced_iff_toInt_eq says balance agrees with equal toInt values. The zero orbit has toInt = 0.
This module builds the internal order surface (comparison, flags, trichotomy) without relying on the verifier display as a definitional source.
proof idea
One-line rewrite proof. Rewrite the left side by abs_eq_zero_iff_toInt_eq_zero to get z.toInt = 0. Rewrite the right side by balanced_iff_toInt_eq to get z.toInt = SignedOrbit.zero.toInt. Finish with zero_toInt, which supplies SignedOrbit.zero.toInt = 0. The three rewrites close the biconditional.
why it matters
Closes a small but load-bearing identity on the signed-orbit order surface: vanishing absolute value is exactly balance with zero. Downstream, recipNonzero_num_not_balanced_zero uses it to keep reciprocal numerators off the zero class, and integer_order_certificate packages the whole internal order surface as closed ("The internal signed-orbit order surface is closed").
In the Recognition foundation this sits under the ledger/forcing layer that eventually feeds the forcing chain (T0–T8). It is not itself a physics landmark; it is bookkeeping that keeps the PRC integer relation choice-free and display-independent before mass ladders or J-cost enter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.