balanced_sub_right_input_iff_of_balanced
plain-language theorem explainer
If two signed orbits represent the same integer, subtracting either from a fixed orbit yields results that agree under the balanced relation with any third orbit. Order and equality lemmas on the internal PRC integer surface cite this to treat right-hand subtraction as well-defined on equivalence classes. The proof rewrites both sides through the toInt bridge and cancels using the hypothesis.
Claim. Let $a,b,b',c$ be signed orbits. If $b$ and $b'$ are balanced (i.e.\ $b.\mathrm{pos}+b'.\mathrm{neg}=b'.\mathrm{pos}+b.\mathrm{neg}$), then $a-b$ is balanced with $c$ if and only if $a-b'$ is balanced with $c$.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair of distinction naturals (pos, neg) with intended meaning pos - neg. Two signed orbits are balanced when a.pos + b.neg = b.pos + a.neg; this is the internal PRC integer relation, defined entirely on δ-orbit positions (K4.9).
The bridge theorem balanced_iff_toInt_eq states that balance agrees with equality of the conservative integer display: balanced a b ↔ a.toInt = b.toInt. Subtraction on signed orbits satisfies (sub a b).toInt = a.toInt - b.toInt, so the integer view is a ring homomorphism for the orbit operations.
This module builds the order surface on that integer view. The present lemma is a congruence fact: balance of the right operand is preserved under left-fixed subtraction when comparing the result to an arbitrary third orbit.
proof idea
Term-mode rewrite proof. Both sides of the target iff are rewritten by balanced_iff_toInt_eq, then each sub is replaced by sub_toInt, yielding (a.toInt - b.toInt = c.toInt) ↔ (a.toInt - b'.toInt = c.toInt). The hypothesis is rewritten the same way to b.toInt = b'.toInt, and a final rewrite of that equality closes the goal.
why it matters
Right-input congruence for subtraction is needed so that order and zero-tests on signed orbits depend only on integer classes, not on particular orbit representatives. Downstream, sub_balanced_zero_iff_of_balanced_right is the specialization c = zero, obtained by applying this lemma directly. That family feeds the closed certificate integer_order_certificate, whose doc states that the internal signed-orbit order surface is closed (nonneg display, flag display, and related truncated-sub facts).
In the Recognition foundation stack this sits under the ledger/forcing layer that eventually supports the T0–T8 chain: integers and their order must be forced from δ-orbit data before cost, φ, and dimension theorems can sit on a clean arithmetic base. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.