log_2_in_interval
plain-language theorem explainer
The declaration proves that the natural logarithm of 2 lies inside the closed rational interval from 693/1000 to 694/1000. Numerics researchers verifying transcendental bounds in formal libraries would cite this when tightening logarithmic intervals. The proof reduces the containment predicate via simplification, splits the conjunction, and chains Mathlib's log_two_gt_d9 and log_two_lt_d9 lemmas with norm_num rational comparisons.
Claim. $693/1000 ≤ log 2 ≤ 694/1000$
background
The module supplies machine-checked interval bounds for the natural logarithm. An Interval is a structure with rational endpoints lo and hi satisfying lo ≤ hi. The predicate contains I x holds precisely when lo ≤ x ≤ hi. The definition log2Interval fixes the concrete interval with lo = 693/1000 and hi = 694/1000. The surrounding module strategy uses monotonicity of log together with Taylor error bounds for log(1+x) when |x|<1, and invokes Mathlib's pre-proved decimal bounds on log 2.
proof idea
The tactic proof first simplifies contains and log2Interval to obtain the two-sided inequality. A constructor splits the conjunction. The lower bound applies Real.log_two_gt_d9 after rewriting 693/1000 to the decimal 0.693 and chaining strict inequalities with norm_num. The upper bound applies Real.log_two_lt_d9, again rewriting 694/1000 to 0.694 and using norm_num to close the comparison.
why it matters
This supplies a verified numeric anchor for log 2 inside the Recognition numerics layer. It directly discharges the log2Interval definition and supports downstream interval arithmetic for constants appearing in phi-ladder mass formulas and alpha-band estimates. No parent theorems are recorded among the used-by edges, so the result functions as a leaf fact rather than an intermediate step in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.