log2Interval
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove that log(2) lies inside the interval.
- Does not supply bounds for log(φ) or other constants.
- Does not tighten the 0.001-width enclosure.
- Does not extend the construction to complex logarithms.
formal statement (Lean)
333def log2Interval : Interval where
334 lo := 693 / 1000
proof body
Definition body.
335 hi := 694 / 1000
336 valid := by norm_num
337
338/-- log(2) is contained in log2Interval - PROVEN using Mathlib's log_two bounds -/