abs_ne_zero_of_not_balanced_zero
plain-language theorem explainer
If a signed orbit is not balanced against zero, its absolute value (as a distinction-orbit length) is nonzero. Integer and ratio constructions cite this to justify taking reciprocals and absolute values without a zero denominator. The proof reduces to the integer display: non-balance implies nonzero toInt, which forces nonzero abs.
Claim. Let $z$ be a signed orbit (pair of distinction-orbit lengths, read as $\mathrm{pos}-\mathrm{neg}$). If $z$ is not balanced with the zero signed orbit (i.e. $\mathrm{pos}_z+\mathrm{neg}_0 \neq \mathrm{pos}_0+\mathrm{neg}_z$), then the absolute value of $z$ is not the zero distinction natural.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair of distinction-orbit positions $(\mathrm{pos},\mathrm{neg})$, intended as $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when $\mathrm{pos}_a+\mathrm{neg}_b=\mathrm{pos}_b+\mathrm{neg}_a$; that is the internal PRC integer equality, defined only on $\delta$-orbit lengths.
The absolute value of a signed orbit is the distinction-orbit absolute difference of its positive and negative parts. A separate verifier map toInt sends signed orbits to ordinary integers. The bridge lemma states that balance agrees with equality of those integer displays: balanced $a,b$ if and only if $a.\mathrm{toInt}=b.\mathrm{toInt}$.
The zero signed orbit has integer display $0$. Thus "not balanced with zero" is the internal way of saying the signed orbit is a nonzero integer, without leaving the orbit calculus.
proof idea
Term-mode reduction through the integer display. Apply the sibling lemma that nonzero toInt forces nonzero absolute value. It remains to show z.toInt ≠ 0. Assume the contrary; rewrite with the zero display identity zero_toInt, then the balance–toInt bridge (balanced_iff_toInt_eq) yields balance with zero, contradicting the hypothesis. No case splits or omega; pure iff transport.
why it matters
This is a small but load-bearing nonzero gate in the PRC integer/rational stack. Downstream, recipNonzero takes a ratio orbit whose numerator is not balanced with zero and builds the reciprocal using the signed-orbit absolute value as denominator; this theorem is exactly the witness that that denominator is a nonzero distinction natural. It also feeds the integer-order certificate that closes the internal signed-orbit order surface (nonnegativity and comparison displays).
In the broader Recognition foundation, signed orbits are the choice-free integer layer under the forcing chain: before J-cost uniqueness (T5) and $\phi$ (T6) appear, one needs a clean internal $\mathbb{Z}$ with absolute value and reciprocals. The result keeps that layer on orbit positions rather than classical integers except at the verifier bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.