polyPrimeCost
plain-language theorem explainer
This definition assigns to each irreducible polynomial P over a finite field the value of the J-cost applied to its norm, supplying the base unit for the polynomial cost spectrum. Number theorists extending the integer prime cost spectrum to function fields cite it when building additive cost functions on F[X]. The definition is a direct one-line composition of the J-cost operator with the polynomial norm map.
Claim. For an irreducible polynomial $P$ over a finite field $F$, the prime cost equals $Jcost$ of the norm of $P$, where the norm is $q$ raised to the degree of $P$ and $q$ is the cardinality of $F$.
background
The module develops the cost spectrum on the polynomial ring $F[X]$ as the function-field counterpart to the integer prime cost spectrum. The norm of a monic polynomial $f$ is $q$ to the power of its degree, with $q = |F|$. Every nonzero polynomial factors uniquely into monic irreducibles, and the cost of an irreducible factor $P$ is obtained by feeding its norm into the J-cost function. This yields the per-factor contribution used in the full cost sum over normalized factors.
proof idea
One-line definition that applies the Jcost operator directly to the output of the polynomial norm map on the input irreducible polynomial.
why it matters
The definition supplies the irreducible building block for the polynomial cost spectrum and feeds the master certificate theorem that bundles positivity, multiplicativity, and normalization properties. It mirrors the integer prime cost construction and supports downstream results such as the additive property under multiplication and strict positivity for non-units. In the Recognition Science setting it extends the discrete cost measure to function fields while preserving compatibility with the recognition composition law and the non-negativity of J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.