Integer polynomials and verified Bernstein sign checkers

Vendored from SevenTriangles/Certificates/IntPoly.lean (commit b17ca52a), with an early failure test (endNeg) inside the bisection and, at the end of the file, consecutive interval chains (chainCheck) and nonnegativity with explicit rational split points (nonnegOnSplit).

IPoly := List Int is a dense coefficient list, lowest degree first. Every operation below is computable, uses only structural recursion (or explicit fuel), and is meant to be unfolded by the kernel inside decide +kernel proofs. The semantic layer (evalR) is noncomputable and the two soundness theorems nonnegOn_sound / posOn_sound are the only trusted statements.

Length conventions (they matter: Bernstein coefficients depend on the formal degree, i.e. on the list length, so trailing zeros are never trimmed):

• add p q has length max p.length q.length; smul c p, sub p q follow;
• mul is the literal recursion mul [] q = [], mul (a :: p) q = add (smul a q) (0 :: mul p q): length p.length + q.length - 1 for nonempty factors, and mul p [] = [0, …, 0] (p.length zeros). Consequently comp p a e d of a nonempty p has length p.length + 1 (one trailing zero: the Bernstein test is degree-elevated by one). The Python exporter reproduces exactly this ("literal mode"); do not "optimise" the representation without changing both sides;
• pascal n has length n + 1; bern p has the same length as p;
• strip p = (j, q) with p = x ^ j * q and q either empty or with nonzero constant term.

@[reducible, inline]

abbrev ConwaySoifer.Certificates.IPoly : Type

Dense integer coefficients in increasing degree order; trailing zeros are retained.

Equations

• ConwaySoifer.Certificates.IPoly = List ℤ

Computable operations

def ConwaySoifer.Certificates.IPoly.add : IPoly → IPoly → IPoly

Coefficientwise addition of dense integer polynomials.

Equations

• ConwaySoifer.Certificates.IPoly.add [] x✝ = x✝
• x✝.add [] = x✝
• ConwaySoifer.Certificates.IPoly.add (a :: p) (b :: q) = (a + b) :: ConwaySoifer.Certificates.IPoly.add p q

def ConwaySoifer.Certificates.IPoly.smul (c : ℤ) : IPoly → IPoly

Multiply every polynomial coefficient by an integer scalar.

Equations

• ConwaySoifer.Certificates.IPoly.smul c [] = []
• ConwaySoifer.Certificates.IPoly.smul c (a :: p) = c * a :: ConwaySoifer.Certificates.IPoly.smul c p

def ConwaySoifer.Certificates.IPoly.sub (p q : IPoly) : IPoly

Subtract dense integer coefficient lists.

Equations

• p.sub q = p.add (ConwaySoifer.Certificates.IPoly.smul (-1) q)

def ConwaySoifer.Certificates.IPoly.shift (p : IPoly) : IPoly

Multiplication by x.

Equations

• p.shift = 0 :: p

def ConwaySoifer.Certificates.IPoly.mul : IPoly → IPoly → IPoly

Product (literal recursion; see the length conventions above).

Equations

• ConwaySoifer.Certificates.IPoly.mul [] x✝ = []
• ConwaySoifer.Certificates.IPoly.mul (a :: p) x✝ = (ConwaySoifer.Certificates.IPoly.smul a x✝).add (0 :: ConwaySoifer.Certificates.IPoly.mul p x✝)

def ConwaySoifer.Certificates.IPoly.strip : IPoly → ℕ × IPoly

Remove the leading (lowest-degree) zero coefficients: strip p = (j, q) with p = x ^ j q.

Equations

• ConwaySoifer.Certificates.IPoly.strip [] = (0, [])
• ConwaySoifer.Certificates.IPoly.strip (a :: p) = if a = 0 then match ConwaySoifer.Certificates.IPoly.strip p with | (j, q) => (j + 1, q) else (0, a :: p)

def ConwaySoifer.Certificates.IPoly.pascal : ℕ → IPoly

Row n of Pascal's triangle, i.e. the coefficients of (1 + x) ^ n.

Equations

