polyCost_le_mul
plain-language theorem explainer
Cost on polynomials over a finite field is monotonic under multiplication by nonzero factors. Workers on the Recognition cost spectrum in function fields cite the result to order elements by their J-weighted factorizations. The proof rewrites the product via additivity of cost and applies nonnegativity of the second factor's cost through linear arithmetic.
Claim. Let $F$ be a finite field. Let $c$ be the cost on $F[X]$ given by summing $J(q^{d})$ over irreducible factors $P$ of degree $d$, each weighted by its multiplicity. For nonzero $f,g$ in $F[X]$, $c(f) ≤ c(f g)$.
background
This module constructs the cost spectrum on the polynomial ring $F[X]$ over a finite field $F$ of cardinality $q$, serving as the function-field counterpart to the integer prime-cost spectrum. The cost $c(f)$ for nonzero $f$ is defined from the unique factorization into monic irreducibles via $c(f) = ∑ v_P(f) · J(q^{deg P})$, where the sum runs over the normalized irreducible factors and $J$ is the Recognition cost function. The module records that $F[X]$ is a UFD, that the norm of a monic irreducible of degree $n$ is $q^n$, and that cost extends to all nonzero polynomials through normalized factors.
proof idea
One-line wrapper that applies the additivity lemma for cost under multiplication and then invokes nonnegativity of the second factor's cost, followed by linear arithmetic to obtain the inequality.
why it matters
The result supplies the monotonicity property required to compare costs across multiples in the polynomial spectrum. It rests on the additivity and nonnegativity statements proved in the same module, which themselves rest on the definition of cost via the J-function applied to field norms. Within the Recognition framework this aligns with the J-uniqueness step of the forcing chain and the composition law for costs; the declaration closes one ordering gap in the function-field analog but records no downstream applications yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.