obsEq_trans
plain-language theorem explainer
Observational equality of Delta-real protocols is transitive: if x and y agree at every precision and y and z agree at every precision, then x and z agree. Anyone building the display real line as a quotient of protocols cites this. The proof is a short term reduction through the faithfulness lemma that observational equality is equality of values, then ordinary equality transitivity.
Claim. Let $x,y,z$ be Delta-real protocols (nested rational-interval families with width at most $1/(n+1)$ at precision $n$). If $x$ and $y$ are observationally equal (their intervals overlap at every precision) and $y$ and $z$ are observationally equal, then $x$ and $z$ are observationally equal.
background
A Protocol is a Delta-real: a nested family of rational intervals approx : ℕ → RatInterval with the nesting condition that each stage sits inside the previous one, and with width bound width(approx n) ≤ 1/(n+1). The intended quantity is the unique real common to all intervals, written value.
Observational equality ObsEq x y means that at every precision n the intervals x.approx n and y.approx n overlap. The central faithfulness theorem obsEq_iff_value states that this relation is exactly equality of values: ObsEq x y ↔ x.value = y.value. That is the bridge from a purely interval-overlap predicate to ordinary real equality.
This module builds the display real line by quotienting protocols by observational equality. Transitivity is one of the three Setoid axioms needed for that quotient.
proof idea
One-line term proof. Apply obsEq_iff_value in both directions: convert ObsEq x y and ObsEq y z into x.value = y.value and y.value = z.value, chain those equalities by Eq.trans to get x.value = z.value, then convert back to ObsEq x z via the reverse direction of obsEq_iff_value. No interval chasing is done here; all work is delegated to the faithfulness lemma.
why it matters
Feeds directly into obsSetoid, which packages observational equality as a Lean Setoid on Protocol with reflexivity, symmetry, and this transitivity proof. The doc-comment on that definition states the purpose: "The quotient is the display real line."
In the Primitive Recognition Calculus, Delta-reals are the constructive stand-in for continuum quantities before the continuum bridge and Hilbert display layers. Without a transitive observational equality, the quotient that identifies protocols with the same value cannot be formed, and the display real line does not exist as a type. This is pure foundation scaffolding for later continuum and gravity bridges, not a physics forcing step (T0–T8), but it is required infrastructure for any continuum-level statement built on protocols.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.