polyPrimeCost_pos
plain-language theorem explainer
For any polynomial of positive degree over a finite field with at least two elements, the J-cost of its norm is strictly positive. Number theorists building the Recognition Science cost spectrum on polynomial rings cite this when proving nonnegativity for the full cost function. The tactic proof unfolds the definition, shows the norm exceeds one via field cardinality and positive degree, then applies the J-cost positivity lemma.
Claim. Let $F$ be a finite field with cardinality $q$ at least 2. For any polynomial $P$ over $F$ with positive degree, the J-cost of the norm $q$ to the power of the degree satisfies $0 < J(q^{d})$ where $d = $ degree of $P$.
background
The module develops the cost spectrum on the polynomial ring $F[X]$, the function-field analog of the integer prime cost spectrum. The norm of a monic polynomial $f$ is $q$ to the power of its degree, and the prime cost of an irreducible $P$ equals the J-cost of that norm. The full cost of a nonzero polynomial sums the J-cost contributions weighted by multiplicities in the unique factorization into irreducibles.
proof idea
The tactic proof unfolds the definition of the prime cost. It obtains positivity of the norm from the sibling result on polynomial norms. It then shows the norm differs from one by casting the field cardinality to reals and applying one_lt_pow using the positive degree hypothesis. Finally it applies the upstream lemma Jcost_pos_of_ne_one to conclude strict positivity.
why it matters
This result supplies the per-irreducible positivity clause inside the master certificate cost_spectrum_poly_certificate, which bundles the elementary properties and is referenced by the companion paper. It mirrors the integer case and supports extension of the J-cost function to polynomials, consistent with J-uniqueness from the forcing chain. It closes the positivity step without touching open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.