obsEq_refl
plain-language theorem explainer
Observational equality of Delta-reals is reflexive: every protocol is observationally equal to itself. Anyone building the quotient display real line via the observational setoid needs this as the first equivalence-law. The proof is a one-line reduction through the faithfulness equivalence to value equality, then reflexivity of real equality.
Claim. For every Delta-real protocol $x$, the intervals of $x$ overlap those of $x$ at every precision: $\mathrm{ObsEq}(x,x)$ holds.
background
A Protocol (Delta-real) 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 all intervals, written $x.\mathrm{value}$.
Observational equality $\mathrm{ObsEq}(x,y)$ means that at every precision $n$ the approximating intervals of $x$ and $y$ overlap. The upstream faithfulness theorem states that this relation is exactly equality of values: $\mathrm{ObsEq}(x,y)\leftrightarrow x.\mathrm{value}=y.\mathrm{value}$. That equivalence is the only nontrivial input here.
The local module develops these constructive reals as the primitive recognition calculus substrate before quotienting to a display real line.
proof idea
One-line wrapper. Apply the reverse direction of the faithfulness equivalence $\mathrm{ObsEq}\leftrightarrow$ value equality at the pair $(x,x)$, then discharge the goal $x.\mathrm{value}=x.\mathrm{value}$ by reflexivity of equality on $\mathbb{R}$. No interval arithmetic is unfolded.
why it matters
This is the reflexivity leg of the observational setoid. Downstream, obsSetoid packages $\mathrm{ObsEq}$ as a Setoid on Protocol with iseqv := ⟨obsEq_refl, obsEq_symm, obsEq_trans⟩; the quotient is the display real line used by the primitive recognition calculus.
In the Recognition Science foundation layer this supplies the first equivalence law so that measurement protocols can be identified exactly when they name the same real, matching the faithfulness claim that the protocol distinguishes two reals iff their values differ. It is pure setoid scaffolding rather than a forcing-chain (T0–T8) step, but without it the quotient real line does not form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.