polyNorm_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply to polynomials over infinite fields.
- Does not give the explicit closed-form expression for polyNorm.
- Does not address the cost function or its additivity.
- Does not require any lower bound on field cardinality beyond positivity.
Lean usage
have hnorm_pos : 0 < polyNorm P := polyNorm_pos Pformal statement (Lean)
72theorem polyNorm_pos (f : Polynomial F) : 0 < polyNorm f := by
proof body
Tactic-mode proof.
73 unfold polyNorm
74 have hq : 0 < (Fintype.card F : ℝ) := by
75 exact_mod_cast Fintype.card_pos
76 exact pow_pos hq _
77
78/-! ## Cost spectrum: per-irreducible and total -/
79
80/-- The cost of an irreducible polynomial `P`, equal to `J(‖P‖)`. -/