log2Interval
plain-language theorem explainer
log2Interval defines the closed rational interval [0.693, 0.694] that encloses the natural logarithm of 2. Numerics code in the Recognition framework cites this definition to obtain machine-checked bounds on log(2) for subsequent interval arithmetic. The construction is a direct record with explicit rational endpoints and a norm_num discharge of the ordering condition.
Claim. The closed interval $I = [693/1000, 694/1000]subseteqmathbb{Q}$ equipped with the proof that $693/1000leq694/1000$.
background
The Interval structure from Numerics.Interval.Basic is a record with rational fields lo and hi together with a proof that lo ≤ hi. This module supplies rigorous interval bounds for the natural logarithm by combining Mathlib's monotonicity and Taylor error estimates. The local setting is interval arithmetic over (0, ∞) for constants such as log(2) and log(φ) that appear in Recognition calculations.
proof idea
One-line definition that directly constructs the Interval record with lo := 693/1000, hi := 694/1000 and discharges the validity field via the norm_num tactic.
why it matters
The definition supplies the concrete interval used by the downstream theorem log_2_in_interval to certify containment of log(2). It supports the module's strategy of bounding logarithms via monotonicity and Taylor remainders, which in turn feeds phi-ladder numerics and the eight-tick octave calculations in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.