diff --git a/Cslib.lean b/Cslib.lean
index 43c374ae7..64c1a5101 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -98,6 +98,12 @@ public import Cslib.Foundations.Semantics.LTS.Notation
 public import Cslib.Foundations.Semantics.LTS.OmegaExecution
 public import Cslib.Foundations.Semantics.LTS.Relation
 public import Cslib.Foundations.Semantics.LTS.Simulation
+public import Cslib.Foundations.Semantics.LTS.Spectrum.Antichain
+public import Cslib.Foundations.Semantics.LTS.Spectrum.BisimPoint
+public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois
+public import Cslib.Foundations.Semantics.LTS.Spectrum.MayTestingPoint
+public import Cslib.Foundations.Semantics.LTS.Spectrum.MustTestingPoint
+public import Cslib.Foundations.Semantics.LTS.Spectrum.TracePoint
 public import Cslib.Foundations.Semantics.LTS.Termination
 public import Cslib.Foundations.Semantics.LTS.Total
 public import Cslib.Foundations.Semantics.LTS.TraceEq
diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean
new file mode 100644
index 000000000..be27aeecb
--- /dev/null
+++ b/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean
@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2026 patchwright. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: patchwright
+-/
+
+module
+
+public import Cslib.Init
+public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois
+
+/-!
+# Spectrum antichain — the closed-element lattice is not a chain
+
+The lattice of testable equivalences is not totally ordered by refinement. Over
+a 4-state witness, two test classes `T₁`, `T₂` (Ω = `Bool`) induce closed
+equivalences that are incomparable:
+  - states a,b are `T₁`-equivalent but `T₂`-distinct;
+  - states a,c are `T₂`-equivalent but `T₁`-distinct.
+
+So the spectrum contains an antichain — it is a lattice, not a linear scale
+(cf. [Glabbeek1990]).
+-/
+
+@[expose] public section
+
+namespace Cslib.LTS.Spectrum
+
+/-- 4-state witness space. -/
+inductive W where
+  | a | b | c | d
+
+open W
+
+/-- Test t₁: groups {a,b} (true) vs {c,d} (false). -/
+def t1 : W → Bool
+  | a | b => true
+  | c | d => false
+
+/-- Test t₂: groups {a,c} (true) vs {b,d} (false). -/
+def t2 : W → Bool
+  | a | c => true
+  | b | d => false
+
+/-- Test class `T₁`: the singleton `{ t₁ }`. -/
+def T1 : Set (W → Bool) := { f | f = t1 }
+/-- Test class `T₂`: the singleton `{ t₂ }`. -/
+def T2 : Set (W → Bool) := { f | f = t2 }
+
+/-- a,b are `T₁`-equivalent but `T₂`-distinct. -/
+theorem T1_ab_not_T2_ab : induced Bool T1 a b ∧ ¬ induced Bool T2 a b := by
+  refine ⟨?_, ?_⟩
+  · intro t ht
+    have ht : t = t1 := ht
+    subst ht
+    rfl
+  · intro h
+    have hh : t2 a = t2 b := h t2 rfl
+    simp only [t2] at hh
+    exact Bool.noConfusion hh
+
+/-- a,c are `T₂`-equivalent but `T₁`-distinct. -/
+theorem T2_ac_not_T1_ac : induced Bool T2 a c ∧ ¬ induced Bool T1 a c := by
+  refine ⟨?_, ?_⟩
+  · intro t ht
+    have ht : t = t2 := ht
+    subst ht
+    rfl
+  · intro h
+    have hh : t1 a = t1 c := h t1 rfl
+    simp only [t1] at hh
+    exact Bool.noConfusion hh
+
+/-- **The closed-element lattice is not a chain.** There exist two incomparable
+    testable (Galois-closed) equivalences. -/
+theorem exists_incomparable_closed :
+    ∃ E₁ E₂ : W → W → Prop,
+      Testable Bool E₁ ∧ Testable Bool E₂ ∧
+        ¬ (∀ p q, E₁ p q → E₂ p q) ∧ ¬ (∀ p q, E₂ p q → E₁ p q) := by
+  refine ⟨induced Bool T1, induced Bool T2,
+          induced_testable Bool T1, induced_testable Bool T2, ?_, ?_⟩
+  · intro h
+    exact T1_ab_not_T2_ab.2 (h a b T1_ab_not_T2_ab.1)
+  · intro h
+    exact T2_ac_not_T1_ac.2 (h a c T2_ac_not_T1_ac.1)
+
+end Cslib.LTS.Spectrum
diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/BisimPoint.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/BisimPoint.lean
new file mode 100644
index 000000000..b33cdf1d3
--- /dev/null
+++ b/Cslib/Foundations/Semantics/LTS/Spectrum/BisimPoint.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 patchwright. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: patchwright
+-/
+
+module
+
+public import Cslib.Init
+public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois
+public import Cslib.Logics.HML.Basic
+
+/-!
+# Spectrum bisim point — bisimilarity is Galois-closed (via Hennessy–Milner)
+
+The non-trivial spectrum point. Unlike trace equivalence (`Spectrum.TracePoint`),
+bisimilarity is not the kernel of its test map by definition; the
+Hennessy–Milner theorem makes it one. CSLib mechanises HM as
+`Cslib.Logic.HML.theoryEq_eq_bisimilarity` (`TheoryEq lts = HomBisimilarity lts`
+for image-finite LTS), and `TheoryEq` is the equivalence induced by the
+HML-theory test class, so:
+
+  `Testable (Set (Proposition Label)) (HomBisimilarity lts)`.
+-/
+
+@[expose] public section
+
+namespace Cslib.LTS.Spectrum
+
+open Cslib Cslib.Logic.HML
+
+variable {State Label : Type*} (lts : LTS State Label)
+
+/-- The HML-theory observer test: a state's full theory (set of satisfied HML
+    propositions). -/
+def hmlTheory (s : State) : Set (Proposition Label) :=
+  theory lts s
+
+/-- Test class for the bisim point: the singleton HML-theory observer. -/
+def hmlTestClass : Set (State → Set (Proposition Label)) :=
+  { f | f = hmlTheory lts }
+
+/-- The equivalence induced by the HML-theory test is CSLib's `TheoryEq`
+    (pointwise iff). -/
+theorem induced_hml_iff (p q : State) :
+    induced (Set (Proposition Label)) (hmlTestClass lts) p q ↔ TheoryEq lts p q := by
+  constructor
+  · intro h
+    exact h _ rfl
+  · intro h t ht
+    have ht : t = hmlTheory lts := ht
+    subst ht
+    exact h
+
+/-- Function-equality form of `induced_hml_iff`. -/
+theorem induced_hml :
+    induced (Set (Proposition Label)) (hmlTestClass lts) = TheoryEq lts := by
+  funext p q
+  exact propext (induced_hml_iff lts p q)
+
+/-- **Bisim point.** `HomBisimilarity lts` is testable for image-finite LTS, via
+    the Hennessy–Milner theorem (`theoryEq_eq_bisimilarity`). -/
+theorem HomBisimilarity_testable [image_finite : ∀ s μ, Finite (lts.image s μ)] :
+    Testable (Set (Proposition Label)) (HomBisimilarity lts) := by
+  rw [← theoryEq_eq_bisimilarity lts, ← induced_hml lts]
+  exact induced_testable (Set (Proposition Label)) (hmlTestClass lts)
+
+end Cslib.LTS.Spectrum
diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean
new file mode 100644
index 000000000..d03f94cbd
--- /dev/null
+++ b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean
@@ -0,0 +1,155 @@
+/-
+Copyright (c) 2026 patchwright. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: patchwright
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Order.GaloisConnection.Basic
+public import Mathlib.Order.Closure
+
+/-!
+# The van Glabbeek spectrum as a Galois connection
+
+The linear time–branching time spectrum of behavioural equivalences is the set
+of *testable* equivalences on a process type: those an observer recovers exactly
+as indistinguishability under the tests that respect them. This set is the
+collection of closed elements of an antitone Galois connection — a *polarity* —
+between equivalences and tests.
+
+The two preorders of the connection are:
+
+* equivalences `E : Proc → Proc → Prop`, ordered by pointwise implication
+  `E ≤ E' ↔ ∀ p q, E p q → E' p q` (graph inclusion);
+* test classes `T : Set (Proc → Ω)`, ordered by `(⊆)`.
+
+The antitone connection is packaged as a monotone `GaloisConnection` into the
+order dual on the test side:
+
+  `polarity : GaloisConnection (toDual ∘ respects Ω) (induced Ω ∘ ofDual)`
+
+Its closure operator is `cl Ω = induced Ω ∘ respects Ω`, and the spectrum is the
+set of its closed elements. A named spectrum point (`HomTraceEq`) is shown closed
+in `Spectrum.TracePoint`; the spectrum is a lattice rather than a chain
+(`Spectrum.Antichain`).
+
+The construction is parameterised by `Proc` (the process type) and `Ω` (the
+observation type; a test is `Proc → Ω`). `Ω` is carried explicitly because the
+closure operator itself mentions only `E`.
+
+## Main definitions
+
+* `induced Ω T`: the equivalence a test class induces.
+* `respects Ω E`: the tests constant on every `E`-pair.
+* `polarity Ω`: the Galois connection above.
+* `cl Ω`: the closure operator `induced Ω ∘ respects Ω`.
+* `Testable Ω E`: the proposition that `E` is `cl Ω`-closed.
+* `spectrum Ω`: the set of testable equivalences.
+
+## Main statements
+
+* `spectrum_eq_closed_elements`: the testable equivalences are exactly the image
+  of `induced`.
+* `spectrumCompleteLattice`: the spectrum is a complete lattice under refinement.
+
+## References
+
+* [R.J. van Glabbeek, *The Linear Time – Branching Time Spectrum*][Glabbeek1990],
+  extended to silent moves in *Spectrum II* [Glabbeek1993].
+* [H. Beohar, *Hennessy-Milner Theorems via Galois Connections*][Beohar2022].
+-/
+
+@[expose] public section
+
+namespace Cslib.LTS.Spectrum
+
+open OrderDual (toDual ofDual)
+
+variable {Proc : Type*}
+
+/-- Equivalence induced by a test class `T`: two processes agree on every test
+    in `T`. -/
+def induced (Ω : Type*) (T : Set (Proc → Ω)) (p q : Proc) : Prop :=
+  ∀ t ∈ T, t p = t q
+
+/-- Tests that respect an equivalence `E`: constant on every `E`-pair. -/
+def respects (Ω : Type*) (E : Proc → Proc → Prop) : Set (Proc → Ω) :=
+  { t | ∀ p q, E p q → t p = t q }
+
+/-- `E` refines `induced Ω T` iff every test in `T` respects `E`. -/
+theorem polarity_iff (Ω : Type*) (T : Set (Proc → Ω)) (E : Proc → Proc → Prop) :
+    (∀ p q, E p q → induced Ω T p q) ↔ T ⊆ respects Ω E := by
+  constructor
+  · intro h t ht p q hpq
+    exact h p q hpq t ht
+  · intro h p q hpq t ht
+    exact h ht p q hpq
+
+/-- The polarity: `respects Ω` and `induced Ω` form an antitone Galois connection
+    between equivalences (pointwise implication) and test classes (`(⊆)`, into
+    the order dual). -/
+theorem polarity (Ω : Type*) :
+    GaloisConnection (fun E : Proc → Proc → Prop => toDual (respects Ω E))
+      (fun T => induced Ω (ofDual T)) := by
+  intro E T
+  rw [OrderDual.toDual_le]
+  simp only [Pi.le_def, le_Prop_eq]
+  exact (polarity_iff Ω (ofDual T) E).symm
+
+/-- Every test in `T` respects the equivalence `T` induces. -/
+theorem test_subset_respects_induced (Ω : Type*) (T : Set (Proc → Ω)) :
+    T ⊆ respects Ω (induced Ω T) :=
+  (polarity Ω).l_u_le (toDual T)
+
+/-- Closure operator `induced Ω ∘ respects Ω`, obtained from `polarity` as a
+    `ClosureOperator`. -/
+def cl (Ω : Type*) : ClosureOperator (Proc → Proc → Prop) :=
+  (polarity (Proc := Proc) Ω).closureOperator
+
+/-- `cl Ω E = induced Ω (respects Ω E)`. -/
+theorem cl_apply (Ω : Type*) (E : Proc → Proc → Prop) :
+    cl Ω E = induced Ω (respects Ω E) :=
+  rfl
+
+/-- An equivalence is *testable* iff it is a closed element of `cl Ω`. -/
+def Testable (Ω : Type*) (E : Proc → Proc → Prop) : Prop :=
+  (cl Ω).IsClosed E
+
+/-- The **van Glabbeek spectrum**: the set of testable equivalences on `Proc`. -/
+def spectrum (Ω : Type*) : Set (Proc → Proc → Prop) :=
+  { E | Testable Ω E }
+
+/-- `Testable Ω E` iff `cl Ω E` and `E` agree pointwise. -/
+theorem testable_iff (Ω : Type*) (E : Proc → Proc → Prop) :
+    Testable Ω E ↔ ∀ p q, cl Ω E p q ↔ E p q := by
+  rw [Testable, ClosureOperator.isClosed_iff]
+  constructor
+  · intro h p q
+    exact iff_of_eq (congrFun (congrFun h p) q)
+  · intro h
+    funext p q
+    exact propext (h p q)
+
+/-- Every induced equivalence is testable. -/
+theorem induced_testable (Ω : Type*) (T : Set (Proc → Ω)) :
+    Testable Ω (induced Ω T) :=
+  (cl Ω).isClosed_iff.2 ((polarity Ω).u_l_u_eq_u (toDual T))
+
+/-- An equivalence is testable iff it is induced by some test class. -/
+theorem spectrum_eq_closed_elements (Ω : Type*) (E : Proc → Proc → Prop) :
+    Testable Ω E ↔ ∃ T : Set (Proc → Ω), induced Ω T = E := by
+  constructor
+  · intro hE
+    exact ⟨respects Ω E, (cl Ω).isClosed_iff.1 hE⟩
+  · rintro ⟨T, rfl⟩
+    exact induced_testable Ω T
+
+/-- The spectrum is a complete lattice under refinement; it is not a chain
+    (see `Spectrum.Antichain`). -/
+instance spectrumCompleteLattice {Ω : Type*} :
+    CompleteLattice ((cl (Proc := Proc) Ω).Closeds) :=
+  (cl Ω).gi.liftCompleteLattice
+
+end Cslib.LTS.Spectrum
diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/MayTestingPoint.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/MayTestingPoint.lean
new file mode 100644
index 000000000..5aaecc8c5
--- /dev/null
+++ b/Cslib/Foundations/Semantics/LTS/Spectrum/MayTestingPoint.lean
@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2026 patchwright. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: patchwright
+-/
+
+module
+
+public import Cslib.Init
+public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois
+public import Cslib.Languages.CCS.Basic
+public import Cslib.Languages.CCS.Semantics
+public import Cslib.Foundations.Semantics.LTS.HasTau
+
+/-!
+# Spectrum may-testing point — may-testing equivalence is Galois-closed
+
+A named point of the van Glabbeek spectrum: (may-)testing equivalence
+[De Nicola & Hennessy, 1984]. A *test* is a process together with a distinguished
+*success* action; a process `p` *may pass* a test `T` when some computation of
+`p ∥ T` performs the success action. Two processes are may-testing-equivalent
+when they may-pass exactly the same tests.
+
+Unlike the bisim point — where bisimilarity is connected to the spectrum via the
+Hennessy–Milner theorem — may-testing equivalence is, by its standard
+definition, exactly the equivalence induced by the class of may-test observers.
+Its closedness is therefore definitional (as for `Spectrum.TracePoint`): it is
+`induced` of the may-test class, and every induced equivalence is testable.
+
+## References
+
+* [R. De Nicola & M. Hennessy, *Testing Equivalences for Processes*][DeNicolaHennessy1984].
+-/
+
+@[expose] public section
+
+namespace Cslib.LTS.Spectrum
+
+open Cslib CCS
+
+variable
+  {Name : Type u}
+  {Constant : Type v}
+
+/-- `p` *may pass* test `T`: some computation of `p ∥ T` performs `success`
+    (it appears among the labels of a multistep computation of the parallel
+    composition). Strong, matching `MustTestingPoint.mustPass`. -/
+def mayPass (defs : Constant → CCS.Process Name Constant → Prop)
+    (success : CCS.Act Name) (p T : CCS.Process Name Constant) : Prop :=
+  ∃ μs s', (CCS.lts (defs := defs)).MTr (Process.par p T) μs s' ∧ success ∈ μs
+
+/-- May-testing equivalence: `p` and `q` may-pass exactly the same tests. -/
+def MayEquiv (defs : Constant → CCS.Process Name Constant → Prop)
+    (success : CCS.Act Name) (p q : CCS.Process Name Constant) : Prop :=
+  ∀ T, mayPass defs success p T ↔ mayPass defs success q T
+
+/-- The may-test observer of a process: the set of tests it may-pass. -/
+def mayTests (defs : Constant → CCS.Process Name Constant → Prop)
+    (success : CCS.Act Name) (p : CCS.Process Name Constant) :
+    Set (CCS.Process Name Constant) :=
+  { T | mayPass defs success p T }
+
+/-- Test class for the may-testing point: the singleton may-test observer. -/
+def mayTestClass (defs : Constant → CCS.Process Name Constant → Prop)
+    (success : CCS.Act Name) :
+    Set (CCS.Process Name Constant → Set (CCS.Process Name Constant)) :=
+  { f | f = mayTests defs success }
+
+/-- The equivalence induced by the may-test observer is may-testing equivalence. -/
+theorem induced_mayTests_iff (defs : Constant → CCS.Process Name Constant → Prop)
+    (success : CCS.Act Name) (p q : CCS.Process Name Constant) :
+    induced (Set (CCS.Process Name Constant)) (mayTestClass defs success) p q ↔
+      MayEquiv defs success p q := by
+  simp only [induced, mayTestClass, Set.mem_setOf_eq, MayEquiv]
+  constructor
+  · intro h T
+    have heq : mayTests defs success p = mayTests defs success q :=
+      h (mayTests defs success) rfl
+    rw [Set.ext_iff] at heq
+    simp only [mayTests, Set.mem_setOf_eq] at heq
+    exact heq T
+  · intro h f hf
+    subst hf
+    ext T
+    simp only [mayTests, Set.mem_setOf_eq]
+    exact h T
+
+/-- Function-equality form of `induced_mayTests_iff`. -/
+theorem induced_mayTests (defs : Constant → CCS.Process Name Constant → Prop)
+    (success : CCS.Act Name) :
+    induced (Set (CCS.Process Name Constant)) (mayTestClass defs success) =
+      MayEquiv defs success := by
+  funext p q
+  exact propext (induced_mayTests_iff defs success p q)
+
+/-- **May-testing point.** May-testing equivalence is a closed element of the
+    spectrum: it is testable for a CCS LTS with a distinguished success action. -/
+theorem MayEquiv_testable (defs : Constant → CCS.Process Name Constant → Prop)
+    (success : CCS.Act Name) :
+    Testable (Set (CCS.Process Name Constant)) (MayEquiv defs success) := by
+  rw [← induced_mayTests defs success]
+  exact induced_testable (Set (CCS.Process Name Constant)) (mayTestClass defs success)
+
+end Cslib.LTS.Spectrum
diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/MustTestingPoint.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/MustTestingPoint.lean
new file mode 100644
index 000000000..a2e0c8305
--- /dev/null
+++ b/Cslib/Foundations/Semantics/LTS/Spectrum/MustTestingPoint.lean
@@ -0,0 +1,120 @@
+/-
+Copyright (c) 2026 patchwright. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: patchwright
+-/
+
+module
+
+public import Cslib.Init
+public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois
+public import Cslib.Foundations.Semantics.LTS.Spectrum.MayTestingPoint
+public import Cslib.Languages.CCS.Basic
+public import Cslib.Languages.CCS.Semantics
+public import Cslib.Foundations.Semantics.LTS.Execution
+public import Cslib.Foundations.Semantics.LTS.OmegaExecution
+public import Cslib.Foundations.Semantics.LTS.Termination
+
+/-!
+# Spectrum must-testing point — must-testing equivalence is Galois-closed
+
+The companion to `Spectrum.MayTestingPoint`. A process `p` *must pass* a test
+`T` when **every maximal computation** of `p ∥ T` performs the success action.
+A maximal computation is either a finite execution whose final state is stuck
+(no outgoing transition), or an infinite (`OmegaExecution`) one — so divergence
+without success fails must, as does deadlock without success. Two processes are
+must-testing-equivalent when they must-pass exactly the same tests.
+
+Like may-testing, must-testing equivalence is by definition the equivalence
+induced by the class of must-test observers, so its closedness is definitional
+(`induced_testable`).
+
+## References
+
+* [R. De Nicola & M. Hennessy, *Testing Equivalences for Processes*][DeNicolaHennessy1984].
+-/
+
+@[expose] public section
+
+namespace Cslib.LTS.Spectrum
+
+open Cslib CCS
+
+variable
+  {Name : Type u}
+  {Constant : Type v}
+
+/-- `p` *must pass* test `T`: every maximal computation of `p ∥ T` performs
+    `success`. A maximal computation is either a finite execution ending in a
+    stuck state, or an infinite `OmegaExecution`; in both, success must appear
+    among the labels. Divergence-without-success and deadlock-without-success
+    both fail must.
+
+    "Stuck" reuses `Cslib.LTS.Stuck`, instantiated with the trivial
+    `Terminated := fun _ => False`: testing has no independent notion of a
+    designated terminal state, so a state counts as a testing endpoint exactly
+    when it has no outgoing transition (`¬False ∧ ¬∃ … ↔ ¬∃ …`). -/
+def mustPass (defs : Constant → CCS.Process Name Constant → Prop)
+    (success : CCS.Act Name) (p T : CCS.Process Name Constant) : Prop :=
+  (∀ μs s₂ ss,
+      (CCS.lts (defs := defs)).Execution (Process.par p T) μs s₂ ss →
+      Cslib.LTS.Stuck (CCS.lts (defs := defs)) (fun _ => False) s₂ →
+      success ∈ μs) ∧
+  (∀ ss μs,
+      (CCS.lts (defs := defs)).OmegaExecution ss μs →
+      ss 0 = Process.par p T →
+      ∃ i, μs i = success)
+
+/-- Must-testing equivalence: `p` and `q` must-pass exactly the same tests. -/
+def MustEquiv (defs : Constant → CCS.Process Name Constant → Prop)
+    (success : CCS.Act Name) (p q : CCS.Process Name Constant) : Prop :=
+  ∀ T, mustPass defs success p T ↔ mustPass defs success q T
+
+/-- The must-test observer of a process: the set of tests it must-pass. -/
+def mustTests (defs : Constant → CCS.Process Name Constant → Prop)
+    (success : CCS.Act Name) (p : CCS.Process Name Constant) :
+    Set (CCS.Process Name Constant) :=
+  { T | mustPass defs success p T }
+
+/-- Test class for the must-testing point: the singleton must-test observer. -/
+def mustTestClass (defs : Constant → CCS.Process Name Constant → Prop)
+    (success : CCS.Act Name) :
+    Set (CCS.Process Name Constant → Set (CCS.Process Name Constant)) :=
+  { f | f = mustTests defs success }
+
+/-- The equivalence induced by the must-test observer is must-testing equivalence. -/
+theorem induced_mustTests_iff (defs : Constant → CCS.Process Name Constant → Prop)
+    (success : CCS.Act Name) (p q : CCS.Process Name Constant) :
+    induced (Set (CCS.Process Name Constant)) (mustTestClass defs success) p q ↔
+      MustEquiv defs success p q := by
+  simp only [induced, mustTestClass, Set.mem_setOf_eq, MustEquiv]
+  constructor
+  · intro h T
+    have heq : mustTests defs success p = mustTests defs success q :=
+      h (mustTests defs success) rfl
+    rw [Set.ext_iff] at heq
+    simp only [mustTests, Set.mem_setOf_eq] at heq
+    exact heq T
+  · intro h f hf
+    subst hf
+    ext T
+    simp only [mustTests, Set.mem_setOf_eq]
+    exact h T
+
+/-- Function-equality form of `induced_mustTests_iff`. -/
+theorem induced_mustTests (defs : Constant → CCS.Process Name Constant → Prop)
+    (success : CCS.Act Name) :
+    induced (Set (CCS.Process Name Constant)) (mustTestClass defs success) =
+      MustEquiv defs success := by
+  funext p q
+  exact propext (induced_mustTests_iff defs success p q)
+
+/-- **Must-testing point.** Must-testing equivalence is a closed element of the
+    spectrum: it is testable for a CCS LTS with a distinguished success action. -/
+theorem MustEquiv_testable (defs : Constant → CCS.Process Name Constant → Prop)
+    (success : CCS.Act Name) :
+    Testable (Set (CCS.Process Name Constant)) (MustEquiv defs success) := by
+  rw [← induced_mustTests defs success]
+  exact induced_testable (Set (CCS.Process Name Constant)) (mustTestClass defs success)
+
+end Cslib.LTS.Spectrum
diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean
new file mode 100644
index 000000000..6dbf9d835
--- /dev/null
+++ b/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean
@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2026 patchwright. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: patchwright
+-/
+
+module
+
+public import Cslib.Init
+public import Cslib.Foundations.Semantics.LTS.TraceEq
+public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois
+
+/-!
+# Spectrum trace point — trace equivalence is Galois-closed
+
+CSLib's homogeneous trace equivalence (`HomTraceEq`) is a Galois-closed
+(testable) equivalence: it is the equivalence induced by the trace-set observer
+test class (`Ω = Set (List Label)`), hence a fixed point of the closure operator
+`cl`.
+
+The companion bisimilarity point (which uses the Hennessy–Milner theorem) is in
+`Spectrum.BisimPoint`.
+-/
+
+@[expose] public section
+
+namespace Cslib.LTS.Spectrum
+
+open Cslib
+
+variable {State Label : Type*} (lts : LTS State Label)
+
+/-- The trace-set observer test: a state's full set of traces. -/
+def traceSetTest (s : State) : Set (List Label) :=
+  lts.traces s
+
+/-- Test class for the trace point: the singleton trace-set observer. -/
+def traceTestClass : Set (State → Set (List Label)) :=
+  { f | f = traceSetTest lts }
+
+/-- The equivalence induced by the trace-set test is CSLib's homogeneous trace
+    equivalence (pointwise iff). -/
+theorem induced_traceSet_iff (p q : State) :
+    induced (Set (List Label)) (traceTestClass lts) p q ↔ HomTraceEq lts p q := by
+  constructor
+  · intro h
+    exact h _ rfl
+  · intro h t ht
+    have ht : t = traceSetTest lts := ht
+    subst ht
+    exact h
+
+/-- Function-equality form of `induced_traceSet_iff`. -/
+theorem induced_traceSet :
+    induced (Set (List Label)) (traceTestClass lts) = HomTraceEq lts := by
+  funext p q
+  exact propext (induced_traceSet_iff lts p q)
+
+/-- **Trace point.** CSLib's homogeneous trace equivalence is a Galois-closed
+    (testable) equivalence. -/
+theorem HomTraceEq_testable :
+    Testable (Set (List Label)) (HomTraceEq lts) := by
+  rw [← induced_traceSet lts]
+  exact induced_testable (Set (List Label)) (traceTestClass lts)
+
+end Cslib.LTS.Spectrum
diff --git a/references.bib b/references.bib
index 18281428d..22207e2d9 100644
--- a/references.bib
+++ b/references.bib
@@ -39,6 +39,15 @@ @book{Baader1998
 address = {USA}
 }
 
