polyNorm_one
plain-language theorem explainer
The polynomial norm of the constant polynomial 1 over a finite field F equals 1. Researchers extending the Recognition cost spectrum to function fields cite this base case when verifying multiplicativity of the cost function on F[X]. The proof is a one-line wrapper that unfolds the norm definition and simplifies.
Claim. For a finite field $F$ with cardinality $q$, the polynomial norm satisfies $q^{0} = 1$, where the norm of a polynomial $f$ is defined by $q$ raised to the natural degree of $f$.
background
The module develops the cost spectrum on the polynomial ring $F[X]$ as the function-field analog of the integer prime cost spectrum. Here the norm of a polynomial $f$ is the real number $q$ raised to the natural degree of $f$, with $q$ the cardinality of the finite field $F$. This quantity appears directly in the definition of polyNorm, which computes $(Fintype.card F : ℝ) ^ f.natDegree.
proof idea
The proof is a one-line wrapper that unfolds polyNorm and applies the simp tactic.
why it matters
This normalization anchors the unit element in the polynomial cost spectrum and supports the additive property of the cost function under multiplication. It parallels the integer case in the Recognition framework where norms feed into the J-cost via the composition law, and it underpins later results such as the cost of the constant polynomial being zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.