polyPrimeCost_nonneg
plain-language theorem explainer
polyPrimeCost_nonneg establishes that the prime cost of any polynomial over a finite field is nonnegative. Researchers extending the Recognition cost spectrum to function fields cite it as the base nonnegativity result for irreducible factors. The proof reduces directly to the nonnegativity of the J-cost function applied to the positive norm of the polynomial.
Claim. For any polynomial $P$ over a finite field $F$, $0 ≤ J(‖P‖)$ where $‖P‖ = q^{deg P} > 0$ and $J$ is the Recognition cost function.
background
The module develops the cost spectrum on the polynomial ring $F[X]$ as the function-field analog of the integer prime cost spectrum. For a finite field $F$ of cardinality $q$, the norm of a monic polynomial $f$ is $‖f‖ := q^{deg f}$, and polyPrimeCost $P$ is defined as $Jcost(q^{deg P})$ for irreducible $P$. The J-cost function is nonnegative for positive arguments by the upstream lemma Jcost_nonneg, which states $J(x) ≥ 0$ for $x > 0$ via the representation $J(x) = (x-1)^2/(2x)$ and direct verification that the expression is nonnegative.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_nonneg to the positive norm of $P$ supplied by polyNorm_pos.
why it matters
This result is invoked by polyCost_nonneg and polyCost_pos in the same module to establish nonnegativity and conditional positivity of the full cost function on $F[X]$. It supplies the required nonnegativity property for the polynomial analog of the prime cost spectrum, consistent with the J-uniqueness property in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.