add_congr_of_balanced
plain-language theorem explainer
Addition on signed orbits respects the internal balance relation: if a ~ a' and b ~ b', then a+b ~ a'+b'. Anyone building the PRC integer order or quotienting by balance cites this. The proof is a three-line rewrite through the toInt bridge and additivity of toInt.
Claim. Let $a,a',b,b'$ be signed orbits (pairs of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$). 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 $a'+b'$.
background
In the Primitive Recognition Calculus, integers are not postulated; they arise as signed orbit differences. A SignedOrbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, intended as $\mathrm{pos}-\mathrm{neg}$. Two such orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$: the internal PRC integer relation, defined only on $\delta$-orbit positions (K4.9).
The bridge to ordinary integers is toInt, with the characterization that balance holds if and only if the integer displays agree. Addition of signed orbits is componentwise on the positive and negative legs, and is compatible with toInt: $(\mathrm{add},a,b).\mathrm{toInt}=a.\mathrm{toInt}+b.\mathrm{toInt}$.
This module develops the order surface on those signed orbits. Congruence of addition under balance is the first algebraic step toward treating balance as a genuine equivalence for arithmetic.
proof idea
Term-style rewrite proof. First rewrite every balance hypothesis and the goal via balanced_iff_toInt_eq, so the claim becomes equality of integer displays. Then rewrite both sides with add_toInt, which turns $(\mathrm{add},a,b).\mathrm{toInt}$ into $a.\mathrm{toInt}+b.\mathrm{toInt}$ (and likewise for the primed pair). The two balance hypotheses supply $a.\mathrm{toInt}=a'.\mathrm{toInt}$ and $b.\mathrm{toInt}=b'.\mathrm{toInt}$, and the goal closes by substitution.
why it matters
Balance must be a congruence for the signed-orbit operations before the PRC integer order can be treated as well-defined on equivalence classes. This lemma is the addition half of that congruence; the subtraction half (sub_congr_of_balanced) is obtained from it by unfolding subtraction as add-of-negate and applying the companion negate congruence.
Downstream, both feed the closed certificate integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages the display lemmas (nonneg, flags, truncated sub, abs-diff) that let later foundation layers quote an ordered integer structure built only from distinction orbits, without importing classical $\mathbb{Z}$ as primitive.
In the broader Recognition stack this sits under the ledger-forcing and primitive-calculus foundation, not yet at the T5–T8 forcing landmarks, but it is part of the integer substrate those later steps rely on when they speak of discrete ticks, rungs, and signed imbalances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.