PhaseState
plain-language theorem explainer
Toy carrier type for phase states in the quotient-selection examples: integers standing in for discrete phase labels. Cited by the empty-observable collapse theorem and the module headline that packages three quotient regimes. The declaration is a one-line type synonym with no proof content.
Claim. Write $\mathrm{PhaseState}$ for the integers $\mathbb{Z}$, used as a discrete toy space of phase labels in the physical-quotient examples.
background
The module develops worked examples of the physical (observable) quotient from QuotientSelection: states are identified precisely when every admitted observable agrees on them. Phase is the natural first toy carrier, because the eight-tick foundation already treats phase as a discrete cyclic label (the eight values $k\pi/4$ for $k=0,\ldots,7$).
Here the carrier is stripped to bare integers so that the quotient machinery can be exercised without Clifford or DFT structure. Upstream, EightTick.phase supplies the geometric phases; OrbitEuclidean.quotient is the object-level division used elsewhere in the primitive calculus. Neither is needed for the type itself; they only set the surrounding vocabulary of phase and quotient.
proof idea
Definitional abbreviation: PhaseState is definitionally equal to $\mathbb{Z}$. No tactics, no lemmas.
why it matters
Supplies the state type for empty_observable_phase_quotient, which proves that with the empty observable family every pair of phase states is identified by proj. That fact is the first conjunct of quotient_examples_headline: phase with no readable observable collapses, a separating gauge family has trivial quotient, and projective-state display is the quotient theorem specialized to projective observables.
In the broader Recognition chain this is scaffolding for the eight-tick octave (T7) and the Clifford/Bott reading of period 8, not a claim about physical phase itself. It lets the quotient selection story be stated before the full phase geometry is wired in.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.