feat(LTS/Spectrum): van Glabbeek spectrum as a Galois connection

[patchwright]

Summary

Organises behavioural equivalences as the fixed points of an antitone Galois connection ("polarity") between test classes (ordered by ⊆) and equivalences (ordered by refinement). The Galois-closed equivalences — the "testable" ones — are exactly the image of induced. Two named behavioural equivalences are exhibited as closed elements of the SAME polarity: trace equivalence (kernel-trivial) and bisimilarity (Hennessy–Milner-mediated) — the actual "spectrum as Galois" statement.

What's added

New module Cslib.Foundations.Semantics.LTS.Spectrum (4 files):

• Galois.lean — the framework (Cslib.Init only): induced Ω T, respects Ω E, closure operator cl Ω, polarity (the antitone Galois connection), induced_testable, spectrum_eq_closed_elements.
• TracePoint.lean — HomTraceEq_testable: homogeneous trace equivalence is Galois-closed, via the trace-set observer test class. (Kernel-trivial bottom point.)
• BisimPoint.lean — HomBisimilarity_testable: homogeneous bisimilarity is Galois-closed for image-finite LTS, via the Hennessy–Milner theorem (theoryEq_eq_bisimilarity). (Non-trivial top point — bisimilarity is not a kernel by definition; HM makes it one.)
• Antichain.lean — exists_incomparable_closed: the closed-element lattice contains an antichain (a lattice, not a chain).

Why it's additive

CSLib has Bisimilarity, Simulation/SimulationEquiv, TraceEq, HML, and the Hennessy–Milner theorem (theoryEq_eq_bisimilarity), but no organisation of the spectrum as a Galois structure. This provides that organisation, reusing CSLib's existing equivalences + HM as named closed instances. It does not redefine any existing equivalence.

Scope notes / honesty

• The trace point is kernel-trivial: the test class IS the trace-set map, so induced = HomTraceEq is near-definitional. It's the honest bottom point; the per-trace Bool-test refinement (decidability-gated) is a finer witness for the same closed element.
• The bisim point is the non-trivial one: it relies on HM (theoryEq_eq_bisimilarity) to connect bisimilarity to the HML-theory kernel. That step does real work — it's what earns the word "spectrum."
• The antichain is framework-internal (two custom test classes over a 4-state space). The named van Glabbeek antichain (simulation vs failures) requires failures semantics, not in CSLib — left as future work.
• (An earlier draft of this PR falsely claimed "CSLib does not yet mechanise HM"; that was a grep miss — corrected by reading Cslib.Logic.HML.Basic.)

Verification

Builds clean (Lean v4.32.0-rc1), 0 sorry / 0 axiom. All four modules compile and reach Cslib.Init transitively. Full-lib CI runs on this PR.

AI use disclosure

Per CSLib's AI policy (following Mathlib): this contribution was developed with AI assistance. An AI coding assistant (Claude Code, glm-5.2 model) wrote the Lean definitions and proofs under the contributor's direction; the contributor designed the approach, reviewed each definition and proof, and accepts responsibility for the content. All proofs are verified by the Lean compiler (0 sorry / 0 axiom), which mitigates the AI-typical errors this disclosure helps reviewers spot. Please flag anything that looks off.

Open questions for maintainers

• Placement: Cslib/Foundations/Semantics/LTS/Spectrum/ — appropriate, or preferred elsewhere?

[ctchou]

It would be helpful if you can provide a reference for the theory formalized in this PR.

[patchwright]

Thanks for taking a look. Two references for the theory here:

1. The spectrum of behavioural equivalences ordered by refinement:
   R.J. van Glabbeek, "The Linear Time – Branching Time Spectrum",
   CONCUR 1990 (LNCS 458); extended in "…Spectrum II" (1993).

2. The reading of those equivalences as the fixed points of an antitone
   Galois connection (polarity) between tests and equivalences, with the
   spectrum as the closure operator's closed elements:
   H. Beohar, "Hennessy-Milner Theorems via Galois Connections",
   arXiv:2207.05407 (2022).

This PR mechanizes that polarity and closure operator, and instantiates the
trace and bisimulation points of the spectrum.

[ctchou]

You can add those papers to references.bib and refer to them from the comments in your code. For an example of such references, see Cslib/Foundations/Semantics/LTS/Basic.lean.

[patchwright]

Thanks @ctchou — done in d83c14e: the two papers are now in references.bib (Glabbeek1990 CONCUR '90, Glabbeek1993 Spectrum II, Beohar2022 arXiv:2207.05407) and cited from a ## References block in Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean, following the [Author, *Title*][Key] style used in LTS/Basic.lean.

[ctchou]

Your code never defines what a Galois connection is, even though the comments talk about it all the time. Mathlib already contains a lot of stuff about Galois connection:

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/GaloisConnection/Defs.html

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/GaloisConnection/Basic.html

You should make connection with mathlib's definitions and leverage its theorems as much as possible.

I'm not sure "Galois-closed" is a standard terminology and your code doesn't seem to define it, either. Please clarify what it means, in terms of the theory of Galois connection in mathlib.

The content of Antichain.lean seems to consist of examples. Such a file should be named ExampleXXX.lean.

[ctchou]

I don't understand this comment. Please clarify.