obs_equiv_symm
plain-language theorem explainer
Observational equivalence of ledger configurations is symmetric: if two N-entry states agree on every observer-index entry of a subsystem partition S, they agree with the order reversed. Anyone building the measurement-mechanism equivalence relation (or quotienting by partial views) cites this. The proof is a one-line term that applies equality symmetry pointwise on the observer indices.
Claim. Let $S$ be a subsystem partition of an $N$-entry ledger and let $c_1,c_2$ be configurations (maps $\mathrm{Fin}\,N\to\mathbb{R}_{>0}$). If $c_1$ and $c_2$ agree on every index in the observer set of $S$, then $c_2$ and $c_1$ agree on those same indices.
background
Module F-009 (Measurement Mechanism) treats observers as internal ledger subsystems, not external agents. A Subsystem of an $N$-entry ledger is a partition: observer indices form a finset of cardinality $K$ with $0<K<N$, and the system occupies the complement. A Configuration is an $N$-tuple of positive real ratios (ledger entries).
Two configurations are observationally equivalent relative to $S$ when they agree on every observer-index entry. The observer literally cannot access the complementary system entries, so this is a structural indistinguishability, not an approximation. The module's key claim is that apparent randomness is ignorance of those complementary entries under a fully deterministic global trajectory.
This lemma is the symmetry half of that relation; siblings supply reflexivity and transitivity.
proof idea
One-line term proof. Unfold observational equivalence to a pointwise equality on $S$'s observer indices, then apply Eq.symm at each index: given $h : \forall i\in S.\mathrm{obs},, c_1(i)=c_2(i)$, the reverse is $\mathrm{fun}, i, hi \mapsto (h, i, hi).\mathrm{symm}$. No auxiliary lemmas are required beyond equality symmetry.
why it matters
Establishes symmetry of observational equivalence, a prerequisite for treating partial views as a genuine equivalence relation on configuration space (with obs_equiv_refl and obs_equiv_trans). That relation is the formal backbone of F-009's answer to how determinism yields apparent randomness: many full states share one observer view, so the outcome fixed by the full state looks undetermined from inside $S$.
Downstream usage is not yet wired in this graph (used_by is empty), but the sibling cluster (MeasurementEvent, outcome_is_determined, same_state_same_outcome) is the intended consumer. In the broader RS chain this sits under the measurement story that complements Determinism and VariationalDynamics (global, non-local updates), not under T5–T8 forcing of $J$, $\varphi$, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.