unitResidue_mul_closed
plain-language theorem explainer
The product of two unit residues modulo N is again a unit residue. Anyone assembling the multiplicative monoid of residues coprime to N cites this closure fact. The proof rewrites the unit predicate to ordinary Nat coprimeness, multiplies under toNat, and applies Nat.Coprime.mul_left.
Claim. Let $N,a,b$ be distinction naturals. If $a$ is $\delta$-coprime to $N$ and $b$ is $\delta$-coprime to $N$, then $a\cdot b$ is $\delta$-coprime to $N$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive Peano-style carrier used throughout the primitive recognition calculus. Residues live on this carrier rather than on Lean's built-in Nat.
A residue representative $a$ is a unit modulo $N$ when it is $\delta$-coprime to $N$ (the predicate unitResidue). That predicate is definitionally coprime on DistinctionNat, and the bridge lemma unitResidue_iff_nat_coprime identifies it with ordinary Nat.Coprime on the toNat images.
Multiplication on DistinctionNat is recovered by the orbit-arithmetic theorem toNat_mul (K4.7): $(a\cdot b).\mathrm{toNat}=a.\mathrm{toNat}\cdot b.\mathrm{toNat}$. The same recovery appears in ArithmeticFromLogic for LogicNat. Together these let unit-group facts reduce to classical Nat coprimeness.
proof idea
Term-mode rewrite proof. First rewrite the goal and both hypotheses along unitResidue_iff_nat_coprime, so the claim becomes Nat.Coprime of the toNat images. Then rewrite the product via toNat_mul, replacing $(a\cdot b).\mathrm{toNat}$ by the product of the images. Finish with Nat.Coprime.mul_left on the rewritten hypotheses.
why it matters
This is the multiplicative closure step for the unit-residue structure in the factorization layer of PrimitiveRecognitionCalculus. Downstream, mul packages two UnitResidue values into their product by invoking this lemma on the isUnit fields. The certificate theorem unit_group_certificate records mul_closed by a direct appeal to the same fact, alongside the display bridge and the unit-one lemma.
In the Recognition foundation stack this is pure arithmetic scaffolding under the orbit calculus: it does not itself force phi, the eight-tick octave, or $D=3$, but it supplies the monoid structure needed before residue orbits can support factorization and recognition-composition arguments higher in the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.