sub_self_balanced_zero
plain-language theorem explainer
For any signed orbit a, the difference a − a is balanced with the zero orbit. Order and comparison lemmas cite this to replace self-subtraction by zero under ≤, <, and cmp. The proof is a short term application of the subtraction-balance iff, discharging reflexivity via the toInt bridge.
Claim. For every signed orbit $a$, the signed-orbit difference $a - a$ is balanced with the zero orbit: $\mathrm{balanced}(a-a,\,0)$. Equivalently, $(a-a).\mathrm{toInt} = 0$ in the verifier integer display.
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 their lengths satisfy the internal integer relation a.pos + b.neg = b.pos + a.neg (K4.9). That relation is the PRC-native equality of integers; the bridge theorem states it is equivalent to equality of the conservative toInt displays.
Subtraction of signed orbits is defined so that sub a b is balanced with zero exactly when a is balanced with b. The present fact is the diagonal case: self-subtraction lands on the zero class. The surrounding IntegerOrder module builds the full order surface (≤, <, cmp, sign flags) on these balanced classes without leaving the δ-orbit language.
proof idea
One short term proof. Apply the right-to-left direction of sub_balanced_zero_iff_balanced at (a, a), reducing the goal to balanced a a. Rewrite that goal with balanced_iff_toInt_eq, which turns it into a.toInt = a.toInt and closes by reflexivity. No case splits and no classical choice.
why it matters
Self-subtraction equaling zero is the algebraic identity that lets every order comparison treat a − a as the zero orbit. Downstream, le_sub_self_left_iff, le_sub_self_right_iff, lt_sub_self_left_iff, lt_sub_self_right_iff, and the two cmp_sub_self_* lemmas are one-line congruences that quote this fact. Those lemmas feed the closed integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed.
In the Recognition foundation this is ledger-level bookkeeping, not a physical forcing step: it keeps the PRC integer order coherent so later mass-ladder and tick-structure arguments can trust signed differences. It does not itself invoke J-cost, φ, or the T0–T8 chain; it is infrastructure those layers sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.