obs_equiv_trans
plain-language theorem explainer
Observational equivalence for a fixed subsystem is transitive: if three ledger configurations agree pairwise on the observer's indices, the outer pair also agrees there. Anyone treating partial views as an equivalence relation (measurement, outcome classes, Born-structure arguments) cites this. The proof is a one-line pointwise composition of real equality.
Claim. Fix $N$ and a subsystem partition $S$ of the $N$ ledger entries. For configurations $c_1,c_2,c_3$, if $c_1$ and $c_2$ agree on every observer-index entry of $S$, and $c_2$ and $c_3$ agree on those same entries, then $c_1$ and $c_3$ agree on every observer-index entry of $S$.
background
Module F-009 formalizes measurement in Recognition Science: observers are internal subsystems of the ledger, not external agents. A configuration is an $N$-tuple of positive real ratios (ledger entries). A subsystem $S$ splits indices into an observer block of size $K$ and its complement (the system).
Two configurations are observationally equivalent relative to $S$ when they agree on all observer-index entries. The observer literally cannot access the complementary entries, so those states are indistinguishable from inside $S$. That relation is the structural source of apparent randomness: many full states share one partial view.
Together with the sibling reflexivity and symmetry facts, transitivity makes observational equivalence a genuine equivalence relation on configurations, so outcome classes and "same view, different full state" arguments are well-typed.
proof idea
Term-mode, one line. Observational equivalence is the pointwise proposition that entries match on every $i$ in the observer index set. Given $h_{12}$ and $h_{23}$, at each such $i$ one has $c_1.entries, i = c_2.entries, i$ and $c_2.entries, i = c_3.entries, i$. Real equality is transitive, so $c_1.entries, i = c_3.entries, i$. No dynamics, cost, or variational lemmas are used.
why it matters
This closes the equivalence-relation package for partial observer views in the measurement mechanism. Without transitivity, one cannot safely quotient configurations by "what the observer sees," nor chain indistinguishability through intermediate states when arguing that a measurement event correlates observer and system while leaving many full states compatible with one outcome.
The module's program is to replace the slogan "quantum randomness is projection through finite resolution" with a ledger mechanism: the full deterministic state fixes the outcome; the observer's partial view does not. Transitivity is bookkeeping infrastructure for that story (outcome spaces, same-state-same-outcome, Born-structure via $J$-cost weighting). No downstream theorems currently depend on it in the graph, but the sibling cluster (measurement events, outcome determination, apparent randomness) is the intended consumer. It does not itself invoke T5–T8 or the RCL; it sits under the foundation layer that makes those later claims observer-relative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.