add_respects_balanced
plain-language theorem explainer
Signed-orbit addition preserves balanced equivalence: if a₁ ~ a₂ and b₁ ~ b₂, then a₁+b₁ ~ a₂+b₂. Anyone constructing PRC integers as a quotient of signed orbits needs this congruence. The proof rewrites balanced to equality of integer displays and uses additivity of toInt.
Claim. Let $a_1,a_2,b_1,b_2$ be signed orbits (pairs of distinction-naturals, read as $\mathrm{pos}-\mathrm{neg}$). If $a_1$ is balanced with $a_2$ and $b_1$ is balanced with $b_2$ (i.e.\ $a_1.\mathrm{pos}+a_2.\mathrm{neg}=a_2.\mathrm{pos}+a_1.\mathrm{neg}$, and likewise for $b$), then the pointwise sums $a_1+b_1$ and $a_2+b_2$ are balanced.
background
In the Primitive Recognition Calculus, integers are built from signed orbits: a SignedOrbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction-naturals, intended as $\mathrm{pos}-\mathrm{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 relation is the internal equivalence for PRC integers, defined only on $\delta$-orbit positions (K4.9).
A verifier display toInt sends a signed orbit to an ordinary integer. The bridge lemma states that balanced holds if and only if the two displays agree. Pointwise addition on signed orbits adds the positive and negative components separately, and add_toInt records that this operation is additive on the integer display: $(a+b).\mathrm{toInt}=a.\mathrm{toInt}+b.\mathrm{toInt}$.
The local module lifts arithmetic from signed orbits to the quotient type of PRC integers. Congruence of addition under balanced is the missing well-definedness step for that lift.
proof idea
Short rewrite proof. First replace every occurrence of balanced by equality of toInt via balanced_iff_toInt_eq. The goal becomes equality of four integer displays. Apply add_toInt on each side so both sides are sums of the original displays, then substitute the two balanced hypotheses (now equalities of displays). The resulting integer equality is immediate.
why it matters
This private lemma is the congruence proof that lets addition descend to PRC integers. Downstream, PRCInt.add is defined by Quot.lift₂ on signed-orbit addition; both well-definedness obligations call add_respects_balanced (once with a reflexivity hypothesis on each argument). Without it, the quotient would not carry a well-defined sum.
In the Recognition stack this sits in the foundation layer that builds integers and rationals from primitive distinction orbits, before mass ladders and physical constants. It is bookkeeping rather than a forcing-chain step (T5–T8), but it closes the arithmetic interface those later constructions assume: integers as balanced classes of signed $\delta$-orbits, with addition induced from the orbit monoid.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.