balanced_sub_inputs_iff_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (same integer value), then subtracting the pairs preserves balance against any third orbit: a−b balances c exactly when a′−b′ does. Order and certificate lemmas in the primitive recognition calculus cite this congruence. The proof is a short term rewrite through the toInt bridge and subtraction homomorphism.
Claim. Let $a,a',b,b',c$ be signed orbits. If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ (i.e.\ $a.\mathrm{pos}+a'.\mathrm{neg}=a'.\mathrm{pos}+a.\mathrm{neg}$ and likewise for $b,b'$), then $a-b$ is balanced with $c$ if and only if $a'-b'$ is balanced with $c$.
background
In the primitive recognition calculus, a SignedOrbit is a pair of distinction-natural counts (pos, neg) with intended meaning pos − neg. Two signed orbits are balanced when their orbit lengths match crosswise: $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That internal relation is the PRC integer equivalence (K4.9).
The bridge to ordinary integers is balanced_iff_toInt_eq: balance holds exactly when the conservative toInt displays agree. Subtraction on signed orbits is defined so that (sub a b).toInt = a.toInt − b.toInt (sub_toInt). The present lemma sits in the IntegerOrder module, which builds the order surface on these signed orbits from the IntegerRational layer.
proof idea
Term-mode rewrite proof. Both sides of the target iff are rewritten with balanced_iff_toInt_eq, then each sub is replaced by sub_toInt, yielding an equality of integer differences. The balance hypotheses are likewise rewritten to toInt equalities and substituted, so the two sides become identical. No case splits or omega are needed once the display bridge is in place.
why it matters
Balance must be a congruence for subtraction if the signed-orbit order is to be well-defined on equivalence classes rather than on raw representatives. Downstream, sub_balanced_zero_iff_of_balanced is the specialization to the zero orbit (one-line application of this lemma), and both 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: the same balance notion that appears in LedgerForcing (event-list balance) is realized here on δ-orbit positions, so integer order and zero tests do not depend on which balanced representative is chosen. It does not itself force φ, the eight-tick octave, or D=3; it stabilizes the integer layer those later forcing steps sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.