obsEquiv_trans
plain-language theorem explainer
Observational equivalence under a family of maps is transitive: if every observable agrees on x and y and on y and z, it agrees on x and z. Anyone assembling the physical quotient of states by indistinguishability cites this. The proof is a one-line term chaining equality of values pointwise on each observable.
Claim. Let $F$ be a family of maps $X\to C$. If $x,y,z\in X$ satisfy $f(x)=f(y)$ for every $f\in F$ and $f(y)=f(z)$ for every $f\in F$, then $f(x)=f(z)$ for every $f\in F$.
background
In the quotient-selection layer of the primitive recognition calculus, two states are observationally equivalent under a family $F\subseteq(X\to C)$ when every map in $F$ returns the same value on them. Formally, $\mathrm{ObsEquiv}(F,x,y)$ means $\forall f\in F,, f(x)=f(y)$.
This is the relation one wants to quotient by: states that no allowed observable can separate should be identified. Reflexivity and symmetry are immediate from equality; transitivity is the remaining Setoid axiom.
The local setting is pure relational bookkeeping on an abstract state space $X$ with codomain $C$. No continuum, gravity, or anchor-policy structure is used here; those appear only as incidental name collisions in the dependency graph.
proof idea
Term-mode proof. Fix $f\in F$. The first hypothesis gives $f(x)=f(y)$; the second gives $f(y)=f(z)$. Apply Eq.trans to those two equalities to obtain $f(x)=f(z)$. Abstract over $f$ and the membership proof to discharge the universal quantifier in the definition of observational equivalence.
why it matters
This lemma is the third leg of the equivalence-relation package. Downstream, obsSetoid installs observational equivalence as a Setoid on $X$ via iseqv := ⟨refl, symm, trans⟩, and that Setoid defines the physically forced quotient: the state space modulo indistinguishability.
In Recognition Science terms, the quotient is how gauge and unobservable degrees of freedom are removed before continuum or ledger structure is imposed. Without transitivity the Setoid instance fails and the projection to physical states is not well-defined. The sibling results on descent of observables and injectivity under separating families sit on top of this Setoid.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.