orthogonality_nonprincipal_sum_zero
plain-language theorem explainer
If a finite multiplicative character χ on unit residues mod N is nontrivial on a unit t, and left multiplication by t merely permutes a list L of unit residues, then the sum of χ over L vanishes. Number theorists and anyone building the δ-residue layer of Recognition factorization will cite this. The proof equates the scaled sum to χ(t) times the original sum, forces (χ(t)−1)S=0, and rules out the left factor by nontriviality.
Claim. Let $N$ be a distinction natural and $\chi$ a finite multiplicative character on unit residues modulo $N$. Let $t$ be a unit residue and $L$ a list of unit residues such that left multiplication by $t$ merely reorders $L$. If $\chi(t)\neq 1$, then $\sum_{a\in L}\chi(a)=0$ in $\mathbb{C}$.
background
The ambient module develops finite multiplicative characters on unit residues modulo a distinction natural $N$. A FiniteMulCharacter is a complex-valued map on orbit representatives that is constant on the native residue relation, sends $1$ to $1$, and multiplies on pairs of unit residues: $\chi(ab)=\chi(a)\chi(b)$ whenever both factors are units mod $N$.
Unit residues are the invertible classes under the native residue relation; the helper unitResidue N a packages that invertibility. The list $L$ is treated as a finite set of such representatives closed under left multiplication by a fixed unit $t$ (the cycle hypothesis). The evaluation sum is ordinary complex list summation.
Upstream, the sibling lemma scaled_list_eval_sum records the multiplicativity identity $\sum_a \chi(t\cdot a)=\chi(t)\sum_a\chi(a)$ under the unit hypotheses. The complex ring has no zero-divisors in the form used here via mul_eq_zero on the difference factor.
proof idea
Write $S:=\sum_{a\in L}\chi(a)$. The cycle hypothesis, pushed through map and sum, gives $\sum_a\chi(t\cdot a)=S$. Multiplicativity via scaled_list_eval_sum rewrites the same scaled sum as $\chi(t)\cdot S$. Hence $\chi(t)\cdot S=S$, so $(\chi(t)-1)S=0$. Complex multiplication has no zero-divisors: either $\chi(t)-1=0$ or $S=0$. The first case contradicts the nontriviality hypothesis $\chi(t)\neq 1$, so $S=0$.
why it matters
This is the finite-character orthogonality identity required by the δ-residue layer of Recognition factorization. It feeds the certificate structure FiniteMulCharacterCertificate and the packing theorem finite_mul_character_certificate, which expose principal existence, multiplicativity, and the nonprincipal vanishing sum as a single Prop interface for downstream factorization code.
In the broader foundation chain, finite multiplicative characters on unit residues sit under the Primitive Recognition Calculus factorization stack (period spectrum, unit group, residue arithmetic). The result is the discrete analogue of classical Dirichlet orthogonality, specialized to the native distinction-natural residue calculus rather than $\mathbb{Z}/n\mathbb{Z}^\times$. It does not itself invoke the T5–T8 forcing landmarks, but it supplies the algebraic cancellation step those layers need when summing over residue orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.