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.

[patchwright]

Thanks @ctchou — addressed in 9be8656 + 6c36cc1:

• polarity is now an actual Mathlib GaloisConnection (stated into the order dual (Set (Proc → Ω))ᵒᵈ, the standard phrasing for an antitone connection), with the pointwise reading kept as polarity_iff.
• cl Ω is now (polarity Ω).closureOperator : ClosureOperator (Proc → Proc → Prop) — the same pattern as PhaseSemantics.biorthogonalClosure — so cl_extensive/cl_monotone/cl_idempotent are inherited from Mathlib's ClosureOperator API instead of proved by hand, and Testable Ω E is (cl Ω).IsClosed E. induced_testable is now GaloisConnection.u_l_u_eq_u applied to the polarity.
• As a corollary this buys a new statement for free: spectrumCompleteLattice — the testable equivalences form a complete lattice under refinement, via (cl Ω).gi.liftCompleteLattice (the Order.Nucleus pattern).

Also rewrote the Spectrum.Antichain module comment you flagged: it now says plainly that the file proves the structural antichain over an explicit 4-state witness, and that the named classical pair (simulation vs failures equivalence) would need failures semantics CSLib doesn't yet define, so it isn't attempted there.

Downstream files (TracePoint, BisimPoint, Antichain) needed no proof changes.

[ctchou]

I've read only Galois.lean so far.

Exactly what is a "spectrum"? You talk about it in comments, but there is not a Lean definition corresponding to it.

In general, I think the comments can use some improvement. Did you have AI write the comments for you? I find some of them very verbose but not very illuminating. Can you write the comments in your own words?

[ctchou]

A Galois connection relates two partial orders. I can see that one of the two orders here is the subset relation over Set (Proc → Ω). What is the other order?

For that matter, what are the intuitive meanings of the types Proc, Ω, and Proc → Ω)?

[ctchou]

When I look up the definition of GaloisConnection in mathlib, I see that it has the following parameters:

[Preorder α ][Preorder β] (l : α → β) (u : β → α)

Can you make clear what the above parameters in this particular instance?

[ctchou]

It seems to me that these are general properties that are true for any closure operator. Is it really necessary to state them? They can be proved on the fly when they are needed.

[patchwright]

@ctchou Addressed in 312d557.

• spectrum is now defined (def spectrum Ω := { E | Testable Ω E }), and both preorders are stated in the module doc: equivalences under pointwise implication E ≤ E' ↔ ∀ p q, E p q → E' p q, test classes under (⊆).
• Removed cl_extensive/cl_monotone/cl_idempotent — the inherited ClosureOperator API under new names.
• Yes, AI-assisted. Comments rewritten across the module — terser, no proof narration in the docstrings.

Builds clean (0 sorry). spectrum is a Set so spectrum_eq_closed_elements reads as the image of induced; I can make it the Closeds subtype if you'd prefer.

[patchwright]

@ctchou No urgency on this — just flagging for visibility: I've opened a
follow-up PR (#752) adding may- and must-testing equivalence as two more
points on the same Galois-connection framework from this PR. It's independent
of anything still open here (doesn't touch Galois.lean or the existing
point files), so happy for it to sit until you have bandwidth for either.

[chenson2018]

@patchwright We appreciate your disclosure of AI usage in this PR, but this still does not follow the full extent of our policy.It appears that your comments, both within the code and in response to reviews, are AI-written. As is stated in the Mathlib AI policy:

Using an LLM when writing comments on GitHub or Zulip is not allowed: use your own words.

along with several general issues with this generated code. For this reason, we will be closing this PR.