log_10_in_interval
plain-language theorem explainer
The declaration proves that the natural logarithm of 10 lies inside the closed interval [2.30, 2.31]. Researchers building rigorous enclosures for transcendental functions in formal numerics would cite this result when anchoring logarithmic computations. The proof decomposes log(10) into 3 log(2) plus log(5/4), invokes Mathlib bounds on log(2), and closes the enclosure with Taylor remainder estimates on log(1.25).
Claim. $2.30 ≤ log 10 ≤ 2.31$
background
The module supplies interval arithmetic for the natural logarithm, using monotonicity on (0, ∞) together with Taylor series error bounds for log(1 + x) when |x| < 1. The predicate contains asserts that a real number x satisfies lo ≤ x ≤ hi for a given Interval. The concrete interval log10Interval is the pointwise enclosure [230/100, 231/100]. Upstream results include the definition of contains, the declaration of log10Interval itself, and Mathlib lemmas Real.log_two_gt_d9 together with Real.exp_bound for remainder control.
proof idea
The tactic proof first simplifies the containment goal. It then proves the algebraic identity log(10) = 3 log(2) + log(5/4) by norm_num rewriting and the lemmas Real.log_mul, Real.log_pow. Separate have statements import the Mathlib bounds log 2 > 0.6931471803 and log 2 < 0.6931471808. For log(5/4) the proof rewrites the target inequalities as exp bounds, applies Real.exp_bound at orders 5 and 4, extracts the Taylor partial sums, and finishes both sides with linarith.
why it matters
The result supplies a verified numerical anchor for log(10) inside the Recognition Science numerics layer. It supports sibling constructions such as logPhiInterval and phi bounds by furnishing a concrete, machine-checked enclosure. In the larger framework it contributes to rigorous control of constants whose decimal representations involve logarithms, consistent with the interval-arithmetic strategy outlined in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.