Overlap
plain-language theorem explainer
Closed rational intervals overlap when each lower endpoint sits at or below the other's upper endpoint. The predicate is the elementary geometric relation used to define observational equality of delta-real protocols: two protocols agree if their approximating intervals overlap at every precision. Downstream it also appears in generation-mixing amplitudes. The body is a two-conjunct inequality on the rational endpoints; no proof work.
Claim. For closed rational intervals $I=[I_\mathrm{lo},I_\mathrm{hi}]$ and $J=[J_\mathrm{lo},J_\mathrm{hi}]$, the intervals overlap when $I_\mathrm{lo}\le J_\mathrm{hi}$ and $J_\mathrm{lo}\le I_\mathrm{hi}$ (equivalently, neither interval lies strictly to one side of the other).
background
In the Primitive Recognition Calculus, continuum quantities are not introduced as classical reals. They are carried by refinement protocols: nested families of closed rational intervals whose widths shrink like $1/(n+1)$ at precision $n$. The intended real is the unique point common to all intervals of the family.
A RatInterval is a closed interval with rational endpoints $lo\le hi$. Its rational width is $hi-lo$. Overlap is the standard closed-interval intersection test on those endpoints: the two intervals share at least one rational (hence real) point precisely when each lower bound does not exceed the other's upper bound.
The local module builds delta-reals from these intervals and then lifts endpoint maps to $\mathbb{R}$. Overlap is the combinatorial relation that later becomes observational equality of two protocols.
proof idea
Pure definition: the proposition is the conjunction $I.lo\le J.hi\land J.lo\le I.hi$ on the rational endpoint fields of two RatInterval values. No lemmas, tactics, or rewriting are involved.
why it matters
Observational equality of two delta-real protocols is defined as overlap of their approximating intervals at every precision $n$. Faithfulness of the protocol representation (two protocols are observationally equal iff they name the same real) therefore rests on this predicate.
Outside the foundation layer, the same geometric language appears in the three-generation sector: CKM matrix elements are described as encoding how generations talk via overlap of 8-tick phases, tying the interval predicate to the T7 eight-tick octave of the forcing chain. The definition is scaffolding-free infrastructure rather than a forcing-chain step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.