balanced_add_left_iff
plain-language theorem explainer
Left-addition by a fixed signed orbit preserves balance: c+a is balanced with c+b exactly when a is balanced with b. Anyone building translation-invariant order or comparison on the PRC integer surface cites this. The proof reduces both sides to integer equality via the toInt bridge and cancels the common summand with omega.
Claim. For signed orbits $a,b,c$ (each a pair of distinction-nats read as $\mathrm{pos}-\mathrm{neg}$), the left translates $c+a$ and $c+b$ are balanced if and only if $a$ and $b$ are balanced. Balance means equal internal orbit lengths $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$, equivalently equal verifier integers.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair of distinction-nats with intended meaning $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when their orbit lengths match: $a.pos+b.neg=b.pos+a.neg$. That internal relation is the PRC integer equality, defined only on $\delta$-orbit positions (K4.9).
The bridge theorem states that balance holds exactly when the verifier integers agree: $\mathrm{balanced},a,b\leftrightarrow a.\mathrm{toInt}=b.\mathrm{toInt}$. Addition of signed orbits is componentwise on the positive and negative parts, and is compatible with the integer display: $(a+b).\mathrm{toInt}=a.\mathrm{toInt}+b.\mathrm{toInt}$.
This module develops the internal order and comparison surface on signed orbits (flags, $\le$, trichotomy, and the selector $\mathrm{cmp}$), without routing definitions through the verifier integer display.
proof idea
Term-mode proof in three steps. Rewrite both occurrences of balance via the characterization that balance is equivalent to equal $\mathrm{toInt}$. Rewrite both left-hand additions via the homomorphism $(c+x).\mathrm{toInt}=c.\mathrm{toInt}+x.\mathrm{toInt}$. The goal becomes $c.\mathrm{toInt}+a.\mathrm{toInt}=c.\mathrm{toInt}+b.\mathrm{toInt}\leftrightarrow a.\mathrm{toInt}=b.\mathrm{toInt}$, which omega discharges by cancellation in $\mathbb{Z}$.
why it matters
Translation invariance of balance is the algebraic fact that lets comparison ignore a common left summand. Downstream, $\mathrm{cmp_add_left}$ uses it to prove $\mathrm{cmp}(c+a,c+b)=\mathrm{cmp}(a,b)$, so the internal ordering selector is left-invariant under addition. That lemma, and this one, feed the closed certificate $\mathrm{integer_order_certificate}$ ("The internal signed-orbit order surface is closed"), which packages display bridges for truncated subtraction, $\le$, absolute difference, and nonnegativity flags.
In the Recognition foundation stack this sits under ledger forcing and the PRC integer rational layer: balance is the internal stand-in for integer equality before any continuum or J-cost structure appears. It does not itself invoke T5–T8 or the Recognition Composition Law; it is pure discrete order infrastructure those later layers rely on when integers are recovered from orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.