empty_observable_phase_quotient
plain-language theorem explainer
With no admitted observables, every pair of integer phase states collapses to one physical class. Anyone citing the forced gauge quotient or the quotient-examples headline needs this boundary case. The proof is a short tactic: indistinguishability is vacuous on the empty family, so the identification lemma applies directly.
Claim. Let phase states be integers. For the empty family $F=\emptyset$ of integer-valued observables on phase states, the physical projection identifies every pair: $\mathrm{proj}_{F}(x)=\mathrm{proj}_{F}(y)$ for all phase states $x,y$.
background
In the primitive recognition calculus, physical states are not bare configurations. They are classes under the forced gauge quotient: two states are identified exactly when no admitted observable separates them. The projection $\mathrm{proj}_{F}$ sends a state to its class in that quotient (the setoid of observational equivalence for family $F$).
Here the carrier is a toy phase line, $\mathrm{PhaseState}:=\mathbb{Z}$. Observables are maps $\mathrm{PhaseState}\to\mathbb{Z}$. The empty family admits nothing readable, so observational equivalence is total.
Upstream, identified_of_obsEquiv states that indistinguishability implies equality of projections: "Indistinguishable states are identified in the quotient." The companion characterization says the quotient adds no identifications beyond indistinguishability and omits none.
proof idea
One short tactic proof. Apply the upstream lemma that observational equivalence forces equal projections. It remains only to show that every $f$ in the empty family agrees on $x$ and $y$. Introduce such an $f$ with membership hypothesis; that hypothesis is impossible, so cases finishes. No computation on integers is needed: emptiness alone makes every pair observationally equivalent.
why it matters
This is the collapse boundary of the gauge-from-indistinguishability story (Phase 7 in the quotient-selection layer). It feeds quotient_examples_headline, which packages three facts: empty observables collapse phase, a fully separating integer family has trivial quotient, and projective display is the same theorem specialized to projective observables.
It also appears in the Delta-native strong-closure certificate surface, as a concrete example that the forced quotient behaves correctly at the extreme of zero readout. In Recognition terms it is the null case of the same mechanism that later forces nontrivial gauge structure once a separating family is admitted: without observables there is no physical distinction, only one class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.