finite_mul_character_certificate
plain-language theorem explainer
Packages the finite multiplicative character interface into a single Prop certificate: principal character exists and multiplies on unit residues, products evaluate pointwise, scaled list sums factor, and nonprincipal characters sum to zero under unit cycling. Cited by the δ-factorization master certificate. Proof is a field-by-field wiring of already-proved lemmas.
Claim. There exists a certificate asserting: (i) for every modulus $N$, the principal finite multiplicative character evaluates to $1$ at the unit; (ii) that principal character is multiplicative on unit residues modulo $N$; (iii) the pointwise product of two characters evaluates as the product of evaluations; (iv) after left multiplication by a unit, the sum of a character over a finite representative list equals the character of the unit times the unscaled sum; (v) if left multiplication by a unit cycles the list and the character is nontrivial on that unit, the sum vanishes.
background
In the Primitive Recognition Calculus factorization layer, a finite multiplicative character on unit residues modulo a distinction-natural $N$ is a complex-valued map on orbit representatives that respects the native residue relation, sends the unit to $1$, and multiplies on unit residues. The constant-one map is the principal character.
The certificate structure collects five interface facts needed downstream: existence and multiplicativity of the principal character, pointwise evaluation of character products, the scaled-list sum identity, and the orthogonality form used by the δ residue layer (if left multiplication by a unit $t$ cycles a representative list of units and the character is nontrivial on $t$, the sum over the list is zero).
These facts live in the same module as the character structure and are already proved individually; the certificate is the Prop that packages them for the master factorization certificate.
proof idea
Structure-mode construction of FiniteMulCharacterCertificate. Each field is discharged by a one-line application of an existing lemma:
principal_existsusesmap_oneof the constant-one principal character.principal_multiplicativeappliesprincipal_map_mul_units.character_product_evalismul_eval(definitional,rfl).scaled_list_eval_sumreuses the same-named theorem on left-multiplied representative lists.orthogonality_nonprincipal_sum_zeroreuses the same-named orthogonality theorem for nontrivial characters under unit cycling.
No new algebra is performed; the proof only assembles prior results into the certificate record.
why it matters
Feeds directly into delta_factorization_character_theory_certificate in the MasterCertificate module, which aggregates chart transition, residue orbit, unit group, period spectrum, and this character-theory certificate into the δ-factorization master bundle.
In the Recognition Science foundation, finite multiplicative characters on unit residues supply the discrete Fourier/orthogonality tool used when factoring recognition distinctions along residue orbits. The packaged orthogonality (nonprincipal sum zero under unit cycling) is the form required by the δ residue layer. Without this certificate, the master factorization certificate cannot close the character-theory slot.
No open scaffolding remains here: claim status is proved, and the downstream master certificate consumes it as a completed interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.