balanced_add_right_iff
plain-language theorem explainer
Right-addition by a fixed signed orbit preserves the balanced relation: a and b balance exactly when a+c and b+c do. Order and comparison lemmas on the internal PRC integer surface cite this cancellation. The proof reduces both sides to integer equality via the toInt bridge, then finishes by omega on ℤ addition.
Claim. For signed orbits $a,b,c$ (each a pair of distinction-nats read as $\mathrm{pos}-\mathrm{neg}$), $a+c$ is balanced with $b+c$ if and only if $a$ is balanced with $b$, where balanced means $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$ (equivalently $a.{\rm toInt}=b.{\rm toInt}$).
background
In the Primitive Recognition Calculus integer layer, a SignedOrbit is a pair of distinction-nats intended as the difference pos − neg. Two signed orbits are balanced when their orbit lengths match crosswise: a.pos + b.neg = b.pos + a.neg. That internal relation is the PRC stand-in for integer equality.
The bridge theorem balanced_iff_toInt_eq states that balanced a b holds exactly when the conservative integer displays agree: a.toInt = b.toInt. Addition of signed orbits is componentwise on the pos/neg legs, and add_toInt records that (a+b).toInt = a.toInt + b.toInt on ℤ.
This module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags). Translation invariance of balance under right addition is the algebraic fact needed before comparison can be shown invariant under the same shift.
proof idea
Term-style tactic proof in three steps. Rewrite both sides of the biconditional with balanced_iff_toInt_eq, turning balanced into equality of toInt values. Rewrite each add with add_toInt, so the goal becomes (a.toInt + c.toInt = b.toInt + c.toInt) ↔ (a.toInt = b.toInt). Close by omega on ℤ.
why it matters
Feeds cmp_add_right, which shows the three-way comparison of signed orbits is invariant under right addition, and is listed among the facts supporting integer_order_certificate (“The internal signed-orbit order surface is closed.”). Without cancellation of a common summand in the balanced relation, the order surface could not treat addition as an order automorphism on the PRC integer display.
In the broader Recognition stack this sits in Foundation under the ledger/forcing layer: balanced ledgers and signed-orbit arithmetic are the discrete substrate before continuum forcing (J-cost, φ, eight-tick structure). It is pure algebraic hygiene on the integer model, not a continuum or physical-constant claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.