logIntervalMono
plain-language theorem explainer
This definition packages supplied rational bounds into an Interval that is guaranteed to contain the image of a positive input interval under the natural logarithm. Numerics code that propagates interval bounds through log operations in the Recognition framework would cite it. The body is a direct structure constructor that assembles the given lo_bound, hi_bound and their ordering hypothesis.
Claim. Let $I$ be a closed interval with positive lower endpoint. Let $l,u$ be rationals satisfying $l ≤ log(lo(I))$, $log(hi(I)) ≤ u$ and $l ≤ u$. The interval with endpoints $l$ and $u$ is returned.
background
The module supplies rigorous interval arithmetic for the natural logarithm on positive intervals. Interval is the structure with rational endpoints lo and hi together with a proof lo ≤ hi. The local strategy rests on monotonicity of log on (0,∞), so that log([a,b]) ⊆ [log a, log b]. Upstream results supply the two Interval structures (one rational, one real) that are instantiated here.
proof idea
The definition is a direct constructor for the Interval structure. It takes the supplied rational bounds and the hypothesis that they are ordered, then returns the interval whose components are exactly those values.
why it matters
This definition supplies the concrete interval object shown to contain the true logarithm in the companion theorem logIntervalMono_contains_log. It forms part of the numerical certification layer that supports interval propagation for log in the Recognition Science numerics, including bounds needed for log(φ) on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.