FiniteMulCharacterCertificate
plain-language theorem explainer
Bundles the finite multiplicative character interface used in the δ-residue factorization lane: existence and multiplicativity of the principal character, pointwise product of characters, scaled list sums, and orthogonality of non-principal characters on cycled unit lists. Factorization and master-certificate authors cite it as the ledger entry for that interface. It is a pure Prop structure; no proof lives here.
Claim. A certificate asserting five facts about finite multiplicative characters on unit residues modulo a distinction integer $N$: (i) the principal (constant-one) character satisfies $\chi_0(1)=1$; (ii) $\chi_0(ab)=\chi_0(a)\chi_0(b)$ whenever $a,b$ are units mod $N$; (iii) the product character evaluates pointwise as $(\chi\psi)(a)=\chi(a)\psi(a)$; (iv) for a unit $t$ and a list $L$ of units, $\sum_{a\in L}\chi(ta)=\chi(t)\sum_{a\in L}\chi(a)$; (v) if left multiplication by $t$ merely permutes $L$ and $\chi(t)\neq 1$, then $\sum_{a\in L}\chi(a)=0$.
background
In the Primitive Recognition Calculus factorization layer, residues live on DistinctionNat, the base-neutral finite orbit of repeated distinction. A residue is a unit modulo $N$ when it is δ-coprime to $N$ (unitResidue).
A finite multiplicative character on those units is a complex-valued map on orbit representatives that is constant on the native residue relation, sends $1$ to $1$, and multiplies on unit residues. The principal character is the constant-one map. Characters form a pointwise product monoid.
The two analytic lemmas packaged here are the scaled-list identity (pulling $\chi(t)$ out of a sum after left multiplication by a unit) and the orthogonality form needed by the δ residue layer: if left multiplication by a unit $t$ cycles a chosen representative list and $\chi(t)\neq 1$, the character sum over that list vanishes.
proof idea
No proof body: this is a Prop-valued structure whose five fields are the interface obligations. Downstream, finite_mul_character_certificate fills each field by direct appeal to the corresponding definitions and theorems (principal.map_one, multiplicativity of the principal character, the product-character evaluation rule, scaled_list_eval_sum, and orthogonality_nonprincipal_sum_zero).
why it matters
This certificate is the finite-character ledger entry for the factorization character-theory lane. It is required as the finite_mul_character field of DeltaFactorizationCharacterTheoryCertificate, which aggregates chart transition, residue orbit, unit group, period spectrum, and finite multiplicative character into one master ledger.
In Recognition Science terms, the orthogonality and scaled-sum facts are the discrete Fourier tools that let the δ-residue layer separate principal from non-principal modes when factoring recognition data on finite unit groups. That sits under the Primitive Recognition Calculus factorization stack feeding the foundation forcing chain, not a T0–T8 step itself, but infrastructure for residue-period analysis tied to the eight-tick / period-spectrum side of the story.
The companion theorem finite_mul_character_certificate discharges the structure; this declaration only names the interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.