prove_lower_bound_le
plain-language theorem explainer
The lemma shows that a rational lower bound b satisfies b ≤ x whenever b ≤ I.lo and x belongs to the closed interval I. Numerics users in Recognition Science invoke it when discharging lower-bound subgoals inside interval-arithmetic proofs of transcendental inequalities. It is realized as a one-line wrapper that forwards the hypotheses to the containment-implication theorem.
Claim. Let $I$ be a closed interval with rational endpoints, let $x$ be a real number, and let $b$ be rational. If $b ≤ I.lo$ and $I$ contains $x$, then $b ≤ x$.
background
The module supplies tactics that certify bounds on expressions such as logarithms and powers by means of interval arithmetic. An Interval is a structure consisting of rational lower and upper endpoints together with a proof that the lower does not exceed the upper. The predicate contains asserts that a real number lies between those endpoints inclusive. The supporting lemma lo_ge_implies_contains_ge states that any real lower bound no larger than the interval's lower endpoint is also a lower bound for every point inside the interval.
proof idea
The proof is a one-line wrapper that applies the lemma lo_ge_implies_contains_ge to the supplied hypotheses h_lo and h_contains.
why it matters
This declaration supplies a basic monotonicity fact required by the interval_bound tactic when the module verifies concrete numerical inequalities that appear in the Recognition Science constants, such as the bounds on log phi or the fine-structure constant alpha. It closes a small gap in the numerics layer that supports the phi-ladder mass formulas and the eight-tick octave. No open questions are attached to this specific wrapper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.