proj
plain-language theorem explainer
Canonical projection from bare states to physical (gauge) classes: each state is sent to its class under observational indistinguishability for a fixed family of admissible observables. Anyone working with forced quotients, gauge collapse, or descent of observables cites this map. It is the standard setoid quotient constructor applied to the observational equivalence relation.
Claim. For a state space $X$, a codomain $C$, and a family $F$ of admissible observables $X\to C$, the projection $\pi_F:X\to X/{\sim_F}$ sends each state $x$ to its class in the physical quotient, where $x\sim_F y$ means no observable in $F$ separates $x$ from $y$.
background
In the primitive recognition calculus, two states are observationally equivalent when every admissible observable returns the same value on both. That relation is packaged as the setoid obsSetoid F on the bare carrier $X$. The physical quotient is then the ordinary setoid quotient: states modulo indistinguishability under $F$.
The local module builds the forced gauge collapse: the quotient adds no identifications beyond indistinguishability and omits none. The projection is the structure map of that quotient. Upstream, the same pattern appears for observational equality on protocols (display reals) and for coarser connectivity quotients in interface-component bounds; here the relation is generated by a set of real- or $C$-valued observables rather than by edges or protocol steps.
Notation: $F\subseteq(X\to C)$ is the admissible family; the physical quotient is written $X/{\sim_F}$. Gauge class means equivalence class under $\sim_F$.
proof idea
One-line definition: apply the library quotient constructor Quotient.mk to the observational setoid of $F$. No extra lemmas; the map is definitionally the class map of that setoid.
why it matters
This is the structure map of the forced physical quotient in Recognition Science: bare microstates are collapsed exactly by what no admissible observable can tell apart. Downstream, objecthood classification uses it to state that every $f\in F$ descends, i.e. there exists $g$ on the quotient with $g(\pi_F(x))=f(x)$ (no observable information is lost). Quotient examples and injectivity-under-separating-families lemmas are stated in terms of this projection.
In the broader foundation stack it is the gauge-class map that later interfaces with Clifford/Bott structure (eight-tick grading) and with component-count bounds on coarser quotients. It does not itself force $J$, $\varphi$, or $D=3$; it supplies the state-space quotient those layers act on once observables are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.