polyCost_nonneg
The cost function on polynomials over a finite field is nonnegative for every polynomial. Researchers establishing positivity properties of the function-field cost spectrum cite this result when building the master certificate. The proof unfolds polyCost to a multiset sum over normalized irreducible factors and reduces each term to the nonnegativity of polyPrimeCost via the multiset sum lemma.
claimFor every polynomial $f$ over a finite field $F$, the cost $c(f)$ satisfies $c(f) ≥ 0$, where $c(f) = ∑ v_P(f) · J(q^{deg P})$ sums the $J$-costs of the normalized irreducible factors of $f$.
background
In this module the polynomial ring $F[X]$ over a finite field $F$ of cardinality $q$ serves as the function-field analog of the integer cost spectrum. The cost of a nonzero polynomial $f$ is defined by $c(f) := ∑ v_P(f) · J(‖P‖)$ where the sum runs over monic irreducibles $P$ with multiplicity $v_P(f)$ taken from normalizedFactors and ‖P‖ = q^{deg P}. The auxiliary function polyPrimeCost P equals J(q^{deg P}) for each irreducible factor. Upstream, the nonnegativity of individual $J$-costs follows from the definition of Jcost in PhiForcingDerived and the recognition-event cost in ObserverForcing, both of which are nonnegative by construction of the multiplicative recognizer.
proof idea
The term-mode proof unfolds polyCost to expose the multiset sum of polyPrimeCost values over the image of normalizedFactors. It then applies Multiset.sum_nonneg, extracts each factor via mem_map, rewrites the equality, and closes with the exact application of polyPrimeCost_nonneg on the irreducible.
why it matters in Recognition Science
This theorem supplies the nonnegativity axiom required by the master certificate cost_spectrum_poly_certificate, which bundles all elementary properties of the polynomial spectrum for the companion paper. It is also invoked directly in polyCost_le_mul to obtain monotonicity under multiplication. The result parallels the nonnegativity of costs in the integer PrimeCostSpectrum module and supports the Recognition Science claim that every recognition cost is nonnegative, consistent with the J-cost definition and the eight-tick octave structure.
scope and limits
- Does not claim strict positivity when f is the unit polynomial.
- Does not extend to polynomials over infinite fields.
- Does not compute explicit numerical values of the cost.
- Does not address factorization uniqueness beyond the UFD property already assumed.
Lean usage
theorem polyCost_le_mul {f g : Polynomial F} (hf : f ≠ 0) (hg : g ≠ 0) : polyCost f ≤ polyCost (f * g) := by rw [polyCost_mul hf hg]; have := polyCost_nonneg g; linarithformal statement (Lean)
122theorem polyCost_nonneg (f : Polynomial F) : 0 ≤ polyCost f := by
proof body
Term-mode proof.
123 unfold polyCost
124 apply Multiset.sum_nonneg
125 intro x hx
126 obtain ⟨P, _, hP_eq⟩ := Multiset.mem_map.mp hx
127 rw [← hP_eq]
128 exact polyPrimeCost_nonneg P
129
130/-! ## Multiplicativity over factorization -/
131
132/-- The total cost is additive under multiplication of nonzero polynomials.
133 This is the function-field analog of `costSpectrumValue_mul`. -/