IndisputableMonolith.Numerics.Interval.Tactic
This module supplies tactics for proving numerical bounds via interval containment arguments over the reals. Researchers verifying constants in Recognition Science numerics cite these helpers when closing bounds on functions such as exp, log, and pow. The module consists of a small set of specialized tactics that compose the interval primitives defined in the sibling Basic, Exp, Log, and Pow modules.
claimTactics establishing lower and upper bounds on real functions via interval containment, using rational endpoints to certify inequalities such as $f([a,b])subseteq [c,d]$.
background
The Numerics.Interval suite implements verified interval arithmetic over the reals. The Basic module supplies the core interval representation with rational endpoints for exact computation. Exp, Log, and Pow extend this to transcendental functions using Taylor series and Mathlib bounds. The Tactic module supplies the user-facing interface that turns these interval facts into proof automation. Upstream documentation states: 'This module provides rigorous interval arithmetic for computing bounds on transcendental functions. The key insight is that we use rational endpoints (which Lean can compute exactly) to bound real values.'
proof idea
This is a tactic module. It defines a collection of one-line wrappers (prove_lower_bound, prove_upper_bound, prove_lower_bound_le, prove_upper_bound_le) together with a few specialized containment lemmas (phi_interval_contains, log_phi_interval_contains, etc.). Each tactic applies the interval lemmas imported from Basic, Exp, Log, and Pow, delegating automation to Mathlib.Tactic.
why it matters in Recognition Science
The module closes the numerical verification layer required by the Recognition Science forcing chain (T5–T7). It supplies the concrete bounds on phi and log phi that appear in the phi-ladder mass formula and the alpha band. Although no direct used_by edges are recorded, the sibling lemmas it exposes are the natural targets for any downstream claim that must certify a numerical inequality inside the framework.
scope and limits
- Does not implement new interval operations beyond composition of the imported Exp, Log, Pow, and Basic primitives.
- Does not address floating-point rounding; all endpoints remain rational.
- Does not cover complex numbers, vectors, or integration.
- Does not supply general-purpose interval solvers outside the listed containment tactics.