Subset
plain-language theorem explainer
Defines closed-interval containment for rational intervals: I is a subset of J when J's lower bound is at most I's and I's upper bound is at most J's. Anyone working with nested rational approximations or protocol intervals in the primitive recognition calculus cites this. The body is a one-line propositional definition, not a proved theorem.
Claim. For closed rational intervals $I=[I_\mathrm{lo},I_\mathrm{hi}]$ and $J=[J_\mathrm{lo},J_\mathrm{hi}]$, write $I \subseteq J$ when $J_\mathrm{lo} \le I_\mathrm{lo}$ and $I_\mathrm{hi} \le J_\mathrm{hi}$.
background
The ambient structure is a closed rational interval: a pair of rationals lo, hi with lo ≤ hi. These intervals are the discrete carriers for nested rational approximations in the primitive recognition calculus (DeltaReal), before endpoints are cast to reals.
Containment is the standard order-theoretic nesting of closed intervals on ℚ. It is the relation one needs before talking about refining protocols, monotone lower endpoints, or anti-monotone upper endpoints. Sibling notions in the same module include width, overlap, and the protocol that packages a sequence of such intervals.
proof idea
Pure definitional abbreviation: the proposition is the conjunction of the two endpoint inequalities. No lemmas, tactics, or proof terms beyond the Prop itself.
why it matters
Interval nesting is the basic geometric relation for rational approximation schemes used later when endpoints are promoted to reals (lo/hi as ℝ). In the Recognition foundation stack this sits under primitive recognition calculus: nested intervals encode successive refinements of a real by rationals. No downstream theorems currently depend on this name in the graph, so it is local scaffolding for overlap, protocol monotonicity, and width arguments rather than a forcing-chain landmark (T5–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.