polyNorm
Analysts extending the cost spectrum to function fields cite polyNorm as the map sending each polynomial f over finite field F to the real number q raised to the degree of f, with q the field cardinality. This supplies the norm input for Jcost in the subsequent prime cost definition. The implementation is a direct one-line abbreviation using cardinality and natural degree extraction.
claimLet $F$ be a finite field with cardinality $q$. For any polynomial $f$ over $F$, the norm is defined by $||f|| = q^{deg(f)}$.
background
This module develops the cost spectrum on the polynomial ring $F[X]$ as the function-field analog of the integer prime cost spectrum. The norm of a polynomial $f$ is $q$ raised to its degree, where $q$ equals the cardinality of the base field $F$. This norm then feeds the cost via summation of $J$ applied to the norms of irreducible factors, using normalizedFactors to handle multiplicities in the UFD.
proof idea
One-line definition that raises the field cardinality to the natural degree of the input polynomial.
why it matters in Recognition Science
polyNorm supplies the norm used by polyPrimeCost to form Jcost(polyNorm P) for irreducibles, which supports the multiplicative property in polyCost_mul and the nonnegativity results. It realizes the norm step in the function-field cost spectrum, paralleling the integer case and tying into J-uniqueness from the forcing chain.
scope and limits
- Does not compute Jcost or the full polynomial cost.
- Applies to all polynomials, including constants and zero.
- Requires F finite so that Fintype.card is defined.
- Does not address irreducibility or factorization.
Lean usage
def polyPrimeCost (P : Polynomial F) : ℝ := Jcost (polyNorm P)formal statement (Lean)
66def polyNorm (f : Polynomial F) : ℝ :=
proof body
Definition body.
67 (Fintype.card F : ℝ) ^ f.natDegree
68