residueAdd_toNat_mod
plain-language theorem explainer
Residue-class addition on distinction orbits, read out as a natural number, is ordinary modular addition of the two summands. Anyone building modular arithmetic on the Recognition orbit (factorization, residue certificates) cites this. The proof is a two-line unfold-and-rewrite through the residue readout and the addition recovery theorem.
Claim. For a nonzero modulus $N$ on the distinction orbit and any orbit positions $a,b$, the natural-number readout of the residue-class sum of $a$ and $b$ equals $(a^{\#}+b^{\#})\bmod N^{\#}$, where $(\cdot)^{\#}$ is the verifier map from orbit positions to $\mathbb{N}$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, carrying its own addition and multiplication. The verifier map toNat reads an orbit position as a Lean natural number by counting steps from zero.
Residue arithmetic lives one level up. The residue of an orbit position $a$ modulo nonzero $N$ is the canonical representative of $a$ in the residue class; its readout theorem states that this representative maps to $a^{#}\bmod N^{#}$. Residue-level addition is defined by adding on the orbit and then taking that residue: $\mathrm{resAdd}_N(a,b):=\mathrm{res}_N(a+b)$.
Upstream, the ArithmeticFromLogic recovery theorem already guarantees that orbit addition agrees with ordinary Nat addition under the readout map. Together these facts pin modular addition on residues to ordinary modular arithmetic on $\mathbb{N}$.
proof idea
Term-mode, two rewrites after unfolding. Unfold the definition of residue-level addition to expose $\mathrm{res}_N(a+b)$. Apply the residue readout theorem to replace the left-hand side by $(a+b)^{#}\bmod N^{#}$. Finish with the addition recovery theorem, which rewrites $(a+b)^{#}$ as $a^{#}+b^{#}$. No induction or case split is required.
why it matters
This is the addition half of the residue-orbit display package. It feeds directly into residue_orbit_certificate, which bundles residue readout, same-residue equivalence, and the modular laws into a single certificate that factorization and chart-transition code can consume.
In the Primitive Recognition Calculus, factorization of orbit positions is organized by residue classes modulo a nonzero orbit modulus. Without a proved bridge from residue addition to ordinary modular addition, downstream certificates would have to re-derive the modular law at every use site. The companion multiplication statement and the same-residue congruence lemmas sit beside it in the same module; together they close the arithmetic interface for residue orbits before any physics-facing forcing step (T5–T8) is invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.