ofInt_add
plain-language theorem explainer
The embedding of ordinary integers into PRC integers preserves addition: ofInt(m+n) equals the PRC sum of the two images. Anyone building arithmetic on the primitive recognition calculus integer layer cites this when commuting sums past the embedding. The proof is a two-step reduction: injectivity of the toInt display, then simplification of the displays.
Claim. For all $m,n\in\mathbb{Z}$, the PRC embedding of verifier integers satisfies $\mathrm{embed}(m+n)=\mathrm{embed}(m)+_{\mathrm{PRC}}\mathrm{embed}(n)$, where $\mathrm{embed}$ routes positive and negative parts through the $\delta$-orbit and $+_{\mathrm{PRC}}$ is addition of PRC integers.
background
In the primitive recognition calculus (PRC), integers are not taken as primitive. A PRC integer is built from a signed pair of distinction-naturals on the $\delta$-orbit; the constructor ofInt embeds a verifier integer $n\in\mathbb{Z}$ by sending the positive part $n.\mathrm{toNat}$ and the negative part $(-n).\mathrm{toNat}$ each through DistinctionNat.ofNat, then packaging them as a PRC integer.
The reverse display toInt recovers a verifier integer from a PRC integer. Upstream result K4.8 states that this display is injective: distinct PRC integers have distinct verifier displays. That injectivity is the standard way to prove equalities in the PRC integer type without unfolding the quotient representation.
This module sits in the Foundation layer of the forcing chain, where integer and rational structure is reconstructed from recognition primitives rather than assumed from Mathlib's $\mathbb{Z}$.
proof idea
Two-line tactic proof. First apply injectivity of the toInt display: it suffices to show the two sides have equal verifier integers. Then simp rewrites both sides using the simplification lemmas for toInt, ofInt, and PRC addition, reducing the goal to the ordinary integer identity $(m+n)=m+n$, which closes automatically.
why it matters
This is a basic homomorphism law for the integer embedding into PRC. Without it, every later arithmetic identity that mixes verifier $\mathbb{Z}$ with PRC integers would have to re-prove that sums transport. It belongs to the Foundation reconstruction of integer structure from recognition primitives (the same layer that forces discrete counting before the T5–T8 chain on $J$, $\varphi$, the eight-tick octave, and $D=3$).
No downstream dependents are recorded yet in the graph, so the lemma is presently a local simp fact for the IntegerRational module rather than a cited step in a paper proposition. It closes the additive half of the embedding interface; the multiplicative companion, if present nearby, would complete the ring-homomorphism picture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.