principal
plain-language theorem explainer
The constant-one principal multiplicative character on unit residues modulo a finite distinction orbit N. Anyone writing character sums, residue factorization, or cost-gauge classification over native orbits cites it as the trivial baseline. The instance sets every evaluation to 1 and discharges the structure axioms by reflexivity and a one-line arithmetic check.
Claim. For every finite distinction orbit $N$, the principal character $\chi_0$ on unit residues modulo $N$ is the complex-valued map with $\chi_0(a)=1$ for every orbit representative $a$. It is constant on native residue classes, sends the multiplicative unit to $1$, and satisfies $\chi_0(ab)=\chi_0(a)\chi_0(b)$ whenever $a$ and $b$ are unit residues.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive copy of the naturals used as orbit representatives rather than ordinary $\mathbb{N}$. Residues and unit residues are taken relative to a fixed nonzero modulus $N$ in that type.
A finite multiplicative character on unit residues modulo $N$ is a complex-valued function on those representatives that (i) is constant on the native same-residue relation, (ii) sends the unit to $1$, and (iii) multiplies on pairs of unit residues. The structure packages exactly those three axioms; no analytic continuation or Dirichlet $L$-function data is present at this layer.
The local module builds the character toolkit used later for factorization of recognition costs and for real-trace candidates on ratio orbits. The principal character is the constant-one inhabitant of that structure.
proof idea
Direct structure instance. Evaluation is the constant function $a\mapsto 1$. Residue-invariance is reflexivity of equality on the constant value. The unit axiom is definitional. Multiplicativity on unit residues reduces to $1\cdot 1=1$, discharged by norm_num. No external lemmas are required.
why it matters
This is the trivial baseline character against which non-principal characters and orthogonality sums are measured in the same module (certificate constructors and the non-principal sum-to-zero lemma). Downstream cost work uses it when classifying anchor-free structural costs as sign or odd-power families, when checking that small real-character traces are rational, and when relating real trace roots to additive inverses. Constants identities such as the light-cone relation $\ell_0=c\cdot\tau_0$ sit in the same dependency neighborhood of the factorization stack. In the broader Recognition chain it supplies the unit of the multiplicative character group on finite distinction orbits, the discrete side of the factorization that eventually feeds J-cost and gauge-orbit analysis (T5 and the RCL layer), without yet forcing $\phi$ or the eight-tick period.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.