negate_ofOrbit_balanced_zero_iff
plain-language theorem explainer
Negating the signed-orbit embedding of a distinction natural is balanced against the zero orbit exactly when that natural is zero. Authors of the internal integer-order surface and its closure certificate cite this to pin the unique zero under negation. The proof rewrites balance to integer equality via the toInt bridge, then finishes by injectivity of toNat and elementary arithmetic.
Claim. For every distinction natural $n$, the signed orbit obtained by embedding $n$ and then negating is balanced with the zero signed orbit if and only if $n=0$.
background
In the Primitive Recognition Calculus, integers are realized as signed orbits: pairs of nonnegative orbit lengths that record how many $\delta$-ticks sit on each side of a ledger cut. Two signed orbits $a$ and $b$ are balanced when $a.pos+b.neg=b.pos+a.neg$. Upstream documentation calls this "the internal PRC integer relation, defined entirely on $\delta$-orbit positions."
Distinction naturals embed into signed orbits by placing their full length on the positive side. Negation swaps the two sides. The zero signed orbit is the balanced origin of that surface. Balance is also characterized by equality of the integer display values toInt, and toNat sends the zero distinction natural to $0$.
The surrounding module builds the order laws (reflexivity, totality, trichotomy, sign flags) on these objects so the usual integer order holds internally before any external $\mathbb{Z}$ is assumed.
proof idea
Rewrite the balance goal through the characterization that two signed orbits are balanced exactly when their toInt values agree. Push toInt through negation, through the ofOrbit embedding, and through zero. The statement collapses to the ordinary integer claim $-(toNat,n)=0$ if and only if $n=0$.
Forward direction: apply injectivity of toNat, rewrite toNat\,zero=0, and close with omega. Reverse direction: substitute $n=0$, use toNat_zero, and finish by norm_num.
why it matters
This equivalence is one of the atomic facts assembled into integer_order_certificate, whose documentation states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and signed nonnegativity so the order surface can be treated as a finished internal interface.
In the Recognition foundation, integer structure is not imported from classical $\mathbb{Z}$; it is forced from $\delta$-orbit combinatorics on the ledger. Pinning that the negated embedding of $n$ balances zero only at $n=0$ is a minimal uniqueness fact needed before sign flags, trichotomy, and nonnegativity displays can be trusted. Downstream tick-counting that feeds the eight-tick octave (T7) and later dimensional forcing sits on this discrete order surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.