PhysicalQuotient
plain-language theorem explainer
The physical state space is the ordinary set-theoretic quotient of raw configurations by observational equivalence under a fixed family of admissible observables. Anyone working on gauge-from-indistinguishability or descent of observables cites this type. It is a one-line abbreviation of Lean’s Quotient applied to the observational setoid.
Claim. For a state space $X$, a codomain $C$, and a family $F$ of maps $X\to C$, write $\mathrm{PhysicalQuotient}(F)$ for the quotient type $X/\sim_F$, where $x\sim_F y$ means every $f\in F$ satisfies $f(x)=f(y)$.
background
In the Primitive Recognition Calculus, two states are observationally equivalent relative to a family $F\subseteq{X\to C}$ when no admissible observable separates them. That relation is packaged as the setoid obsSetoid F (reflexive, symmetric, transitive observational equivalence).
The module’s job is quotient selection: form the coarsest identification forced by the absence of distinguishing recognition acts, without adding extra collapses. Upstream, the same pattern appears for display reals (observational equality as a setoid whose quotient is the display line). Here the carrier is an arbitrary state space $X$ and the relation is induced by a chosen observable family $F$.
Notation: $C$ is the value type of observables; $F$ is the admitted family. The quotient is the candidate physical (gauge) configuration space on which every $f\in F$ should still be well-defined.
proof idea
Definitional abbreviation only: expand to Lean’s Quotient applied to the observational setoid of $F$. No tactics, no lemmas. The setoid itself is assembled from the three observational-equivalence proofs (refl, symm, trans) already established for ObsEquiv F.
why it matters
This type is the carrier for the Phase 7 headline that gauge is forced by indistinguishability. Downstream, the projection into the quotient, the universal property that every admissible observable descends, injectivity when the family separates, and the bundled theorem gauge_from_indistinguishability all live on this quotient. Objecthood classification reuses the descent fact: every admissible observable factors through the physical classes, so the quotient loses no observable information. The recognition-signature gauge certificate likewise states exactness and descent over this same type. In RS terms it is the formal home of “identifications only where no recognition act distinguishes,” not a free gauge choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.