polyCost_pow
plain-language theorem explainer
Researchers extending the cost spectrum from integers to polynomials over finite fields cite this result to confirm that cost scales linearly with exponentiation. It shows that for nonzero P in F[X] the cost of P to the k-th power equals k times the cost of P. The proof is a straightforward induction on k that invokes the already-established multiplicativity of cost and reduces the arithmetic via ring normalization.
Claim. Let $c$ denote the polynomial cost function on $F[X]$ for a finite field $F$. For any nonzero polynomial $P$ and natural number $k$, $c(P^k) = k · c(P)$.
background
The module develops the cost spectrum for the polynomial ring $F[X]$ over a finite field $F$, serving as the function-field counterpart to the integer prime cost spectrum. The cost of a nonzero polynomial $f$ is defined via the sum over its irreducible factors $P$ of the valuation $v_P(f)$ times $J$ of the norm of $P$, where the norm is $q$ raised to the degree and $J$ is the J-cost function. This builds directly on the multiplicative property in polyCost_mul, which states that cost is additive under multiplication for nonzero polynomials.
proof idea
The proof proceeds by induction on the exponent $k$. The zero case reduces to the fact that any polynomial to the zero power equals 1, whose cost is zero by polyCost_one. In the successor step, the identity $P^{k+1} = P^k · P$ is substituted, polyCost_mul is applied to the nonzero factors, the inductive hypothesis replaces the cost of the lower power, and the resulting real arithmetic is normalized by push_cast followed by ring.
why it matters
This theorem completes the elementary multiplicative properties of the polynomial cost spectrum and feeds directly into the master certificate cost_spectrum_poly_certificate, which bundles the facts for the companion paper. It mirrors the corresponding integer result and confirms that cost behaves as a valuation-like function on the UFD $F[X]$, consistent with the Recognition Science composition law. No open questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.