log10Interval
plain-language theorem explainer
The definition supplies a rational interval [2.30, 2.31] guaranteed to contain the natural logarithm of 10. Numerics code in the Recognition framework cites it to obtain certified bounds on the logarithm of ten without floating-point error. The definition is a direct construction of an interval structure with endpoints 230/100 and 231/100, validated by norm_num.
Claim. Define the closed interval $I = [230/100, 231/100]$ with rational endpoints.
background
Interval is the structure from Numerics.Interval.Basic consisting of rational lower and upper bounds together with a proof that the lower bound does not exceed the upper bound. The module develops interval arithmetic for the natural logarithm, using monotonicity on (0, ∞) and Taylor series error estimates for log(1+x) when |x|<1. This particular definition supplies a simple rational enclosure for log(10) that later steps certify.
proof idea
The definition constructs the Interval record directly by setting the lower endpoint to 230/100 and the upper endpoint to 231/100, then discharges the ordering obligation with the norm_num tactic.
why it matters
This interval serves as the target for the containment result in the same module that places log(10) inside [2.30, 2.31]. It supplies one of the certified numerical constants required for downstream computations involving the phi-ladder and the recognition composition law. No open scaffolding questions are closed by this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.