obsEq_symm
plain-language theorem explainer
Observational equality of Delta-real protocols is symmetric: if two nested rational-interval families overlap at every precision, the reverse pair does too. Anyone assembling the quotient display real line from protocols cites this. The proof is a short term that routes through the faithfulness lemma equating observational equality with equality of realized values, then uses symmetry of real equality.
Claim. Let $x$ and $y$ be Delta-real protocols (nested rational intervals with width at most $1/(n+1)$ at precision $n$). If $x$ and $y$ are observationally equal, meaning $(x.\\mathrm{approx}\, n)$ overlaps $(y.\\mathrm{approx}\, n)$ for every $n$, then $y$ and $x$ are observationally equal.
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, written as the protocol's value.
Observational equality says the approximating intervals of two protocols overlap at every precision. The upstream faithfulness theorem states that this relation is exactly equality of values: the protocol distinguishes two reals if and only if their values differ.
This module builds a constructive presentation of the reals from nested rational data, before quotienting by observational equality to obtain the display real line.
proof idea
One-line term proof. Apply the faithfulness equivalence in the forward direction to turn the hypothesis into equality of values $x.\mathrm{value}=y.\mathrm{value}$; take the symmetric equality on reals; then apply the equivalence in the reverse direction with arguments swapped to recover observational equality of $y$ with $x$. No separate interval-chasing is needed once faithfulness is available.
why it matters
This is the symmetry leg of the setoid on protocols. Downstream, observational equality is packaged as a Setoid whose relation is ObsEq and whose equivalence proof is the triple of reflexivity, this symmetry lemma, and transitivity; the quotient is the display real line.
In the Recognition foundation stack, Delta-reals supply the primitive real carrier before measurement protocols and cost calculus attach. Closing the setoid laws is a prerequisite for any later construction that treats observationally indistinguishable nested-interval families as the same real.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.