Bernstein polynomial bounds

bernstein_bound proves ∀ x ∈ I, f x ⋈ c for a univariate rational polynomial f by the recursive Bernstein certificate LeanCert.Validity.Bernstein.checkPoly*Bound. Untrusted search finds the least bisection depth at which the certificate succeeds; the retained proof closes that single Boolean certificate through the configured verification route and lifts it with the matching golden theorem.

The strategy is typed and transactional: every non-success restores the complete caller state, and a goal that is not a polynomial reports notPolynomial so the semantic router can skip it without spending budget.

structure LeanCert.Tactic.Auto.BernsteinBoundOutcome : Type

Runtime facts retained by a successful Bernstein certificate.

• checker : Lean.Name
• verifier : Lean.Name
• verification : VerificationUsage
• configuredDepth : ℕ
• depthUsed : ℕ
• boxesExamined : ℕ
• enclosure : Core.IntervalRat

  Bernstein enclosure of the polynomial on the whole interval.

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedBernsteinBoundOutcome : Inhabited BernsteinBoundOutcome

Equations

• LeanCert.Tactic.Auto.instInhabitedBernsteinBoundOutcome = { default := LeanCert.Tactic.Auto.instInhabitedBernsteinBoundOutcome.default }

inductive LeanCert.Tactic.Auto.BernsteinBoundFailure : Type

Expected non-successes of the Bernstein strategy.

• unsupported (expression detail : String) : BernsteinBoundFailure
• notPolynomial (expression : String) : BernsteinBoundFailure
• exhausted (configuredDepth : ℕ) (enclosure : Core.IntervalRat) : BernsteinBoundFailure
• rejected (checker : Lean.Name) (detail : String) : BernsteinBoundFailure
• transportFailure (detail : String) : BernsteinBoundFailure
• internalFailure (detail : String) : BernsteinBoundFailure

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedBernsteinBoundFailure : Inhabited BernsteinBoundFailure

Equations

• LeanCert.Tactic.Auto.instInhabitedBernsteinBoundFailure = { default := LeanCert.Tactic.Auto.instInhabitedBernsteinBoundFailure.default }

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprBernsteinBoundFailure : Repr BernsteinBoundFailure

Equations

• LeanCert.Tactic.Auto.instReprBernsteinBoundFailure = { reprPrec := LeanCert.Tactic.Auto.instReprBernsteinBoundFailure.repr }

def LeanCert.Tactic.Auto.instReprBernsteinBoundFailure.repr : BernsteinBoundFailure → ℕ → Std.Format

Equations

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

def LeanCert.Tactic.Auto.BernsteinBoundFailure.message (tacticName : String) : BernsteinBoundFailure → Lean.MessageData

Equations

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

unsafe def LeanCert.Tactic.Auto.evalQPoly? (ast : Lean.Expr) : Lean.MetaM (Option Engine.QPoly)

Untrusted: recognise the reified AST as a QPoly.

Equations

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

unsafe def LeanCert.Tactic.Auto.isPolynomialAst (ast : Lean.Expr) : Lean.MetaM Bool

Untrusted: is the reified AST a univariate rational polynomial? Used by the router to decide applicability before spending budget.

Equations

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

unsafe def LeanCert.Tactic.Auto.bernsteinBoundCoreTyped (maxDepth : ℕ) : Lean.Elab.Tactic.TacticM (Except BernsteinBoundFailure BernsteinBoundOutcome)

Typed and exception-total Bernstein entry point. Every non-success restores the complete caller tactic state. Success preserves pending sibling goals.

Equations

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

def LeanCert.Tactic.Auto.tacticBernstein_bound__ : Lean.ParserDescr

bernstein_bound [depth] proves a univariate polynomial interval bound by Bernstein coefficients, bisecting at most depth times (default 8).

Equations

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