prove_upper_bound_le
plain-language theorem explainer
The theorem states that if a real x belongs to an interval I whose upper endpoint is at most a rational b, then x is at most b. Numerics users in the Recognition framework cite it when discharging upper bounds on expressions such as log phi during tactic verification. The proof is a direct one-line term application of the hi_le_implies_contains_le lemma from the basic interval module.
Claim. If $x$ belongs to interval $I$ and the upper endpoint of $I$ satisfies $I.hi ≤ b$ for rational $b$, then $x ≤ b$.
background
The module supplies tactics for proving bounds on transcendental expressions via interval arithmetic, with the main tactic interval_bound used to verify statements such as (0.481 : ℝ) < Real.log 1.618. Interval is the core type carrying lower and upper endpoints together with a contains predicate that checks membership of a real. The hi_le_implies_contains_le lemma from the Basic submodule supplies the key implication that an upper-endpoint bound plus membership yields the desired real inequality.
proof idea
The proof is a one-line term wrapper that applies hi_le_implies_contains_le directly to the hypotheses h_hi and h_contains.
why it matters
This lemma belongs to the interval-bound tactic suite that supports verification of phi-ladder constants and related bounds inside the Recognition framework. It feeds the sibling results such as log_phi_gt_048 and phi_gt_161 that appear in the same module. The declaration closes a small but necessary gap in the numerics layer used to confirm constants such as alpha inverse inside the documented band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.