cost_spectrum_poly_certificate
plain-language theorem explainer
The cost spectrum polynomial certificate establishes seven elementary properties of the cost function on the polynomial ring over a finite field: strict positivity on positive-degree irreducibles, vanishing at the constant 1, global nonnegativity, strict positivity on non-units when the field has at least two elements, additivity under multiplication of nonzero polynomials, equality between total cost and prime cost for monic irreducibles, and scaling under powers. Number theorists and Recognition Science researchers modeling costs in function
Claim. Let $F$ be a finite field with cardinality $q = |F|$. Let $c$ be the cost function on $F[X]$ defined by $c(f) = J(q) + J(q^2) + J(q^3) + J(q^4) + J(q^5) + J(q^6) + J(q^7) + J(q^8) + J(q^9) + J(q^{10}) + J(q^{11}) + J(q^{12}) + J(q^{13}) + J(q^{14}) + J(q^{15}) + J(q^{16}) + J(q^{17}) + J(q^{18}) + J(q^{19}) + J(q^{20}) + J(q^{21}) + J(q^{22}) + J(q^{23}) + J(q^{24}) + J(q^{25}) + J(q^{26}) + J(q^{27}) + J(q^{28}) + J(q^{29}) + J(q^{30}) + J(q^{31}) + J(q^{32}) + J(q^{33}) + J(q^{34}) + J(q^{35}) + J(q^{36}) + J(q^{37}) + J(q^{38}) + J(q^{39}) + J(q^{40}) + J(q^{41}) + J(q^{42}) + J(q^{43}) + J(q^{44}) + J(q^{45}) + J(q^{46}) + J(q^{47}) + J(q^{48}) + J(q^{49}) + J(q^{50}) + J(q^{51}) + J(q^{52}) + J(q^{53}) + J(q^{54}) + J(q^{55}) + J(q^{56}) + J(q^{57}) + J(q^{58}) + J(q^{59}) + J(q^{60})
background
The module develops the cost spectrum on the polynomial ring $F[X]$ over a finite field $F$ of cardinality $q$. The norm of a monic polynomial $f$ is $q$ raised to its degree. The cost $c(f)$ is the sum over irreducible factors $P$ of the valuation $v_P(f)$ times $J$ of the norm of $P$, where $J$ is the Recognition cost function. This is the direct analog of the integer case in PrimeCostSpectrum. Key definitions include polyCost, which computes this sum using normalized factors, and polyPrimeCost for irreducibles equal to $J(q^{deg P})$. Upstream results include the definition of cost in MultiplicativeRecognizerL4 as derivedCost, and in ObserverForcing as Jcost of the state.
proof idea
The proof is a term-mode one-liner that constructs the seven-tuple by applying the lemmas polyPrimeCost_pos, polyCost_one, polyCost_nonneg, polyCost_pos, polyCost_mul, polyCost_irreducible, and polyCost_pow, each specialized to the field $F$.
why it matters
This certificate mirrors the cost_spectrum_certificate from the integer module and is intended for use in the companion paper on Recognition Science. It confirms that the polynomial cost spectrum satisfies the same elementary properties as its integer counterpart, supporting the extension of the cost framework to function fields. In the broader Recognition Science setting, this aligns with the J-uniqueness (T5) and the multiplicative properties derived from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.