polyCost_one
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not claim positivity or lower bounds for non-unit polynomials.
- Does not depend on the specific cardinality of the base field.
- Does not address non-monic representatives beyond the normalization already built into the definition.
- Does not extend the cost to the zero polynomial.
Lean usage
simp [polyCost_one]formal statement (Lean)
95@[simp] theorem polyCost_one : polyCost (1 : Polynomial F) = 0 := by
proof body
Term-mode proof.
96 unfold polyCost
97 simp [normalizedFactors_one]
98
99/-- The norm of a monic polynomial of positive degree is at least `q ≥ 2`,
100 hence at least `2`. Combined with `Jcost_pos_of_ne_one`, this gives
101 `polyPrimeCost P > 0` for any irreducible polynomial of positive degree
102 over a field with at least 2 elements. -/