negate_ofOrbit_not_balanced_zero_of_ne_zero
plain-language theorem explainer
Negating the positive signed orbit of a nonzero distinction natural is never balanced against the zero orbit. Sign-flag and order lemmas in the primitive recognition calculus cite this to keep the negative cone disjoint from zero. The proof rewrites balance to integer equality via toInt, uses injectivity of the natural readout, and closes with omega.
Claim. Let $n$ be a distinction natural with $n \neq 0$. Then the signed orbit obtained by negating the positive embedding of $n$ is not balanced with the zero signed orbit: if $a = \mathrm{negate}(\mathrm{ofOrbit}(n))$, then $a$ is not balanced with $0$.
background
In the primitive recognition calculus, integers are carried as signed orbits: pairs of nonnegative orbit lengths (pos, neg). Two signed orbits $a,b$ are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That is the internal integer equality (K4.9), defined entirely on $\delta$-orbit positions, and it is equivalent to equality of the integers read by toInt.
DistinctionNat is the nonnegative side, obtained from logic-level iteration counts via the forward map toNat (with toNat of zero equal to $0$). ofOrbit embeds a distinction natural as a nonnegative signed orbit; negate swaps the positive and negative legs. SignedOrbit.zero is the identity of this construction. The IntegerOrder module builds order and sign structure on these internal integers from those primitives.
proof idea
Rewrite balance with balanced_iff_toInt_eq, then push toInt through negate, ofOrbit, and zero. The goal reduces to $-(\mathrm{toNat},n)\neq 0$ in $\mathbb{Z}$. From $n\neq 0$, injectivity of toNat, and toNat_zero, deduce $\mathrm{toNat},n\neq 0$. Finish with omega.
why it matters
Local non-degeneracy for the signed-orbit model of integers: a nonzero positive stays nonzero after negation. Downstream, integer_order_certificate consumes it while packaging the closed order surface (nonneg flags, leq display, absdiff, truncated subtraction) for the PRC integer layer. Without this fact the negative cone could meet zero, and sibling trichotomy and sign-flag exclusivity lemmas would fail. It sits in the Foundation arithmetic stack that underwrites ledger balance and discrete counting, not a T0–T8 landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.