proj_injective_of_separating
plain-language theorem explainer
When an observable family separates points, the forced physical-quotient projection is injective, so the quotient is trivial and no gauge identification appears. Anyone citing the Phase 7 gauge-from-indistinguishability package or recognition-signature injectivity needs this lemma. The proof is a short application of the characterization that equal projections mean observational equivalence.
Claim. Let $F$ be a family of maps $X\to C$. If observational equivalence under $F$ implies equality of states (every $f\in F$ agrees on $x$ and $y$ forces $x=y$), then the canonical projection from $X$ onto the physical quotient by that equivalence is injective.
background
In the Primitive Recognition Calculus, physical states arise by quotienting the raw state space by observational indistinguishability. Two states $x,y$ are observationally equivalent under a family $F$ when every $f\in F$ returns the same value on them. The physical quotient is the setoid quotient by that relation, and the projection sends each state to its class.
The local setting is forced quotient selection: the quotient is not an extra structure imposed by hand. Upstream, the forced-iff theorem states that two states map to the same physical class if and only if no admissible observable separates them. That biconditional is the exact content of the indistinguishability collapse. The present result is the injectivity half when the family does separate.
proof idea
Assume the projections of $x$ and $y$ coincide. By the left-to-right direction of forced-iff, equal projections are equivalent to observational equivalence under $F$. The separating hypothesis then yields $x=y$. The proof is a two-line intro-and-exact: feed the projection equality into forced-iff, then apply separation.
why it matters
This is the "no gauge from a separating family" clause of the Phase 7 headline on gauge from indistinguishability. That parent packages three facts: the forced-iff characterization, descent of every admissible observable to the quotient, and this injectivity statement. Downstream, the recognition-signature gauge module specializes it to complete recognizer families ("the precise complete-recognizer-family condition"), and the quotient-examples module uses it to show that the full integer-valued observable family yields a trivial quotient on $\mathbb{Z}$.
In the Recognition foundation, gauge is not a native operation of distinction. It appears only when recognition acts fail to separate. This lemma pins the complementary case: separation forces the identity quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.