funcFieldNormStructure
funcFieldNormStructure supplies a PrimeNormStructure instance for the set of monic irreducible polynomials over a finite field F with cardinality q at least 2. The norm on each such polynomial is q raised to its degree. Researchers abstracting cost spectra across arithmetic settings would cite this to obtain the function-field case of the universal cost function. The definition directly equips the type with the required norm map and verifies the norm exceeds one via degree positivity for irreducibles.
claimLet $F$ be a finite field with $q = |F| = q_0$ where $q_0$ is an integer at least 2. Let $P$ range over monic irreducible polynomials in the polynomial ring $F[X]$. The set of such polynomials carries a PrimeNormStructure whose norm map sends each $P$ to $q_0$ raised to the degree of $P$.
background
The module UniversalCostSpectrum abstracts the prime cost spectrum to any type equipped with a norm greater than one. A PrimeNormStructure on a type $P$ consists of a map from elements of $P$ to real numbers together with the axiom that every norm value exceeds one. This abstraction covers both ordinary primes in the naturals and monic irreducibles in finite fields, allowing a uniform definition of the universal cost $c(f) = sum_p f(p) J(norm p)$ on finitely supported functions $f$. The present definition instantiates the class for the function-field setting, where the norm is the field cardinality raised to polynomial degree.
proof idea
The definition supplies the norm map directly as cardinality to the power of natDegree. The accompanying norm_gt_one proof first shows that an irreducible polynomial cannot have degree zero, because degree zero would imply it is a nonzero constant and hence a unit, contradicting irreducibility. With positive degree established, the base cardinality exceeds one by the hypothesis, so the power is strictly greater than one by the standard inequality for real exponents.
why it matters in Recognition Science
This definition completes the pair of concrete PrimeNormStructure instances required by the universal cost spectrum abstraction. It supplies the function-field case parallel to the integer-prime case, enabling the uniform statements universalCost_zero, universalCost_add, and universalCost_pos to apply to both settings. The construction directly supports the module's goal of showing that cost-spectrum constructions across the Selberg class arise from a single abstract framework parameterized by any norm-equipped prime structure.
scope and limits
- Does not apply when the base field is infinite.
- Does not include reducible or non-monic polynomials.
- Does not compute explicit J-cost values or sums.
- Does not furnish a global type-class instance usable without parameters.
formal statement (Lean)
198def funcFieldNormStructure (F : Type*) [Field F] [Fintype F]
199 [DecidableEq F] (h2 : 2 ≤ Fintype.card F) :
200 PrimeNormStructure {P : Polynomial F // P.Monic ∧ Irreducible P} where
201 norm := fun P => (Fintype.card F : ℝ) ^ P.val.natDegree
proof body
Definition body.
202 norm_gt_one := fun P => by
203 have hP_irr : Irreducible P.val := P.prop.2
204 have hP_ne : P.val ≠ 0 := hP_irr.ne_zero
205 have hP_deg : 0 < P.val.natDegree := by
206 rw [Nat.pos_iff_ne_zero]
207 intro h_zero
208 obtain ⟨c, hc⟩ := Polynomial.natDegree_eq_zero.mp h_zero
209 have hc_ne : c ≠ 0 := by
210 intro h_c_zero
211 apply hP_ne
212 rw [← hc, h_c_zero]; simp
213 have hP_unit : IsUnit P.val := by
214 rw [← hc]
215 exact Polynomial.isUnit_C.mpr (isUnit_iff_ne_zero.mpr hc_ne)
216 exact hP_irr.not_isUnit hP_unit
217 have hq_real : (1 : ℝ) < (Fintype.card F : ℝ) := by exact_mod_cast h2
218 exact one_lt_pow₀ hq_real (Nat.pos_iff_ne_zero.mp hP_deg)
219
220end
221
222end UniversalCostSpectrum
223end NumberTheory
224end IndisputableMonolith