gauge_from_indistinguishability
plain-language theorem explainer
Packages the three structural facts that make the physical quotient a gauge: projection identifies states exactly when no admitted observable separates them; every observable descends to the quotient; and a separating family forces the projection to be injective. Cited by the RecognitionCore re-export and the Delta-native strong-closure certificate. Proof is a three-component term assembling the three prior lemmas.
Claim. For any family $F$ of maps $X\to C$, the projection to the physical quotient satisfies: (i) $\mathrm{proj}_F(x)=\mathrm{proj}_F(y)$ if and only if every $f\in F$ has $f(x)=f(y)$; (ii) every $f\in F$ factors through the quotient as some $g$ on physical classes with $g(\mathrm{proj}_F(x))=f(x)$; (iii) if observational equivalence implies $x=y$, then $\mathrm{proj}_F$ is injective.
background
In the Primitive Recognition Calculus, an admissible observable family $F\subseteq(X\to C)$ defines observational equivalence: $x\sim_F y$ when every $f\in F$ returns the same value on $x$ and $y$. The physical quotient is the setoid quotient of $X$ by that relation; its projection sends each state to its gauge class.
The module's Phase 7 claim is that this quotient is forced by indistinguishability alone, not imposed as a native distinction operation. Upstream, forced_iff states that two states land in the same class exactly when they are observationally equivalent ("adds no identifications beyond indistinguishability and omits none"). The universal property observable_descends guarantees every admitted observable factors through the quotient. Separating families collapse the quotient via injectivity of the projection.
proof idea
One-line term proof that packages three already-proved components as a conjunction: forced_iff F supplies the biconditional between equal projected classes and observational equivalence; the middle conjunct is the lambda that applies observable_descends F f hf for each $f\in F$; the third conjunct is proj_injective_of_separating F. No new reasoning is introduced beyond assembling those three lemmas.
why it matters
Phase 7 headline of QuotientSelection: gauge structure is derived from the absence of a distinguishing recognition act, not postulated. Downstream, RecognitionCore re-exports the statement as the public interface ("the physically forced quotient is exactly indistinguishability under the admitted observable family; observables descend; a separating family collapses the quotient to the identity"). It also feeds the Delta-native strong-closure certificate that assembles the closed theorem surface for the foundation layer.
In the broader Recognition Science forcing chain this is the structural justification for treating gauge as forced identification under observational equivalence, prior to the J-cost uniqueness (T5), the golden-ratio fixed point (T6), and the eight-tick / $D=3$ steps (T7–T8). It closes the quotient-selection phase rather than leaving a scaffolding hole.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.