ResidueOrbitCertificate
plain-language theorem explainer
Bundles the residue-orbit layer on distinction naturals: residues match ordinary modular reduction, same-residue is the congruence relation (reflexive, symmetric, transitive, and compatible with + and *), and residue-level sum/product display as modular arithmetic. Factorization character-theory ledgers cite it as a required subcertificate. Pure Prop-structure packing already-proved display and congruence lemmas; no new mathematics inside the structure itself.
Claim. A residue-orbit certificate is a package of nine statements on nonzero moduli $N$ in the distinction-natural orbit: the native residue of $a$ satisfies $\mathrm{toNat}(\mathrm{res}_N(a)) = \mathrm{toNat}(a)\bmod\mathrm{toNat}(N)$; same-residue is equivalent to congruence modulo $N$ and is an equivalence relation compatible with addition and multiplication; residue-level sum and product satisfy $\mathrm{toNat}(\mathrm{resAdd}_N(a,b))=(a+b)\bmod N$ and $\mathrm{toNat}(\mathrm{resMul}_N(a,b))=(ab)\bmod N$.
background
Distinction naturals are the base-neutral finite orbit of repeated distinction (zero and successor), the K2.12 carrier used throughout the primitive recognition calculus. The forward map toNat reads off the iteration count into ordinary Nat, so modular arithmetic can be stated on the image and pulled back.
In this module, the native residue of $a$ modulo a nonzero orbit modulus $N$ is the remainder of $a$ by $N$. Same-residue is equality of those native residues. Residue-level addition and multiplication are ordinary sum/product followed by reduction back to a residue representative.
The certificate sits in the factorization lane after chart transition: it records that the orbit-level residue calculus is faithful to ordinary modular arithmetic and that same-residue is a ring congruence. Upstream siblings already prove each display and congruence fact individually; this structure only names the bundle.
proof idea
No proof body: this is a Prop-valued structure definition whose nine fields are the residue-orbit interface. Inhabitation is deferred to the sibling theorem residue_orbit_certificate, which fills each field by the corresponding lemma (residue_toNat, sameResidue_iff_mod_eq, sameResidue_refl/symm/trans, sameResidue_add/mul, and the residueAdd/Mul display lemmas). Symmetry is discharged by a short intro/rewrite tactic; the rest are direct applications.
why it matters
The master factorization character-theory ledger (DeltaFactorizationCharacterTheoryCertificate) requires a residue_orbit field of exactly this type, alongside chart transition, unit group, period spectrum, and finite multiplicative characters. Without a filled residue-orbit certificate, the factorization lane cannot claim that modular arithmetic on distinction orbits is available for character sums and period spectra.
In the Recognition foundation stack this is scaffolding for arithmetic-from-logic: once residues behave as $\mathbb{Z}/N\mathbb{Z}$ on the orbit carrier, later steps can talk about multiplicative characters and factorization without leaving the native distinction language. It does not itself touch T5–T8 or the J-cost; it is pure arithmetic infrastructure under the primitive recognition calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.