zero_sub_balanced_negate
plain-language theorem explainer
Zero minus a signed orbit is balanced with the pointwise negation of that orbit: both display the same integer. Order and comparison lemmas cite this to replace 0−a by −a without changing ≤, <, or cmp. The proof rewrites through the toInt bridge and closes by omega on 0−n=−n.
Claim. For every signed orbit $a$, the signed-orbit difference $0-a$ is balanced with the pointwise negation of $a$: $(0-a).\mathrm{pos}+(-a).\mathrm{neg}=(-a).\mathrm{pos}+(0-a).\mathrm{neg}$. Equivalently, $(0-a).\mathrm{toInt}=(-a).\mathrm{toInt}$.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction-natural lengths (pos, neg) with intended meaning pos − neg. Two signed orbits are balanced when a.pos + b.neg = b.pos + a.neg; that internal relation is the PRC integer equivalence, defined only on δ-orbit positions.
The bridge theorem balanced_iff_toInt_eq states that balance holds exactly when the conservative integer displays agree: a.toInt = b.toInt. Pointwise negation swaps the two components, and negate_toInt records (negate a).toInt = −a.toInt. Subtraction and zero have matching toInt laws (sub_toInt, zero_toInt).
This module builds the internal order surface on those signed orbits. The present fact is the algebraic identity that makes unary minus interchangeable with subtraction from zero under balance.
proof idea
Term-style tactic proof. Rewrite the goal with balanced_iff_toInt_eq, so it becomes an equality of integer displays. Unfold via sub_toInt, zero_toInt, and negate_toInt to obtain 0 − a.toInt = −a.toInt on ℤ. Close with omega. No case splits and no classical choice.
why it matters
Feeds the left/right congruence facts that identify order and comparison after replacing 0−a by negate a: le_zero_sub_left_iff, le_zero_sub_right_iff, lt_zero_sub_left_iff, lt_zero_sub_right_iff, cmp_zero_sub_left, and cmp_zero_sub_right. Those sit on the path to integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed.
In the Recognition foundation this is bookkeeping inside the integer layer of the primitive recognition calculus, not a forcing-chain landmark (T5–T8). It keeps the order API coherent so later ledger and mass constructions can treat unary minus and zero-subtraction as the same balanced class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.