Foundation Primitive Recognition Calculus Quotient Selection Obs Equiv Symm

Symmetry of indistinguishability

In the Recognition Science framework, a state space is a collection of possible configurations, and an observable is a measurement that assigns a value to each configuration. Two states are observationally equivalent when every observable in the family returns the same value on both of them. The declaration obsEquiv_symm proves that this relation is symmetric: if state x is observationally equivalent to state y, then state y is observationally equivalent to state x. This is not an assumption or a definitional choice; it is a theorem proved in the framework's machine-checked library of formal theorems.

The proof is immediate from the definition. Observational equivalence says that for every observable f in the family F, f x = f y. Equality in the underlying value type is itself symmetric, so from f x = f y we get f y = f x, which is exactly the statement that y is observationally equivalent to x. The framework's library also proves reflexivity (every state is equivalent to itself) and transitivity (if x is equivalent to y and y to z, then x is equivalent to z). Together, these three properties make observational equivalence an equivalence relation, which the library packages as a setoid, a structure that supports quotienting the state space.

The symmetry theorem matters because it is one of the three pillars that justify the framework's physically forced quotient. The quotient construction identifies states that no observable can distinguish, collapsing the raw state space into physical classes. Symmetry guarantees that this collapse is well-behaved: the identification does not depend on which state you start from. Without symmetry, the notion of "indistinguishable from" would be one-directional and could not support a coherent notion of physical equivalence classes.

What obsEquiv_symm does not claim is equally important. It does not assert that any particular pair of states is equivalent; it only says that if they are equivalent in one direction, they are equivalent in the other. It does not say that the observable family F is separating, meaning that distinct states can always be distinguished; that is a separate condition. And it does not by itself establish that the quotient is physically meaningful, only that the underlying equivalence relation has the symmetry property needed for the quotient construction to proceed.

theorem obsEquiv_symm (F : Set (X → C)) {x y : X} (h : ObsEquiv F x y) : ObsEquiv F y x :=
  fun f hf => (h f hf).symm

/-- Observational equivalence packaged as a `Setoid`. -/
def obsSetoid (F : Set (X → C)) : Setoid X where
  r := ObsEquiv F
  iseqv := ⟨obsEquiv_refl F, obsEquiv_symm F, obsEquiv_trans F⟩

What this page does not claim

The theorem does not assert that any particular pair of states is observationally equivalent. The theorem does not claim the observable family separates all distinct states. The theorem alone does not establish the physical interpretation of the quotient.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/QuotientSelection.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: