funcFieldNormStructure
plain-language theorem explainer
funcFieldNormStructure equips the set of monic irreducible polynomials over a finite field F (q >= 2) with the norm q to the degree, satisfying the axioms of a PrimeNormStructure. Researchers extending the universal cost spectrum to function fields in the Selberg class would cite this construction. The definition directly supplies the norm map and verifies the strict inequality greater than one via degree positivity for irreducibles.
Claim. Let $F$ be a finite field with cardinality $q = |F|$, where $q >= 2$. The set of monic irreducible polynomials $P$ over $F$ carries the norm structure given by $||P|| = q^{deg P}$, which satisfies $||P|| > 1$ for every such $P$.
background
PrimeNormStructure is the typeclass requiring a type P together with a map norm : P → ℝ such that norm p > 1 for all p. The module abstracts this from integer primes and from monic irreducibles in F_q[T], then builds the universal cost c(f) := Σ_p f(p) · J(||p||) on finitely supported functions f : P →₀ ℕ. This setting supports the Cost-Reciprocity synthesis by treating both classical and function-field cases uniformly under one arithmetic function.
proof idea
The definition supplies the norm map directly as q raised to the natural degree. The accompanying norm_gt_one proof proceeds by contradiction on degree zero: an irreducible of degree zero is a nonzero constant, hence a unit, contradicting irreducibility; the base q > 1 then yields the strict inequality via the power rule.
why it matters
This definition supplies the function-field instance of PrimeNormStructure, allowing the universalCost construction and its elementary properties (additivity, positivity) to apply to L-functions over finite fields. It parallels the integer-prime case inside the same abstract framework described in the module documentation for the Cost-Reciprocity synthesis paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.