Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.FiniteMulCharacter

show as:
view Lean formalization →

Defines finite multiplicative characters on unit residues modulo N as complex-valued maps on orbit representatives that respect the native residue relation and multiply on units. Supplies the principal character, pointwise multiplication, evaluation identities, and the non-principal orthogonality sum. Recognition-lower-bound arguments cite this layer when they need character sums over the period spectrum.

claimA finite multiplicative character modulo $N$ is a map $\chi$ from orbit representatives of unit residues to $\mathbb{C}$ such that $\chi$ is compatible with the native residue relation and $\chi(ab)=\chi(a)\chi(b)$ on units. The principal character is identically $1$ on units; characters multiply pointwise; non-principal characters satisfy $\sum \chi = 0$ on the relevant scaled lists.

background

In the Primitive Recognition Calculus factorization stack, one works with residues modulo a period $N$ drawn from the period spectrum. Unit residues form a multiplicative monoid; orbit representatives give a finite set of labels on which analytic objects can be evaluated.

A finite multiplicative character is the discrete analogue of a Dirichlet character: a complex-valued function on those representatives that respects the residue identification and is completely multiplicative on units. The principal character is the constant-$1$ character on units. Pointwise products of characters remain characters.

The module sits directly on PeriodSpectrum, which supplies the ambient period and residue geometry. Downstream RecognitionLowerBound imports these characters to control recognition sums via orthogonality.

proof idea

Definition-first module. FiniteMulCharacter packages the character data and the multiplicative law. principal and principal_eval build the trivial character and its evaluation. mul and mul_eval close characters under pointwise product. scaled_list_eval_sum and orthogonality_nonprincipal_sum_zero establish the standard sum-to-zero identity for non-principal characters on scaled residue lists. FiniteMulCharacterCertificate and finite_mul_character_certificate package a checkable witness that a given map is such a character.

why it matters in Recognition Science

Character orthogonality is the standard tool that isolates the principal contribution in multiplicative sums. RecognitionLowerBound imports this module to convert period-spectrum residue sums into lower bounds on recognition cost: non-principal modes cancel, leaving only the principal term that feeds the recognition inequality.

Within the broader Foundation forcing chain, factorization and period structure sit under the eight-tick octave and the discrete residue geometry that eventually constrain spatial dimension and the cost functional $J$. This module does not itself force $J$ or $\varphi$; it supplies the multiplicative Fourier layer those later bounds need.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)