obsEq_iff_value
plain-language theorem explainer
Observational equality of two Delta-real protocols is equivalent to equality of their classical real values. Anyone reconstructing ℝ from nested rational intervals cites this as faithfulness of the presentation: protocols distinguish reals exactly when values differ. The forward direction squeezes the absolute difference by twice the width bound at every precision and applies a vanishing lemma; the converse uses that each value sits in every approximating interval.
Claim. Let $x$ and $y$ be Delta-real protocols (nested families of rational intervals with width at most $1/(n+1)$ at stage $n$). Their approximating intervals overlap at every precision if and only if the unique real values they determine coincide.
background
A Protocol (Delta-real) is a nested family of rational intervals whose width at precision $n$ is bounded by $1/(n+1)$. The intended quantity is the unique real common to all intervals, recovered as the protocol's value. Observational equality asserts that the intervals of two protocols overlap at every $n$: each lower endpoint is at most the other's upper endpoint.
The module develops a constructive presentation of the reals so that classical $\mathbb{R}$ appears as the forgetful display of the Delta-real line. Upstream facts used here place each value inside every approximating interval and control the real diameter of those intervals by the rational width bound.
proof idea
Bidirectional constructor. Forward: from overlap at every $n$, combine membership of each value in its $n$-th interval with the two width bounds to obtain $|x.\mathrm{value}-y.\mathrm{value}|\le 2/(n+1)$ for all $n$. Specialize the index to $2n+1$ so the right-hand side becomes $1/(n+1)$, then apply the vanishing lemma that a nonnegative real bounded by every $1/(n+1)$ is zero; absolute-value zero yields equality.
Converse: if the values agree, membership of the common value in both intervals plus the endpoint comparisons give the two overlap inequalities after casting rationals to reals; ordinary real transitivity of $\le$ chains them.
why it matters
This is the faithfulness clause of the Phase 1 headline: classical $\mathbb{R}$ is the forgetful value of a Delta-real protocol, and observational equality of protocols is exactly equality of value. Downstream it yields that observational equality is an equivalence relation by transporting reflexivity, symmetry, and transitivity along value equality; that the rational embedding is faithful; and that value is surjective onto $\mathbb{R}$. The quotient by observational equality is the display real line. In the Recognition foundation stack this anchors the passage from primitive recognition calculus to ordinary analysis without collapsing distinct reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.