toRat_add'
plain-language theorem explainer
Addition of PRC rationals commutes with the verifier map into ordinary rationals: the display of a sum is the sum of the displays. Anyone building the real-completion or square-gap layer from PRC rationals cites this. The proof is a one-line simp wrapper over the underlying quotient arithmetic.
Claim. For any two PRC rationals $a$ and $b$ (nonzero-denominator ratio-orbit quotient classes), the verifier display satisfies $(a+b)^{\sim} = a^{\sim} + b^{\sim}$ in $\mathbb{Q}$, where $(\cdot)^{\sim}$ is the map sending a ratio orbit to the ordinary rational formed by its integer numerator over its natural denominator.
background
PRC rationals are the K4.8 construction: quotient classes of ratio orbits with nonzero denominator, identified when cross-multiplication of orbit-level numerators and denominators agrees. They sit in the Primitive Recognition Calculus stack that builds integers, then rationals, then reals from recognition orbits rather than from classical set-theoretic foundations.
The verifier map toRat (spec tag A5) is a transport wrapper: on a ratio orbit it returns $(\mathrm{num.toInt}:\mathbb{Q})/(\mathrm{den.toNat}:\mathbb{Q})$. On the quotient PRCRat it descends to a well-defined map into ordinary rationals. The companion recovery map from the RationalsFromLogic layer plays the same role for logic-level rationals.
This lemma is the additive half of the statement that the verifier is a ring homomorphism from PRC rationals into $\mathbb{Q}$. Multiplicative companions appear alongside it in the same module.
proof idea
One-line wrapper: simp discharges the goal. The simp set already knows how addition is defined on the quotient, how toRat lifts through the quotient, and that ordinary rational addition matches the transported formula. No manual case split on representatives is required.
why it matters
The real-completion embedding uses this directly: ofRat_add rewrites ofRat (a + b) = ofRat a + ofRat b by unfolding ofRat and applying this identity, then normalizing. The Cauchy/square-gap layer likewise needs it: PRCSquareGap_toRat expands the square-gap display as $1+(a^{\sim}-b^{\sim})^2$ via toRat_add' and the multiplicative twin toRat_mul'.
In the broader Recognition stack this is plumbing, not a forcing-chain landmark. It keeps the K4 rational layer honest so later continuity and completeness arguments (and the K7 first-pass kernel certificate that depends on the same arithmetic surface) can treat verifier equality as ordinary rational arithmetic. Without additivity of the display, the passage from orbit rationals to completed reals would not be a homomorphism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.