• ConwaySoifer.Certificates.IPoly.pascal 0 = [1]
• ConwaySoifer.Certificates.IPoly.pascal n.succ = ConwaySoifer.Certificates.IPoly.add (0 :: ConwaySoifer.Certificates.IPoly.pascal n) (ConwaySoifer.Certificates.IPoly.pascal n ++ [0])

def ConwaySoifer.Certificates.IPoly.bern : IPoly → IPoly

Coefficients of p in the (unnormalised) Bernstein basis t ^ k (1-t) ^ (n-k), n = p.length - 1.

Equations

• ConwaySoifer.Certificates.IPoly.bern [] = []
• ConwaySoifer.Certificates.IPoly.bern (a :: p) = (ConwaySoifer.Certificates.IPoly.smul a (ConwaySoifer.Certificates.IPoly.pascal p.length)).add (0 :: ConwaySoifer.Certificates.IPoly.bern p)

def ConwaySoifer.Certificates.IPoly.ipow (b : ℤ) : ℕ → ℤ

Structural integer exponentiation.

Equations

• ConwaySoifer.Certificates.IPoly.ipow b 0 = 1
• ConwaySoifer.Certificates.IPoly.ipow b n.succ = b * ConwaySoifer.Certificates.IPoly.ipow b n

def ConwaySoifer.Certificates.IPoly.comp : IPoly → ℤ → ℤ → ℤ → IPoly

comp p a e d = Σ_j c_j d ^ (n-j) (a + e t) ^ j where n = p.length - 1; the affine substitution x = (a + e t) / d cleared of denominators.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.IPoly.comp [] x✝² x✝¹ x✝ = []

def ConwaySoifer.Certificates.IPoly.allNonneg : IPoly → Bool

Test that every integer coefficient is nonnegative.

Equations

• ConwaySoifer.Certificates.IPoly.allNonneg [] = true
• ConwaySoifer.Certificates.IPoly.allNonneg (a :: p) = (decide (0 ≤ a) && ConwaySoifer.Certificates.IPoly.allNonneg p)

def ConwaySoifer.Certificates.IPoly.allPos : IPoly → Bool

Test that every integer coefficient is strictly positive.

Equations

• ConwaySoifer.Certificates.IPoly.allPos [] = true
• ConwaySoifer.Certificates.IPoly.allPos (a :: p) = (decide (0 < a) && ConwaySoifer.Certificates.IPoly.allPos p)

def ConwaySoifer.Certificates.evalScaledN : IPoly → ℤ → ℤ → ℕ → ℤ

Σ_j c_j num ^ j den ^ (N-j) (with truncated subtraction); equals den ^ N * p (num/den) whenever N ≥ p.length - 1. Used only for exact sign comparisons inside the untrusted search.

Equations

• ConwaySoifer.Certificates.evalScaledN [] x✝² x✝¹ x✝ = 0
• ConwaySoifer.Certificates.evalScaledN (c :: p) x✝² x✝¹ x✝ = c * ConwaySoifer.Certificates.IPoly.ipow x✝¹ x✝ + x✝² * ConwaySoifer.Certificates.evalScaledN p x✝² x✝¹ (x✝ - 1)

def ConwaySoifer.Certificates.endNeg (c : IPoly) : Bool

The first or last Bernstein coefficient (the values at the ends of the interval) is negative: bisection cannot succeed. Only an optimisation of the search; soundness never uses it.

Equations

• ConwaySoifer.Certificates.endNeg c = match List.head? c, List.getLast? c with | some x, some y => decide (x < 0) || decide (y < 0) | x, x_1 => false

def ConwaySoifer.Certificates.endNonpos (c : IPoly) : Bool

Detect a nonpositive endpoint Bernstein coefficient before attempting bisection.

Equations

• ConwaySoifer.Certificates.endNonpos c = match List.head? c, List.getLast? c with | some x, some y => decide (x ≤ 0) || decide (y ≤ 0) | x, x_1 => false

def ConwaySoifer.Certificates.nonnegOn (p : IPoly) : ℤ → ℤ → ℤ → ℕ → Bool

p ≥ 0 on [a/d, b/d], by Bernstein coefficients with adaptive bisection.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.nonnegOn p x✝² x✝¹ x✝ 0 = (p.comp x✝² (x✝¹ - x✝²) x✝).bern.allNonneg

def ConwaySoifer.Certificates.posOn' (q : IPoly) : ℤ → ℤ → ℤ → ℕ → Bool

