add_toInt
plain-language theorem explainer
Addition of signed orbits is compatible with the integer display map: the integer value of a sum equals the sum of the integer values. Anyone proving order, divisibility, or congruence facts about signed orbits cites this as the bridge to ordinary integer arithmetic. The proof expands both sides, applies natural-number addition recovery on each component, and closes by ring.
Claim. For signed orbits $a=(a_+,a_-)$ and $b=(b_+,b_-)$ (pairs of distinction naturals, read as $a_+-a_-$), with componentwise sum $\mathrm{add}(a,b)=(a_++b_+,\,a_-+b_-)$, the recovery map $[\cdot]$ to $\mathbb{Z}$ satisfies $[\mathrm{add}(a,b)]=[a]+[b]$, where $[z]=z_+.{\rm toNat}-z_-.{\rm toNat}$.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction naturals (pos, neg), with intended meaning pos − neg (K4.6). The verifier display toInt reads iteration counts and returns the ordinary integer difference. Addition of signed orbits is defined componentwise on the positive and negative parts.
Upstream, ArithmeticFromLogic.toNat_add is the recovery theorem that LogicNat (hence DistinctionNat) addition agrees with Nat addition under toNat. The IntegersFromLogic layer develops the same difference-of-pairs pattern for LogicInt; signed orbits mirror that construction before any quotient by balance.
The IntegerRational module builds the integer and rational layers of recognition calculus from orbit arithmetic, so later order and divisibility can be stated natively and checked against ℤ.
proof idea
Both sides are expanded into explicit integer differences of natural counts. After unfolding add and toInt, the goal is
((a.pos+b.pos).toNat:ℤ)−((a.neg+b.neg).toNat:ℤ)
equal to the sum of the two separate differences. Rewrite with DistinctionNat.toNat_add on each component (orbit addition recovers Nat addition), push Nat-to-Int casts inward with push_cast, and finish by ring.
why it matters
This is the basic additive homomorphism that lets every subsequent integer-order and divisibility argument reduce to ordinary Int arithmetic. Downstream it feeds abs_add_le_add_abs (triangle inequality for absolute value), add_le_add and the balanced_add_*_iff family (order and balance are translation-invariant), add_congr_of_balanced, dvdZ_add (divisibility closed under sums), and leQ_add_right (translation invariance of the ratio order on RatioOrbit). Without it the signed-orbit layer could not inherit the additive structure of ℤ while remaining native to recognition orbits. It sits in the foundation stack that supports the arithmetic substrate of the forcing chain, though it does not itself touch T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.