A Classifying Topos for the Spectrum of Equivalences

What makes two computational systems equivalent? Topos theory answers with classifying toposes: a system’s semantic content is encoded in the geometric theory it classifies, and two presentations are equivalent when their classifying toposes coincide. Process algebra answers with the linear time-branching time spectrum of van Glabbeek: a hierarchy of behavioral equivalences from trace equivalence to bisimilarity, each determined by which observations can distinguish processes. We show these are aspects of a single structure in which behavioral abstraction is localization. Each labeled transition system receives a geometric theory ${\mathbb{T}}_M$ whose classifying topos $\mathcal{E}[{\mathbb{T}}_M]$ determines its provable geometric sequents. Mutual simulation is strictly coarser than bisimulation, strictly coarser than topos equivalence; diamond-only Hennessy-Milner logic characterizes the bisimulation-invariant fragment of geometric logic – a geometric van Benthem theorem. Grothendieck topologies yield $J_{\mathrm{b}\mathrm{i}\mathrm{s}\mathrm{i}\mathrm{m}}⊊J_{\mathrm{s}\mathrm{i}\mathrm{m}}⊊J_{\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}}$, constructive for trace and bisimulation; a counterexample shows the observation-class approach inadequate for simulation, motivating Caramello’s duality. Energy-topology extends this to all 13 named equivalences. Lattice closure yields 30 elements including 17 unnamed hybrids absent because the energy-game framework computes but does not close. $L_{30}$ is indecomposable with $S\to F=\mathrm{I}\mathrm{F}$; a Geometric Closure Theorem computes presheaf Heyting implications at a single free extension. The hierarchy, bi-Heyting structure, and Closure Theorem are proved constructively with no known process-algebraic proof. The spectrum is a finite sub-poset of an infinite coframe whose operations (meets, implications, subtractions) yield structure inaccessible from process algebra. Formalized in Lean 4/Mathlib.