ObsEq
plain-language theorem explainer
Observational equality of two Delta-real protocols means their rational approximating intervals overlap at every finite precision. Anyone building the display real line or proving faithfulness of the protocol presentation cites this relation. The body is a one-line definition: universal quantification of interval overlap over all n.
Claim. Two Delta-real protocols $x$ and $y$ are observationally equal when, for every natural number $n$, the rational intervals $x_n$ and $y_n$ overlap: neither lies strictly to the left of the other ($x_n^{\mathrm{lo}} \le y_n^{\mathrm{hi}}$ and $y_n^{\mathrm{lo}} \le x_n^{\mathrm{hi}}$).
background
A Delta-real protocol is a nested family of rational intervals whose width at precision $n$ is at most $1/(n+1)$. The intended quantity is the unique real common to every interval in the family. Nesting forces later intervals inside earlier ones; the width bound forces the intersection to a singleton.
Two rational intervals overlap when neither lies strictly to one side of the other: the lower endpoint of each is at most the upper endpoint of the other. Observational equality lifts that relation to protocols by requiring overlap at every precision level.
The local setting is the constructive presentation of reals inside Primitive Recognition Calculus: reals appear as refinement protocols rather than as completed Dedekind or Cauchy objects. Evaluation maps (value) later extract the classical real from a protocol.
proof idea
Pure definition: expand to $\forall n,\ (x.\mathrm{approx}, n).\mathrm{Overlap}\ (y.\mathrm{approx}, n)$. No lemmas, no tactics. Overlap itself is the two-sided endpoint comparison $I.lo \le J.hi \land J.lo \le I.hi$.
why it matters
This is the raw equivalence relation on protocols. Downstream, obsEq_iff_value proves it coincides with equality of classical values: the protocol distinguishes two reals exactly when their values differ (the central faithfulness statement). Reflexivity, symmetry, and transitivity are then immediate corollaries, and obsSetoid packages them so the quotient is the display real line.
The Phase 1 headline display_real_forgetful lists observational equality matching value equality as one of its four clauses, alongside surjectivity of value, rational embedding, and native ring operations. In the Recognition stack this keeps continuum structure from being smuggled in: only what protocols can observe counts as equal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.