Failure diagnostics for interval proofs

Tactic.diagnoseFailure explains a failed binary-grid check without constructing proof evidence. Algebraic failures follow the checker's subdivision order and use the existing evaluator to locate the first rejected operation. Registered functions are inspected through their actual quoted backend. An enclosure that includes a forbidden value is reported as an enclosure obstruction, not as a claim about the real subexpression.

Diagnostic retries change one accuracy setting at a time. They describe only the inspected box; the tactic must still verify every successful proof with its usual kernel check. All work is confined to the failure path, and the entry point restores the caller's metavariable state.

def FloatLib.Numerics.Interval.Tactic.diagnoseRegisteredFailure (expression : Q(Expr)) (backend : Q(Backend ℤ)) (box : Q(Box)) (config : Q(Backend.Config)) (relation : Q(Relation)) (depth : Q(ℕ)) (atoms : Array Lean.Expr := #[]) : Lean.MetaM Lean.MessageData

Inspect the actual registered backend by reduction, within the caller's diagnostic budget. The displayed enclosure belongs to the original box; subdivision may have narrower children.

def FloatLib.Numerics.Interval.Tactic.preflightCheck (expression : Q(Expr)) (box : Q(Box)) (config : Q(Backend.Config)) (relation : Q(Relation)) (depth : Q(ℕ)) : Lean.MetaM (Option Bool)

Inspect the executable checker before kernel verification. A failed leaf can reject the attempt early; this advisory result never supplies evidence for a successful proof.

def FloatLib.Numerics.Interval.Tactic.diagnoseFailure (expression : Q(Expr)) (box : Q(Box)) (config : Q(Backend.Config)) (relation : Q(Relation)) (depth : Q(ℕ)) (atoms : Array Lean.Expr := #[]) : Lean.MetaM Lean.MessageData

Explain a failed Expr.check using its quoted expression, box, binary-grid configuration, relation, and subdivision depth. The optional atoms array supplies the original real terms in variable index order; otherwise variables are displayed as x[i].

Call only after the kernel verification fails. This function returns advisory text, never proof evidence. It restores Meta state even on exceptions and propagates interrupts, heartbeat exhaustion, and recursion limits. Unknown inspection failures receive a generic diagnostic. A bounded search can report that its own diagnostic budget ran out, without claiming subdivision was exhausted.