polyCost_pos
plain-language theorem explainer
The result shows that every nonzero non-unit polynomial over a finite field with cardinality at least 2 has strictly positive cost in the Recognition Science polynomial cost spectrum. Number theorists extending the prime cost spectrum to function fields would cite this lemma when establishing non-negativity and positivity properties. The proof extracts an irreducible factor from the normalized factorization and combines its positive prime cost with the non-negativity of the remaining terms.
Claim. Let $F$ be a field with $|F| = q$ where $q$ is an integer satisfying $q$ at least 2. If $f$ is a nonzero polynomial in $F[X]$ that is not a unit, then the cost $c(f)$ satisfies $c(f) > 0$, where $c(f)$ denotes the sum of the $J$-costs of the normalized irreducible factors of $f$.
background
The module develops the cost spectrum for the polynomial ring $F[X]$ over a finite field $F$ as the function-field analog of the integer prime cost spectrum. The cost $c(f)$ is computed from the multiset of normalized factors of $f$ via the sum of prime costs, each equal to the $J$-cost of the norm $q$ raised to the degree of the irreducible factor. This construction relies on the $J$-cost induced by multiplicative recognizers and the non-negativity properties of recognition events.
proof idea
The tactic proof first shows that the normalized factors multiset cannot be empty, as that would force $f$ to be a unit. It extracts an irreducible factor $P$ of positive degree, invokes the positivity of its prime cost, decomposes the multiset sum into the contribution from $P$ plus the image of the remainder, and applies add_pos_of_pos_of_nonneg together with the non-negativity of every prime cost term.
why it matters
This supplies the strict positivity needed for the master certificate that bundles the elementary properties of the polynomial cost spectrum and mirrors the integer version used by the companion paper. It ensures the cost function acts as a positive measure on the polynomial ring, consistent with the $J$-cost structure from the multiplicative recognizer and the forcing chain. The result closes one link in the chain of cost-spectrum theorems without introducing new scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.