principal_eval
plain-language theorem explainer
The principal finite multiplicative character on distinction residues is the constant function 1. Anyone simplifying character sums or residue maps in the primitive recognition factorization layer cites this. The proof is pure definitional equality from the constant-one constructor.
Claim. For all distinction naturals $N$ and $a$, the evaluation of the principal finite multiplicative character of modulus $N$ at $a$ equals $1$.
background
DistinctionNat is the base-neutral inductive copy of the naturals used as the finite orbit of repeated distinction (K2.12): zero and successor, with decidable equality. It is the ambient index type for residues and periods in the primitive recognition calculus.
A FiniteMulCharacter on modulus $N$ is a multiplicative map on unit residues that respects the residue relation and sends one to one. The principal character is the constant-one instance: its evaluation map is fun _ => 1, with the residue and unit axioms discharged by reflexivity.
This module sits under Foundation.PrimitiveRecognitionCalculus.Factorization and imports the period spectrum. The principal character is the trivial baseline against which non-principal orthogonality and scaled list sums are measured.
proof idea
One-line definitional proof: rfl. Unfolding principal N exposes eval := fun _ => 1, so the equality (principal N).eval a = 1 holds by construction. Marked @[simp] so the constant value rewrites automatically in character-sum goals.
why it matters
Supplies the trivial evaluation identity for the principal character in the finite multiplicative character package. Downstream siblings (map-mul-units, scaled list sums, non-principal orthogonality) treat the constant-one map as the reference character; this simp lemma keeps those reductions mechanical.
In the Recognition Science foundation stack this is bookkeeping inside Primitive Recognition Calculus factorization, not a forcing-chain step (T5–T8). It does not itself force $\phi$, the eight-tick octave, or $D=3$; it only normalizes the trivial character so residue and period arguments can separate principal from non-principal contributions cleanly. No external used-by edges are recorded yet; the lemma is local infrastructure for the certificate and orthogonality results in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.