obsEquiv_symm
plain-language theorem explainer
Observational equivalence is symmetric: if every observable in a family F agrees on states x and y, then it agrees on y and x. Anyone assembling the setoid of states modulo indistinguishability cites this. The proof is a one-line term that applies equality symmetry pointwise on F.
Claim. Let $F$ be a set of maps $X\to C$. If $x,y\in X$ satisfy $f(x)=f(y)$ for every $f\in F$, then $f(y)=f(x)$ for every $f\in F$.
background
In the Primitive Recognition Calculus quotient-selection layer, physical states are identified when no available measurement can tell them apart. The relation ObsEquiv formalizes that: for a family $F$ of observables $X\to C$, two states $x,y$ are observationally equivalent when $\forall f\in F,, f(x)=f(y)$.
To pass to the quotient of states modulo indistinguishability one needs a Setoid, hence reflexivity, symmetry, and transitivity of that relation. This declaration is the symmetry leg. The ambient module packages those three legs into obsSetoid and then forms the physically forced quotient.
(The name collisions with unrelated helper functions called $F$ in gravity and anchor-policy modules are irrelevant here; the parameter is simply the observable family.)
proof idea
Term-mode proof. Unfolding observational equivalence, the hypothesis is a pointwise equality $f,x=f,y$ for each $f\in F$. The term fun f hf => (h f hf).symm reindexes that family and applies Eq.symm on each equality, yielding $f,y=f,x$. No auxiliary lemmas are required.
why it matters
This is one of the three equivalence-relation axioms fed directly into obsSetoid, whose doc-comment states it packages observational equivalence as a Setoid and introduces the physically forced quotient (state space modulo indistinguishability). Downstream constructions (PhysicalQuotient, projection, descent of observables, gauge-from-indistinguishability) all sit on that setoid. In Recognition Science terms it is pure foundation: the quotient that collapses gauge-redundant microstates before any forcing-chain or mass-ladder work begins.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.