prove_lower_bound
plain-language theorem explainer
A helper theorem shows that if a rational b lies strictly below the lower endpoint of a closed rational interval I and a real x lies inside I, then b is strictly less than x. Numerics code in the Recognition framework invokes it to discharge lower bounds during interval arithmetic verification of expressions involving phi. The proof is a direct one-line wrapper around the core containment implication lemma.
Claim. Let $I$ be a closed interval with rational endpoints. If $b$ is rational with $b < I.lo$ and $x$ is real satisfying $I.lo ≤ x ≤ I.hi$, then $b < x$.
background
Interval is the structure of closed intervals with rational endpoints lo and hi obeying lo ≤ hi. The contains predicate asserts that a real x satisfies lo ≤ x ≤ hi after casting the rationals to reals. The upstream lemma lo_gt_implies_contains_gt states that b < I.lo implies b < x for every x in I, obtained by casting the strict inequality and using the left conjunct of containment.
proof idea
One-line wrapper that applies lo_gt_implies_contains_gt to the hypotheses h_lo and h_contains.
why it matters
The declaration supplies a reusable step inside the interval_bound tactic for certifying numerical inequalities on phi, log phi, and related constants. It supports verification of bounds such as those appearing in the phi-ladder and the alpha inverse interval (137.030, 137.039). Sibling declarations in the same module perform analogous upper-bound and specific phi checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.