Roots And No-Root Proofs

Use this path for root existence, uniqueness, and no-root goals over an interval.

Typical goals:

∃ x ∈ I, f x = 0
∃! x ∈ I, f x = 0
∀ x ∈ I, f x ≠ 0

Main tools:

interval_roots
interval_unique_root
root_bound

Minimal root-existence example:

import LeanCert.Tactic.Discovery

open LeanCert.Core

def I12 : IntervalRat := { lo := 1, hi := 2, le := by norm_num }

example : ∃ x ∈ I12, Expr.eval (fun _ => x)
    (Expr.add (Expr.mul (Expr.var 0) (Expr.var 0)) (Expr.neg (Expr.const 2))) = 0 := by
  interval_roots

Architecture background for how the certified root pipeline works is in Root Finding.

For tactic details, see Reference → Tactics.