FiniteMulCharacter
plain-language theorem explainer
Defines a finite multiplicative character modulo a distinction orbit N: a complex function on orbit representatives that is constant on native residues, sends the unit to 1, and multiplies on δ-coprime residues. Number theorists and RS factorization proofs cite it as the native stand-in for Dirichlet characters on (Z/NZ)*. The declaration is a structure package of three axioms; no proof body.
Claim. A finite multiplicative character modulo a nonzero distinction orbit $N$ is a map $\chi$ from distinction orbits to $\mathbb{C}$ such that (i) if $a$ and $b$ have the same native residue modulo $N$ then $\chi(a)=\chi(b)$, (ii) $\chi(1)=1$, and (iii) whenever $a$ and $b$ are $\delta$-coprime to $N$, $\chi(a\cdot b)=\chi(a)\chi(b)$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive copy of the naturals used as the native carrier for factorization and residue arithmetic. Residues modulo $N$ are compared by the native predicate sameResidue, equality of the residue maps rather than classical modular arithmetic. A residue representative is a unit when it is $\delta$-coprime to $N$ (unitResidue).
This module sits in the factorization layer that builds period spectra and character sums over those orbits. The structure packages the minimal interface of a Dirichlet-style character on the unit group of residues, valued in $\mathbb{C}$, without assuming classical $\mathbb{Z}/N\mathbb{Z}$. The constant-one principal character is the canonical inhabitant of the type.
proof idea
No proof: this is a structure definition. It bundles an evaluation map eval : DistinctionNat → ℂ with three fields: residue-invariance under sameResidue, normalization eval one = 1, and multiplicativity on pairs of unitResidue arguments. Downstream defs (e.g. principal, mul) inhabit the structure by supplying those fields.
why it matters
This is the native character type for the δ-residue factorization layer. It feeds the product of characters, evaluation lemmas, and the finite orthogonality theorem: if left multiplication by a unit $t$ cycles a representative list and $\chi$ is nontrivial on $t$, the character sum over the list vanishes. That orthogonality is the form needed by the residue layer.
The bundled certificate FiniteMulCharacterCertificate records existence and multiplicativity of the principal character, discharged by the constant-one inhabitant. In the broader Recognition stack this is scaffolding for discrete spectral analysis on finite orbits (period spectrum, factorization), not yet the continuous J-cost or T5–T8 forcing chain, but the algebraic character interface those discrete sums rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.