polyNorm_pos
plain-language theorem explainer
The norm of any polynomial over a finite field is strictly positive. Number theorists working in function fields cite this when proving positivity of J-costs on irreducible factors. The short tactic proof unfolds the definition of polyNorm as a power of the field cardinality and applies the standard fact that a positive real raised to any exponent remains positive.
Claim. For any polynomial $f$ over a finite field $F$ with cardinality $q$, the polynomial norm satisfies $0 < q^{deg f}$.
background
This module is the function-field analog of the integer prime cost spectrum. It equips the polynomial ring $F[X]$ over a finite field $F$ with a cost function built from the norm $‖f‖ := q^{deg f}$ and the J-cost applied to irreducible factors. The cost of a general polynomial is the sum of $J(‖P‖)$ weighted by multiplicities in its normalized factorization.
proof idea
The proof is a short tactic sequence: unfold polyNorm, obtain $0 < q$ from Fintype.card_pos via exact_mod_cast, then conclude by pow_pos.
why it matters
This lemma supplies the positivity of the norm that is invoked by polyPrimeCost_nonneg and polyPrimeCost_pos. It completes the base case for the cost spectrum on $F[X]$, ensuring every irreducible factor carries positive J-cost exactly as required by the multiplicative cost axioms and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.