toInt_add
plain-language theorem explainer
Addition on PRC integers is compatible with the display map into ordinary integers: the integer of a sum equals the sum of the integers. Anyone proving ring laws for LogicInt or PRCInt by transfer to ℤ cites this. The proof is quotient induction on both arguments, then the representative-level additivity lemma for signed orbits.
Claim. For any two PRC integers $a$ and $b$ (equivalence classes of signed orbits under the balanced-length relation), the display map into $\mathbb{Z}$ satisfies $\mathrm{toInt}(a+b)=\mathrm{toInt}(a)+\mathrm{toInt}(b)$.
background
PRC integers are the quotient of signed orbits by the internal balanced-length relation: two signed orbits $a,b$ are equivalent when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. Each class is a primitive recognition calculus integer; the map into ordinary $\mathbb{Z}$ is a downstream verifier display, not part of the internal definition.
A signed orbit carries a positive and a negative distinction-orbit length. Its integer display is the difference of those lengths as naturals coerced to $\mathbb{Z}$. Addition of signed orbits adds the positive parts and the negative parts separately; the representative-level lemma add_toInt already shows that this operation is additive under the display.
The module sits in the Primitive Recognition Calculus layer that builds integers from orbit arithmetic before the LogicInt ring structure is assembled by transfer.
proof idea
Term-mode proof by double quotient induction. Apply Quot.induction_on to $a$, then to $b$, reducing the goal to representatives. After the show that rewrites the quotient addition as SignedOrbit.add, the goal is exactly the representative lemma SignedOrbit.add_toInt, which expands both sides as differences of naturals and rewrites with DistinctionNat.toNat_add. No further case analysis is needed.
why it matters
This is the PRC-side additivity of the integer display. Downstream, the parallel toInt_add on LogicInt and the transfer principle eq_iff_toInt_eq use it (directly or by analogy) to discharge the additive ring axioms: add_assoc', add_comm', add_zero', zero_add', add_left_neg', and the distributive laws mul_add' and add_mul'. Those proofs reduce an identity in the constructed integers to the corresponding identity in $\mathbb{Z}$ via repeated toInt_add rewrites and ring.
In the Recognition Science foundation, integers must arise from recognition/ledger structure rather than being postulated. Establishing that the display is a monoid homomorphism is the bridge that lets ordinary integer arithmetic certify the forced ring laws on the recognition-side integers, feeding the IntegersFromLogic development that underpins later forcing-chain arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.