obsSetoid
plain-language theorem explainer
Observational equality of Delta-real protocols is packaged as a setoid. Anyone building the display real line as a quotient of nested rational-interval protocols cites this. The body is a one-line assembly of the already-proved reflexivity, symmetry, and transitivity lemmas for interval-overlap equality.
Claim. Observational equality of protocols (nested rational-interval approximations with width bound $1/(n+1)$ at precision $n$) is an equivalence relation on the type of protocols, and is therefore a setoid. The intended quotient is the display real line.
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 value is the unique real common to every interval in the family.
Observational equality says that two protocols have overlapping intervals at every precision. Upstream lemmas already show this relation is reflexive, symmetric, and transitive, via the faithfulness fact that observational equality coincides with equality of the underlying real values.
This module sits in the primitive recognition calculus: reals are recovered from finite-precision rational data rather than postulated as a completed continuum. Packaging the relation as a setoid is the standard Lean step before forming the quotient type.
proof idea
One-line setoid constructor. The relation field is observational equality. The equivalence proof is the triple of upstream theorems: reflexivity of observational equality, symmetry, and transitivity. No new arithmetic is done here.
why it matters
This setoid is the concrete carrier for the display real line in the Delta-real development. Downstream, the quotient-selection layer reuses the same packaging pattern for observational equivalence of states, defines the physically forced quotient as the quotient by that setoid, and projects states to gauge classes. The parent docs stress that the forced quotient adds no identifications beyond indistinguishability and omits none. In the Recognition framework this is foundation infrastructure: measurement and display quantities live on the quotient of protocols, not on raw nested-interval data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.