sub_congr_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (same integer value), their differences are balanced. Anyone building order or comparison lemmas on the PRC integer surface cites this. The proof unfolds subtraction as addition of a negation and applies the existing add and negate congruence lemmas.
Claim. Let $a,a',b,b'$ be signed orbits (pairs of distinction-natural lengths standing for $a_{+} - a_{-}$). If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ in the sense $x_{+} + y_{-} = y_{+} + x_{-}$, then $a - b$ is balanced with $a' - b'$.
background
In the Primitive Recognition Calculus, integers are not postulated; they arise as signed orbit differences. A SignedOrbit is a pair $(p,n)$ of distinction-natural lengths with intended meaning $p - n$. Two signed orbits are balanced when their lengths satisfy $a_{+} + b_{-} = b_{+} + a_{-}$, the internal PRC integer relation (K4.9), equivalent to equal integer values under the toInt map.
Subtraction on signed orbits is defined by $a - b := a + (-b)$, so congruence for subtraction reduces to congruence for addition and negation. The sibling lemmas add_congr_of_balanced and negate_congr_of_balanced already show that balancing is preserved by those operations, each by rewriting through balanced_iff_toInt_eq and the corresponding toInt identities.
This module builds the order surface on that integer quotient: comparison, absolute value, and the eventual integer_order_certificate all need operations to respect balancing.
proof idea
Term-mode, three steps. Unfold the definition of signed-orbit subtraction (which is addition of a negation). Apply add_congr_of_balanced to the given balance hypothesis on the minuends together with the balance of the negated subtrahends. The latter comes from one application of negate_congr_of_balanced to the subtrahend hypothesis. No further rewriting is needed.
why it matters
This is the subtraction half of the congruence package that makes the signed-orbit quotient a well-defined ordered abelian group surface. Downstream it feeds absolute-value equality (abs_sub_eq_of_balanced), all comparison-stability lemmas for differences (cmp_of_sub_inputs_of_balanced, cmp_sub_inputs_of_balanced, cmp_subtractions_of_balanced), and the corresponding $\le$ biconditionals (le_of_sub_inputs_iff_of_balanced, le_sub_inputs_iff_of_balanced, le_subtractions_iff_of_balanced). Those close into integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed.
In the broader Recognition stack this sits under the foundation forcing chain: before J-cost uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), or $D=3$ (T8), the ledger must already support a coherent integer order built only from $\delta$-orbit positions. Without subtraction congruence, order and comparison on differences would depend on representative choice and the certificate would fail.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.