contains_point
plain-language theorem explainer
The theorem states that the degenerate interval with both endpoints at a rational q contains the real number q. Code that certifies bounds on powers of the golden ratio or other constants in the Recognition numerics layer cites this fact as a base case. The proof is a one-line term that applies reflexivity of the order relation to each endpoint.
Claim. For every rational number $q$, let $I$ be the closed interval whose lower and upper bounds are both equal to $q$. Then the real number obtained by casting $q$ satisfies $q$ lies between the lower and upper bounds of $I$.
background
The module supplies verified interval arithmetic that uses exact rational endpoints to bound real values. An Interval is a structure carrying rational lower and upper bounds together with a proof that the lower bound is at most the upper bound. The contains predicate holds precisely when the lower bound is at most the real number and the real number is at most the upper bound. The point constructor produces the degenerate interval whose bounds are both $q$ and whose validity proof is supplied by reflexivity of the order on rationals.
proof idea
The proof is a one-line term that constructs the required pair of inequalities by applying the reflexivity theorem le_refl to the lower bound and again to the upper bound.
why it matters
The result is invoked by the theorem phi_pow_142_in_interval that places a high power of the golden ratio inside a precomputed rational interval. It therefore supports the larger effort to obtain rigorous bounds on constants that appear on the phi-ladder and in the Recognition Science mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.