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. Registered in the Lax archive as Lax945089.PebbleInvariance.realize_equivK₂.