separating_gauge_family_injective
plain-language theorem explainer
When every integer-valued map is admitted as an observable, integer states are fully separated, so the physical (gauge) quotient of the integers is trivial: the projection is injective. Anyone citing the forced-quotient construction in Recognition calculus uses this as the canonical separating-family example. The proof is a short application of the general separating-family injectivity lemma, witnessed by the identity observable.
Claim. The projection from integer states to the physical quotient induced by the family of all maps $\mathbb{Z}\to\mathbb{Z}$ is injective. Equivalently, if every integer-valued observable is admitted, then two integers lie in the same gauge class if and only if they are equal, so the forced quotient is trivial.
background
In the Primitive Recognition Calculus, physical states arise by quotienting a raw state space $X$ by indistinguishability under an admitted family $F$ of observables $X\to C$. The projection sends each state to its physical (gauge) class. Two states map to the same class exactly when no admissible observable separates them; the forced quotient adds no identifications beyond that indistinguishability and omits none.
The upstream lemma records the dual fact: if $F$ separates points (indistinguishability implies equality), the projection is injective and the quotient is trivial. Gauge identification appears precisely when the observables fail to separate. The present result specializes that principle to $X=C=\mathbb{Z}$ with $F$ the universal set of all integer-valued maps.
This module collects concrete quotient examples: empty observable families collapse everything; separating families give trivial quotients; projective observables recover the standard projective-state display.
proof idea
Short term-mode proof: apply the general separating-family injectivity lemma, then check that the universal family of all maps $\mathbb{Z}\to\mathbb{Z}$ separates points. If every such map agrees on $x$ and $y$, the identity map in particular agrees, so $x=y$. Membership of the identity in the universal set and the agreement hypothesis are discharged by simplification.
why it matters
One of three legs of the quotient-examples headline, which packages empty-family collapse, separating-family triviality, and projective-state display as the canonical illustrations of forced gauge identification. Downstream it is assembled into the strong-closure certificate for the Delta-native theorem surface.
In the foundation layer it makes precise the slogan that gauge appears exactly when observables fail to separate: admitting all integer observables leaves no residual gauge on $\mathbb{Z}$. It is an example, not a forcing-chain step (T0–T8), but it anchors the quotient-selection layer that the primitive recognition calculus uses before cost and ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.