residue_orbit_certificate
plain-language theorem explainer
Assembles the full residue-orbit certificate: modular display of residues on DistinctionNat, congruence as equality of remainders, and closure of that congruence under addition and multiplication. Factorization and character-theory layers cite it as the residue half of the delta-factorization master certificate. The proof is a structure pack that wires already-proved residue lemmas into each certificate field.
Claim. There exists a residue-orbit certificate on nonzero distinction naturals $N$: the residue of $a$ displays as $a\bmod N$; two values are same-residue iff their natural remainders agree; same-residue is an equivalence relation compatible with $+$ and $\times$; and the residue-sum and residue-product operations display as $(a+b)\bmod N$ and $(a\cdot b)\bmod N$.
background
In the Primitive Recognition Calculus factorization layer, DistinctionNat is the native counting type. For nonzero modulus $N$, residue N a is the canonical remainder of $a$ modulo $N$, and sameResidue is the congruence relation that identifies values with equal remainders. The companion operations residueAdd and residueMul lift ordinary sum and product back into the residue class.
The certificate structure packages the display laws (residue and residue-arithmetic equal ordinary modular arithmetic on underlying naturals) together with the algebraic facts that same-residue is reflexive, symmetric, transitive, and closed under addition and multiplication. Upstream lemmas already prove each piece: residue_toNat, sameResidue_iff_mod_eq, the equivalence and congruence lemmas, and the two display identities residueAdd_toNat_mod and residueMul_toNat_mod.
This sits under chart-transition and feeds the broader delta-factorization character-theory stack, where residue orbits are the modular bookkeeping for period and unit-group data.
proof idea
Structure construction, not a deep argument. Each field of ResidueOrbitCertificate is filled by an existing lemma or a one-line intro that applies it:
residue_display:=residue_toNatsame_residue_display:=sameResidue_iff_mod_eqsame_residue_refl:=sameResidue_refl- symmetry and transitivity: intro the hypotheses and apply
sameResidue_symm/sameResidue_trans - add/mul compatibility: intro and apply
sameResidue_add/sameResidue_mul residue_add_display/residue_mul_display:=residueAdd_toNat_mod/residueMul_toNat_mod
No new modular arithmetic is proved here; the certificate only records that the residue-orbit API is fully witnessed.
why it matters
This is the residue-orbit leg of the factorization master certificate. Downstream, delta_factorization_character_theory_certificate installs it beside chart-transition, unit-group, and period-spectrum certificates:
residue_orbit := residue_orbit_certificate
Without a packed residue layer, the character-theory side cannot treat congruence classes, modular addition/multiplication, or period spectra as certified data. In the Recognition foundation stack this is bookkeeping infrastructure rather than a forcing-chain landmark (T5–T8, RCL, phi): it makes the modular arithmetic of distinction counts formally reusable so later factorization and spectral claims can cite one object instead of a scatter of lemmas.
It closes the residue-orbit certificate interface; no scaffolding remains on this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.