mul
plain-language theorem explainer
Pointwise product of two finite multiplicative characters on unit residues modulo N is again a finite multiplicative character. Anyone building character sums, orthogonality, or period-spectrum factorizations in the primitive recognition calculus will cite this. The construction is a structure instance: eval multiplies pointwise and the three axioms are discharged by rewriting with each factor's axioms plus ring arithmetic.
Claim. Let $N$ be a distinction-natural and let $\chi,\psi$ be finite multiplicative characters on unit residues modulo $N$ (complex-valued maps constant on native residue classes, sending $1$ to $1$, and multiplicative on unit residues). Their product $\chi\psi$, defined by $(\chi\psi)(a)=\chi(a)\psi(a)$ for every orbit representative $a$, is again a finite multiplicative character modulo $N$.
background
The ambient type is DistinctionNat, the base-neutral finite orbit of repeated distinction (K2.12): an inductive copy of the naturals used as orbit representatives rather than ordinary $\mathbb{N}$.
A finite multiplicative character on unit residues modulo $N$ is a complex-valued map on those representatives that (i) is constant on the native residue relation sameResidue, (ii) sends the unit $1$ to $1$, and (iii) multiplies on pairs of unit residues: $\chi(ab)=\chi(a)\chi(b)$ whenever both factors are units mod $N$. This is the structure FiniteMulCharacter N.
The module sits in the factorization layer of the primitive recognition calculus, imported alongside the period spectrum. Characters here are the discrete multiplicative data used to probe residue orbits and period factorizations, not yet the continuous $J$-cost of the forcing chain.
proof idea
Structure construction, not a deep lemma. Set eval to the pointwise product $a\mapsto\chi(a)\psi(a)$. Residue invariance: if $a$ and $b$ are same residue mod $N$, rewrite each factor by its respects_residue axiom. Value at one: rewrite by both map_one fields and close with norm_num ($1\cdot 1=1$). Multiplicativity on units: rewrite by both map_mul_units fields and finish with ring on $\mathbb{C}$.
why it matters
Closes the monoid structure on finite multiplicative characters under pointwise product, so the character group (or at least the monoid) is available inside the Lean development. Downstream siblings in the same module include evaluation lemmas, scaled-list sum identities, and the non-principal orthogonality sum-zero statement; those proofs need a well-typed product of characters. In the broader Recognition framework this is scaffolding for discrete spectral analysis on distinction orbits (period spectrum / factorization), not a direct T0–T8 forcing step. No used_by edges are recorded yet, so the immediate consumers are the in-module certificate and orthogonality results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.