Computable polynomials

Mathlib's Polynomial is noncomputable (it is Finsupp-based), which rules out native_decide verification of identities in polynomial or rational-function coefficients. This file provides CPoly K, a computable polynomial ring over a DecidableEq commutative ring, as trimmed coefficient lists (little-endian, no trailing zeros).

The ring axioms are not proven from scratch: the coefficient-list operations are transported along the injective evaluation CPoly.toPoly : CPoly K → Polynomial K via Function.Injective.commRing.

The intended use is the generic-parameter verification of order conditions for the parametric EES(2,5;x) family: with a computable fraction field of CPoly ℚ the symbolic identities of arXiv:2509.20599, Theorem E.1, become native_decide checks.

def BSeries.CPoly (K : Type u) [Zero K] [DecidableEq K] : Type u

Trailing-zero-free little-endian coefficient lists.

Equations

• BSeries.CPoly K = { l : List K // l.getLast? ≠ some 0 }

def BSeries.CPoly.trim {L : Type u} [Zero L] [DecidableEq L] (l : List L) : List L

Remove trailing zeros.

Equations

• BSeries.CPoly.trim l = (List.dropWhile (fun (x : L) => x == 0) l.reverse).reverse

theorem BSeries.CPoly.getLast?_trim {K : Type u} [Zero K] [DecidableEq K] (l : List K) : (trim l).getLast? ≠ some 0

Raw coefficient-list operations

def BSeries.CPoly.rawAdd {K : Type u} [CommRing K] : List K → List K → List K

Pointwise addition (little-endian, ragged).

Equations

• BSeries.CPoly.rawAdd [] x✝ = x✝
• BSeries.CPoly.rawAdd (a :: l) [] = a :: l
• BSeries.CPoly.rawAdd (a :: l) (b :: m) = (a + b) :: BSeries.CPoly.rawAdd l m

def BSeries.CPoly.rawNeg {K : Type u} [CommRing K] (l : List K) : List K

Negation.

Equations

• BSeries.CPoly.rawNeg l = List.map Neg.neg l

def BSeries.CPoly.rawMul {K : Type u} [CommRing K] : List K → List K → List K

Convolution product.

Equations

• BSeries.CPoly.rawMul [] x✝ = []
• BSeries.CPoly.rawMul (a :: l) x✝ = BSeries.CPoly.rawAdd (List.map (fun (x : K) => a * x) x✝) (0 :: BSeries.CPoly.rawMul l x✝)

noncomputable def BSeries.CPoly.toPolyList {K : Type u} [CommRing K] : List K → Polynomial K

Interpret a coefficient list as a polynomial.

Equations

• BSeries.CPoly.toPolyList [] = 0
• BSeries.CPoly.toPolyList (a :: l) = Polynomial.C a + Polynomial.X * BSeries.CPoly.toPolyList l

@[simp]

theorem BSeries.CPoly.toPolyList_nil {K : Type u} [CommRing K] : toPolyList [] = 0

@[simp]

theorem BSeries.CPoly.toPolyList_cons {K : Type u} [CommRing K] (a : K) (l : List K) : toPolyList (a :: l) = Polynomial.C a + Polynomial.X * toPolyList l

theorem BSeries.CPoly.toPolyList_rawAdd {K : Type u} [CommRing K] (l m : List K) : toPolyList (rawAdd l m) = toPolyList l + toPolyList m

theorem BSeries.CPoly.toPolyList_rawNeg {K : Type u} [CommRing K] (l : List K) : toPolyList (rawNeg l) = -toPolyList l

theorem BSeries.CPoly.toPolyList_map_mul {K : Type u} [CommRing K] (c : K) (l : List K) : toPolyList (List.map (fun (x : K) => c * x) l) = Polynomial.C c * toPolyList l

theorem BSeries.CPoly.toPolyList_rawMul {K : Type u} [CommRing K] (l m : List K) : toPolyList (rawMul l m) = toPolyList l * toPolyList m

theorem BSeries.CPoly.toPolyList_append_zero {K : Type u} [CommRing K] (l : List K) : toPolyList (l ++ [0]) = toPolyList l

noncomputable def BSeries.CPoly.toPoly {K : Type u} [CommRing K] [DecidableEq K] (p : CPoly K) : Polynomial K

Interpret a trimmed coefficient list as a polynomial.

Equations

• p.toPoly = BSeries.CPoly.toPolyList ↑p

theorem BSeries.CPoly.toPolyList_trim {K : Type u} [CommRing K] [DecidableEq K] (l : List K) : toPolyList (trim l) = toPolyList l

theorem BSeries.CPoly.toPoly_injective {K : Type u} [CommRing K] [DecidableEq K] : Function.Injective toPoly

Ring structure by injective transfer

def BSeries.CPoly.C {K : Type u} [CommRing K] [DecidableEq K] (c : K) : CPoly K

Constant polynomials.

Equations

• BSeries.CPoly.C c = ⟨BSeries.CPoly.trim [c], ⋯⟩

theorem BSeries.CPoly.toPoly_C {K : Type u} [CommRing K] [DecidableEq K] (c : K) : (C c).toPoly = Polynomial.C c

@[implicit_reducible]

instance BSeries.CPoly.instZero {K : Type u} [CommRing K] [DecidableEq K] : Zero (CPoly K)

Equations

• BSeries.CPoly.instZero = { zero := ⟨[], ⋯⟩ }

@[implicit_reducible]

instance BSeries.CPoly.instOne {K : Type u} [CommRing K] [DecidableEq K] : One (CPoly K)

Equations

• BSeries.CPoly.instOne = { one := BSeries.CPoly.C 1 }

@[implicit_reducible]

instance BSeries.CPoly.instAdd {K : Type u} [CommRing K] [DecidableEq K] : Add (CPoly K)

Equations

• BSeries.CPoly.instAdd = { add := fun (p q : BSeries.CPoly K) => ⟨BSeries.CPoly.trim (BSeries.CPoly.rawAdd ↑p ↑q), ⋯⟩ }

@[implicit_reducible]

instance BSeries.CPoly.instMul {K : Type u} [CommRing K] [DecidableEq K] : Mul (CPoly K)

Equations

• BSeries.CPoly.instMul = { mul := fun (p q : BSeries.CPoly K) => ⟨BSeries.CPoly.trim (BSeries.CPoly.rawMul ↑p ↑q), ⋯⟩ }

@[implicit_reducible]

instance BSeries.CPoly.instNeg {K : Type u} [CommRing K] [DecidableEq K] : Neg (CPoly K)

Equations

• BSeries.CPoly.instNeg = { neg := fun (p : BSeries.CPoly K) => ⟨BSeries.CPoly.trim (BSeries.CPoly.rawNeg ↑p), ⋯⟩ }

@[implicit_reducible]

instance BSeries.CPoly.instDecidableEq {K : Type u} [CommRing K] [DecidableEq K] : DecidableEq (CPoly K)

Equations

• p.instDecidableEq q = decidable_of_iff (↑p = ↑q) ⋯

theorem BSeries.CPoly.toPoly_zero {K : Type u} [CommRing K] [DecidableEq K] : toPoly 0 = 0

theorem BSeries.CPoly.toPoly_one {K : Type u} [CommRing K] [DecidableEq K] : toPoly 1 = 1

theorem BSeries.CPoly.toPoly_add {K : Type u} [CommRing K] [DecidableEq K] (p q : CPoly K) : (p + q).toPoly = p.toPoly + q.toPoly

theorem BSeries.CPoly.toPoly_mul {K : Type u} [CommRing K] [DecidableEq K] (p q : CPoly K) : (p * q).toPoly = p.toPoly * q.toPoly

theorem BSeries.CPoly.toPoly_neg {K : Type u} [CommRing K] [DecidableEq K] (p : CPoly K) : (-p).toPoly = -p.toPoly

@[implicit_reducible]

instance BSeries.CPoly.instCommRing {K : Type u} [CommRing K] [DecidableEq K] : CommRing (CPoly K)

The commutative ring structure: axioms transported from Polynomial K through the injection, data fully computable.

Equations

• BSeries.CPoly.instCommRing = CommRing.ofMinimalAxioms ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable def BSeries.CPoly.toPolyHom {K : Type u} [CommRing K] [DecidableEq K] : CPoly K →+* Polynomial K

toPoly as a ring homomorphism.

Equations

• BSeries.CPoly.toPolyHom = { toFun := BSeries.CPoly.toPoly, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

def BSeries.CPoly.X {K : Type u} [CommRing K] [DecidableEq K] : CPoly K

The polynomial variable.

Equations

• BSeries.CPoly.X = ⟨BSeries.CPoly.trim [0, 1], ⋯⟩

theorem BSeries.CPoly.toPoly_X {K : Type u} [CommRing K] [DecidableEq K] : X.toPoly = Polynomial.X

instance BSeries.CPoly.instIsDomain {K : Type u} [CommRing K] [DecidableEq K] [IsDomain K] : IsDomain (CPoly K)

No zero divisors, transported along the injection.

Unverified division and gcd

Polynomial long division and the Euclidean algorithm, for use as runtime-checked reductions: callers verify the defining equations by a decidable guard, so no correctness theory is needed here.

def BSeries.CPoly.rawDivModAux {L : Type u} [Field L] [DecidableEq L] (q : List L) : ℕ → List L → List L × List L

One pass of polynomial long division (fuelled; little-endian).

Equations

• One or more equations did not get rendered due to their size.
• BSeries.CPoly.rawDivModAux q 0 x✝ = ([], x✝)

def BSeries.CPoly.rawDivMod {L : Type u} [Field L] [DecidableEq L] (p q : List L) : List L × List L

Quotient and remainder of polynomial division (unverified).

Equations

• BSeries.CPoly.rawDivMod p q = BSeries.CPoly.rawDivModAux (BSeries.CPoly.trim q) (p.length + 1) p

def BSeries.CPoly.rawGcd {L : Type u} [Field L] [DecidableEq L] : ℕ → List L → List L → List L

Euclidean gcd, normalised to be monic (unverified).

Equations

• One or more equations did not get rendered due to their size.
• BSeries.CPoly.rawGcd 0 x✝¹ x✝ = BSeries.CPoly.trim x✝¹

def BSeries.CPoly.cGcd {L : Type u} [Field L] [DecidableEq L] (p q : CPoly L) : CPoly L

Monic gcd of two computable polynomials (unverified).

Equations

• p.cGcd q = ⟨BSeries.CPoly.trim (BSeries.CPoly.rawGcd ((↑p).length + (↑q).length + 2) ↑p ↑q), ⋯⟩

def BSeries.CPoly.cDiv {L : Type u} [Field L] [DecidableEq L] (p q : CPoly L) : CPoly L

Quotient of polynomial division (unverified).

Equations

• p.cDiv q = ⟨BSeries.CPoly.trim (BSeries.CPoly.rawDivMod ↑p ↑q).1, ⋯⟩