polyCost_one
plain-language theorem explainer
The cost function on the polynomial ring over a finite field vanishes at the constant polynomial 1. Researchers extending the Recognition Science cost spectrum to function fields cite this when establishing additivity and non-negativity of the cost. The proof is a direct simplification after unfolding the definition, relying on the empty factorization of the constant 1.
Claim. Let $F$ be a finite field with cardinality $q$. Let $c$ be the cost on $F[X]$ given by summing $J(q^{d})$ over each irreducible factor of degree $d$ counted with multiplicity. Then $c(1)=0$.
background
This theorem belongs to the module that constructs the cost spectrum on the polynomial ring $F[X]$, the function-field analog of the integer prime cost spectrum. The cost $c(f)$ for nonzero $f$ is defined via the multiset of normalized irreducible factors: $c(f) := sum v_P(f) J(q^{deg P})$, where the norm of an irreducible $P$ is $q^{deg P}$. The constant polynomial 1 has the empty factorization, so its cost is zero by construction.
proof idea
The proof is a term-mode simplification. It unfolds the definition of the cost and applies the fact that the normalized factors of the unit polynomial form the empty multiset, which immediately yields zero.
why it matters
This result supplies the zero-cost case for the master certificate cost_spectrum_poly_certificate, which bundles the elementary properties of the polynomial cost spectrum and is referenced by the companion paper. It mirrors the corresponding integer fact and confirms that cost vanishes on units, consistent with the Recognition Science requirement that cost be zero at the multiplicative identity. It is invoked directly in the induction base of the power rule for cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.