logIntervalMono
logIntervalMono constructs a rational-endpoint interval that encloses the image of a positive input interval under the natural logarithm, by direct packaging of supplied lower and upper rational bounds. Numerics code establishing rigorous enclosures for log(φ) or related constants in the Recognition Science pipeline would invoke it. The definition is a direct structure constructor that assigns the provided bounds and their ordering hypothesis to the Interval fields.
claimLet $I$ be a closed interval with positive lower endpoint. Given rationals $l,u$ such that $l$ is at most the natural logarithm of the lower endpoint of $I$, the natural logarithm of the upper endpoint of $I$ is at most $u$, and $l$ is at most $u$, the closed interval with endpoints $l$ and $u$ is returned.
background
Interval is the structure consisting of rational lower and upper endpoints together with a proof that the lower endpoint is at most the upper endpoint. The module develops interval arithmetic for the natural logarithm on positive reals, using the fact that the logarithm is monotonically increasing to obtain an enclosure directly from the endpoints of the input interval. Upstream, the rational-endpoint Interval from Numerics.Interval.Basic supplies the concrete type constructed here, while the real-endpoint Interval from Recognition.Certification supplies the variant used elsewhere in the framework.
proof idea
The definition is a direct structure constructor that assigns the supplied lo_bound to the lower endpoint, hi_bound to the upper endpoint, and the supplied validity hypothesis to the ordering field.
why it matters in Recognition Science
This definition produces the concrete interval object consumed by the theorem logIntervalMono_contains_log, which verifies enclosure of the logarithm. It supplies the basic enclosure step in the module's strategy for rigorous logarithm bounds, supporting later computations of constants such as ħ = φ^{-5} that rely on tight enclosures of log(φ).
scope and limits
- Does not verify that the supplied rational bounds actually enclose the logarithm of the input interval.
- Does not apply to intervals containing non-positive numbers.
- Does not compute or refine the logarithm bounds internally; the caller must supply them.
formal statement (Lean)
37def logIntervalMono (I : Interval) (_hI_pos : 0 < I.lo)
38 (lo_bound hi_bound : ℚ)
39 (_h_lo : (lo_bound : ℝ) ≤ log I.lo)
40 (_h_hi : log I.hi ≤ (hi_bound : ℝ))
41 (h_valid : lo_bound ≤ hi_bound) : Interval where
42 lo := lo_bound
proof body
Definition body.
43 hi := hi_bound
44 valid := h_valid
45