Bisimulation invariance for BSML

The carrier-level bisimulation substrate (WorldBisim, StateBisim, and the Lemma 3.7 transport lemmas of [AAY24]) lives in Logic/Team/Bisimulation.lean, shared across the modal team logics. This file specialises it to BSML: the modal-depth measure on Formula and the invariance result (Theorem 3.8) for BSML's bilateral evaluation, which the [Ant25] expressive-completeness development consumes in BSML/ExpressiveCompleteness.lean.

Main declarations

• Formula.modalDepth — modal depth (page 9): atoms/NE are 0, conj/disj take max, poss increments.
• bisim_invariant_eval — Theorem 3.8 for BSML: k-bisimilar states agree on eval for all formulas of modal depth ≤ k, for both polarities.

Implementation notes

The bisim-invariance proof inducts on the formula, handling both polarities (eval M b φ s) jointly at each step. The negation case flips polarity without changing depth; the modal case recurses at depth k through WorldBisim.accessStateBisim (the singleton form of Lemma 3.7(i)), with StateBisim.exists_image_subset transporting the poss-support witness sub-team; conjunction and disjunction use StateBisim.splitPreserve (Lemma 3.7(ii)) for the split-existential clauses (conj-antiSupport and disj-support).

Todo

• Hennessy-Milner direction (Theorem 3.3): k-equivalence implies k-bisimilarity, via Hintikka formulas. Requires a finite atom set hypothesis ([Fintype Atom]) for the characteristic-formula construction. Deferred — Theorem 3.8 alone is enough for the soundness half of the expressive-completeness theorem in BSML/ExpressiveCompleteness.lean.

Modal depth

def BSML.Formula.modalDepth {Atom : Type u_3} : Formula Atom → ℕ

Modal depth of a Formula (page 9 of [AAY24]). Atoms and NE are 0; neg preserves depth; conj and disj take the max; poss increments.

Equations

• (BSML.Formula.atom a).modalDepth = 0
• BSML.Formula.ne.modalDepth = 0
• ψ.neg.modalDepth = ψ.modalDepth
• (ψ₁.conj ψ₂).modalDepth = max ψ₁.modalDepth ψ₂.modalDepth
• (ψ₁.disj ψ₂).modalDepth = max ψ₁.modalDepth ψ₂.modalDepth
• ψ.poss.modalDepth = ψ.modalDepth + 1

Theorem 3.8: bisimulation invariance for BSML

theorem BSML.bisim_invariant_eval {W : Type u_1} {W' : Type u_2} [DecidableEq W] [DecidableEq W'] {Atom : Type u_3} {M : ModalLogic.KripkeModel W Atom} {M' : ModalLogic.KripkeModel W' Atom} (φ : Formula Atom) {k : ℕ} (hd : φ.modalDepth ≤ k) {s : Finset W} {s' : Finset W'} (hbisim : ModalLogic.StateBisim k M s M' s') (b : Bool) : eval M b φ s ↔ eval M' b φ s'

Theorem 3.8 of [AAY24] specialised to BSML: if s ⇌_k s' and φ : Formula Atom has modal depth ≤ k, then eval M b φ s ↔ eval M' b φ s' for both polarities.

Proved by structural induction on φ, with both polarities handled jointly at each step. The neg case flips polarity without changing depth; the poss case recurses at depth k through WorldBisim.accessStateBisim; conjunction and disjunction use Lemma 3.7(ii) for the split-existential clauses (conj-antiSupport and disj-support).