prove_upper_bound
plain-language theorem explainer
The theorem states that if a real number x lies inside a closed rational interval I and the upper endpoint of I is strictly below a rational b, then x is strictly below b. Numerics developers building interval tactics for transcendental bounds would invoke it to discharge upper-bound subgoals. The proof is a direct one-line wrapper around the core containment implication from the basic interval module.
Claim. Let $I$ be a closed interval with rational endpoints, let $x$ be real, and let $b$ be rational. If $x$ is contained in $I$ (i.e., $I$.lo $≤ x ≤ I$.hi) and $I$.hi $< b$, then $x < b$.
background
The module supplies tactics that discharge bounds on expressions such as logarithms and powers of phi by interval arithmetic. An Interval is the structure with rational lo and hi satisfying lo ≤ hi. Containment of a real x in I means lo ≤ x ≤ hi. The upstream lemma hi_lt_implies_contains_lt records the fact that if I.hi < b then every x contained in I satisfies x < b, proved by casting the rational inequality and using the right-hand part of the containment conjunction.
proof idea
One-line wrapper that applies hi_lt_implies_contains_lt to the supplied hypotheses h_hi and h_contains.
why it matters
The result belongs to the numerics layer that certifies concrete bounds on phi and its logarithms, supporting the Recognition Science constants (phi-ladder, alpha band) that appear in mass formulas and the eight-tick octave. It feeds the interval_bound tactic used to verify statements such as log_phi_gt_048 and phi_gt_161. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.