+@misc{Beohar2022,
+  author       = {Beohar, Harsh and Gurke, Sebastian and K{\"o}nig, Barbara and Messing, Karla},
+  title        = {Hennessy-Milner Theorems via Galois Connections},
+  year         = {2022},
+  eprint       = {2207.05407},
+  archiveprefix = {arXiv},
+  url          = {https://arxiv.org/abs/2207.05407}
+}
+
 @book{Blackburn2001,
   place={Cambridge},
   series={Cambridge Tracts in Theoretical Computer Science},
@@ -176,6 +185,24 @@ @inbook{          Girard1995
   collection={London Mathematical Society Lecture Note Series}
 }
 
+@inproceedings{Glabbeek1990,
+  author       = {van Glabbeek, R.J.},
+  title        = {The Linear Time -- Branching Time Spectrum},
+  booktitle    = {CONCUR '90: Theories of Concurrency (Unification and Extension)},
+  series       = {Lecture Notes in Computer Science},
+  volume       = {458},
+  year         = {1990},
+  pages        = {278--297},
+  publisher    = {Springer}
+}
+
+@misc{Glabbeek1993,
+  author       = {van Glabbeek, R.J.},
+  title        = {The Linear Time -- Branching Time Spectrum II},
+  year         = {1993},
+  note         = {Extended manuscript; adds silent moves (branching/weak semantics)}
+}
+
 @article{Haussler1992,
   author       = {Haussler, David},
   title        = {Decision Theoretic Generalizations of the {PAC} Model for Neural Net and Other Learning Applications},