q > 0 on [a/d, b/d], by strictly positive Bernstein coefficients (needs q ≠ []).

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.posOn' q x✝² x✝¹ x✝ 0 = (q.comp x✝² (x✝¹ - x✝²) x✝).bern.allPos

def ConwaySoifer.Certificates.posOn (p : IPoly) (a b d : ℤ) (fuel : ℕ) : Bool

p > 0 on [a/d, b/d] ∩ (0, ∞): strip the factor x ^ j, then posOn' on the quotient.

Equations

• ConwaySoifer.Certificates.posOn p a b d fuel = match p.strip with | (fst, []) => false | (fst, c :: q) => ConwaySoifer.Certificates.posOn' (c :: q) a b d fuel

Semantics

noncomputable def ConwaySoifer.Certificates.evalR : IPoly → ℝ → ℝ

Horner evaluation over the reals.

Equations

• ConwaySoifer.Certificates.evalR [] x✝ = 0
• ConwaySoifer.Certificates.evalR (c :: p) x✝ = ↑c + x✝ * ConwaySoifer.Certificates.evalR p x✝

@[simp]

theorem ConwaySoifer.Certificates.IPoly.evalR_nil (x : ℝ) : evalR [] x = 0

@[simp]

theorem ConwaySoifer.Certificates.IPoly.evalR_cons (c : ℤ) (p : IPoly) (x : ℝ) : evalR (c :: p) x = ↑c + x * evalR p x

theorem ConwaySoifer.Certificates.IPoly.evalR_add (p q : IPoly) (x : ℝ) : evalR (p.add q) x = evalR p x + evalR q x

theorem ConwaySoifer.Certificates.IPoly.evalR_smul (c : ℤ) (p : IPoly) (x : ℝ) : evalR (smul c p) x = ↑c * evalR p x

theorem ConwaySoifer.Certificates.IPoly.evalR_sub (p q : IPoly) (x : ℝ) : evalR (p.sub q) x = evalR p x - evalR q x

theorem ConwaySoifer.Certificates.IPoly.evalR_shift (p : IPoly) (x : ℝ) : evalR p.shift x = x * evalR p x

theorem ConwaySoifer.Certificates.IPoly.evalR_mul (p q : IPoly) (x : ℝ) : evalR (p.mul q) x = evalR p x * evalR q x

theorem ConwaySoifer.Certificates.IPoly.cast_ipow (b : ℤ) (n : ℕ) : ↑(ipow b n) = ↑b ^ n

theorem ConwaySoifer.Certificates.IPoly.evalR_strip (p : IPoly) (x : ℝ) : evalR p x = x ^ p.strip.1 * evalR p.strip.2 x

Lengths

theorem ConwaySoifer.Certificates.IPoly.length_add (p q : IPoly) : List.length (p.add q) = max (List.length p) (List.length q)

theorem ConwaySoifer.Certificates.IPoly.length_smul (c : ℤ) (p : IPoly) : List.length (smul c p) = List.length p

theorem ConwaySoifer.Certificates.IPoly.length_pascal (n : ℕ) : List.length (pascal n) = n + 1

theorem ConwaySoifer.Certificates.IPoly.length_bern (p : IPoly) : List.length p.bern = List.length p

theorem ConwaySoifer.Certificates.IPoly.comp_ne_nil (p : IPoly) (a e d : ℤ) (hp : p ≠ []) : p.comp a e d ≠ []

theorem ConwaySoifer.Certificates.IPoly.bern_ne_nil (p : IPoly) (hp : p ≠ []) : p.bern ≠ []

Homogeneous (Bernstein) evaluation

noncomputable def ConwaySoifer.Certificates.IPoly.evalH : IPoly → ℝ → ℝ → ℝ

evalH b s t = Σ_k b_k t ^ k s ^ (n-k) with n = b.length - 1.

Equations

• ConwaySoifer.Certificates.IPoly.evalH [] x✝¹ x✝ = 0
• ConwaySoifer.Certificates.IPoly.evalH (c :: cs) x✝¹ x✝ = ↑c * x✝¹ ^ cs.length + x✝ * ConwaySoifer.Certificates.IPoly.evalH cs x✝¹ x✝

