polyCost_irreducible
plain-language theorem explainer
For a monic irreducible polynomial P over a finite field F, the polynomial cost equals the prime cost of that single factor. Researchers establishing the cost spectrum on F[X] cite this as the base case that reduces the sum over normalized factors to J of the norm. The proof is a direct term-mode reduction that applies normalizedFactors_irreducible, normalizes via the monic hypothesis, and simplifies.
Claim. Let $P$ be a monic irreducible polynomial in $F[X]$. Then the cost $c(P)$ equals $J(q^{deg P})$, where $q = |F|$ and $J$ denotes the J-cost function.
background
The module develops the cost spectrum on the polynomial ring $F[X]$ as the function-field counterpart to the integer prime-cost spectrum. The cost of a nonzero polynomial $f$ is defined by summing $Jcost(polyNorm P)$ over the multiset of normalized irreducible factors of $f$, where $polyNorm P = q^{deg P}$ and $q = |F|$. For an irreducible monic $P$ the multiset contains only $P$ itself, so the sum collapses to the single term $J(q^{deg P})$. This construction rests on the J-cost already introduced in the Recognition Science core and on Mathlib's normalizedFactors for unique factorization domains.
proof idea
The term proof unfolds polyCost, rewrites the factor multiset via normalizedFactors_irreducible applied to the irreducibility hypothesis, proves normalize P = P from the monic assumption, and finishes by simp.
why it matters
This supplies the irreducible base case bundled into the master certificate cost_spectrum_poly_certificate, which mirrors the integer version and is referenced by the companion paper. It confirms that the cost spectrum on F[X] inherits the same additive and positivity properties as the integer spectrum, thereby extending the J-cost construction from the forcing chain (T5 J-uniqueness) to the polynomial setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.