polyCost_nonneg
The polynomial cost function on F[X] is nonnegative for every polynomial f over a finite field. Researchers working on the function-field analog of prime cost spectra in Recognition Science would cite this result. The proof unfolds the multiset sum definition of the cost and reduces nonnegativity to the irreducible case via the already-proved nonnegativity for prime factors.
claimLet $F$ be a finite field with $q$ elements and let $f$ be any polynomial in $F[X]$. Define the cost $c(f)$ as the sum over irreducible factors $P$ of $v_P(f) · J(q^{deg P})$, where $v_P(f)$ is the multiplicity in the normalized factorization. Then $c(f) ≥ 0$.
background
This module constructs the cost spectrum for the polynomial ring $F[X]$ as the function-field counterpart to the integer prime cost spectrum. For a finite field $F$ of cardinality $q$, the cost of a nonzero polynomial $f$ is $c(f) := Σ_P v_P(f) · J(‖P‖)$, where the sum runs over monic irreducibles, $v_P(f)$ is the multiplicity, and ‖P‖ = q^{deg P}. The auxiliary function polyPrimeCost records the cost of a single irreducible factor as J(q^{deg P}). The module imports the general cost construction from MultiplicativeRecognizerL4 and ObserverForcing, where the latter states that the cost of any recognition event is nonnegative.
proof idea
The proof is a term-mode reduction. It unfolds the definition of polyCost, applies the lemma that a multiset sum is nonnegative whenever every term is nonnegative, extracts an irreducible factor via the map used in the definition, and invokes the nonnegativity theorem already established for irreducible polynomials.
why it matters in Recognition Science
This nonnegativity statement is a prerequisite for the master certificate cost_spectrum_poly_certificate, which assembles all elementary properties of the polynomial cost spectrum and is used by the companion paper. It also supports the monotonicity theorem polyCost_le_mul. In the Recognition framework it confirms that the J-cost construction remains nonnegative when lifted from recognition events to the polynomial ring, consistent with the nonnegativity of costs derived from the forcing chain.
scope and limits
- Does not apply to the zero polynomial.
- Does not claim strict positivity.
- Does not depend on a specific value of the field cardinality beyond finiteness.
- Does not address polynomials over infinite fields.
Lean usage
have h := polyCost_nonneg gformal 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`. -/