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 converting period-spectrum data into character sums. The development is definitional plus elementary algebraic identities.

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 a full set of scaled residues.

background

In the Primitive Recognition Calculus factorization stack, period data live on residue orbits modulo a fixed $N$. A finite multiplicative character is the standard number-theoretic device that turns those orbits into complex amplitudes while preserving multiplication on $(\mathbb{Z}/N\mathbb{Z})^\times$.

The module sits directly on PeriodSpectrum: orbit representatives and the native residue relation are already fixed there. Here one equips those representatives with a $\mathbb{C}$-valued function that is constant on the residue relation and is a group homomorphism on units. The principal character is the trivial homomorphism; the product of two characters is again a character.

Orthogonality for non-principal characters (the sum over a complete scaled list of residues vanishes) is the analytic identity that later converts spectral support into quantitative lower bounds on recognition cost.

proof idea

Definition module with supporting algebraic lemmas. FiniteMulCharacter packages the residue-compatible multiplicative map. principal and principal_eval record the trivial character and its values; mul and mul_eval give the pointwise product and its evaluation. scaled_list_eval_sum and orthogonality_nonprincipal_sum_zero establish the standard complete-sum identity for non-principal characters. FiniteMulCharacterCertificate and finite_mul_character_certificate package a checkable witness that a given map meets the character axioms. No deep analytic input; proofs are direct from the multiplicative and residue axioms.

why it matters in Recognition Science

RecognitionLowerBound imports this module to turn period-spectrum support into character-sum estimates. In the Recognition Science factorization path, lower bounds on recognition cost need a clean separation between the trivial (principal) mode and oscillating non-principal modes; the orthogonality identity supplies that separation.

The construction is classical Dirichlet-character arithmetic, specialized to the orbit-representative presentation used by PeriodSpectrum. It does not itself force physical constants, but it is the bridge from discrete period data to the quantitative recognition lower bound that feeds the broader Primitive Recognition Calculus.

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)