scaled_list_eval_sum
plain-language theorem explainer
For a finite multiplicative character χ on unit residues modulo N, left-multiplying a list of units by a unit t scales the character sum by χ(t). Anyone proving finite-character orthogonality or assembling the FiniteMulCharacter certificate cites this. The proof is list induction using multiplicativity on units and distributivity of multiplication over addition.
Claim. Let $N$ be a distinction natural, $\chi$ a finite multiplicative character on unit residues modulo $N$, $t$ a unit residue modulo $N$, and $L$ a finite list of unit residues modulo $N$. Then $\sum_{a \in L} \chi(t\cdot a) = \chi(t)\cdot\sum_{a \in L} \chi(a)$.
background
In the Primitive Recognition Calculus factorization layer, residues live on the base-neutral orbit type DistinctionNat (K2.12). A residue representative is a unit modulo $N$ when it is $\delta$-coprime to $N$ (unitResidue).
A FiniteMulCharacter on $N$ is a complex-valued map on orbit representatives that is constant on the native residue relation, sends $1$ to $1$, and is multiplicative on pairs of unit residues: $\chi(ab)=\chi(a)\chi(b)$ whenever both factors are units. Evaluation is written $\chi.\mathrm{eval}$.
The local setting is the finite multiplicative character interface used by the $\delta$ residue layer. Upstream arithmetic supplies distributivity $a(b+c)=ab+ac$ on the logic naturals, which lifts to the list-sum algebra used here.
proof idea
List induction on $L$. The empty list is immediate by simp (both sides zero). For cons a rest, pull the unit hypothesis on the head and the restricted unit hypothesis on the tail, apply the inductive hypothesis to the tail, then rewrite with multiplicativity χ.map_mul_units on the unit pair $(t,a)$ and with mul_add to factor $\chi(t)$ out of the two-term sum. The result is the scaled sum identity.
why it matters
This is the scaling lemma that feeds finite-character orthogonality. Downstream, orthogonality_nonprincipal_sum_zero uses it: if left multiplication by a unit $t$ merely permutes the representative list and $\chi(t)\neq 1$, the character sum over the list vanishes. That orthogonality form is exactly what the $\delta$ residue layer needs.
It also sits under the FiniteMulCharacterCertificate interface and the packaged theorem finite_mul_character_certificate, which record that principal characters exist and multiply on units. In the broader Recognition foundation this is bookkeeping for multiplicative characters on finite unit groups of residue orbits, not yet the T5–T8 forcing chain, but it is the algebraic step that makes non-principal sums cancel in the factorization spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.