mul_eval
plain-language theorem explainer
The pointwise product of two finite multiplicative characters on unit residues modulo N evaluates to the ordinary product of their values at every orbit representative. Anyone building the character ring or discharging the finite-multiplicative-character certificate cites this identity. The proof is pure definitional reflexivity: the product character is defined by multiplying evaluations.
Claim. For any modulus $N$ in the distinction naturals and any two finite multiplicative characters $\chi,\psi$ on unit residues modulo $N$, the product character satisfies $(\chi\cdot\psi)(a)=\chi(a)\,\psi(a)$ for every orbit representative $a$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (the inductive type with zero and successor). Multiplicative structure on this orbit is native: the only unit is the one-step orbit.
A FiniteMulCharacter on modulus $N$ is a complex-valued map on orbit representatives that is constant on the native residue relation, sends the unit to $1$, and multiplies on pairs of unit residues. The sibling constructor mul builds a new character by pointwise complex multiplication of two such maps; the present lemma records that this construction really is pointwise on evaluations.
The ambient module develops factorization tools (period spectrum, character certificates) used later in the forcing chain around discrete recognition structure.
proof idea
One-line term proof by rfl. Because mul is defined so that its eval field is the pointwise product of the two input eval maps, the claimed equality is definitional and needs no further lemmas.
why it matters
Feeds the package theorem finite_mul_character_certificate, which assembles existence of the principal character, multiplicativity, and related certificate fields into a single FiniteMulCharacterCertificate. Without the pointwise product law, the certificate cannot treat the set of finite characters as closed under multiplication.
In the broader Recognition Science foundation this sits inside PrimitiveRecognitionCalculus factorization: discrete multiplicative characters on distinction orbits are the algebraic substrate for period-spectrum arguments that later connect to the eight-tick octave (T7) and related forcing steps. The lemma itself is elementary bookkeeping, but it is the exact identity the certificate proof invokes when it multiplies characters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.