From the paper — Session Type State Spaces Form Lattices · ICE 2026
Theorem 15 · Reticulate Theorem
For every well-formed session type S over the six constructors, with single or mutual recursion, ℒ(S)/≡ is a bounded lattice.
Definition 6 · SCC quotient
The SCC quotient ℒ(S)/≡ identifies mutually reachable states, collapsing each recursion cycle to one class. It is ordered by [s₁] ≤ [s₂] iff s₂ ↠ s₁: a state is smaller when less of the protocol remains, so execution descends from q⊤ to q⊥.
Lemma 8 · End
ℒ(end)/≡ is a bounded lattice.
Proposition 18 · Duality isomorphism
For every well-formed session type S, there is a bounded-lattice isomorphism ℒ(S)/≡ ≅ ℒ(dual(S))/≡.