Exact polynomial integral certificates

This module recognizes the rational-polynomial fragment of LeanCert.Core.Expr and checks exact definite integrals using executable rational arithmetic. The checker is intentionally small: certificate discovery may happen in tactics or external tooling, while Lean verifies the reflected polynomial and endpoint evaluation.

def LeanCert.Engine.QPoly.ofExpr : Core.Expr → Option QPoly

Recognize a single-variable rational polynomial expression.

Equations

• LeanCert.Engine.QPoly.ofExpr (LeanCert.Core.Expr.const q) = some (LeanCert.Engine.QPoly.constant q)
• LeanCert.Engine.QPoly.ofExpr (LeanCert.Core.Expr.var 0) = some LeanCert.Engine.QPoly.X
• LeanCert.Engine.QPoly.ofExpr (LeanCert.Core.Expr.var idx) = none
• LeanCert.Engine.QPoly.ofExpr (e₁.add e₂) = match LeanCert.Engine.QPoly.ofExpr e₁, LeanCert.Engine.QPoly.ofExpr e₂ with | some p₁, some p₂ => some (p₁.add p₂) | x, x_1 => none
• LeanCert.Engine.QPoly.ofExpr (e₁.mul e₂) = match LeanCert.Engine.QPoly.ofExpr e₁, LeanCert.Engine.QPoly.ofExpr e₂ with | some p₁, some p₂ => some (p₁.mul p₂) | x, x_1 => none
• LeanCert.Engine.QPoly.ofExpr e.neg = match LeanCert.Engine.QPoly.ofExpr e with | some p => some ((LeanCert.Engine.QPoly.constant (-1)).mul p) | none => none
• LeanCert.Engine.QPoly.ofExpr (LeanCert.Core.Expr.const q).inv = if q = 0 then none else some (LeanCert.Engine.QPoly.constant q⁻¹)
• LeanCert.Engine.QPoly.ofExpr x✝ = none

theorem LeanCert.Engine.QPoly.ofExpr_correct {e : Core.Expr} {p : QPoly} (h : ofExpr e = some p) (x : ℝ) : Core.Expr.eval (fun (x_1 : ℕ) => x) e = Core.Expr.eval (fun (x_1 : ℕ) => x) p.toExpr

Successful polynomial recognition preserves real semantics.

def LeanCert.Engine.QPoly.checkExactIntegral (e : Core.Expr) (a b value : ℚ) : Bool

Boolean checker for an exact rational-polynomial definite integral.

Equations

• LeanCert.Engine.QPoly.checkExactIntegral e a b value = match LeanCert.Engine.QPoly.ofExpr e with | some p => decide (p.integralRat a b = value) | none => false

theorem LeanCert.Engine.QPoly.integral_eq_of_check (e : Core.Expr) (a b value : ℚ) (hcheck : checkExactIntegral e a b value = true) : ∫ (x : ℝ) in ↑a..↑b, Core.Expr.eval (fun (x_1 : ℕ) => x) e = ↑value

Golden theorem for exact rational-polynomial integration certificates.