point
plain-language theorem explainer
Point constructs a degenerate interval from a single rational q by setting both endpoints equal. Numerical analysts in the Recognition framework cite it to embed exact rationals into the interval type for bounding computations. The definition is a direct structure constructor that discharges the ordering constraint with the reflexivity lemma on the order relation.
Claim. For a rational $q$, the point interval is the closed interval with lower endpoint $q$ and upper endpoint $q$.
background
Interval is the structure with rational fields lo and hi together with a proof that lo ≤ hi. The module supplies verified interval arithmetic that uses exact rational endpoints to bound real values of transcendental functions. The upstream le_refl result states that every element satisfies n ≤ n and is invoked here to validate the degenerate case.
proof idea
The definition is a direct structure constructor. It assigns the input q to both lo and hi, then applies le_refl to discharge the valid field.
why it matters
This definition supplies the embedding of exact rationals into the interval layer that supports the convexity and uniqueness theorems for the J-action. It is invoked in costRateEL_implies_const_one, actionJ_convex_on_interp, actionJ_minimum_unique_value and geodesic_minimizes_unconditional, which establish that geodesics minimize the Recognition cost functional. The construction therefore underpins numerical verification of the Recognition Composition Law and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.