Interval proofs from rational bounds

interval proves real inequalities by evaluating certified interval expressions. It reads rational bounds from the local context and first tries algebraic expressions with exact rational endpoints. The binary-grid backend then handles remaining goals and subdivides the widest input interval when its first enclosure is inconclusive.

Finite sums, dot products, matrix products, and supported norms expand using Mathlib equalities. Pointwise hypotheses supply the bounds of their entries. Real and nonnegative-real inequalities use the same checker; nonnegative-real inputs supply their zero lower bound automatically.

The options precision, degree, and depth control fractional endpoint bits, elementary-function approximation degree, and subdivision depth. A closed Boolean check is verified by Lean's kernel; the expression equality and the input bounds are also proved. No sampled values enter the proof.

def FloatLib.Numerics.Interval.Tactic.close (precision degree depth : ℕ) (maxHeartbeats : ℕ := 20000) : Lean.Elab.Tactic.TacticM Unit

Verify a real or nonnegative-real inequality with exact rational or binary-grid bounds.

def interval : Lean.ParserDescr

Prove a real or nonnegative-real inequality from rational bounds in the local context.

For example, interval (precision := 64) (degree := 16) (depth := 8) chooses a binary endpoint grid with 64 fractional bits, degree-16 elementary enclosures, and at most eight midpoint subdivisions along any branch. These are also the defaults. Each verification attempt and failure diagnostics have separate budgets of 20,000 heartbeats, even when the surrounding declaration disables heartbeat limits. Use (maxHeartbeats := 40000) for a larger finite budget.

Algebraic goals first use exact rational endpoints without subdivision, preserving equality at non-dyadic hypothesis bounds. For arithmetic without registered calls, an advisory executable check rejects failing binary-grid leaves before kernel reduction. Registered calls use bounded kernel reduction directly; every successful proof requires kernel verification.

Concrete finite sums and matrix expressions are expanded automatically, including pointwise bounds such as ∀ i, x i ∈ Set.Icc 0 1. Norms use the instances selected in the goal.

Division requires a denominator interval away from zero; logarithm requires positive inputs, and square root requires nonnegative inputs. Inverse sine and cosine require inputs in [-1, 1]; tangent requires a cosine enclosure excluding zero. Failure reports the obstructing range or insufficient bound and restores the original proof state.