ObservationallyEquivalent
plain-language theorem explainer
Two N-entry ledger configurations are observationally equivalent relative to a subsystem observer when they agree on every observer-index entry. Anyone formalizing measurement, partial views, or epistemic randomness in RS cites this relation. It is a one-line pointwise equality on the observer Finset, not a derived theorem.
Claim. Fix $N\in\mathbb{N}$ and a subsystem partition $S$ of the $N$ ledger indices (observer block of size $K$ with $0<K<N$). Configurations $c_1,c_2$ (maps $\mathrm{Fin}\,N\to\mathbb{R}_{>0}$) are observationally equivalent for $S$ when $c_1(i)=c_2(i)$ for every index $i$ in the observer index set of $S$.
background
Module F-009 (Measurement Mechanism) explains how a fully deterministic ledger trajectory can look random to an internal observer. The key move is to treat the observer as a proper subsystem of the $N$-entry configuration, not as an external agent.
A Configuration N is an $N$-tuple of positive real ratios (ledger entries). A Subsystem N partitions $\mathrm{Fin},N$ into observer indices of cardinality $K$ ($0<K<N$) and complementary system indices. The observer's partial view is exactly the restriction of the configuration to those observer indices; the complementary entries are structurally inaccessible.
Observational equivalence packages that inaccessibility: two full states that agree on the observer block are indistinguishable to $S$, even if they differ on the system block. The module stresses this is not a Bell-style local hidden-variable story; the full state carries nonlocal correlations from the variational update.
proof idea
Pure definition: the proposition is the universal quantification that $c_1$ and $c_2$ agree on every index in $S$'s observer Finset. No lemmas, tactics, or algebraic reduction. Downstream reflexivity, symmetry, and transitivity proofs are immediate from equality of reals on that Finset.
why it matters
This relation is the primitive for the measurement-layer story in F-009. It feeds the equivalence-relation lemmas (refl/symm/trans), partial_view_underdetermines_outcome (observationally equivalent states can still be distinct full configurations), subsystem_cannot_know_whole, and the headline theorem deterministic_but_unpredictable: outcomes are unique functions of the full state yet not fixed by the observer's partial view.
It is also cited by measurement_mechanism_certificate and by MeasurementLayer_Forced in the unified forcing chain, locking the epistemic-randomness mechanism into the T0–T8 stack. Without a crisp observational equivalence, the gap between Determinism's lossy project and a concrete internal-observer mechanism would remain informal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.