polyCost_mul
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.