log2Interval
plain-language theorem explainer
This definition supplies the closed rational interval [693/1000, 694/1000] containing the natural logarithm of 2. Numerics code establishing rigorous bounds on logarithmic expressions would reference it when avoiding floating-point error. The construction is a direct record whose only non-trivial field is discharged by norm_num.
Claim. Let $I = [693/1000, 694/1000] subset mathbb{R}$ with rational endpoints satisfying the lower bound at most the upper bound. Then $I$ is a closed interval containing $log 2$.
background
The Interval structure from Numerics.Interval.Basic is a record with rational fields lo and hi together with the proposition lo ≤ hi. A parallel real-valued Interval appears in Recognition.Certification. The module supplies interval arithmetic for the logarithm via monotonicity on (0, ∞) and Taylor remainder estimates for log(1 + x) when |x| < 1. Upstream results supply the basic Interval record and several is predicates from Foundation and GameTheory modules that are referenced only as dependencies.
proof idea
Direct definition of an Interval record. The valid field is discharged by a single norm_num tactic on the rational inequality 693/1000 ≤ 694/1000.
why it matters
The interval is consumed by the sibling theorem log_2_in_interval, which certifies containment of log 2 and thereby supports error-controlled numerical work throughout the Log module. It forms part of the interval infrastructure required for precise constant bounds inside the Recognition Science numerics layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.