Sparse exact polynomial certificate

This module implements a computable dense representation of trivariate integer polynomials. Its proved evaluator is used to kernel-check every coefficient in the four Bellman charts without materializing enormous ring_nf goals.

structure FD1D.BellmanCertificate.DPoly (R : Type) : Type

A dense polynomial represented by its coefficient list, in increasing degree order.

• coeffs : List R

  Coefficients in increasing degree order; trailing zero coefficients are permitted.

@[instance_reducible]

instance FD1D.BellmanCertificate.instDecidableEqDPoly {R✝ : Type} [DecidableEq R✝] : DecidableEq (DPoly R✝)

Equations

• FD1D.BellmanCertificate.instDecidableEqDPoly = FD1D.BellmanCertificate.instDecidableEqDPoly.decEq

def FD1D.BellmanCertificate.instDecidableEqDPoly.decEq {R✝ : Type} [DecidableEq R✝] (x✝ x✝¹ : DPoly R✝) : Decidable (x✝ = x✝¹)

Equations

• FD1D.BellmanCertificate.instDecidableEqDPoly.decEq { coeffs := a } { coeffs := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def FD1D.BellmanCertificate.instReprDPoly.repr {R✝ : Type} [Repr R✝] : DPoly R✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance FD1D.BellmanCertificate.instReprDPoly {R✝ : Type} [Repr R✝] : Repr (DPoly R✝)

Equations

• FD1D.BellmanCertificate.instReprDPoly = { reprPrec := FD1D.BellmanCertificate.instReprDPoly.repr }

def FD1D.BellmanCertificate.DPoly.const {R : Type} (a : R) : DPoly R

The dense representation of a constant polynomial.

Equations

• FD1D.BellmanCertificate.DPoly.const a = { coeffs := [a] }

def FD1D.BellmanCertificate.DPoly.addCoeffs {R : Type u_1} [Add R] : List R → List R → List R

Coefficientwise addition, extending the shorter list by zeros.

Equations

• FD1D.BellmanCertificate.DPoly.addCoeffs [] x✝ = x✝
• FD1D.BellmanCertificate.DPoly.addCoeffs x✝ [] = x✝
• FD1D.BellmanCertificate.DPoly.addCoeffs (a :: p) (b :: q) = (a + b) :: FD1D.BellmanCertificate.DPoly.addCoeffs p q

def FD1D.BellmanCertificate.DPoly.neg {R : Type} [Neg R] (p : DPoly R) : DPoly R

Negation of every coefficient.

Equations

• p.neg = { coeffs := List.map (fun (x : R) => -x) p.coeffs }

def FD1D.BellmanCertificate.DPoly.add {R : Type} [Add R] (p q : DPoly R) : DPoly R

Addition of dense polynomials by their coefficient lists.

Equations

• p.add q = { coeffs := FD1D.BellmanCertificate.DPoly.addCoeffs p.coeffs q.coeffs }

def FD1D.BellmanCertificate.DPoly.scale {R : Type} [Mul R] (a : R) (p : DPoly R) : DPoly R

Left multiplication of every coefficient by the given scalar.

Equations

• FD1D.BellmanCertificate.DPoly.scale a p = { coeffs := List.map (fun (x : R) => a * x) p.coeffs }

def FD1D.BellmanCertificate.DPoly.mulCoeffs {R : Type u_1} [Zero R] [Add R] [Mul R] : List R → List R → List R

Convolution of coefficient lists for polynomial multiplication.

Equations

• FD1D.BellmanCertificate.DPoly.mulCoeffs [] x✝ = []
• FD1D.BellmanCertificate.DPoly.mulCoeffs (a :: p) x✝ = FD1D.BellmanCertificate.DPoly.addCoeffs (List.map (fun (x : R) => a * x) x✝) (0 :: FD1D.BellmanCertificate.DPoly.mulCoeffs p x✝)

def FD1D.BellmanCertificate.DPoly.mul {R : Type} [Zero R] [Add R] [Mul R] (p q : DPoly R) : DPoly R

Multiplication of dense polynomials by coefficient convolution.

Equations

• p.mul q = { coeffs := FD1D.BellmanCertificate.DPoly.mulCoeffs p.coeffs q.coeffs }

def FD1D.BellmanCertificate.DPoly.pow {R : Type} [Zero R] [One R] [Add R] [Mul R] (p : DPoly R) : ℕ → DPoly R

Natural powers computed by repeated polynomial multiplication.

Equations

• p.pow 0 = FD1D.BellmanCertificate.DPoly.const 1
• p.pow n.succ = (p.pow n).mul p

@[instance_reducible]

instance FD1D.BellmanCertificate.DPoly.instZero {R : Type} : Zero (DPoly R)

Equations

• FD1D.BellmanCertificate.DPoly.instZero = { zero := { coeffs := [] } }

@[instance_reducible]

instance FD1D.BellmanCertificate.DPoly.instOne {R : Type} [One R] : One (DPoly R)

Equations

• FD1D.BellmanCertificate.DPoly.instOne = { one := FD1D.BellmanCertificate.DPoly.const 1 }

@[instance_reducible]

instance FD1D.BellmanCertificate.DPoly.instAdd {R : Type} [Add R] : Add (DPoly R)

Equations

• FD1D.BellmanCertificate.DPoly.instAdd = { add := FD1D.BellmanCertificate.DPoly.add }

@[instance_reducible]

instance FD1D.BellmanCertificate.DPoly.instNeg {R : Type} [Neg R] : Neg (DPoly R)

Equations

• FD1D.BellmanCertificate.DPoly.instNeg = { neg := FD1D.BellmanCertificate.DPoly.neg }

@[instance_reducible]

instance FD1D.BellmanCertificate.DPoly.instSubOfNegOfAdd {R : Type} [Neg R] [Add R] : Sub (DPoly R)

Equations

• FD1D.BellmanCertificate.DPoly.instSubOfNegOfAdd = { sub := fun (p q : FD1D.BellmanCertificate.DPoly R) => p + -q }

@[instance_reducible]

instance FD1D.BellmanCertificate.DPoly.instMulOfZeroOfAdd {R : Type} [Zero R] [Add R] [Mul R] : Mul (DPoly R)

Equations

• FD1D.BellmanCertificate.DPoly.instMulOfZeroOfAdd = { mul := FD1D.BellmanCertificate.DPoly.mul }

@[instance_reducible]

instance FD1D.BellmanCertificate.DPoly.instPowNatOfZeroOfOneOfAddOfMul {R : Type} [Zero R] [One R] [Add R] [Mul R] : Pow (DPoly R) ℕ

Equations

• FD1D.BellmanCertificate.DPoly.instPowNatOfZeroOfOneOfAddOfMul = { pow := FD1D.BellmanCertificate.DPoly.pow }

@[instance_reducible]

instance FD1D.BellmanCertificate.DPoly.instOfNatHAddNatOfNat {R : Type} (n : ℕ) [OfNat R (n + 2)] : OfNat (DPoly R) (n + 2)

Equations

• FD1D.BellmanCertificate.DPoly.instOfNatHAddNatOfNat n = { ofNat := FD1D.BellmanCertificate.DPoly.const (OfNat.ofNat (n + 2)) }

@[simp]

theorem FD1D.BellmanCertificate.DPoly.coeffs_zero {R : Type} : coeffs 0 = []

@[simp]

theorem FD1D.BellmanCertificate.DPoly.coeffs_one {R : Type} [One R] : coeffs 1 = [1]

@[simp]

theorem FD1D.BellmanCertificate.DPoly.coeffs_ofNat {R : Type} (n : ℕ) [OfNat R (n + 2)] : coeffs (OfNat.ofNat (n + 2)) = [OfNat.ofNat (n + 2)]

def FD1D.BellmanCertificate.DPoly.X {R : Type} [Zero R] [One R] : DPoly R

The indeterminate, with coefficient list [0, 1].

Equations

• FD1D.BellmanCertificate.DPoly.X = { coeffs := [0, 1] }

def FD1D.BellmanCertificate.DPoly.evalCoeffs {S : Type u_1} {R : Type u_2} [Zero S] [Add S] [Mul S] (f : R → S) (x : S) : List R → S

Horner evaluation of a coefficient list after applying the coefficient map.

Equations

• FD1D.BellmanCertificate.DPoly.evalCoeffs f x [] = 0
• FD1D.BellmanCertificate.DPoly.evalCoeffs f x (a :: p) = f a + x * FD1D.BellmanCertificate.DPoly.evalCoeffs f x p

def FD1D.BellmanCertificate.DPoly.eval {S : Type u_1} {R : Type} [Zero S] [Add S] [Mul S] (f : R → S) (x : S) (p : DPoly R) : S

Evaluation of a dense polynomial using the given coefficient map.

Equations

• FD1D.BellmanCertificate.DPoly.eval f x p = FD1D.BellmanCertificate.DPoly.evalCoeffs f x p.coeffs

@[simp]

theorem FD1D.BellmanCertificate.DPoly.evalCoeffs_nil {S : Type u_1} {R : Type u_2} [Zero S] [Add S] [Mul S] (f : R → S) (x : S) : evalCoeffs f x [] = 0

@[simp]

theorem FD1D.BellmanCertificate.DPoly.evalCoeffs_cons {S : Type u_1} {R : Type u_2} [Zero S] [Add S] [Mul S] (f : R → S) (x : S) (a : R) (p : List R) : evalCoeffs f x (a :: p) = f a + x * evalCoeffs f x p

theorem FD1D.BellmanCertificate.DPoly.evalCoeffs_add {R : Type u_1} {S : Type u_2} [Add R] [CommRing S] (f : R → S) (hfadd : ∀ (a b : R), f (a + b) = f a + f b) (x : S) (p q : List R) : evalCoeffs f x (addCoeffs p q) = evalCoeffs f x p + evalCoeffs f x q

theorem FD1D.BellmanCertificate.DPoly.evalCoeffs_neg {R : Type u_1} {S : Type u_2} [Neg R] [CommRing S] (f : R → S) (hfneg : ∀ (a : R), f (-a) = -f a) (x : S) (p : List R) : evalCoeffs f x (List.map (fun (x : R) => -x) p) = -evalCoeffs f x p

theorem FD1D.BellmanCertificate.DPoly.evalCoeffs_scale {R : Type u_1} {S : Type u_2} [Mul R] [CommRing S] (f : R → S) (hfmul : ∀ (a b : R), f (a * b) = f a * f b) (x : S) (a : R) (p : List R) : evalCoeffs f x (List.map (fun (x : R) => a * x) p) = f a * evalCoeffs f x p

theorem FD1D.BellmanCertificate.DPoly.evalCoeffs_mul {R : Type u_1} {S : Type u_2} [Zero R] [Add R] [Mul R] [CommRing S] (f : R → S) (hf0 : f 0 = 0) (hfadd : ∀ (a b : R), f (a + b) = f a + f b) (hfmul : ∀ (a b : R), f (a * b) = f a * f b) (x : S) (p q : List R) : evalCoeffs f x (mulCoeffs p q) = evalCoeffs f x p * evalCoeffs f x q

@[simp]

theorem FD1D.BellmanCertificate.DPoly.eval_zero {S : Type u_1} {R : Type} [CommRing S] (f : R → S) (x : S) : eval f x 0 = 0

@[simp]

theorem FD1D.BellmanCertificate.DPoly.eval_const {S : Type u_1} {R : Type} [CommRing S] (f : R → S) (x : S) (a : R) : eval f x (const a) = f a

theorem FD1D.BellmanCertificate.DPoly.eval_add {R : Type} {S : Type u_1} [Add R] [CommRing S] (f : R → S) (hfadd : ∀ (a b : R), f (a + b) = f a + f b) (x : S) (p q : DPoly R) : eval f x (p.add q) = eval f x p + eval f x q

theorem FD1D.BellmanCertificate.DPoly.eval_neg {R : Type} {S : Type u_1} [Neg R] [CommRing S] (f : R → S) (hfneg : ∀ (a : R), f (-a) = -f a) (x : S) (p : DPoly R) : eval f x p.neg = -eval f x p

theorem FD1D.BellmanCertificate.DPoly.eval_mul {R : Type} {S : Type u_1} [Zero R] [Add R] [Mul R] [CommRing S] (f : R → S) (hf0 : f 0 = 0) (hfadd : ∀ (a b : R), f (a + b) = f a + f b) (hfmul : ∀ (a b : R), f (a * b) = f a * f b) (x : S) (p q : DPoly R) : eval f x (p.mul q) = eval f x p * eval f x q

theorem FD1D.BellmanCertificate.DPoly.eval_pow {R : Type} {S : Type u_1} [Zero R] [One R] [Add R] [Mul R] [CommRing S] (f : R → S) (hf0 : f 0 = 0) (hf1 : f 1 = 1) (hfadd : ∀ (a b : R), f (a + b) = f a + f b) (hfmul : ∀ (a b : R), f (a * b) = f a * f b) (x : S) (p : DPoly R) (n : ℕ) : eval f x (p.pow n) = eval f x p ^ n

@[reducible, inline]

abbrev FD1D.BellmanCertificate.Poly3 : Type

Integer polynomials in three variables, represented by nested dense polynomials.

Equations

• FD1D.BellmanCertificate.Poly3 = FD1D.BellmanCertificate.DPoly (FD1D.BellmanCertificate.DPoly (FD1D.BellmanCertificate.DPoly ℤ))

def FD1D.BellmanCertificate.U : Poly3

The outermost variable of a three-variable polynomial.

Equations

• FD1D.BellmanCertificate.U = FD1D.BellmanCertificate.DPoly.X

def FD1D.BellmanCertificate.V : Poly3

The middle variable of a three-variable polynomial.

Equations

• FD1D.BellmanCertificate.V = FD1D.BellmanCertificate.DPoly.const FD1D.BellmanCertificate.DPoly.X

def FD1D.BellmanCertificate.Z : Poly3

The innermost variable of a three-variable polynomial.

Equations

• FD1D.BellmanCertificate.Z = FD1D.BellmanCertificate.DPoly.const (FD1D.BellmanCertificate.DPoly.const FD1D.BellmanCertificate.DPoly.X)

def FD1D.BellmanCertificate.eval1 (p : DPoly ℤ) (z : ℝ) : ℝ

Real evaluation of an integer polynomial at its single argument.

Equations

• FD1D.BellmanCertificate.eval1 p z = FD1D.BellmanCertificate.DPoly.eval (fun (c : ℤ) => ↑c) z p

def FD1D.BellmanCertificate.eval2 (p : DPoly (DPoly ℤ)) (v z : ℝ) : ℝ

Real evaluation of a nested polynomial at the middle and innermost variables.

Equations

• FD1D.BellmanCertificate.eval2 p v z = FD1D.BellmanCertificate.DPoly.eval (fun (q : FD1D.BellmanCertificate.DPoly ℤ) => FD1D.BellmanCertificate.eval1 q z) v p

def FD1D.BellmanCertificate.eval3 (p : Poly3) (u v z : ℝ) : ℝ

Real evaluation of a three-variable integer polynomial.

Equations

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

@[simp]

theorem FD1D.BellmanCertificate.eval1_zero (z : ℝ) : eval1 0 z = 0

@[simp]

theorem FD1D.BellmanCertificate.eval1_one (z : ℝ) : eval1 1 z = 1

@[simp]

theorem FD1D.BellmanCertificate.eval1_add (p q : DPoly ℤ) (z : ℝ) : eval1 (p + q) z = eval1 p z + eval1 q z

@[simp]

theorem FD1D.BellmanCertificate.eval1_neg (p : DPoly ℤ) (z : ℝ) : eval1 (-p) z = -eval1 p z

@[simp]

theorem FD1D.BellmanCertificate.eval1_mul (p q : DPoly ℤ) (z : ℝ) : eval1 (p * q) z = eval1 p z * eval1 q z

@[simp]

theorem FD1D.BellmanCertificate.eval1_pow (p : DPoly ℤ) (z : ℝ) (n : ℕ) : eval1 (p ^ n) z = eval1 p z ^ n

@[simp]

theorem FD1D.BellmanCertificate.eval2_zero (v z : ℝ) : eval2 0 v z = 0

@[simp]

theorem FD1D.BellmanCertificate.eval2_one (v z : ℝ) : eval2 1 v z = 1

@[simp]

theorem FD1D.BellmanCertificate.eval2_add (p q : DPoly (DPoly ℤ)) (v z : ℝ) : eval2 (p + q) v z = eval2 p v z + eval2 q v z

@[simp]

theorem FD1D.BellmanCertificate.eval2_neg (p : DPoly (DPoly ℤ)) (v z : ℝ) : eval2 (-p) v z = -eval2 p v z

@[simp]

theorem FD1D.BellmanCertificate.eval2_mul (p q : DPoly (DPoly ℤ)) (v z : ℝ) : eval2 (p * q) v z = eval2 p v z * eval2 q v z

@[simp]

theorem FD1D.BellmanCertificate.eval2_pow (p : DPoly (DPoly ℤ)) (v z : ℝ) (n : ℕ) : eval2 (p ^ n) v z = eval2 p v z ^ n

@[simp]

theorem FD1D.BellmanCertificate.eval3_zero (u v z : ℝ) : eval3 0 u v z = 0

@[simp]

theorem FD1D.BellmanCertificate.eval3_one (u v z : ℝ) : eval3 1 u v z = 1

@[simp]

theorem FD1D.BellmanCertificate.eval3_add (p q : Poly3) (u v z : ℝ) : eval3 (p + q) u v z = eval3 p u v z + eval3 q u v z

@[simp]

theorem FD1D.BellmanCertificate.eval3_neg (p : Poly3) (u v z : ℝ) : eval3 (-p) u v z = -eval3 p u v z

@[simp]

theorem FD1D.BellmanCertificate.eval3_mul (p q : Poly3) (u v z : ℝ) : eval3 (p * q) u v z = eval3 p u v z * eval3 q u v z

@[simp]

theorem FD1D.BellmanCertificate.eval3_pow (p : Poly3) (u v z : ℝ) (n : ℕ) : eval3 (p ^ n) u v z = eval3 p u v z ^ n

@[simp]

theorem FD1D.BellmanCertificate.eval3_sub (p q : Poly3) (u v z : ℝ) : eval3 (p - q) u v z = eval3 p u v z - eval3 q u v z

@[simp]

theorem FD1D.BellmanCertificate.eval3_U (u v z : ℝ) : eval3 U u v z = u

@[simp]

theorem FD1D.BellmanCertificate.eval3_V (u v z : ℝ) : eval3 V u v z = v

@[simp]

theorem FD1D.BellmanCertificate.eval3_Z (u v z : ℝ) : eval3 Z u v z = z

@[simp]

theorem FD1D.BellmanCertificate.eval3_two (u v z : ℝ) : eval3 2 u v z = 2

@[simp]

theorem FD1D.BellmanCertificate.eval3_three (u v z : ℝ) : eval3 3 u v z = 3

@[simp]

theorem FD1D.BellmanCertificate.eval3_four (u v z : ℝ) : eval3 4 u v z = 4

@[simp]

theorem FD1D.BellmanCertificate.eval3_seven (u v z : ℝ) : eval3 7 u v z = 7

@[simp]

theorem FD1D.BellmanCertificate.eval3_twelve (u v z : ℝ) : eval3 12 u v z = 12

@[simp]

theorem FD1D.BellmanCertificate.eval3_twentyFive (u v z : ℝ) : eval3 25 u v z = 25

@[simp]

theorem FD1D.BellmanCertificate.eval3_fifty (u v z : ℝ) : eval3 50 u v z = 50

@[simp]

theorem FD1D.BellmanCertificate.eval3_sixHundred (u v z : ℝ) : eval3 600 u v z = 600

def FD1D.BellmanCertificate.bellmanAt (s r v : Poly3) : Poly3

Polynomial numerator used to certify the Bellman inequality in affine coordinates.

Equations

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

def FD1D.BellmanCertificate.projectiveBellmanAt (den s num v : Poly3) : Poly3

Homogenized Bellman polynomial for a rational coordinate with the given denominator.

Equations

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

def FD1D.BellmanCertificate.bellmanRealAt (s r v : ℝ) : ℝ

Real-valued expression corresponding to the affine Bellman polynomial.

Equations

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

def FD1D.BellmanCertificate.projectiveBellmanRealAt (den s num v : ℝ) : ℝ

Real-valued expression corresponding to the homogenized Bellman polynomial.

Equations

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

theorem FD1D.BellmanCertificate.eval3_bellmanAt (s r v : Poly3) (u₀ v₀ z₀ : ℝ) : eval3 (bellmanAt s r v) u₀ v₀ z₀ = bellmanRealAt (eval3 s u₀ v₀ z₀) (eval3 r u₀ v₀ z₀) (eval3 v u₀ v₀ z₀)

theorem FD1D.BellmanCertificate.eval3_projectiveBellmanAt (den s num v : Poly3) (u₀ v₀ z₀ : ℝ) : eval3 (projectiveBellmanAt den s num v) u₀ v₀ z₀ = projectiveBellmanRealAt (eval3 den u₀ v₀ z₀) (eval3 s u₀ v₀ z₀) (eval3 num u₀ v₀ z₀) (eval3 v u₀ v₀ z₀)

theorem FD1D.BellmanCertificate.projectiveBellmanRealAt_eq {den s num v : ℝ} (hden : den ≠ 0) : projectiveBellmanRealAt den s num v = den ^ 5 * bellmanRealAt s (num / den) v

def FD1D.BellmanCertificate.chartPlus : Poly3

Bellman certificate in the positive projective chart.

Equations

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

def FD1D.BellmanCertificate.chartOne : Poly3

Bellman certificate after the first negative-coordinate chart substitution.

Equations

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

def FD1D.BellmanCertificate.chartTwo : Poly3

Bellman certificate after the second negative-coordinate chart substitution.

Equations

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

def FD1D.BellmanCertificate.chartThree : Poly3

Bellman certificate after the third negative-coordinate chart substitution.

Equations

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

def FD1D.BellmanCertificate.chartEndpoint : Poly3

Projective Bellman certificate at the endpoint coordinate 1 / 2.

Equations

• FD1D.BellmanCertificate.chartEndpoint = FD1D.BellmanCertificate.projectiveBellmanAt 2 (2 * FD1D.BellmanCertificate.V + FD1D.BellmanCertificate.Z) 1 FD1D.BellmanCertificate.V

def FD1D.BellmanCertificate.allNonnegative1 (p : DPoly ℤ) : Bool

Decidable check that every integer coefficient is nonnegative.

Equations

• FD1D.BellmanCertificate.allNonnegative1 p = p.coeffs.all fun (c : ℤ) => decide (0 ≤ c)

def FD1D.BellmanCertificate.allNonnegative2 (p : DPoly (DPoly ℤ)) : Bool

Decidable check of nonnegativity of every coefficient in two variables.

Equations

• FD1D.BellmanCertificate.allNonnegative2 p = p.coeffs.all FD1D.BellmanCertificate.allNonnegative1

def FD1D.BellmanCertificate.allNonnegative3 (p : Poly3) : Bool

Decidable check of nonnegativity of every coefficient in three variables.

Equations

• FD1D.BellmanCertificate.allNonnegative3 p = p.coeffs.all FD1D.BellmanCertificate.allNonnegative2

def FD1D.BellmanCertificate.nonzeroCount1 (p : DPoly ℤ) : ℕ

Number of nonzero coefficients in a dense polynomial.

Equations

• FD1D.BellmanCertificate.nonzeroCount1 p = List.countP (fun (x : ℤ) => decide (x ≠ 0)) p.coeffs

def FD1D.BellmanCertificate.nonzeroCount2 (p : DPoly (DPoly ℤ)) : ℕ

Number of nonzero integer coefficients in a two-variable polynomial.

Equations

• FD1D.BellmanCertificate.nonzeroCount2 p = (List.map FD1D.BellmanCertificate.nonzeroCount1 p.coeffs).sum

def FD1D.BellmanCertificate.nonzeroCount3 (p : Poly3) : ℕ

Number of nonzero integer coefficients in a three-variable polynomial.

Equations

• FD1D.BellmanCertificate.nonzeroCount3 p = (List.map FD1D.BellmanCertificate.nonzeroCount2 p.coeffs).sum

theorem FD1D.BellmanCertificate.DPoly.eval_nonnegative_of_all {R : Type} (good : R → Bool) (f : R → ℝ) (hgood : ∀ (a : R), good a = true → 0 ≤ f a) {x : ℝ} (hx : 0 ≤ x) (p : DPoly R) (hp : p.coeffs.all good = true) : 0 ≤ eval f x p

theorem FD1D.BellmanCertificate.eval1_nonnegative {p : DPoly ℤ} (hp : allNonnegative1 p = true) {z : ℝ} (hz : 0 ≤ z) : 0 ≤ eval1 p z

theorem FD1D.BellmanCertificate.eval2_nonnegative {p : DPoly (DPoly ℤ)} (hp : allNonnegative2 p = true) {v z : ℝ} (hv : 0 ≤ v) (hz : 0 ≤ z) : 0 ≤ eval2 p v z

theorem FD1D.BellmanCertificate.eval3_nonnegative {p : Poly3} (hp : allNonnegative3 p = true) {u v z : ℝ} (hu : 0 ≤ u) (hv : 0 ≤ v) (hz : 0 ≤ z) : 0 ≤ eval3 p u v z

theorem FD1D.BellmanCertificate.chartPlus_check : allNonnegative3 chartPlus = true

theorem FD1D.BellmanCertificate.chartOne_check : allNonnegative3 chartOne = true

theorem FD1D.BellmanCertificate.chartTwo_check : allNonnegative3 chartTwo = true

theorem FD1D.BellmanCertificate.chartThree_check : allNonnegative3 chartThree = true

theorem FD1D.BellmanCertificate.chartEndpoint_check : allNonnegative3 chartEndpoint = true

theorem FD1D.BellmanCertificate.chartPlus_nonnegative {u v z : ℝ} (hu : 0 ≤ u) (hv : 0 ≤ v) (hz : 0 ≤ z) : 0 ≤ projectiveBellmanRealAt (2 * (1 + u)) (2 * v + z) u v

theorem FD1D.BellmanCertificate.chartOne_nonnegative {u v z : ℝ} (hu : 0 ≤ u) (hv : 0 ≤ v) (hz : 0 ≤ z) : 0 ≤ bellmanRealAt (2 * u + 2 * v + z) (-u) (u + v)

theorem FD1D.BellmanCertificate.chartTwo_nonnegative {u v z : ℝ} (hu : 0 ≤ u) (hv : 0 ≤ v) (hz : 0 ≤ z) : 0 ≤ bellmanRealAt (2 * u + 2 * v + z) (-2 * u - v) (u + v)

theorem FD1D.BellmanCertificate.chartThree_nonnegative {u v z : ℝ} (hu : 0 ≤ u) (hv : 0 ≤ v) (hz : 0 ≤ z) : 0 ≤ bellmanRealAt (u + 2 * v + z) (-u - 2 * v) v

theorem FD1D.BellmanCertificate.chartEndpoint_nonnegative {v z : ℝ} (hv : 0 ≤ v) (hz : 0 ≤ z) : 0 ≤ projectiveBellmanRealAt 2 (2 * v + z) 1 v