toInt_add'
plain-language theorem explainer
The integer display of a sum of two primitive-recognition integers equals the sum of their displays. Anyone assembling the ring structure on these quotient classes, or checking that the verifier map into ordinary integers is a homomorphism, cites this. The proof is a one-line simplification against the orbit-arithmetic simp set.
Claim. Let $a,b$ be primitive-recognition integers (quotient classes of signed orbits under the balanced-length relation). Writing $(\cdot)^{\sim}$ for the verifier display into $\mathbb{Z}$ given by the difference of positive and negative orbit lengths, one has $(a+b)^{\sim}=a^{\sim}+b^{\sim}$.
background
Primitive-recognition integers are the quotient of signed orbits by the internal balanced-length relation. A signed orbit carries a positive and a negative component; its display into $\mathbb{Z}$ is the difference of those components' natural-number lengths. Addition on the quotient is induced from componentwise orbit arithmetic.
The surrounding module (K4.8) builds enough arithmetic on these classes that the verifier display into ordinary integers becomes a ring homomorphism. Upstream recovery maps from logic integers and forced iteration counts supply the concrete $\mathbb{Z}$-values that the display lands on; the present lemma is the additive half of that homomorphism claim.
proof idea
One-line wrapper: a single simp call. Unfolding addition on the quotient and the display on representatives reduces the goal to additivity of length-differences on signed orbits, which is already in the orbit-arithmetic simp set. No manual case split or quotient induction is written by hand.
why it matters
This is the additive half of K4.8: the verifier display from primitive-recognition integers into $\mathbb{Z}$ is a ring homomorphism. The multiplicative companion is the next declaration in the same module. Together they certify that integers forced inside the recognition calculus coincide, as a ring, with ordinary $\mathbb{Z}$ via the display.
No downstream dependents are recorded yet; the lemma is Foundation infrastructure. Integers appear later as iteration counts, rung indices on the $\phi$-ladder, and inputs to the forcing chain (T0–T8), so a clean additive display is a prerequisite rather than a terminal result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.