principal_map_mul_units
plain-language theorem explainer
The constant-one principal character on unit residues modulo N is multiplicative: its value on a product equals the product of its values, whenever both factors are δ-coprime to N. Number theorists and RS factorization proofs cite this when assembling the finite-multiplicative-character certificate. The proof is a one-line projection of the structure field map_mul_units.
Claim. Let $N,a,b$ be distinction naturals. If $a$ and $b$ are unit residues modulo $N$ (i.e., $\delta$-coprime to $N$), then the principal finite multiplicative character $\chi_1$ satisfies $\chi_1(ab)=\chi_1(a)\,\chi_1(b)$.
background
In the Primitive Recognition Calculus factorization layer, residues live on DistinctionNat, the base-neutral finite orbit of repeated distinction. A residue $a$ is a unit modulo $N$ when it is $\delta$-coprime to $N$ (unitResidue).
A finite multiplicative character on those units is a residue-respecting map that sends $1$ to $1$ and multiplies on unit pairs. The principal character is the constant map $\mathrm{eval}\equiv 1$. Multiplicativity for general $J$-automorphisms is already recorded in CostAlgebra (multiplicative), but here the object is the discrete character structure, not a continuous $J$-auto.
Local setting: FiniteMulCharacter packages the discrete Dirichlet-style characters used to factor recognition orbits and certify orthogonality sums.
proof idea
One-line term proof. The principal character is constructed as a FiniteMulCharacter N, so it already carries a map_mul_units field. The proof is exact (principal N).map_mul_units ha hb, discharging the two unit-residue hypotheses and returning the required equality on evaluations.
why it matters
Feeds finite_mul_character_certificate, which packages existence of the principal character together with its multiplicativity on units. That certificate is the discrete analogue of the trivial Dirichlet character and is the base case for orthogonality and factorization arguments in the Primitive Recognition Calculus.
In the broader RS chain this sits under foundation factorization infrastructure rather than a numbered T0–T8 forcing step: it supplies the trivial multiplicative character needed before non-principal characters and period-spectrum comparisons can be stated cleanly. Without principal multiplicativity, the certificate structure cannot close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.