RatInterval
plain-language theorem explainer
A closed interval with rational endpoints and a proof that the lower bound does not exceed the upper. It is the atomic carrier for Delta-real approximation protocols: every nested refinement step is a value of this type. Downstream arithmetic (add, neg, ofRat) and geometric relations (Subset, Overlap, width) are defined directly on it. The declaration is pure data with an inequality witness; no proof content beyond the field type.
Claim. A closed rational interval is a triple $(a,b,p)$ where $a,b\in\mathbb{Q}$ and $p$ is a proof that $a\le b$.
background
The module builds reals from nested rational intervals rather than Dedekind cuts or Cauchy sequences. The primitive object is a closed interval with rational endpoints; the inequality field records that the interval is nonempty in the order sense.
Width is the difference of endpoints, later bounded by $1/(n+1)$ at precision $n$. Subset and Overlap are the two geometric relations used to state nesting and consistency of successive approximations. Upstream order infrastructure (LogicNat and SignedOrbit non-strict orders) supplies the ambient $\le$ on rationals once they are constructed from the logic layer.
Local setting: Primitive Recognition Calculus, DeltaReal layer. The intended real is the unique point common to a nested, width-controlled family of these intervals.
proof idea
No proof body: this is a structure declaration. The only content is three fields (lower rational, upper rational, and the inequality $lo\le hi$). Downstream definitions pattern-match on those fields and discharge the inequality with linarith or le_refl when constructing new intervals.
why it matters
Every Delta-real protocol is a sequence of RatInterval values with nesting and width bounds. Addition, negation, and constant-rational embedding build new protocols by operating on these intervals endpointwise. Subset and Overlap are stated on this type and feed the nested-family axioms. Width and its nonnegativity lemma sit immediately above it.
In the Recognition stack this is foundation scaffolding, not a forcing-chain step (T0–T8). It supplies the concrete carrier so that later continuum and spacetime constructions can treat reals as certified nested rational intervals rather than an external axiom. Parent consumers include Protocol, add, neg, ofRat, Subset, Overlap, and width.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.