module module moderate

`IndisputableMonolith.NumberTheory.PrimeCostSpectrumPoly`

This module defines polynomial norm and cost functions over finite fields to support prime cost spectrum calculations in Recognition Science number theory. It centers on polyNorm as q to the degree of a polynomial, with q the field cardinality, plus variants like polyPrimeCost and polyCost along with their basic algebraic properties. The module imports the Cost module and consists entirely of definitions and elementary lemmas. It supplies the algebraic machinery needed for spectrum constructions without containing complex proofs.

claimFor a polynomial $f$ over a finite field $F$, the norm is defined by $q = |F|$ and $||f|| = q^{deg(f)}$. Related maps include polyPrimeCost and polyCost, satisfying non-negativity, multiplicativity, and positivity at 1.

background

The module sits in the NumberTheory domain and imports Mathlib together with IndisputableMonolith.Cost. It extends cost concepts from the Cost module to the polynomial ring over a finite field, using the standard Fintype.card construction for the base $q$. The central definition is the real-valued norm $q^{deg(f)}$ that converts polynomial degree into a multiplicative cost measure.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the polynomial cost primitives that feed the prime-cost-spectrum constructions in the Recognition Science framework. It provides the algebraic layer required for spectrum analysis of prime costs, connecting directly to the Cost module and the broader number-theoretic components of the monolith.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (17)

def polyNorm L66
theorem polyNorm_one L69
theorem polyNorm_pos L72
def polyPrimeCost L81
def polyCost L86
theorem polyCost_zero L91
theorem polyCost_one L95
theorem polyPrimeCost_pos L103
theorem polyPrimeCost_nonneg L118
theorem polyCost_nonneg L122
theorem polyCost_mul L134
theorem polyCost_irreducible L145
theorem polyCost_pow L157
theorem polyCost_le_mul L168
lemma irreducible_natDegree_pos L179
theorem polyCost_pos L200
theorem cost_spectrum_poly_certificate L240