The k-variable invariance lemma, across two structures

DescriptiveComplexity.realize_equivK says a formula with room for its quantifier depth cannot separate two ≡ᵏ-equivalent tuples of one structure. This file proves the same for tuples of two structures (DescriptiveComplexity.realize_equivK₂), against the game of DescriptiveComplexity.Invariant.TwoPebble – the proof is the textbook pebble argument once more, each quantifier spending one fresh pebble, placed by the game move DescriptiveComplexity.EquivK₂.update, with the two sides of the quantifier now ranging over different universes.

Read at a sentence, this is what separates a Boolean query: two structures with a k-pebble equivalent pair of tuples satisfy the same formulas of k variables.

theorem DescriptiveComplexity.realize_equivK₂ {L : FirstOrder.Language} {M N : Type} {k : ℕ} [L.IsRelational] [L.Structure M] [L.Structure N] [Finite M] [Finite N] {S : Set ((n : ℕ) × L.Relations n)} {α : Type} [Fintype α] {n : ℕ} (φ : L.BoundedFormula α n) (g : α → Fin k) (h : Fin n → Fin k) : Function.Injective h → (∀ (i : α) (j : Fin n), g i ≠ h j) → (Finset.image g Finset.univ ∪ Finset.image h Finset.univ).card + qdepth φ ≤ k → RelsIn S φ → ∀ (v : Fin k → M) (w : Fin k → N), EquivK₂ (atomicAgreeOn₂ S M N k) v w → ((φ.Realize (fun (i : α) => v (g i)) fun (j : Fin n) => v (h j)) ↔ φ.Realize (fun (i : α) => w (g i)) fun (j : Fin n) => w (h j))

The k-variable invariance lemma, between two structures. A formula over a relational vocabulary, with relation symbols in S, cannot separate a pair of k-pebble equivalent tuples of two structures: its free variables read the tuples through an arbitrary selection of coordinates, its bound variables through an injective selection disjoint from it, and the coordinates left over leave room for its quantifier depth.

theorem DescriptiveComplexity.realize_formula_equivK₂ {L : FirstOrder.Language} {M N : Type} {k : ℕ} [L.IsRelational] [L.Structure M] [L.Structure N] [Finite M] [Finite N] {S : Set ((n : ℕ) × L.Relations n)} {α : Type} [Fintype α] (φ : L.Formula α) (g : α → Fin k) (hroom : (Finset.image g Finset.univ).card + qdepth φ ≤ k) (hS : RelsIn S φ) {v : Fin k → M} {w : Fin k → N} (hvw : EquivK₂ (atomicAgreeOn₂ S M N k) v w) : (φ.Realize fun (i : α) => v (g i)) ↔ φ.Realize fun (i : α) => w (g i)

The formula form: a formula whose free variables read the tuples through a selection of coordinates, with room left for its quantifier depth, cannot separate an equivalent pair.

theorem DescriptiveComplexity.realize_sentence_equivK₂ {L : FirstOrder.Language} {M N : Type} {k : ℕ} [L.IsRelational] [L.Structure M] [L.Structure N] [Finite M] [Finite N] {S : Set ((n : ℕ) × L.Relations n)} (φ : L.Sentence) (hdepth : qdepth φ ≤ k) (hS : RelsIn S φ) {v : Fin k → M} {w : Fin k → N} (hvw : EquivK₂ (atomicAgreeOn₂ S M N k) v w) : M ⊨ φ ↔ N ⊨ φ

The sentence form: two structures carrying a k-pebble equivalent pair of k-tuples satisfy the same sentences of quantifier depth at most k.