polyCost_mul
The polynomial cost function over a finite field is additive under multiplication for nonzero inputs. Researchers extending the Recognition Science cost spectrum to function fields cite this when establishing the full elementary properties certificate. The proof is a direct term-mode reduction that unfolds the cost definition and applies multiset additivity on normalized irreducible factors.
claimFor nonzero polynomials $f, g$ in the polynomial ring $F[X]$ over a finite field $F$, the cost satisfies $c(f g) = c(f) + c(g)$, where $c$ is the sum of $J$-costs of the norms of monic irreducible factors weighted by their multiplicities.
background
In the module on the cost spectrum for polynomials over a finite field $F$ with cardinality $q$, the cost of a nonzero polynomial $f$ is defined via the multiset of normalized monic irreducible factors: $c(f) :=$ sum of $J(q^{deg P})$ times the valuation $v_P(f)$ for each irreducible $P$. This is the function-field analog of the integer prime cost spectrum, with the norm of a monic irreducible of degree $n$ equal to $q^n$ and polyPrimeCost assigning the corresponding $J$-cost. Upstream results include the cost definitions from MultiplicativeRecognizerL4.cost (derived cost of a comparator on positive ratios) and ObserverForcing.cost (J-cost of a recognition event), which supply the underlying $J$-cost mechanism.
proof idea
The proof unfolds the definition of polyCost, rewrites the normalized factors of the product via normalizedFactors_mul, and applies the additivity of Multiset.map and Multiset.sum to obtain the sum of the individual costs.
why it matters in Recognition Science
This supplies the multiplicative property required by the master certificate cost_spectrum_poly_certificate, which bundles all elementary properties of the polynomial cost spectrum and mirrors the integer version. It directly enables downstream results polyCost_pow and polyCost_le_mul. In the Recognition framework it contributes to the cost spectrum construction, linking to the J-cost from the forcing chain (T5 J-uniqueness) and the phi-ladder via the norm definitions.
scope and limits
- Does not apply when either polynomial is the zero polynomial.
- Does not depend on a specific value of the field cardinality beyond finiteness.
- Does not address factorization uniqueness beyond Mathlib's normalizedFactors.
- Does not claim positivity or nonnegativity of the cost (handled by sibling theorems).
formal statement (Lean)
134theorem polyCost_mul {f g : Polynomial F} (hf : f ≠ 0) (hg : g ≠ 0) :
135 polyCost (f * g) = polyCost f + polyCost g := by
proof body
Term-mode proof.
136 unfold polyCost
137 rw [normalizedFactors_mul hf hg]
138 rw [Multiset.map_add, Multiset.sum_add]
139
140/-! ## Cost on irreducibles and powers -/
141
142/-- For a monic irreducible polynomial `P`, the cost equals `J(‖P‖)`.
143 Mathlib's `normalizedFactors` returns the multiset of monic
144 irreducible factors. -/