polyCost_zero
plain-language theorem explainer
The theorem establishes that the cost of the zero polynomial is zero under the summation definition over normalized irreducible factors in F[X]. Researchers extending prime cost spectra to function fields over finite fields cite this base case when proving additivity and nonnegativity for the full cost function. The proof is a direct term-mode reduction that unfolds the summation and applies the fact that normalized factors of zero yield the empty multiset.
Claim. Let $c(f)$ denote the cost of a polynomial $f$ over a field $F$, defined as the sum of per-factor costs over the multiset of normalized irreducible factors of $f$. Then $c(0) = 0$.
background
In the module treating the cost spectrum on the polynomial ring F[X] as the function-field analog of the integer prime cost spectrum, every nonzero monic polynomial factors uniquely into monic irreducibles, with norm q to the degree. The cost c(f) is obtained by mapping each normalized irreducible factor to its J-cost (via polyPrimeCost) and summing the resulting real numbers; the zero polynomial is assigned cost zero by convention to make the function total on the ring. This construction relies on mathlib's normalizedFactors to handle arbitrary (not necessarily monic) polynomials in any UFD. The upstream definition of polyCost supplies exactly this summation structure, while the broader Recognition Science setting supplies the J-cost via the forcing chain (T5) and the Recognition Composition Law.
proof idea
The proof is a one-line term-mode wrapper: unfold the definition of polyCost to expose the sum over the image of normalizedFactors under polyPrimeCost, then invoke simp with the lemma normalizedFactors_zero, which shows that the normalized factors of the zero polynomial form the empty multiset and therefore the sum is zero.
why it matters
This base case anchors the elementary properties section of the polynomial cost spectrum, enabling the subsequent proofs of polyCost_one, polyCost_mul, polyCost_nonneg, and the bundled certificate. It mirrors the zero-cost convention for the unit in the integer setting and supports the extension of J-cost and phi-ladder structures to function fields, consistent with the eight-tick octave and D=3 landmarks of the forcing chain. No downstream uses are recorded, leaving open whether the polynomial spectrum will be invoked in explicit mass or alpha calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.