polyCost
plain-language theorem explainer
The polynomial cost function sums the J-costs of normalized irreducible factors of a polynomial over a finite field, assigning zero to the zero polynomial by convention. Researchers extending the Recognition Science cost spectrum from integers to function fields cite this as the direct analog. It is realized as a one-line wrapper that maps the irreducible cost over normalized factors and sums the image.
Claim. Let $F$ be a finite field with cardinality $q$. For a polynomial $f$ over $F$, the cost is $c(f) = sum J(q^{deg P})$, where the sum runs over the normalized irreducible factors $P$ of $f$ counted with multiplicity, and $c(0) = 0$.
background
This module develops the cost spectrum on the polynomial ring $F[X]$ as the function-field analog of the integer prime cost spectrum. The norm of a monic irreducible $P$ of degree $n$ is $q^n$, and the irreducible cost equals $J$ applied to this norm. The polynomial cost aggregates these via the multiset of normalized factors, which is well-defined in any UFD.
proof idea
The definition is a one-line wrapper that maps the irreducible cost function over the normalized factors of the input polynomial and sums the resulting multiset.
why it matters
This definition supplies the core cost function for the polynomial ring and is invoked by the master certificate that bundles positivity, additivity under multiplication, and nonnegativity. It mirrors the integer cost spectrum and supports the Recognition Science extension of the J-uniqueness and phi fixed point to polynomial norms on the phi-ladder. The construction feeds the forcing chain steps toward D=3 and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.