theorem ConwaySoifer.Certificates.IPoly.evalH_add (p q : IPoly) (hlen : List.length p = List.length q) (s t : ℝ) : (p.add q).evalH s t = p.evalH s t + q.evalH s t

theorem ConwaySoifer.Certificates.IPoly.evalH_smul (c : ℤ) (p : IPoly) (s t : ℝ) : (smul c p).evalH s t = ↑c * p.evalH s t

theorem ConwaySoifer.Certificates.IPoly.evalH_append_zero (p : IPoly) (s t : ℝ) : (p ++ [0]).evalH s t = s * p.evalH s t

theorem ConwaySoifer.Certificates.IPoly.evalH_pascal (n : ℕ) (s t : ℝ) : (pascal n).evalH s t = (s + t) ^ n

theorem ConwaySoifer.Certificates.IPoly.evalH_bern (p : IPoly) (t : ℝ) : p.bern.evalH (1 - t) t = evalR p t

theorem ConwaySoifer.Certificates.IPoly.allNonneg_iff (b : IPoly) : b.allNonneg = true ↔ ∀ c ∈ b, 0 ≤ c

theorem ConwaySoifer.Certificates.IPoly.allPos_iff (b : IPoly) : b.allPos = true ↔ ∀ c ∈ b, 0 < c

theorem ConwaySoifer.Certificates.IPoly.evalH_nonneg (b : IPoly) (h : b.allNonneg = true) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) : 0 ≤ b.evalH s t

theorem ConwaySoifer.Certificates.IPoly.evalH_pos (b : IPoly) (h : b.allPos = true) (hb : b ≠ []) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : 0 < s + t) : 0 < b.evalH s t

Affine substitution

theorem ConwaySoifer.Certificates.IPoly.evalR_comp (p : IPoly) (a e d : ℤ) (hd : ↑d ≠ 0) (t : ℝ) : ↑d * evalR (p.comp a e d) t = ↑d ^ List.length p * evalR p ((↑a + ↑e * t) / ↑d)

theorem ConwaySoifer.Certificates.exists_param (a b d : ℤ) (hd : 0 < d) (x : ℝ) (hlo : ↑a / ↑d ≤ x) (hhi : x ≤ ↑b / ↑d) : ∃ (t : ℝ), 0 ≤ t ∧ t ≤ 1 ∧ ↑a + ↑(b - a) * t = ↑d * x

theorem ConwaySoifer.Certificates.bern_comp_nonneg_sound (p : IPoly) (a b d : ℤ) (h : (p.comp a (b - a) d).bern.allNonneg = true) (hd : 0 < d) (x : ℝ) (hlo : ↑a / ↑d ≤ x) (hhi : x ≤ ↑b / ↑d) : 0 ≤ evalR p x

theorem ConwaySoifer.Certificates.bern_comp_pos_sound (q : IPoly) (hq : q ≠ []) (a b d : ℤ) (h : (q.comp a (b - a) d).bern.allPos = true) (hd : 0 < d) (x : ℝ) (hlo : ↑a / ↑d ≤ x) (hhi : x ≤ ↑b / ↑d) : 0 < evalR q x

theorem ConwaySoifer.Certificates.half_lo (a d : ℤ) (x : ℝ) (hlo : ↑a / ↑d ≤ x) : ↑(2 * a) / ↑(2 * d) ≤ x

theorem ConwaySoifer.Certificates.half_hi (b d : ℤ) (x : ℝ) (hhi : x ≤ ↑b / ↑d) : x ≤ ↑(2 * b) / ↑(2 * d)

theorem ConwaySoifer.Certificates.nonnegOn_sound (p : IPoly) (a b d : ℤ) (fuel : ℕ) (h : nonnegOn p a b d fuel = true) (hd : 0 < d) (x : ℝ) (hlo : ↑a / ↑d ≤ x) (hhi : x ≤ ↑b / ↑d) : 0 ≤ evalR p x

theorem ConwaySoifer.Certificates.posOn'_sound (q : IPoly) (hq : q ≠ []) (a b d : ℤ) (fuel : ℕ) (h : posOn' q a b d fuel = true) (hd : 0 < d) (x : ℝ) (hlo : ↑a / ↑d ≤ x) (hhi : x ≤ ↑b / ↑d) : 0 < evalR q x

