IndisputableMonolith.NumberTheory.PrimeCostSpectrumPoly
The PrimeCostSpectrumPoly module defines the norm of a polynomial f over a finite field F as q to the power of its degree, with q the field cardinality. Number theorists extending cost functions to polynomial spectra cite these basic properties when building prime cost models. The module supplies a collection of definitions and elementary lemmas establishing positivity, multiplicativity, and non-negativity.
claimFor a polynomial $f$ over a finite field $F$, define the polynomial norm by $q(f) = q^{deg(f)}$ where $q = |F|$. Related cost functions polyPrimeCost and polyCost adapt this norm to prime and general settings.
background
This module sits in the NumberTheory domain and imports the Cost module to extend its cost functions to polynomials over finite fields. The central object is the norm $q^{deg f}$ with $q = Fintype.card F$, together with derived quantities polyPrimeCost, polyCost, and their variants that record positivity and multiplicativity. The setting uses these polynomial norms to model spectral contributions inside the Recognition Science cost framework.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The polynomial norms supply the concrete objects needed for prime cost spectrum calculations that sit above the Cost module. They support the J-cost and phi-ladder constructions by furnishing multiplicative cost measures on irreducible polynomials.
scope and limits
- Does not treat polynomials over infinite fields.
- Does not compute explicit factorizations or zeta functions.
- Does not link the norms to physical constants or the forcing chain T0-T8.
depends on (1)
declarations in this module (17)
-
def
polyNorm -
theorem
polyNorm_one -
theorem
polyNorm_pos -
def
polyPrimeCost -
def
polyCost -
theorem
polyCost_zero -
theorem
polyCost_one -
theorem
polyPrimeCost_pos -
theorem
polyPrimeCost_nonneg -
theorem
polyCost_nonneg -
theorem
polyCost_mul -
theorem
polyCost_irreducible -
theorem
polyCost_pow -
theorem
polyCost_le_mul -
lemma
irreducible_natDegree_pos -
theorem
polyCost_pos -
theorem
cost_spectrum_poly_certificate