theorem ConwaySoifer.Certificates.posOn_sound (p : IPoly) (a b d : ℤ) (fuel : ℕ) (h : posOn p a b d fuel = true) (hd : 0 < d) (x : ℝ) (hx : 0 < x) (hlo : ↑a / ↑d ≤ x) (hhi : x ≤ ↑b / ↑d) : 0 < evalR p x

Consecutive interval chains and rational split points

@[reducible, inline]

abbrev ConwaySoifer.Certificates.IRat : Type

Rational number n/m with m > 0, as a pair.

Equations

• ConwaySoifer.Certificates.IRat = (ℤ × ℤ)

def ConwaySoifer.Certificates.chainCheck (f : ℤ → ℤ → ℤ → Bool) (hi : IRat) : IRat → List (ℤ × ℤ × ℤ) → Bool

chainCheck f hi cur pieces: pieces = [(a₁, b₁, d₁), …] are consecutive rational intervals [aᵢ/dᵢ, bᵢ/dᵢ] (all dᵢ > 0) starting at cur, ending at hi, and f aᵢ bᵢ dᵢ holds on each. Endpoint equality is tested by cross-multiplication.

Equations

• One or more equations did not get rendered due to their size.
• ConwaySoifer.Certificates.chainCheck f hi x✝ [] = false
• ConwaySoifer.Certificates.chainCheck f hi (cn, cd) [(a', b', d')] = (decide (0 < d') && decide (cn * d' = a' * cd) && f a' b' d' && decide (b' * hi.2 = hi.1 * d'))

def ConwaySoifer.Certificates.piecesFrom (b d : ℤ) : IRat → List IRat → List (ℤ × ℤ × ℤ)

The consecutive pieces of [cur, b/d] cut at the split points pts (each n/m, m > 0), produced by the untrusted search.

Equations

• ConwaySoifer.Certificates.piecesFrom b d (n, m) [] = [(n * d, b * m, m * d)]
• ConwaySoifer.Certificates.piecesFrom b d (n, m) ((n', m') :: rest) = (n * m', n' * m, m * m') :: ConwaySoifer.Certificates.piecesFrom b d (n', m') rest

def ConwaySoifer.Certificates.piecesOf (a b d : ℤ) (pts : List IRat) : List (ℤ × ℤ × ℤ)

Build exact adjacent rational intervals between supplied split points.

Equations

• ConwaySoifer.Certificates.piecesOf a b d pts = ConwaySoifer.Certificates.piecesFrom b d (a, d) pts

def ConwaySoifer.Certificates.nonnegOnSplit (p : IPoly) (a b d : ℤ) (fuel : ℕ) (pts : List IRat) : Bool

Nonnegativity on [a/d, b/d] with explicit split points: trusted only through chainCheck and nonnegOn on each piece.

Equations

• One or more equations did not get rendered due to their size.

theorem ConwaySoifer.Certificates.rat_eq_of_cross {a b c d : ℤ} (hb : 0 < b) (hd : 0 < d) (h : a * d = c * b) : ↑a / ↑b = ↑c / ↑d

theorem ConwaySoifer.Certificates.chainCheck_sound (f : ℤ → ℤ → ℤ → Bool) (hi : IRat) (hhi : 0 < hi.2) (x : ℝ) (hx : x ≤ ↑hi.1 / ↑hi.2) (pieces : List (ℤ × ℤ × ℤ)) (cur : IRat) : 0 < cur.2 → chainCheck f hi cur pieces = true → ↑cur.1 / ↑cur.2 ≤ x → ∃ (a' : ℤ) (b' : ℤ) (d' : ℤ), 0 < d' ∧ f a' b' d' = true ∧ ↑a' / ↑d' ≤ x ∧ x ≤ ↑b' / ↑d'

theorem ConwaySoifer.Certificates.nonnegOnSplit_sound (p : IPoly) (a b d : ℤ) (fuel : ℕ) (pts : List IRat) (h : nonnegOnSplit p a b d fuel pts = true) (hd : 0 < d) (x : ℝ) (hlo : ↑a / ↑d ≤ x) (hhi : x ≤ ↑b / ↑d) : 0 ≤ evalR p x