Paper

First-Order Model Checking on Monadically Dependent Graph Classes

65 pages · 151 marked passages · pdflatex · download PDF · lax-185574

thm✓Lax185574.IndependenceProperty

Monadic dependence through the independence property

A formula φ(x, y) in the signature of colored graphs has the independence property on a graph class 𝒞 if for every n there are a coloring G⁺ of a graph G ∈ 𝒞, vertices a₁, …, aₙ, and vertices b_J for J ⊆ [n] such that G⁺ ⊨ φ(aᵢ, b_J) holds exactly when i ∈ J. A class is monadically dependent if and only if no formula has the independence property on it.

By a result of Baldwin and Shelah, one may equivalently allow formulas φ(x̄, ȳ) with tuples of variables, and tuples āᵢ and b̄_J. On a monadically dependent class, no such formula has the independence property either.

1	import Lax185574.MonadicDependence
2
	… module docstring, 33 lines
36
37	namespace Lax185574.IndependenceProperty
38
39	open Lax185574.Graphs Lax185574.FirstOrderLogic Lax185574.MonadicDependence
40
41	/-- The formula `φ(x̄, ȳ)` with `k` colors, whose free variables are a
42	tuple `x̄` of `p` variables followed by a tuple `ȳ` of `p'` variables,
43	has the independence property on `C`: for every `m` there are a graph
44	`G ∈ C`, a coloring of `G`, tuples `a i` for `i < m` and tuples `b J`
45	for `J ⊆ {0, …, m - 1}` such that `φ(a i, b J)` holds exactly when
46	`i ∈ J`. -/
47	def HasIP (C : GraphClass) {k p p' : ℕ} (φ : Formula (Fin k) (p + p')) : Prop :=
48	∀ m : ℕ, ∃ G ∈ C, ∃ (col : Fin k → Set (Fin G.n)) (a : Fin m → Fin p → Fin G.n)
49	(b : Finset (Fin m) → Fin p' → Fin G.n),
50	∀ (i : Fin m) (J : Finset (Fin m)), φ.Holds G col (Fin.append (a i) (b J)) ↔ i ∈ J
51
52	/-- A graph class is monadically dependent if and only if no formula
53	`φ(x, y)` of colored graphs, in two single variables, has the
54	independence property on it. -/
55	axiom monadicallyDependent_iff_forall_not_hasIP (C : GraphClass) :
56	MonadicallyDependent C ↔ ∀ (k : ℕ) (φ : Formula (Fin k) (1 + 1)), ¬ HasIP C φ
57
58	/-- On a monadically dependent class, no formula `φ(x̄, ȳ)` of colored
59	graphs, in tuples of variables, has the independence property
60	(Baldwin–Shelah). -/
61	axiom not_hasIP_of_monadicallyDependent (C : GraphClass) (hC : MonadicallyDependent C)
62	{k p p' : ℕ} (φ : Formula (Fin k) (p + p')) : ¬ HasIP C φ
63
64	end Lax185574.IndependenceProperty
65

lem✓Lax185574.BipartiteHomogeneity

⊢Lax185574Proofs.ForbiddenPhiPsiPatterns.forbidden_phiPsi_patterns
- lem✓Lax185574.BipartiteHomogeneity
- thm✓Lax185574.IndependenceProperty
→
lem✓Lax185574.ForbiddenPhiPsiPatterns
The proof in the paper. Color a pair of index pairs $((i, i'), (j, j'))$ by the truth values of φ(āᵢ', c_{i,j}) and $ψ(b̄ⱼ', c_{i,j})$ , and take homogeneous sets $I$ , $J$ by the bipartite Ramsey lemma. Pair up consecutive elements of $I$ and $J$ : with ūᵢ = āᵣ āᵣ' for the $2i$ -th and $(2i+1)$ -st elements $r < r'$ of $I$ , likewise $w̄ⱼ$ , and $d_{i,j} = c_{r,s}$ , the exclusive or $φ(x̄₁, z) ⊕ φ(x̄₂, z)$ holds of ūᵢ', d_{i,j} exactly when $i' = i$ : earlier pairs see two equal truth values by homogeneity, the pair itself sees true then false, and later pairs see false twice. The same holds for the columns. Then the formula $γ = ∃z (U(z) ∧ (φ ⊕ φ) ∧ (ψ ⊕ ψ))$ , with $U$ coloring the grid points $d_{i, h(J)}$ for $i ∈ J$ , encodes membership $i ∈ J$ for an injection $h$ of the subsets of $[k]$ into the columns. By Baldwin–Shelah this bounds $k$ , hence the order of the pattern.

The argument is carried out for the graph classes of the archive and their monadic dependence, and transferred to the graph classes used here.

defLax185574.LocalFormulas

Local formulas and basic local sentences

Fix a finite relational signature σ of arity α. Two σ-formulas φ(x̄) and ψ(x̄) are equivalent if for every σ-structure A and every tuple ā ∈ V(A)^{|x̄|}, A ⊨ φ(ā) if and only if A ⊨ ψ(ā).

The formula adj_σ(x₁, x₂) tests whether x₁ and x₂ are adjacent in the Gaifman graph. For every relation R ∈ σ of arity β ≤ α it tests whether there are elements x₃, …, x_β such that some permutation of x₁, …, x_β satisfies R. Its quantifier rank is at most α − 2. From it one derives the formula dist(x₁, x₂) ≤ r, which checks whether x₁ and x₂ have distance at most r in the Gaifman graph. It quantifies the candidate vertices of a path and checks the required adjacencies in parallel, so its quantifier rank is at most r + α.

A σ-formula φ(x̄) is r-local if every quantifier appearing in φ(x̄) is of the form ∀y ∈ Ball_s(x̄) or ∃y ∈ Ball_s(x̄) for some s ≤ r, where the ball checks are implemented using the dist formulas, which are exempt from this condition. A sentence ψ is basic r-local if there is some r' ≤ r such that ψ is of the form

∃x₁, …, x_m ( ⋀{1 ≤ i < j ≤ m} dist(xᵢ, xⱼ) > 2r' ∧ ⋀{1 ≤ i ≤ m} φ(xᵢ) )

for an r'-local formula φ.

1	import Lax185574.GaifmanGraph
2	import Mathlib.ModelTheory.Satisfiability
3	import Mathlib.Logic.Equiv.Fin.Basic
4
	… module docstring, 74 lines
79
80	namespace Lax185574.LocalFormulas
81
82	open FirstOrder FirstOrder.Language
83
84	universe u v w a
85
86	variable {L : Language.{u, v}}
87
88	/-- Two formulas are equivalent if they hold of the same tuples in
89	every structure whose domain lies in the universe `w`. -/
90	def Equivalent {α : Type a} (φ ψ : L.Formula α) : Prop :=
91	∀ (M : Type w) [L.Structure M] (x : α → M), φ.Realize x ↔ ψ.Realize x
92
93	/-- Two formulas are equivalent on finite structures if they hold of
94	the same tuples in every finite structure whose domain lies in the
95	universe `w`. -/
96	def FinitelyEquivalent {α : Type a} (φ ψ : L.Formula α) : Prop :=
97	∀ (M : Type w) [Finite M] [L.Structure M] (x : α → M), φ.Realize x ↔ ψ.Realize x
98
99	/-- The formula `φ(x₁, …, x_j)` with each `xᵢ` replaced by the term
100	`t i`, as a subformula with `n` bound variables in scope. -/
101	def instantiate {β : Type*} {j n : ℕ} (φ : L.Formula (Fin j))
102	(t : Fin j → L.Term (β ⊕ Fin n)) : L.BoundedFormula β n :=
103	(φ.subst t).relabel id
104
105	/-- The variable term in position `m` of a relation atom in `adj_σ`:
106	positions `0` and `1` are `x₁` and `x₂`, and position `m ≥ 2` is the
107	bound variable `x_{m+1}`. -/
108	def adjSlot {l : ℕ} (m : Fin l) : L.Term (Fin 2 ⊕ Fin (l - 2)) :=
109	if h : m.val < 2 then Term.var (Sum.inl ⟨m.val, h⟩)
110	else Term.var (Sum.inr ⟨m.val - 2, by omega⟩)
111
112	/-- The part of `adj_σ` for one relation symbol `R` of arity `l`:
113	`∃x₃ … ∃x_l ⋁_π R(x_{π(1)}, …, x_{π(l)})` if `l ≥ 2`, and falsum
114	otherwise. -/
115	noncomputable def adjVia {l : ℕ} (R : L.Relations l) : L.Formula (Fin 2) :=
116	if 2 ≤ l then
117	BoundedFormula.exs
118	(BoundedFormula.iSup fun π : Equiv.Perm (Fin l) =>
119	BoundedFormula.rel R fun m => adjSlot (π m))
120	else ⊥
121
122	variable (L) in
123	/-- `adj_σ(x₁, x₂)`: the formula stating that `x₁` and `x₂` are adjacent
124	in the Gaifman graph. -/
125	noncomputable def adjFormula [Finite (Σ l, L.Relations l)] : L.Formula (Fin 2) :=
126	∼((Term.var (Sum.inl 0)).bdEqual (Term.var (Sum.inl 1))) ⊓
127	BoundedFormula.iSup fun R : Σ l, L.Relations l => adjVia R.2
128
129	/-- The vertex `v_i` of the walk quantified in `dist(x₁, x₂) ≤ r`:
130	`v₀ = x₁`, and `v_i` for `i ≥ 1` is the `i`-th bound variable. -/
131	def walkVertex {r : ℕ} (i : Fin (r + 1)) : L.Term (Fin 2 ⊕ Fin r) :=
132	Fin.cases (motive := fun _ => L.Term (Fin 2 ⊕ Fin r))
133	(Term.var (Sum.inl 0)) (fun j => Term.var (Sum.inr j)) i
134
135	variable (L) in
136	/-- `dist(x₁, x₂) ≤ r`: there are `v₁, …, v_r` with `v_r = x₂` such that
137	each step of `x₁ = v₀, v₁, …, v_r` is an equality or an adjacency. -/
138	noncomputable def distFormula [Finite (Σ l, L.Relations l)] (r : ℕ) :
139	L.Formula (Fin 2) :=
140	BoundedFormula.exs
141	(((walkVertex (L := L) (Fin.last r)).bdEqual (Term.var (Sum.inl 1))) ⊓
142	BoundedFormula.iInf fun i : Fin r =>
143	((walkVertex (L := L) i.castSucc).bdEqual (walkVertex i.succ)) ⊔
144	instantiate (adjFormula L) ![walkVertex i.castSucc, walkVertex i.succ])
145
146	variable (L) in
147	/-- The guard `y ∈ Ball_s(x̄)` of a local quantifier, where `x̄` are the
148	`k` free variables and `y` is the newly bound variable: the disjunction
149	over `i` of `dist(xᵢ, y) ≤ s`. -/
150	noncomputable def ballGuard [Finite (Σ l, L.Relations l)] (k s n : ℕ) :
151	L.BoundedFormula (Fin k) (n + 1) :=
152	BoundedFormula.iSup fun i : Fin k =>
153	instantiate (distFormula L s) ![Term.var (Sum.inl i), Term.var (Sum.inr (Fin.last n))]
154
155	/-- `IsLocal r φ`: the formula `φ` with free variables `x̄ = x₁, …, x_k`
156	and `n` further bound variables in scope is `r`-local. It is built from
157	atoms by falsum, implication and quantifiers guarded by `Ball_s(x̄)` for
158	some `s ≤ r`. -/
159	inductive IsLocal [Finite (Σ l, L.Relations l)] (r : ℕ) {k : ℕ} :
160	{n : ℕ} → L.BoundedFormula (Fin k) n → Prop
161	/-- Falsum is local. -/
162	\| falsum {n : ℕ} : IsLocal r (BoundedFormula.falsum : L.BoundedFormula (Fin k) n)
163	/-- Equality atoms are local. -/
164	\| equal {n : ℕ} (t₁ t₂ : L.Term (Fin k ⊕ Fin n)) :
165	IsLocal r (BoundedFormula.equal t₁ t₂)
166	/-- Relation atoms are local. -/
167	\| rel {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (Fin k ⊕ Fin n)) :
168	IsLocal r (BoundedFormula.rel R ts)
169	/-- Implications of local formulas are local. -/
170	\| imp {n : ℕ} {φ ψ : L.BoundedFormula (Fin k) n} :
171	IsLocal r φ → IsLocal r ψ → IsLocal r (φ.imp ψ)
172	/-- `∀y ∈ Ball_s(x̄) φ`, that is `∀y (y ∈ Ball_s(x̄) → φ)`, for `s ≤ r`. -/
173	\| all {n s : ℕ} {φ : L.BoundedFormula (Fin k) (n + 1)} :
174	s ≤ r → IsLocal r φ → IsLocal r (∀' (ballGuard L k s n ⟹ φ))
175	/-- `∃y ∈ Ball_s(x̄) φ`, that is `∃y (y ∈ Ball_s(x̄) ∧ φ)`, for `s ≤ r`. -/
176	\| ex {n s : ℕ} {φ : L.BoundedFormula (Fin k) (n + 1)} :
177	s ≤ r → IsLocal r φ → IsLocal r (∃' (ballGuard L k s n ⊓ φ))
178
179	variable (L) in
180	/-- The sentence `∃x₁, …, x_m (⋀_{i < j} dist(xᵢ, xⱼ) > 2r' ∧ ⋀_i φ(xᵢ))`. -/
181	noncomputable def basicLocalSentence [Finite (Σ l, L.Relations l)] (r' m : ℕ)
182	(φ : L.Formula (Fin 1)) : L.Sentence :=
183	BoundedFormula.exs
184	((BoundedFormula.iInf fun p : {p : Fin m × Fin m // p.1 < p.2} =>
185	∼(instantiate (distFormula L (2 * r'))
186	![Term.var (Sum.inr p.1.1), Term.var (Sum.inr p.1.2)])) ⊓
187	BoundedFormula.iInf fun i : Fin m => instantiate φ ![Term.var (Sum.inr i)])
188
189	/-- `IsBasicLocal r ψ`: the sentence `ψ` is basic `r`-local. -/
190	def IsBasicLocal [Finite (Σ l, L.Relations l)] (r : ℕ) (ψ : L.Sentence) : Prop :=
191	∃ r' ≤ r, ∃ (m : ℕ) (φ : L.Formula (Fin 1)),
192	IsLocal r' φ ∧ ψ = basicLocalSentence L r' m φ
193
194	end Lax185574.LocalFormulas
195

lem✓Lax185574.LocalSubstructure

⊢Lax185574Proofs.LocalSubstructure.realize_iff_realize_induced

thm✓Lax185574.GaifmanLocality

Gaifman's locality theorem with a rank bound

For all α, q, k ∈ ℕ there is a p = p(α, q, k), computable from α, q, k, with the following property. Let σ be a finite relational signature of arity at most α. Every σ-formula φ(x̄) of quantifier rank at most q and with |x̄| ≤ k free variables is equivalent to a σ-formula φ^loc(x̄), computable from φ, that is a Boolean combination of basic 7^q-local sentences and 7^q-local formulas, each of quantifier rank at most p.

This is Gaifman's locality theorem. Gaifman's paper does not state the bound p explicitly. An analysis of its proof shows that p depends only on α, q and k, and not on the signature σ, as the rank-preserving locality theorems of Dreier and Toruńczyk and of van Bergerem, Grohe and Schweikardt make explicit for their variants of local formulas. The dependence of p on α comes from expressing the distance predicates in plain first-order logic.

1	import Lax185574.FirstOrderTypes
2	import Lax185574.LocalFormulas
3
	… module docstring, 39 lines
43
44	namespace Lax185574.GaifmanLocality
45
46	open FirstOrder FirstOrder.Language
47	open Lax185574.FirstOrderTypes Lax185574.LocalFormulas
48
49	universe u v w z
50
51	variable {L : Language.{u, v}}
52
53	/-- `IsBooleanCombination P φ`: the formula `φ` is a Boolean combination
54	of formulas satisfying `P`, built by falsum and implication. -/
55	inductive IsBooleanCombination {α : Type w} (P : L.Formula α → Prop) :
56	L.Formula α → Prop
57	/-- A constituent is a Boolean combination. -/
58	\| atom {φ : L.Formula α} : P φ → IsBooleanCombination P φ
59	/-- Falsum is a Boolean combination. -/
60	\| falsum : IsBooleanCombination P ⊥
61	/-- Implications of Boolean combinations are Boolean combinations. -/
62	\| imp {φ ψ : L.Formula α} :
63	IsBooleanCombination P φ → IsBooleanCombination P ψ →
64	IsBooleanCombination P (φ.imp ψ)
65
66	/-- The constituents of a Gaifman normal form with radius `h` and rank
67	bound `p`: `h`-local formulas and basic `h`-local sentences, each of
68	quantifier rank at most `p`. -/
69	def IsLocalConstituent [Finite (Σ l, L.Relations l)] (h p : ℕ) {n : ℕ}
70	(χ : L.Formula (Fin n)) : Prop :=
71	(IsLocal h χ ∧ quantifierRank χ ≤ p) ∨
72	∃ ψ : L.Sentence, IsBasicLocal h ψ ∧ quantifierRank ψ ≤ p ∧
73	χ = ψ.relabel Empty.elim
74
75	/-- Gaifman's locality theorem. For all `α, q, k` there is a rank
76	bound `p` such that every formula of quantifier rank at most `q` with at
77	most `k` free variables, over a finite relational signature of arity at
78	most `α`, is equivalent to a Boolean combination of `7^q`-local formulas
79	and basic `7^q`-local sentences of quantifier rank at most `p`. -/
80	axiom exists_local_equivalent (α q k : ℕ) :
81	∃ p : ℕ, ∀ (L : Language.{u, v}) [L.IsRelational] [Finite (Σ l, L.Relations l)],
82	(∀ l, α < l → IsEmpty (L.Relations l)) →
83	∀ (n : ℕ), n ≤ k → ∀ φ : L.Formula (Fin n), quantifierRank φ ≤ q →
84	∃ ψ : L.Formula (Fin n), FinitelyEquivalent.{u, v, z, 0} φ ψ ∧
85	IsBooleanCombination (IsLocalConstituent (7 ^ q) p) ψ
86
87	end Lax185574.GaifmanLocality
88

lem✓Lax185574.SeparatingTypes

lem✓Lax185574.VCDuality

⊢Lax185574Proofs.BallFlip.exists_ball_flip
- lem✓Lax185574.VCDuality
→
lem✓Lax185574.BallFlip
The proof in the paper. Group $A$ by neighborhoods in the ball $B$ and $B$ by neighborhoods in $A$ . The parameter set consists of representatives of all groups and of a bounded-VC duality sample for every pair of groups of $A$ and for every group of $B$ against the inner ball. The $S$ -flip toggles exactly the pairs of atomic types joined by an edge of $G$ between $A$ and $B$ . Then $A$ and $B$ are non-adjacent in the flip, the inner ball is unchanged, and it has no edges to the outside of $B$ , so the ball of radius $r + 1$ still avoids $A$ . The duality is used in a form without exception for the sample, obtained from the concept at the cost of doubling the sample.

defLax185574.AtomicMatching

thm✓Lax185574.MatchedTuples

⊢Lax185574Proofs.MatchedTuples.exists_atomicallyMatched

defLax185574.PhiPsiPatterns

(φ, ψ)-patterns

Fix first-order formulas φ(x̄, z) and ψ(ȳ, z). A (φ, ψ)-pattern of order s × t in a graph G consists of tuples ā₁, …, ā_s ∈ V(G)^{|x̄|}, b̄₁, …, b̄t ∈ V(G)^{|ȳ|}, and vertices (c{i,j} : i ∈ [s], j ∈ [t]) such that the following holds for all i, i' ∈ [s] and j, j' ∈ [t]:

G ⊨ φ(āᵢ, c_{i,j}), and G ⊭ φ(ā_{i'}, c_{i,j}) if i' > i,
G ⊨ ψ(b̄ⱼ, c_{i,j}), and G ⊭ ψ(b̄_{j'}, c_{i,j}) if j' > j.

The set { c_{i,j} : i ∈ [s], j ∈ [t] } is the set of grid-points of the pattern, and s is its height.

1	import Mathlib.ModelTheory.Graph
2	import Mathlib.ModelTheory.Semantics
3
	… module docstring, 26 lines
30
31	namespace Lax185574.PhiPsiPatterns
32
33	open FirstOrder FirstOrder.Language
34
35	universe u
36
37	variable {V : Type u}
38
39	/-- `G ⊨ φ(ā, c)` for a formula `φ(x̄, z)` of the language of graphs. -/
40	def Holds (G : SimpleGraph V) {p : ℕ}
41	(φ : Language.graph.Formula (Fin p ⊕ Fin 1)) (a : Fin p → V) (c : V) :
42	Prop :=
43	@Formula.Realize Language.graph V G.structure _ φ (Sum.elim a ![c])
44
45	/-- The tuples `a i`, `b j` and the vertices `c i j` form a
46	`(φ, ψ)`-pattern of order `s × t` in `G`. -/
47	def IsPattern (G : SimpleGraph V) {p p' : ℕ}
48	(φ : Language.graph.Formula (Fin p ⊕ Fin 1))
49	(ψ : Language.graph.Formula (Fin p' ⊕ Fin 1)) {s t : ℕ}
50	(a : Fin s → Fin p → V) (b : Fin t → Fin p' → V) (c : Fin s → Fin t → V) :
51	Prop :=
52	∀ i j,
53	(Holds G φ (a i) (c i j) ∧ ∀ i', i < i' → ¬ Holds G φ (a i') (c i j)) ∧
54	(Holds G ψ (b j) (c i j) ∧ ∀ j', j < j' → ¬ Holds G ψ (b j') (c i j))
55
56	/-- `G` contains a `(φ, ψ)`-pattern of order `s × t`. -/
57	def HasPattern (G : SimpleGraph V) {p p' : ℕ}
58	(φ : Language.graph.Formula (Fin p ⊕ Fin 1))
59	(ψ : Language.graph.Formula (Fin p' ⊕ Fin 1)) (s t : ℕ) : Prop :=
60	∃ (a : Fin s → Fin p → V) (b : Fin t → Fin p' → V) (c : Fin s → Fin t → V),
61	IsPattern G φ ψ a b c
62
63	end Lax185574.PhiPsiPatterns
64

lem✓Lax185574.ForbiddenPhiPsiPatterns

defLax185574.PhiPatterns

cor✓Lax185574.ForbiddenPhiPatterns

obs✓Lax185574.FlipMetricMonotone

lem✓Lax185574.PartitionMetricConversion

thm✓Lax185574.ClosureTheorem

thm✓Lax185574.ClosureTheoremTuples

defLax185574.DefinableFlips

defLax185574.AtomicTypes

Atomic types of vertices and of pairs

The atomic type of a tuple v̄ over a set Y of elements of a structure A is atp^A(v̄/Y) ≔ tp^A_0(v̄/Y), and ATypes^A(X/Y) ≔ Types^A_{1,0}(X/Y) is the set of atomic types over Y of the elements of X.

For a graph, Π = {(x = y), (x ≠ y) ∧ E(x, y), (x ≠ y) ∧ ¬E(x, y)} is the set of the three possible atomic types of a pair of vertices. For an s-tuple p̄ = (p₁, …, p_s) of vertices and a vertex v, the atomic type atp(v/p̄) is identified with the s-tuple in Π^s whose i-th component is the atomic type of the pair (v, pᵢ).

1	import Lax185574.FirstOrderTypes
2	import Mathlib.ModelTheory.Graph
3
	… module docstring, 27 lines
31
32	namespace Lax185574.AtomicTypes
33
34	open FirstOrder FirstOrder.Language
35	open Lax185574.FirstOrderTypes
36
37	universe u
38
39	variable {V : Type u}
40
41	/-- `\|ATypes^G(X/Y)\|`: the number of atomic types over `Y`, in the graph
42	`G`, of the vertices of `X`. -/
43	noncomputable def atomicTypeCount (G : SimpleGraph V) (X Y : Set V) : ℕ :=
44	@typeCountOver Language.graph V G.structure 1 0 X Y
45
46	/-- The three atomic types of a pair of vertices in a graph, the set Π. -/
47	inductive PairType
48	/-- The type `x = y`. -/
49	\| eq
50	/-- The type `x ≠ y ∧ E(x, y)`. -/
51	\| adj
52	/-- The type `x ≠ y ∧ ¬E(x, y)`. -/
53	\| nonAdj
54	deriving DecidableEq
55
56	/-- There are three atomic types of pairs. -/
57	instance : Fintype PairType :=
58	⟨{.eq, .adj, .nonAdj}, fun x => by cases x <;> decide⟩
59
60	open Classical in
61	/-- The atomic type of the pair `(u, v)` in the graph `G`. -/
62	noncomputable def pairType (G : SimpleGraph V) (u v : V) : PairType :=
63	if u = v then .eq else if G.Adj u v then .adj else .nonAdj
64
65	/-- `atp(v/p̄)`, as an element of `Π^s`: its `i`-th component is the
66	atomic type of the pair `(v, pᵢ)`. -/
67	noncomputable def atomicTypeOver (G : SimpleGraph V) {s : ℕ} (p : Fin s → V)
68	(v : V) : Fin s → PairType :=
69	fun i => pairType G v (p i)
70
71	end Lax185574.AtomicTypes
72

obs✓Lax185574.DefinableFlipFormula

⊢Lax185574Proofs.DefinableFlipFormula.exists_isQF_flipOver_formula

obs✓Lax185574.FlipsMonadicallyDependent

fac✓Lax185574.DefinableFlipTransitivity

lem✓Lax185574.BallTypes

lem✓Lax185574.BallFlip

⊢Lax185574Proofs.ClosureTheorem.closure_theorem
- lem✓Lax185574.BallFlip
- lem✓Lax185574.BallTypes
- fac✓Lax185574.DefinableFlipTransitivity
- obs✓Lax185574.FlipsMonadicallyDependent
- thm✓Lax185574.IndependenceProperty
- lem✓Lax185574.NeighborhoodComplexityBound
→
thm✓Lax185574.ClosureTheorem
Induction on $r$ , as in the paper. At radius 0 take $A* = A$ and no flip. For the step, enlarge $A$ to $A₁$ by the ball-types lemma for the current parameter bound $s$ , and apply the induction hypothesis to $A₁$ , giving $B$ . The $s$ -definable flips of graphs of the class form a monadically dependent class, so they have VC-dimension at most some $d$ . For every set $S ⊆ B$ of at most $s$ vertices and every $S$ -flip $H$ (at most $2^{9^s}$ of them), group the vertices whose radius- $r$ ball in $H$ avoids $A₁$ by the set of atomic types over $A$ that the ball meets. By the ball-types lemma these profiles have at most $t$ members, and by the Sauer–Shelah lemma there are at most $|A| + (|A| + 1)^d$ atomic types over $A$ , so there are polynomially many groups. The ball flip lemma gives a $z$ -definable flip of $H$ that $(r + 1)$ -separates each group from $A$ , which is an $(s + z)$ -definable flip of $G$ by transitivity. The new closure is $A₁$ together with the parameters of all these flips. Vertices of $A₁ ∖ A$ are isolated by the flip over themselves.

The argument is carried out for the graph classes of the archive and their monadic dependence, and transferred to the graph classes used here.

defLax185574.Chains

⊢Lax185574Proofs.ComputingChains.exists_program_chain
- thm✓Lax185574.ChainTheorem
→
thm✓Lax185574.ComputingChains
The statement for graphs, graph classes and $Algorithm.Computes$ , from the version for simple graphs applied to the class of the simple graphs of the members. The algorithm is the program with its exponent, the chain of a graph is that of its simple graph, and the constant $c$ becomes $⌈c · 2^(3+δ)⌉$ , so that $c' · n^(3+δ) + c'$ bounds the time $⌊c · (n+1)^(3+δ)⌋$ .

thm✓Lax185574.ComputingChains

lem✓Lax185574.ChainConstructionSequences

⊢Lax185574Proofs.DefinableSequences.exists_program_definableSequence
- obs✓Lax185574.BoundedVCClasses
- lem✓Lax185574.ChainConstructionSequences
- thm✓Lax185574.ComputingChains
- lem✓Lax185574.NeighborhoodComplexityBound
→
thm✓Lax185574.DefinableSequences
The proof of the theorem on definable construction sequences. Compute a chain at radius $5r + 1$ and accuracy $ε$ (the chain theorem), of length $m ≤ O(r/ε)$ , and turn it into a construction sequence (the lemma turning chains into construction sequences). With $k_r ≤ c (n+1)^ε$ the radius- $(5r+1)$ width of the chain, $d$ a bound on the VC-dimension of the graphs of the class (the observation on bounded VC-dimension) and $π_G(k) ≤ (k+1)^d$ (the Sauer–Shelah lemma), $w_r ≤ (k_r + 1)^(d+1)$ , so $a₀ = d + 1$ . The length is $O(n w₁) ≤ O(n w_r)$ , as the width of a chain grows with the radius. The number of predicates is $2m + 1 ≤ ⌈A r/ε⌉ + A$ . On the word RAM, a first phase converts the compressed sparse row form of the graph into the word of the graph that the two cited programs read.

The proof is carried out for the input format with the graph in compressed sparse row form and the notion $Lax185574.Computing.Computes$ . The algorithm converts the word of the graph into compressed sparse rows ( $Interface.nbr_bridge$ ) and runs that program. The script of a graph is the one whose encoding the program outputs on the converted input.

defLax185574.MergeSequences

Merge sequences and their radius-r width

A merge sequence of a graph G is a sequence (𝒫₁, R₁), …, (𝒫_m, R_m) such that:

𝒫₁ is the partition into singletons and 𝒫_m = {V(G)},
𝒫₁ ≼ ⋯ ≼ 𝒫_m,
R₁ ⊆ ⋯ ⊆ R_m ⊆ (V(G) choose 2), and
for every i ∈ [m] and X, Y ∈ 𝒫_i, the set XY ∖ R_i is contained either in E(G) or in E(Ḡ), that is, the pair X, Y is homogeneous once pairs in R_i are ignored.

Here XY is the set of pairs xy with x ∈ X, y ∈ Y and x ≠ y. Condition 4 says that 𝒫_i is homogeneous modulo R_i. The radius-r width of the merge sequence is

max_{2 ≤ i ≤ m} max_{v ∈ V(G)} |Ball^{R_i}r(v)/𝒫{i−1}|.

The offset in the indices of R_i and 𝒫_{i−1} is intentional.

1	import Lax185574.Partitions
2	import Lax185574.GraphBalls
3	import Mathlib.Order.Lattice.Nat
4
	… module docstring, 40 lines
45
46	namespace Lax185574.MergeSequences
47
48	open Lax185574.Partitions Lax185574.GraphBalls
49
50	universe z
51
52	variable {V : Type z}
53
54	/-- `P` is homogeneous modulo `R`: for every pair of parts `𝒫(a)`,
55	`𝒫(b)`, the pairs of distinct vertices between them that are not in
56	`R` are all edges of `G`, or all non-edges of `G`. -/
57	def HomogeneousModulo (G : SimpleGraph V) (P : Setoid V) (R : SimpleGraph V) : Prop :=
58	∀ a b : V,
59	(∀ x y : V, P x a → P y b → x ≠ y → ¬ R.Adj x y → G.Adj x y) ∨
60	(∀ x y : V, P x a → P y b → x ≠ y → ¬ R.Adj x y → ¬ G.Adj x y)
61
62	/-- `ms` is a merge sequence of `G`: it starts with the partition into
63	singletons and ends with the partition with one part, the partitions
64	get coarser and the relations grow, and every partition is homogeneous
65	modulo its relation. -/
66	def IsMergeSequence (G : SimpleGraph V) (ms : List (Setoid V × SimpleGraph V)) : Prop :=
67	∃ h : ms ≠ [],
68	(ms.head h).1 = ⊥ ∧ (ms.getLast h).1 = ⊤ ∧
69	(∀ (t : ℕ) (ht : t + 1 < ms.length), ms[t].1 ≤ ms[t + 1].1 ∧ ms[t].2 ≤ ms[t + 1].2) ∧
70	∀ (t : ℕ) (ht : t < ms.length), HomogeneousModulo G ms[t].1 ms[t].2
71
72	/-- The radius-`r` width of the merge sequence `ms`: the largest number
73	of parts of `𝒫_t` that meet a ball of radius `r` in `R_{t+1}`. -/
74	noncomputable def mergeWidth (r : ℕ) (ms : List (Setoid V × SimpleGraph V)) : ℕ :=
75	sSup {K \| ∃ (t : ℕ) (ht : t + 1 < ms.length) (v : V),
76	K = partCount ms[t].1 (graphBall ms[t + 1].2 r {v})}
77
78	end Lax185574.MergeSequences
79

lem✓Lax185574.BetterMergeSequences

lem✓Lax185574.ComplementDiameter

⊢Lax185574Proofs.ComplementDiameter.diameter_le_three_or_compl

defLax185574.BipartiteGraphs

lem✓Lax185574.BipartiteFlip

⊢Lax185574Proofs.BipartiteFlip.exists_flip_close

defLax185574.TypeSplitting

lem✓Lax185574.SplitBalls

⊢Lax185574Proofs.SplitBalls.partCount_split_le

defLax185574.BipartiteGraphs

defLax185574.PairRelation

lem✓Lax185574.PairRelationDefinable

⊢Lax185574Proofs.PairRelationDefinable.exists_formula_pairRelation

lem✓Lax185574.PairRelationMonotone

⊢Lax185574Proofs.PairRelationMonotone.pairRelation_mono

lem✓Lax185574.PairRelationBalls

⊢Lax185574Proofs.PairRelationBalls.graphBall_pairRelation_subset

lem✓Lax185574.HomogeneousSplitting

lem✓Lax185574.SplittingMonotone

⊢Lax185574Proofs.SplittingMonotone.split_minimalVertices_mono

lem✓Lax185574.MergeToConstruction

thm✓Lax185574.ModelChecking

thm✓Lax185574.TypeBound

defLax185574.Width

thm✓Lax185574.FewTypes

Construction sequences with few realized types

Let 𝒞 be a monadically dependent graph class, r, q ∈ ℕ, and let ε > 0 be a rational. There is a constant α ≥ 1 depending only on 𝒞 and q such that every graph G ∈ 𝒞 has a construction sequence of radius-r depth-q width O_{𝒞,r,q,ε}(n^{αε}) and length O_{𝒞,r,q,ε}(n^{1+αε}). Moreover, there is an algorithm (independent of 𝒞) which, given r, q ∈ ℕ, a rational ε > 0 and an n-vertex graph G ∈ 𝒞, computes such a construction sequence in time Ô_{𝒞,r,q,ε}(n³). Here Ô_k(n³) stands for a bound O_{k,η}(n^{3+η}) for every η > 0.

It is important that α does not depend on ε, as this makes the exponent αε of the width as small as one likes.

1	import Lax185574.Width
2	import Lax185574.ConstructionSequences
3	import Lax185574.MonadicDependence
4	import Lax185574.Algorithms
5	import Mathlib.Analysis.SpecialFunctions.Pow.Real
6
	… module docstring, 37 lines
44
45	namespace Lax185574.FewTypes
46
47	open Lax185574.Graphs Lax185574.MonadicDependence Lax185574.Algorithms
48	open Lax185574.ConstructionSequences Lax185574.Width
49
50	/-- Construction sequences with few realized types. One algorithm
51	computes, from `r`, `q`, a rational `ε > 0` and a graph `G`, a
52	construction sequence of `G`, given by its script. On members of a
53	monadically dependent class it takes time `O(n^(3+η))` for every
54	`η > 0`, and the sequence has length at most `c · (n+1)^(1+aε)` and
55	radius-`r` depth-`q` width at most `c · (n+1)^(aε)`. Here `a ≥ 1`
56	depends only on the class and `q`, and `c` on the class, `r`, `q`, `ε`
57	and `η`. -/
58	axiom exists_program_fewTypes :
59	∃ (A : Algorithm) (script : ℕ → ℕ → ℚ → (G : Graph) → Script G.n),
60	(∀ (r q : ℕ) (ε : ℚ) (G : Graph), 0 < ε →
61	IsConstructionSequence G.toSimpleGraph (script r q ε G).run ∧
62	(script r q ε G).HasSmallNumbers) ∧
63	∀ C : GraphClass, MonadicallyDependent C → ∀ q : ℕ, ∃ a : ℕ, 1 ≤ a ∧
64	∀ (r : ℕ) (ε : ℚ), 0 < ε → ∀ η : ℝ, 0 < η → ∃ c : ℕ,
65	∀ G ∈ C,
66	A.Computes c (r, q, ε, G) (script r q ε G) ((G.n : ℝ) ^ (3 + η)) ∧
67	((script r q ε G).run.length : ℝ) ≤ c * ((G.n : ℝ) + 1) ^ (1 + (a : ℝ) * ε) ∧
68	(width r q (script r q ε G).run : ℝ) ≤ c * ((G.n : ℝ) + 1) ^ ((a : ℝ) * ε)
69
70	end Lax185574.FewTypes
71

thm✓Lax185574.ConstructionModelChecking

⊢Lax185574Proofs.ModelChecking.exists_program_modelChecking
- thm✓Lax185574.ConstructionModelChecking
- thm✓Lax185574.FewTypes
→
thm✓Lax185574.ModelChecking
The proof of the main theorem. The algorithm converts the word of the graph into its compressed sparse row form and runs the program of $exists_program_modelChecking_csr$ on it. The conversion takes time linear in the length of the input, which is $O(n²)$ .

thm✓Lax185574.TypeBound

defLax185574.LocalDefinability

Locally definable construction sequences

Let A be a structure and H a partial graph with V(H) ⊆ V(A). Then H is definable in A by formulas of quantifier rank q₀ with parameters from a set S ⊆ V(A) if for every relation R of H of arity k there is a formula φ_R(x₁, …, x_k) of quantifier rank at most q₀ with parameters from S such that, for all v̄ ∈ V(A)^k,

A ⊨ φ_R(v̄) ⟺ v̄ ∈ V(H)^k and H ⊨ R(v̄).

Let G be a graph and r, c, s, q₀ ∈ ℕ. A construction sequence G₁, …, G_λ of G is radius-r definable with c unary predicates, s parameters and quantifier rank q₀ if, for all t ∈ [λ−1] and v ∈ V(G), the induced partial graph G_t[Ball^{G_{t+1}}_r(v)] is definable in some expansion of G by c unary predicates, by formulas of quantifier rank q₀ with parameters from a set of at most s vertices. The expansion and the parameters may depend on t and v.

1	import Lax185574.ConstructionSequences
2	import Lax185574.Colorings
3	import Lax185574.FirstOrderTypes
4
	… module docstring, 32 lines
37
38	namespace Lax185574.LocalDefinability
39
40	open FirstOrder FirstOrder.Language
41	open Lax185574.PartialGraphs Lax185574.FirstOrderTypes Lax185574.Colorings
42	open Lax710763.Transductions
43
44	universe u v z
45
46	variable {V : Type z}
47
48	/-- The induced partial graph `H[B]` is definable in the structure on
49	`V` by formulas of quantifier rank at most `q₀` with parameters from
50	`S`. -/
51	def DefinableIn {L : Language.{u, v}} [L.Structure V] (q₀ : ℕ) (S : Set V)
52	(H : PartialGraph V) (B : Set V) : Prop :=
53	∀ {k : ℕ} (R : PartialGraphs.language.Relations k),
54	∃ φ : L.Formula (Fin k ⊕ S), quantifierRank φ ≤ q₀ ∧
55	∀ x : Fin k → V,
56	φ.Realize (Sum.elim x Subtype.val) ↔
57	(∀ i, x i ∈ B) ∧ @Structure.RelMap _ V H.structure k R x
58
59	/-- The sequence `s` is radius-`r` definable in the graph `G` with `c`
60	unary predicates, `s'` parameters and quantifier rank `q₀`: for every
61	step `t` and vertex `v`, the induced partial graph
62	`s[t][Ball^{s[t+1]}_r(v)]` is definable in some expansion of `G` by `c`
63	unary predicates, by formulas of quantifier rank at most `q₀` with at
64	most `s'` parameters. -/
65	def IsRadiusDefinable (G : SimpleGraph V) (s : List (PartialGraph V))
66	(r c s' q₀ : ℕ) : Prop :=
67	∀ (t : ℕ) (ht : t + 1 < s.length) (v : V),
68	∃ (colors : Fin c → Set V) (S : Finset V), S.card ≤ s' ∧
69	@DefinableIn V (withColors Language.graph c) (expansion G colors) q₀ S
70	s[t] (s[t + 1].ball r v)
71
72	end Lax185574.LocalDefinability
73

thm✓Lax185574.DefinableSequences

Computing locally definable construction sequences

Let r ≥ 1 be an integer, ε > 0 a rational, and 𝒞 a monadically dependent graph class. There is a constant δ ≥ 1 depending only on 𝒞 such that every n-vertex graph G ∈ 𝒞 has a construction sequence of G which is radius-r definable with O(r/ε) unary predicates, O_{𝒞,r,ε}(n^{δε}) parameters and quantifier rank 7, and has length O_{𝒞,r,ε}(n^{1+δε}). Moreover, there is an algorithm (independent of 𝒞) which, given r, ε and G, computes such a sequence, and runs in time Ô_{𝒞,r,ε}(n³) whenever G ∈ 𝒞. Here Ô_k(n³) stands for a bound O_{k,η}(n^{3+η}) for every η > 0.

1	import Lax185574.LocalDefinability
2	import Lax185574.ConstructionSequences
3	import Lax185574.MonadicDependence
4	import Lax185574.Algorithms
5	import Mathlib.Analysis.SpecialFunctions.Pow.Real
6
	… module docstring, 46 lines
53
54	namespace Lax185574.DefinableSequences
55
56	open Lax185574.Graphs Lax185574.MonadicDependence Lax185574.Algorithms
57	open Lax185574.ConstructionSequences Lax185574.LocalDefinability
58
59	/-- Locally definable construction sequences. One algorithm
60	computes, from `r ≥ 1`, a rational `ε > 0` and a graph `G`, a
61	construction sequence of `G`, given by its script. On members of a
62	monadically dependent class it takes time `O(n^(3+η))` for every
63	`η > 0`, and the sequence has length at most `c · (n+1)^(1+aε)` and is
64	radius-`r` definable with `⌈K·r/ε⌉ + K` unary predicates,
65	`⌊c · (n+1)^(aε)⌋` parameters and quantifier rank `7`. Here `a ≥ 1`
66	depends only on the class, and `c` on the class, `r`, `ε` and `η`. -/
67	axiom exists_program_definableSequence :
68	∃ (A : Algorithm) (K : ℕ) (script : ℕ → ℚ → (G : Graph) → Script G.n),
69	(∀ (r : ℕ) (ε : ℚ) (G : Graph), 1 ≤ r → 0 < ε →
70	IsConstructionSequence G.toSimpleGraph (script r ε G).run ∧
71	(script r ε G).HasSmallNumbers) ∧
72	∀ C : GraphClass, MonadicallyDependent C → ∃ a : ℕ, 1 ≤ a ∧
73	∀ (r : ℕ) (ε : ℚ), 1 ≤ r → 0 < ε → ∀ η : ℝ, 0 < η → ∃ c : ℕ,
74	∀ G ∈ C,
75	A.Computes c (r, ε, G) (script r ε G) ((G.n : ℝ) ^ (3 + η)) ∧
76	((script r ε G).run.length : ℝ) ≤ c * ((G.n : ℝ) + 1) ^ (1 + (a : ℝ) * ε) ∧
77	IsRadiusDefinable G.toSimpleGraph (script r ε G).run r (⌈(K : ℚ) * r / ε⌉₊ + K)
78	⌊(c : ℝ) * ((G.n : ℝ) + 1) ^ ((a : ℝ) * ε)⌋₊ 7
79
80	end Lax185574.DefinableSequences
81

thm✓Lax185574.LocalToGlobal

thm✓Lax185574.DefinableToTypes

defLax185574.PartialGraphs

Partial graphs

A partial graph H consists of a finite vertex set V = V(H), two disjoint sets E(H), N(H) ⊆ (V choose 2) of edges and non-edges, and a partition of V whose parts are treated as colors. The pairs in R(H) = E(H) ∪ N(H) are resolved, and all other pairs are unresolved. H is viewed as a logical structure with binary relations E and N and a unary predicate for every color. Distances dist^H and balls Ball^H_r(v) are measured in the Gaifman graph (V, R(H)), the graph of resolved pairs.

For the model-checking algorithm, the parts are given names, to track them over time. Fix a countably infinite set of unary symbols, called colors. A partial graph G is regarded as a relational structure with the two symmetric binary relations E and N and a unary relation Y for every color Y. The vertices of color Y form its color class Y^G, and the nonempty color classes are the parts of G. The size of the representation of G is given by |G| = |V(G)| and ‖G‖ = |V(G)| + |R(G)|.

1	import Lax185574.GaifmanGraph
2	import Lax185574.Encodings
3	import Mathlib.Combinatorics.SimpleGraph.Basic
4	import Mathlib.Data.Set.Card
5
	… module docstring, 54 lines
60
61	namespace Lax185574.PartialGraphs
62
63	open FirstOrder FirstOrder.Language
64	open Lax185574.GaifmanGraph
65
66	universe z
67
68	/-- A partial graph on the vertex type `V`: disjoint edges and
69	non-edges, and one color per vertex. -/
70	structure PartialGraph (V : Type z) where
71	/-- The edges `E(G)`. -/
72	edge : SimpleGraph V
73	/-- The non-edges `N(G)`. -/
74	nonEdge : SimpleGraph V
75	/-- No pair is both an edge and a non-edge. -/
76	disjoint : Disjoint edge nonEdge
77	/-- The color of each vertex. -/
78	color : V → ℕ
79
80	variable {V : Type z}
81
82	namespace PartialGraph
83
84	/-- The resolved pairs `R(G) = E(G) ∪ N(G)`, the Gaifman graph of the
85	partial graph. -/
86	def resolved (G : PartialGraph V) : SimpleGraph V := G.edge ⊔ G.nonEdge
87
88	/-- `Ball^G_r(v)`: the vertices within distance `r` of `v` along
89	resolved pairs. -/
90	def ball (G : PartialGraph V) (r : ℕ) (v : V) : Set V :=
91	{u \| WithinDist G.resolved r v u}
92
93	/-- The color class `Y^G`. -/
94	def colorClass (G : PartialGraph V) (Y : ℕ) : Set V := {v \| G.color v = Y}
95
96	/-- The size `‖G‖ = \|V(G)\| + \|R(G)\|` of a partial graph on `Fin n`. -/
97	noncomputable def size {n : ℕ} (G : PartialGraph (Fin n)) : ℕ :=
98	n + Set.ncard G.resolved.edgeSet
99
100	end PartialGraph
101
102	/-- The relation symbols of partial graphs: edges, non-edges and one
103	unary symbol per color. -/
104	inductive Rel : ℕ → Type
105	\| edge : Rel 2
106	\| nonEdge : Rel 2
107	\| color (Y : ℕ) : Rel 1
108
109	/-- The language of partial graphs. -/
110	def language : Language :=
111	⟨fun _ => Empty, Rel⟩
112	deriving Language.IsRelational
113
114	/-- A partial graph as a relational structure. -/
115	@[implicit_reducible]
116	def PartialGraph.structure (G : PartialGraph V) : language.Structure V where
117	funMap f := isEmptyElim f
118	RelMap
119	\| .edge => fun x => G.edge.Adj (x 0) (x 1)
120	\| .nonEdge => fun x => G.nonEdge.Adj (x 0) (x 1)
121	\| .color Y => fun x => G.color (x 0) = Y
122
123	open Lax185574.Encoding in
124	/-- A partial graph on `Fin n` is encoded by the family of its colors,
125	then its edges and then its non-edges, each graph as in
126	`Lax185574.Encodings`. So the encoding is `n` and the `n` colors, then
127	`n` and for every vertex in order the set of its neighbors along edges,
128	then `n` and for every vertex the set of its neighbors along non-edges.
129	It is determined by the partial graph and has length O(‖G‖). Running
130	times are stated in terms of ‖G‖, which is only meaningful for an
131	encoding without padding. The edges and non-edges are relations, so the
132	encoding is not derived. -/
133	noncomputable instance {n : ℕ} : Encode (PartialGraph (Fin n)) where
134	encode G := encode (G.color, G.edge, G.nonEdge)
135
136	end Lax185574.PartialGraphs
137

defLax185574.DistanceMatrix

defLax185574.ConstructionSequences

Construction sequences

For colors P, Q and a partial graph G, the partial graphs merge_{P,Q}(G) (for P ≠ Q), resolve⁺{P,Q}(G) and resolve⁻{P,Q}(G) are obtained from G by leaving everything unchanged, apart from the following:

merge_{P,Q}(G): P^H = P^G ∪ Q^G and Q^H = ∅, for P ≠ Q;
resolve⁺_{P,Q}(G): E(H) = E(G) ∪ (P^G Q^G ∖ N(G));
resolve⁻_{P,Q}(G): N(H) = N(G) ∪ (P^G Q^G ∖ E(G)).

Here P^G Q^G is the set of pairs xy of distinct vertices with x ∈ P^G and y ∈ Q^G. After either resolve, every pair in P^G Q^G is resolved.

An initial partial graph has no resolved pairs, and every part is a singleton. A construction sequence of a graph G = (V, E) is a sequence G₁, …, G_λ of partial graphs with vertex set V such that G₁ is initial, every step is one merge or one resolve, and G_λ has a single part, E(G_λ) = E and N(G_λ) = (V choose 2) ∖ E.

1	import Lax185574.PartialGraphs
2
	… module docstring, 52 lines
55
56	namespace Lax185574.ConstructionSequences
57
58	open Lax185574.PartialGraphs
59
60	universe z
61
62	variable {V : Type z}
63
64	/-- The pairs `P^G Q^G`: distinct vertices, one of color `P` and the
65	other of color `Q`. -/
66	def between (G : PartialGraph V) (P Q : ℕ) : SimpleGraph V :=
67	SimpleGraph.fromRel fun x y => G.color x = P ∧ G.color y = Q
68
69	/-- `merge_{P,Q}(G)`: the vertices of color `Q` get color `P`. -/
70	def merge (G : PartialGraph V) (P Q : ℕ) : PartialGraph V :=
71	{ G with color := fun v => if G.color v = Q then P else G.color v }
72
73	/-- `resolve⁺_{P,Q}(G)`: the unresolved pairs in `P^G Q^G` become
74	edges. -/
75	def resolvePos (G : PartialGraph V) (P Q : ℕ) : PartialGraph V where
76	edge := G.edge ⊔ (between G P Q \ G.nonEdge)
77	nonEdge := G.nonEdge
78	disjoint := disjoint_sup_left.2 ⟨G.disjoint, disjoint_sdiff_self_left⟩
79	color := G.color
80
81	/-- `resolve⁻_{P,Q}(G)`: the unresolved pairs in `P^G Q^G` become
82	non-edges. -/
83	def resolveNeg (G : PartialGraph V) (P Q : ℕ) : PartialGraph V where
84	edge := G.edge
85	nonEdge := G.nonEdge ⊔ (between G P Q \ G.edge)
86	disjoint := disjoint_sup_right.2 ⟨G.disjoint, disjoint_sdiff_self_right⟩
87	color := G.color
88
89	/-- An initial partial graph: no resolved pairs, and every part is a
90	singleton. -/
91	def IsInitial (G : PartialGraph V) : Prop :=
92	G.edge = ⊥ ∧ G.nonEdge = ⊥ ∧ Function.Injective G.color
93
94	/-- `H` is obtained from `G` by one merge or one resolve. -/
95	def IsStep (G H : PartialGraph V) : Prop :=
96	∃ P Q : ℕ, (P ≠ Q ∧ H = merge G P Q) ∨ H = resolvePos G P Q ∨
97	H = resolveNeg G P Q
98
99	/-- `s` is a construction sequence of the graph `G`: it starts with an
100	initial partial graph, each entry is obtained from the previous one by
101	one merge or one resolve, and the last entry has a single part, the
102	edges of `G` as edges and the non-edges of `G` as non-edges. -/
103	def IsConstructionSequence (G : SimpleGraph V) (s : List (PartialGraph V)) :
104	Prop :=
105	∃ h : s ≠ [],
106	IsInitial (s.head h) ∧
107	(∀ (t : ℕ) (ht : t + 1 < s.length), IsStep s[t] s[t + 1]) ∧
108	(∀ u v : V, (s.getLast h).color u = (s.getLast h).color v) ∧
109	(s.getLast h).edge = G ∧ (s.getLast h).nonEdge = Gᶜ
110
111	open Lax185574.Encoding
112
113	/-- One step of a construction sequence. -/
114	inductive Step
115	/-- `merge_{P,Q}`. -/
116	\| merge (P Q : ℕ)
117	/-- `resolve⁺_{P,Q}`. -/
118	\| resolvePos (P Q : ℕ)
119	/-- `resolve⁻_{P,Q}`. -/
120	\| resolveNeg (P Q : ℕ)
121	deriving Encode
122
123	/-- The partial graph obtained by applying a step. -/
124	def apply (G : PartialGraph V) : Step → PartialGraph V
125	\| .merge P Q => merge G P Q
126	\| .resolvePos P Q => resolvePos G P Q
127	\| .resolveNeg P Q => resolveNeg G P Q
128
129	/-- The partial graph with no resolved pairs and the given colors. -/
130	def unresolved (color : V → ℕ) : PartialGraph V where
131	edge := ⊥
132	nonEdge := ⊥
133	disjoint := disjoint_bot_left
134	color := color
135
136	/-- A construction script on `Fin n`: the colors of the initial partial
137	graph, which has no resolved pairs, and the steps. -/
138	structure Script (n : ℕ) where
139	/-- The colors of the initial partial graph. -/
140	colors : Fin n → ℕ
141	/-- The steps, in order. -/
142	steps : List Step
143	deriving Encode
144
145	/-- The sequence produced by a script: the initial partial graph
146	followed by the results of the steps. -/
147	def Script.run {n : ℕ} (σ : Script n) : List (PartialGraph (Fin n)) :=
148	σ.steps.scanl apply (unresolved σ.colors)
149
150	/-- Every number in the encoding of the script `σ` is at most the
151	length of the encoding plus `n`. This holds when the colors of the
152	initial partial graph and of the steps are vertices. It lets an
153	algorithm pass the script on to another one, whose word length depends
154	on the numbers of its input. -/
155	def Script.HasSmallNumbers {n : ℕ} (σ : Script n) : Prop :=
156	∀ v ∈ encode σ, v ≤ (encode σ).length + n
157
158	/-- The list `y` encodes the sequence `s` of partial graphs on `n`
159	vertices: it is the encoding of a script that produces `s`. -/
160	def EncodesSequence {n : ℕ} (y : List ℕ) (s : List (PartialGraph (Fin n))) :
161	Prop :=
162	∃ σ : Script n, y = encode σ ∧ s = σ.run
163
164	end Lax185574.ConstructionSequences
165

defLax185574.DistanceLogic

Distance logic over partial graphs and distance rank

The logic distFO extends first-order logic over partial graphs by distance atoms. Its atoms are

the first-order atoms x = y, E(x, y), N(x, y) and Y(x), for colors Y;
for each radius r ∈ ℕ, the binary distance atom dist(x, y) ≤ r;
for each radius r ∈ ℕ and color Y, the unary distance atom dist(x, Y) < r, equivalent to ∃y (Y(y) ∧ dist(x, y) < r).

Distances are measured in the Gaifman graph of the partial graph, that is, along resolved pairs. A formula is built from atoms by negation, conjunction and the local quantifier ∃y (dist(xᵢ, y) ≤ s ∧ φ(x̄ y)).

The horizon functions are ρ⁻(k, q) = 9^((k+q+1)q) and ρ⁺(k, q) = 9^((k+q)(q+1)). A formula has distance rank (k, q) if it is a Boolean combination of

first-order atoms,
binary distance atoms of radius at most ρ⁻(k, q),
unary distance atoms of radius at most ρ⁺(k, q), and
formulas ∃y (dist(xᵢ, y) ≤ ρ⁺(k+1, q−1) ∧ φ(x̄ y)), where q ≥ 1, xᵢ is a free variable and φ has distance rank (k+1, q−1).

1	import Lax185574.PartialGraphs
2	import Lax185574.Encodings
3	import Lax3.DistFO
4
	… module docstring, 51 lines
56
57	namespace Lax185574.DistanceLogic
58
59	open Lax185574.PartialGraphs Lax185574.GaifmanGraph Lax185574.Encoding
60	open Lax3.DistFO (rhoMinus rhoPlus)
61
62	/-- Formulas of distance logic over partial graphs with `ℓ` free
63	variables. -/
64	inductive DistFO : ℕ → Type
65	/-- `xᵢ = xⱼ`. -/
66	\| eq {ℓ : ℕ} (i j : Fin ℓ) : DistFO ℓ
67	/-- `E(xᵢ, xⱼ)`. -/
68	\| edge {ℓ : ℕ} (i j : Fin ℓ) : DistFO ℓ
69	/-- `N(xᵢ, xⱼ)`. -/
70	\| nonEdge {ℓ : ℕ} (i j : Fin ℓ) : DistFO ℓ
71	/-- `Y(xᵢ)`. -/
72	\| color {ℓ : ℕ} (Y : ℕ) (i : Fin ℓ) : DistFO ℓ
73	/-- `dist(xᵢ, xⱼ) ≤ r`. -/
74	\| distLe {ℓ : ℕ} (r : ℕ) (i j : Fin ℓ) : DistFO ℓ
75	/-- `dist(xᵢ, Y) < r`. -/
76	\| distColorLt {ℓ : ℕ} (r Y : ℕ) (i : Fin ℓ) : DistFO ℓ
77	/-- Negation. -/
78	\| not {ℓ : ℕ} (φ : DistFO ℓ) : DistFO ℓ
79	/-- Conjunction. -/
80	\| and {ℓ : ℕ} (φ ψ : DistFO ℓ) : DistFO ℓ
81	/-- `∃y (dist(xᵢ, y) ≤ s ∧ φ(x̄ y))`, binding the new last variable. -/
82	\| exLocal {ℓ : ℕ} (i : Fin ℓ) (s : ℕ) (φ : DistFO (ℓ + 1)) : DistFO ℓ
83	deriving Encode
84
85	namespace DistFO
86
87	/-- The formula is an atom. -/
88	def IsAtom {ℓ : ℕ} : DistFO ℓ → Prop
89	\| .not _ \| .and _ _ \| .exLocal _ _ _ => False
90	\| _ => True
91
92	/-- Some walk of length less than `r` joins `u` and `v`. -/
93	def WithinDistLt {W : Type*} (G : SimpleGraph W) (r : ℕ) (u v : W) : Prop :=
94	∃ p : G.Walk u v, p.length < r
95
96	variable {V : Type*}
97
98	/-- Satisfaction in the partial graph `G` under the assignment `m` of
99	vertices to the free variables. -/
100	def Sat (G : PartialGraph V) : {ℓ : ℕ} → (Fin ℓ → V) → DistFO ℓ → Prop
101	\| _, m, .eq i j => m i = m j
102	\| _, m, .edge i j => G.edge.Adj (m i) (m j)
103	\| _, m, .nonEdge i j => G.nonEdge.Adj (m i) (m j)
104	\| _, m, .color Y i => G.color (m i) = Y
105	\| _, m, .distLe r i j => WithinDist G.resolved r (m i) (m j)
106	\| _, m, .distColorLt r Y i => ∃ v, G.color v = Y ∧ WithinDistLt G.resolved r (m i) v
107	\| _, m, .not φ => ¬ Sat G m φ
108	\| _, m, .and φ ψ => Sat G m φ ∧ Sat G m ψ
109	\| _, m, .exLocal i s φ =>
110	∃ v, WithinDist G.resolved s (m i) v ∧ Sat G (Fin.snoc m v) φ
111
112	/-- `DRank k q φ`: the formula `φ` has distance rank `(k, q)`. -/
113	inductive DRank : ℕ → ℕ → {ℓ : ℕ} → DistFO ℓ → Prop
114	\| eq {k q ℓ : ℕ} (i j : Fin ℓ) : DRank k q (.eq i j)
115	\| edge {k q ℓ : ℕ} (i j : Fin ℓ) : DRank k q (.edge i j)
116	\| nonEdge {k q ℓ : ℕ} (i j : Fin ℓ) : DRank k q (.nonEdge i j)
117	\| color {k q ℓ : ℕ} (Y : ℕ) (i : Fin ℓ) : DRank k q (.color Y i)
118	\| distLe {k q ℓ : ℕ} (r : ℕ) (i j : Fin ℓ) :
119	r ≤ rhoMinus k q → DRank k q (.distLe r i j)
120	\| distColorLt {k q ℓ : ℕ} (r Y : ℕ) (i : Fin ℓ) :
121	r ≤ rhoPlus k q → DRank k q (.distColorLt r Y i)
122	\| not {k q ℓ : ℕ} {φ : DistFO ℓ} : DRank k q φ → DRank k q (.not φ)
123	\| and {k q ℓ : ℕ} {φ ψ : DistFO ℓ} :
124	DRank k q φ → DRank k q ψ → DRank k q (.and φ ψ)
125	\| exLocal {k q ℓ : ℕ} (i : Fin ℓ) {φ : DistFO (ℓ + 1)} :
126	DRank (k + 1) q φ → DRank k (q + 1) (.exLocal i (rhoPlus (k + 1) q) φ)
127
128	end DistFO
129
130	end Lax185574.DistanceLogic
131

defLax185574.TypeTrees

Type trees and their canonical representation

Let G be a partial graph, k, q ∈ ℕ and ā a tuple of ℓ vertices. The atomic (k, q)-type atp_{k,q}(ā) is the set of atomic distFO formulas of distance rank (k, q) with free variables among x₁, …, x_ℓ that ā satisfies in G. The (k, q)-type tree of ā is

tree_{k,q}(ā) = (atp_{k,q}(ā), 𝓔_{k,q}(ā)),

where 𝓔_{k,0}(ā) = ∅ and, for q ≥ 1,

𝓔_{k,q}(ā) = {(i, tree_{k+1,q−1}(ā b)) | i ∈ [ℓ], b ∈ V(G), dist(aᵢ, b) ≤ ρ⁺(k+1, q−1)}.

The members of 𝓔_{k,q}(ā) are the extensions, and i is the guard of the extension. The number ℓ is the arity and (k, q) is the rank of the tree.

Type trees are represented on the RAM in a canonical form, with all sets sorted and free of duplicates, so that two trees are equal exactly when their representations are. The size ‖τ‖ of a tree is the size of its representation, which includes k, q and ℓ.

For a type tree ν of arity one, [ν]^G is the set of vertices b with tree_{k,q}(b) = ν, where (k, q) is the rank of ν.

1	import Lax185574.DistanceLogic
2	import Mathlib.Data.Fin.VecNotation
3
	… module docstring, 61 lines
65
66	namespace Lax185574.TypeTrees
67
68	open Lax185574.PartialGraphs Lax185574.GaifmanGraph Lax185574.Encoding
69	open Lax185574.DistanceLogic Lax185574.DistanceLogic.DistFO
70	open Lax3.DistFO (rhoMinus rhoPlus)
71
72	/-- `Node q ℓ`: the roots of the type trees of depth `q` and arity `ℓ`.
73	A root of depth `0` is its set of atoms. A root of depth `q + 1` is its
74	set of atoms together with its set of extensions, pairs of a guard and
75	a root of depth `q` and arity `ℓ + 1`. -/
76	def Node : ℕ → ℕ → Type
77	\| 0, ℓ => Finset (DistFO ℓ)
78	\| q + 1, ℓ => Finset (DistFO ℓ) × Finset (Fin ℓ × Node q (ℓ + 1))
79
80	/-- A root of depth `0` is encoded by its set of atoms. A root of depth
81	`q + 1` is encoded by its set of atoms followed by its set of
82	extensions. `Node` is defined by recursion on the depth and is not an
83	inductive type, so its encoding is given by the same recursion. -/
84	@[instance_reducible] def Node.instEncode : (q ℓ : ℕ) → Encode (Node q ℓ)
85	\| 0, ℓ => inferInstanceAs (Encode (Finset (DistFO ℓ)))
86	\| q + 1, ℓ =>
87	letI := Node.instEncode q (ℓ + 1)
88	inferInstanceAs (Encode (Finset (DistFO ℓ) × Finset (Fin ℓ × Node q (ℓ + 1))))
89
90	instance {q ℓ : ℕ} : Encode (Node q ℓ) := Node.instEncode q ℓ
91
92	/-- A type tree: its rank `(k, q)`, its arity `ℓ` and its root. -/
93	structure TypeTree where
94	/-- The first component of the rank. -/
95	k : ℕ
96	/-- The depth, the second component of the rank. -/
97	q : ℕ
98	/-- The arity. -/
99	ℓ : ℕ
100	/-- The root. -/
101	root : Node q ℓ
102	deriving Encode
103
104	variable {V : Type*}
105
106	/-- The finite set with the elements of `S`, and `∅` if `S` is
107	infinite. -/
108	noncomputable def finsetOf {α : Type*} (S : Set α) : Finset α :=
109	open Classical in if h : S.Finite then h.toFinset else ∅
110
111	/-- `atp_{k,q}(a)`: the atoms of distance rank `(k, q)` satisfied by the
112	tuple `a`. -/
113	def atp (G : PartialGraph V) (k q : ℕ) {ℓ : ℕ} (a : Fin ℓ → V) : Set (DistFO ℓ) :=
114	{φ \| IsAtom φ ∧ DRank k q φ ∧ Sat G a φ}
115
116	/-- The root of `tree_{k,q}(a)`: the atoms of `atp_{k,q}(a)` and, for
117	`q ≥ 1`, the extensions `(i, tree_{k+1,q−1}(a b))`. -/
118	noncomputable def node (G : PartialGraph V) : (k q : ℕ) → {ℓ : ℕ} → (Fin ℓ → V) → Node q ℓ
119	\| k, 0, _, a => finsetOf (atp G k 0 a)
120	\| k, q + 1, ℓ, a =>
121	(finsetOf (atp G k (q + 1) a),
122	finsetOf {e \| ∃ (i : Fin ℓ) (b : V),
123	WithinDist G.resolved (rhoPlus (k + 1) q) (a i) b ∧
124	e = (i, node G (k + 1) q (Fin.snoc a b))})
125
126	/-- `tree_{k,q}(a)`. -/
127	noncomputable def tree (G : PartialGraph V) (k q : ℕ) {ℓ : ℕ} (a : Fin ℓ → V) : TypeTree :=
128	⟨k, q, ℓ, node G k q a⟩
129
130	/-- `[ν]^G`: the vertices whose type tree is `ν`. The rank is read off
131	`ν`, which records it. -/
132	def realizations (G : PartialGraph V) (ν : TypeTree) : Set V :=
133	{b \| tree G ν.k ν.q ![b] = ν}
134
135	/-- The family `(tree_{k,q}(a) : a ∈ V(G))` of the type trees of all
136	vertices. -/
137	noncomputable def family {n : ℕ} (G : PartialGraph (Fin n)) (k q : ℕ) : Fin n → TypeTree :=
138	fun a => tree G k q ![a]
139
140	/-- The largest size of a tree of the family. -/
141	noncomputable def maxTreeSize {n : ℕ} (G : PartialGraph (Fin n)) (k q : ℕ) : ℕ :=
142	Finset.univ.sup fun a : Fin n => wordLength (family G k q a)
143
144	end Lax185574.TypeTrees
145

obs✓Lax185574.CanonicalForm

⊢Lax185574Proofs.CanonicalForm.exists_program_canonical

lem✓Lax185574.Evaluation

⊢Lax185574Proofs.Evaluation.exists_program_eval

cor✓Lax185574.TreeEquivalence

⊢Lax185574Proofs.TreeEquivalence.tree_eq_iff
- lem✓Lax185574.Evaluation
→
cor✓Lax185574.TreeEquivalence
The rightwards implication follows from the evaluation lemma: the evaluation program receives equal inputs for the two tuples, so it gives equal answers. The vertex type is renamed to $Fin n$ for this. The converse is $node_eq_of_sat_iff$ , by induction on $q$ .

lem✓Lax185574.TreeLocality

⊢Lax185574Proofs.TreeLocality.ball_of_guarded

lem✓Lax185574.Restriction

⊢Lax185574Proofs.Restriction.exists_program_restrict
- obs✓Lax185574.CanonicalForm
→
lem✓Lax185574.Restriction
The program is one pass over the tree followed by restoring canonical form, as in the proof of the restriction lemma. The pass reads the tree and $J$ , the latter into a table of the places of the positions, lists the nodes of the tree in breadth-first order, and writes for every node, from the last to the first, its transformed atoms and its transformed extensions. An atom is transformed by renaming its positions along $J$ , and dropped if a position lies outside $J$ . An extension is transformed by renaming its guard in the same way, and dropped if the guard lies outside $J$ , and its child is referred to by the indices of the jobs of the child. Positions beyond the arity $ℓ$ , the new positions of the nodes below the root, are moved down by $ℓ - |J|$ . Nothing is sorted in the pass. The canonical form is then restored from the leaves up by the program of the canonical form observation, called once for every set of the result ( $TreeCanon.treeCanon$ ). The result is the semantic core $restrictNode$ along the partial inverse of $J$ , whose correctness is $restrictTree_tree$ . The sets of the result are no larger than those of the input, so the time is polynomial in the length of the input.

The proof is carried out for the notion $Lax185574.Computing.Computes$ , and transferred to $Lax185574.Algorithms.Algorithm.Computes$ through $Lax185574Proofs.Interface$ .

lem✓Lax185574.RankShift

⊢Lax185574Proofs.RankShift.exists_program_shift
- lem✓Lax185574.Restriction
→
lem✓Lax185574.RankShift
The program runs the glue program $ShiftRam.glue$ and the restriction program of the restriction lemma in the loop driver $loop_sound$ . In its first round the glue program reads the tree, finds the first extension with guard $0$ , which exists since $dist(a₁, a₁) = 0$ , and asks for the restriction of its child to the first $ℓ$ positions. In its second round it outputs the answer. The child is tree_{k+1,q−1}(ā b) for a vertex $b$ , so the answer is tree_{k+1,q−1}(ā), as in the proof of the rank shift lemma. Every run inside the driver is right at an admissible word length: the runs of the glue program because their values are polynomial in the input, the run of the restriction program because its query is admissible at the word length of its region. The constant absorbs the constant of the restriction program at rank $(k + 1, q)$ , and the degree is that of the restriction program plus two.

The proof is carried out for the notion $Lax185574.Computing.Computes$ , and transferred to $Lax185574.Algorithms.Algorithm.Computes$ through $Lax185574Proofs.Interface$ .

lem✓Lax185574.FarComposition

⊢Lax185574Proofs.FarComposition.exists_program_compose
- obs✓Lax185574.CanonicalForm
- lem✓Lax185574.RankShift
- lem✓Lax185574.Restriction
→
lem✓Lax185574.FarComposition
The program runs a glue program and the three programs of the restriction lemma, the rank shift lemma and the canonical form observation in the loop driver. The glue program runs the recursion of the far composition with an explicit stack of frames: each round reads the stack and the answer to its last question, does one step of the recursion and asks the next question, a rank shift, a restriction or a canonical form, or writes the type tree of the concatenation. Before it halts, every round checks that the question is admissible for the program that answers it, that the round counter is small against the word length of its region, and that its output fits, so every halting run inside the driver is right.

The proof is carried out for the notion $Lax185574.Computing.Computes$ , and transferred to $Lax185574.Algorithms.Algorithm.Computes$ through $Lax185574Proofs.Interface$ .

defLax185574.ScatterTypes

Scatter types

Let G be a partial graph. A set S of vertices is r-scattered if all vertices of S have pairwise distance larger than r. Fix a linear order on V(G). For X ⊆ V(G) and r ∈ ℕ, S_r(X) is the inclusion-wise maximal r-scattered subset of X built by the greedy process that repeatedly adds the least available vertex.

The (k, q)-scatter type stp^G_{k,q} is the function with domain

{(r, tree_{k+i,q−i}(b)) | i ∈ [q], b ∈ V(G), r ∈ [9^{k+i} · ρ⁻(k+i, q−i)]}

given by stp^G_{k,q}(r, ν) = min(|S_r([ν]^G)|, k + q). For q = 0 the domain is empty. A scatter type is represented canonically as the sorted list of its triples (r, ν, stp_{k,q}(r, ν)), using the canonical representation of ν. Its size ‖stp_{k,q}‖ is the size of this list.

1	import Lax185574.TypeTrees
2	import Mathlib.Data.List.FinRange
3
	… module docstring, 35 lines
39
40	namespace Lax185574.ScatterTypes
41
42	open Lax185574.PartialGraphs Lax185574.GaifmanGraph
43	open Lax185574.TypeTrees
44	open Lax3.DistFO (rhoMinus rhoPlus)
45
46	variable {n : ℕ}
47
48	/-- `S_r(X)`: the greedy maximal `r`-scattered subset of `X`, scanning
49	the vertices in increasing order. -/
50	noncomputable def greedyScattered (G : PartialGraph (Fin n)) (r : ℕ) (X : Set (Fin n)) :
51	List (Fin n) :=
52	open Classical in
53	(List.finRange n).foldl
54	(fun S v => if v ∈ X ∧ ∀ u ∈ S, ¬ WithinDist G.resolved r u v then S ++ [v] else S) []
55
56	/-- The domain `domain(stp_{k,q})` of the scatter type. -/
57	def domain (G : PartialGraph (Fin n)) (k q : ℕ) : Set (ℕ × TypeTree) :=
58	{p \| ∃ (i : ℕ) (b : Fin n), 1 ≤ i ∧ i ≤ q ∧ 1 ≤ p.1 ∧
59	p.1 ≤ 9 ^ (k + i) * rhoMinus (k + i) (q - i) ∧
60	p.2 = tree G (k + i) (q - i) ![b]}
61
62	/-- The value `min(\|S_r([ν]^G)\|, k + q)` at the pair `p = (r, ν)`. -/
63	noncomputable def value (G : PartialGraph (Fin n)) (k q : ℕ) (p : ℕ × TypeTree) : ℕ :=
64	min (greedyScattered G p.1 (realizations G p.2)).length (k + q)
65
66	/-- The graph `{(x, f x) \| x ∈ D}` of a function on a finite domain. -/
67	noncomputable def graphOn {α β : Type*} (D : Set α) (f : α → β) : Finset (α × β) :=
68	finsetOf {p \| p.1 ∈ D ∧ p.2 = f p.1}
69
70	/-- `stp^G_{k,q}`, as its graph: the pairs `((r, ν), stp(r, ν))` with
71	`(r, ν) ∈ domain(stp_{k,q})`. -/
72	noncomputable def stp (G : PartialGraph (Fin n)) (k q : ℕ) : Finset ((ℕ × TypeTree) × ℕ) :=
73	graphOn (domain G k q) (value G k q)
74
75	end Lax185574.ScatterTypes
76

defLax185574.TypeTrees

Type trees and their canonical representation

tree_{k,q}(ā) = (atp_{k,q}(ā), 𝓔_{k,q}(ā)),

where 𝓔_{k,0}(ā) = ∅ and, for q ≥ 1,

𝓔_{k,q}(ā) = {(i, tree_{k+1,q−1}(ā b)) | i ∈ [ℓ], b ∈ V(G), dist(aᵢ, b) ≤ ρ⁺(k+1, q−1)}.

The members of 𝓔_{k,q}(ā) are the extensions, and i is the guard of the extension. The number ℓ is the arity and (k, q) is the rank of the tree.

For a type tree ν of arity one, [ν]^G is the set of vertices b with tree_{k,q}(b) = ν, where (k, q) is the rank of ν.

1	import Lax185574.DistanceLogic
2	import Mathlib.Data.Fin.VecNotation
3
	… module docstring, 61 lines
65
66	namespace Lax185574.TypeTrees
67
68	open Lax185574.PartialGraphs Lax185574.GaifmanGraph Lax185574.Encoding
69	open Lax185574.DistanceLogic Lax185574.DistanceLogic.DistFO
70	open Lax3.DistFO (rhoMinus rhoPlus)
71
72	/-- `Node q ℓ`: the roots of the type trees of depth `q` and arity `ℓ`.
73	A root of depth `0` is its set of atoms. A root of depth `q + 1` is its
74	set of atoms together with its set of extensions, pairs of a guard and
75	a root of depth `q` and arity `ℓ + 1`. -/
76	def Node : ℕ → ℕ → Type
77	\| 0, ℓ => Finset (DistFO ℓ)
78	\| q + 1, ℓ => Finset (DistFO ℓ) × Finset (Fin ℓ × Node q (ℓ + 1))
79
80	/-- A root of depth `0` is encoded by its set of atoms. A root of depth
81	`q + 1` is encoded by its set of atoms followed by its set of
82	extensions. `Node` is defined by recursion on the depth and is not an
83	inductive type, so its encoding is given by the same recursion. -/
84	@[instance_reducible] def Node.instEncode : (q ℓ : ℕ) → Encode (Node q ℓ)
85	\| 0, ℓ => inferInstanceAs (Encode (Finset (DistFO ℓ)))
86	\| q + 1, ℓ =>
87	letI := Node.instEncode q (ℓ + 1)
88	inferInstanceAs (Encode (Finset (DistFO ℓ) × Finset (Fin ℓ × Node q (ℓ + 1))))
89
90	instance {q ℓ : ℕ} : Encode (Node q ℓ) := Node.instEncode q ℓ
91
92	/-- A type tree: its rank `(k, q)`, its arity `ℓ` and its root. -/
93	structure TypeTree where
94	/-- The first component of the rank. -/
95	k : ℕ
96	/-- The depth, the second component of the rank. -/
97	q : ℕ
98	/-- The arity. -/
99	ℓ : ℕ
100	/-- The root. -/
101	root : Node q ℓ
102	deriving Encode
103
104	variable {V : Type*}
105
106	/-- The finite set with the elements of `S`, and `∅` if `S` is
107	infinite. -/
108	noncomputable def finsetOf {α : Type*} (S : Set α) : Finset α :=
109	open Classical in if h : S.Finite then h.toFinset else ∅
110
111	/-- `atp_{k,q}(a)`: the atoms of distance rank `(k, q)` satisfied by the
112	tuple `a`. -/
113	def atp (G : PartialGraph V) (k q : ℕ) {ℓ : ℕ} (a : Fin ℓ → V) : Set (DistFO ℓ) :=
114	{φ \| IsAtom φ ∧ DRank k q φ ∧ Sat G a φ}
115
116	/-- The root of `tree_{k,q}(a)`: the atoms of `atp_{k,q}(a)` and, for
117	`q ≥ 1`, the extensions `(i, tree_{k+1,q−1}(a b))`. -/
118	noncomputable def node (G : PartialGraph V) : (k q : ℕ) → {ℓ : ℕ} → (Fin ℓ → V) → Node q ℓ
119	\| k, 0, _, a => finsetOf (atp G k 0 a)
120	\| k, q + 1, ℓ, a =>
121	(finsetOf (atp G k (q + 1) a),
122	finsetOf {e \| ∃ (i : Fin ℓ) (b : V),
123	WithinDist G.resolved (rhoPlus (k + 1) q) (a i) b ∧
124	e = (i, node G (k + 1) q (Fin.snoc a b))})
125
126	/-- `tree_{k,q}(a)`. -/
127	noncomputable def tree (G : PartialGraph V) (k q : ℕ) {ℓ : ℕ} (a : Fin ℓ → V) : TypeTree :=
128	⟨k, q, ℓ, node G k q a⟩
129
130	/-- `[ν]^G`: the vertices whose type tree is `ν`. The rank is read off
131	`ν`, which records it. -/
132	def realizations (G : PartialGraph V) (ν : TypeTree) : Set V :=
133	{b \| tree G ν.k ν.q ![b] = ν}
134
135	/-- The family `(tree_{k,q}(a) : a ∈ V(G))` of the type trees of all
136	vertices. -/
137	noncomputable def family {n : ℕ} (G : PartialGraph (Fin n)) (k q : ℕ) : Fin n → TypeTree :=
138	fun a => tree G k q ![a]
139
140	/-- The largest size of a tree of the family. -/
141	noncomputable def maxTreeSize {n : ℕ} (G : PartialGraph (Fin n)) (k q : ℕ) : ℕ :=
142	Finset.univ.sup fun a : Fin n => wordLength (family G k q a)
143
144	end Lax185574.TypeTrees
145

lem✓Lax185574.ScatterTypeRestriction

⊢Lax185574Proofs.ScatterTypeRestriction.stp_restrict

lem✓Lax185574.ComputeScatterType

⊢Lax185574Proofs.ComputeScatterType.exists_program_stp
- lem✓Lax185574.RankShift
→
lem✓Lax185574.ComputeScatterType
The program runs the glue program $StpRam.glue$ and the program of the rank shift lemma in the loop driver $loop_sound$ , as in the proof of the lemma on computing scatter types. The first round reads the graph, $k$ and $q$ , skips the distance matrix $D_G$ and reads the family of type trees. For $q = 0$ it outputs the empty scatter type. Otherwise the rounds ask for the shifts of the entries of the list of the family trees followed by the answers, one by one, so that the answers are the trees $tree_{k+i,q−i}(v)$ for $1 ≤ i ≤ q$ and all vertices $v$ , in this order. After a dummy call the final round reads the graph, $D_G$ and the answers and computes the scatter type ( $StpRam.finalRound_run$ ). Its greedy scans test whether a vertex is within distance $r$ of a chosen vertex by one entry of the row of $D_G$ of the chosen vertex, in place of a breadth-first search. The script has $q · n + 1$ calls. Every run inside the driver is right at an admissible word length: the runs of the glue program because their values are below a constant in $k, q$ times the cube of $|x| + max x + 1$ , the runs of the rank shift because their queries are admissible at the word lengths of their regions. The time is that of the first round, $O_{k,q}(n² + n · L)$ , and of the final round, $O_{k,q}(n² · (L + 1))$ , plus $q · n$ middle rounds of time $O_{k,q}(n · L)$ and $q · n + 1$ calls of time $O_{k,q}((L + 1)^a)$ .

The proof is carried out for the notion $Lax185574.Computing.Computes$ , and transferred to $Lax185574.Algorithms.Algorithm.Computes$ through $Lax185574Proofs.Interface$ .

defLax185574.FarTrees

⊢Lax185574Proofs.Clustering.clustering

lem✓Lax185574.Clustering

Clustering of a tuple

Let r ∈ ℕ, ℓ ≥ 1, G a graph and ā = (a₁, …, a_ℓ) ∈ V(G)^ℓ. There exist a radius ρ with r ≤ ρ ≤ 9^{ℓ−1} r and a partition 𝓑 of {a₁, …, a_ℓ} with the following property. For every X ⊆ V(G), every inclusion-wise maximal 4ρ-scattered subset S ⊆ X, and every H ≥ 4ρ + r,

∃x ∈ X: dist(x, ā) > r ⟺ ∃x ∈ X: r < dist(x, ā) ≤ H, or |{B ∈ 𝓑 | ∃x ∈ X: dist(x, B) ≤ r}| < |S|.

Moreover, ρ and 𝓑 can be determined by tests of the form dist(aᵢ, aⱼ) ≤ s, where i, j ∈ [ℓ] and s ≤ 8 · 9^{ℓ−1} r.

1	import Lax185574.GaifmanGraph
2	import Mathlib.Data.Set.Card
3
	… module docstring, 38 lines
42
43	namespace Lax185574.Clustering
44
45	open Lax185574.GaifmanGraph
46
47	variable {V : Type*}
48
49	/-- The radius `ρ` and the partition `β` of the positions are
50	admissible for `a` at radius `r`: entries in one block are within
51	distance `4ρ − 2r`, and entries in different blocks are not within
52	distance `4ρ + 2r`. -/
53	def Admissible (G : SimpleGraph V) (r : ℕ) {ℓ : ℕ} (a : Fin ℓ → V) (ρ : ℕ)
54	(β : Fin ℓ → Fin ℓ) : Prop :=
55	∀ i j, (β i = β j → WithinDist G (4 * ρ - 2 * r) (a i) (a j)) ∧
56	(β i ≠ β j → ¬ WithinDist G (4 * ρ + 2 * r) (a i) (a j))
57
58	/-- Clustering. Some admissible radius lies between `r` and
59	`9^(ℓ−1) r`, and every admissible pair detects the vertices of a set `X`
60	far from `a`: by vertices at bounded distance, or by counting a maximal
61	scattered subset of `X`. -/
62	axiom clustering [Finite V] (G : SimpleGraph V) (r ℓ : ℕ) (hℓ : 1 ≤ ℓ) (a : Fin ℓ → V) :
63	(∃ ρ β, r ≤ ρ ∧ ρ ≤ 9 ^ (ℓ - 1) * r ∧ Admissible G r a ρ β) ∧
64	∀ ρ β, r ≤ ρ → Admissible G r a ρ β →
65	∀ (X S : Set V) (H : ℕ), S ⊆ X →
66	(∀ x ∈ S, ∀ y ∈ S, x ≠ y → ¬ WithinDist G (4 * ρ) x y) →
67	(∀ x ∈ X, ∃ y ∈ S, WithinDist G (4 * ρ) x y) →
68	4 * ρ + r ≤ H →
69	((∃ x ∈ X, ∀ i, ¬ WithinDist G r (a i) x) ↔
70	(∃ x ∈ X, (∀ i, ¬ WithinDist G r (a i) x) ∧ ∃ i, WithinDist G H (a i) x) ∨
71	(β '' {i \| ∃ x ∈ X, WithinDist G r (a i) x}).ncard < S.ncard)
72
73	end Lax185574.Clustering
74

lem✓Lax185574.ToFarTree

⊢Lax185574Proofs.ToFarTree.exists_program_ftree
- lem✓Lax185574.Clustering
- lem✓Lax185574.Restriction
→
lem✓Lax185574.ToFarTree
The program runs the glue program $FarRam.glue$ and the restriction program of the restriction lemma in the loop driver $loop_sound$ . Round $j$ of the glue program reads the tree, the scatter type and the answers so far, and asks for the restriction $μ ↾ (ℓ+1)$ of the child of extension $j$ to its last position, one call per extension. The last round reads the radius and the blocks off the root, the met and far bits off the roots of the children, scans the scatter type and writes the selected trees, as in the proof of the far tree lemma. Its output is the far tree by $farTree_tree$ , which applies the clustering lemma. Every run inside the driver is right at an admissible word length: the runs of the glue program because their values are polynomial in the input with a factor depending on the rank, the runs of the restriction program because their queries are admissible at the word lengths of their regions.

The proof is carried out for the notion $Lax185574.Computing.Computes$ , and transferred to $Lax185574.Algorithms.Algorithm.Computes$ through $Lax185574Proofs.Interface$ .

lem✓Lax185574.MergeLift

⊢Lax185574Proofs.MergeLift.exists_program_mergeLift
- obs✓Lax185574.CanonicalForm
→
lem✓Lax185574.MergeLift
The program is one pass over the tree followed by restoring canonical form, as in the proof of the merge lift lemma. The pass reads the tree and the colors $P$ and $Q$ , lists the nodes of the tree in breadth-first order, and writes for every node, from the last to the first, its transformed atoms and its extensions. An atom is transformed by replacing the color $Q$ by $P$ in every atom $Y(x)$ and $dist(x, Y) < r$ . The guards are kept, and the child of an extension is referred to by the indices of the jobs of the child. Nothing is sorted in the pass. The canonical form is then restored from the leaves up by the program of the canonical form observation, called once for every set of the result ( $TreeCanon.treeCanon$ ), which merges atoms that become equal. This is the semantic core $mergeNode$ , whose correctness is $mergeNode_node$ . No tree grows, so the time is polynomial in the length of the input.

The proof is carried out for the notion $Lax185574.Computing.Computes$ , and transferred to $Lax185574.Algorithms.Algorithm.Computes$ through $Lax185574Proofs.Interface$ .

lem✓Lax185574.ResolveLift

Lifting type trees through a resolve

Let k ≥ 1 and q ∈ ℕ. Given a partial graph G, its distance matrix D_G, colors P, Q, a sign ±, and (tree^G_{k,q}(a) : a ∈ V(G)), one can compute H = resolve^±{P,Q}(G), its distance matrix D_H, and (tree^H{k,q}(a) : a ∈ V(G)) in time

|G|² · poly_{k,q}(M + T),

where

M = max_{a ∈ V(G)} ‖tree^G_{k,q}(a)‖, T = max_{a ∈ V(G)} |{tree^G_{k+i,q−i}(v̄) | 0 ≤ i ≤ q, ℓ ∈ [k+i], v̄ ∈ (Ball^H_{ρ⁺(k,q)}(a))^ℓ}|.

Each output tree has size poly_{k,q}(T).

1	import Lax185574.TypeTrees
2	import Lax185574.ConstructionSequences
3	import Lax185574.DistanceMatrix
4	import Lax185574.Algorithms
5
	… module docstring, 34 lines
40
41	namespace Lax185574.ResolveLift
42
43	open Lax185574.Encoding Lax185574.Algorithms
44	open Lax185574.PartialGraphs Lax185574.TypeTrees Lax185574.ConstructionSequences
45	open Lax185574.DistanceMatrix
46	open Lax3.DistFO (rhoMinus rhoPlus)
47
48	variable {n : ℕ}
49
50	/-- `resolve^±_{P,Q}(G)`, positive for `true`. -/
51	def resolveBy (G : PartialGraph (Fin n)) (s : Bool) (P Q : ℕ) : PartialGraph (Fin n) :=
52	if s then resolvePos G P Q else resolveNeg G P Q
53
54	/-- The parameter `T`: the largest number of type trees in `G` of
55	tuples from a ball of radius `ρ⁺(k, q)` in `H`, over all ranks
56	`(k+i, q−i)` and arities `ℓ ∈ [k+i]`. -/
57	noncomputable def treeCount (G H : PartialGraph (Fin n)) (k q : ℕ) : ℕ :=
58	Finset.univ.sup fun a : Fin n =>
59	Set.ncard {τ : TypeTree \| ∃ (i ℓ : ℕ) (v : Fin ℓ → Fin n), i ≤ q ∧ 1 ≤ ℓ ∧ ℓ ≤ k + i ∧
60	(∀ j, v j ∈ H.ball (rhoPlus k q) a) ∧ τ = tree G (k + i) (q - i) v}
61
62	/-- Resolve lift. One algorithm computes the partial graph `H` after
63	a resolve, its distance matrix and the type trees of all vertices in it,
64	from the partial graph `G` before, its distance matrix, `P`, `Q`, the
65	sign and its type trees, in time `O(n² · (M + T + 1)^a)`. Each new tree
66	has size `O((T + 1)^a)`. -/
67	axiom exists_program_resolveLift :
68	∃ A : Algorithm, ∀ k q : ℕ, ∃ c a : ℕ,
69	∀ (n : ℕ) (G : PartialGraph (Fin n)) (P Q : ℕ) (s : Bool), 1 ≤ k →
70	let H := resolveBy G s P Q
71	let T := treeCount G H k q
72	A.Computes c (G, distMatrix G, P, Q, s, family G k q) (H, distMatrix H, family H k q)
73	(n ^ 2 * (maxTreeSize G k q + T + 1) ^ a) ∧
74	∀ b : Fin n, (encode (tree H k q ![b])).length ≤ c * (T + 1) ^ a
75
76	end Lax185574.ResolveLift
77

⊢Lax185574Proofs.ResolveLift.exists_program_resolveLift
- obs✓Lax185574.CanonicalForm
- lem✓Lax185574.ComputeScatterType
- lem✓Lax185574.FarComposition
- lem✓Lax185574.RankShift
- lem✓Lax185574.ScatterTypeRestriction
- lem✓Lax185574.ToFarTree
- lem✓Lax185574.TreeLocality
→
lem✓Lax185574.ResolveLift
The program is the loop driver of the glue program of the resolve lift with the switch of its five callees: the rank shift (the rank shift lemma), the far tree (the far tree lemma), the far composition (the far composition lemma), the canonical form (the canonical form observation) and the scatter type (the lemma on computing scatter types). The glue program first computes the scatter type of the input, then walks down the levels of the items, asking for the shift, the far tree and the compositions of each item, and walks up again, asking for the canonical forms of the atoms and of the children of each item. Its last round builds the resolved graph and its distance matrix, by the formula for distances after a resolve, and writes the output. Every round runs within a constant times $(n + 1) Y^a$ steps, with $Y = M + T + 1$ , except the first two and the last round, which read the input or write the output and run within a constant times $(n + 1)² Y^a$ steps. With at most a constant times $(n + 1)(T + 1)^(q + 1)$ rounds, the total time of the glue program is within the bound. The sizes of the output trees are those of the type trees of the resolved graph.

The proof is carried out for the notion $Lax185574.Computing.Computes$ , and transferred to $Lax185574.Algorithms.Algorithm.Computes$ through $Lax185574Proofs.Interface$ .

lem✓Lax185574.TypeTreeSizes

defLax185574.PartialGraphs

Partial graphs

1	import Lax185574.GaifmanGraph
2	import Lax185574.Encodings
3	import Mathlib.Combinatorics.SimpleGraph.Basic
4	import Mathlib.Data.Set.Card
5
	… module docstring, 54 lines
60
61	namespace Lax185574.PartialGraphs
62
63	open FirstOrder FirstOrder.Language
64	open Lax185574.GaifmanGraph
65
66	universe z
67
68	/-- A partial graph on the vertex type `V`: disjoint edges and
69	non-edges, and one color per vertex. -/
70	structure PartialGraph (V : Type z) where
71	/-- The edges `E(G)`. -/
72	edge : SimpleGraph V
73	/-- The non-edges `N(G)`. -/
74	nonEdge : SimpleGraph V
75	/-- No pair is both an edge and a non-edge. -/
76	disjoint : Disjoint edge nonEdge
77	/-- The color of each vertex. -/
78	color : V → ℕ
79
80	variable {V : Type z}
81
82	namespace PartialGraph
83
84	/-- The resolved pairs `R(G) = E(G) ∪ N(G)`, the Gaifman graph of the
85	partial graph. -/
86	def resolved (G : PartialGraph V) : SimpleGraph V := G.edge ⊔ G.nonEdge
87
88	/-- `Ball^G_r(v)`: the vertices within distance `r` of `v` along
89	resolved pairs. -/
90	def ball (G : PartialGraph V) (r : ℕ) (v : V) : Set V :=
91	{u \| WithinDist G.resolved r v u}
92
93	/-- The color class `Y^G`. -/
94	def colorClass (G : PartialGraph V) (Y : ℕ) : Set V := {v \| G.color v = Y}
95
96	/-- The size `‖G‖ = \|V(G)\| + \|R(G)\|` of a partial graph on `Fin n`. -/
97	noncomputable def size {n : ℕ} (G : PartialGraph (Fin n)) : ℕ :=
98	n + Set.ncard G.resolved.edgeSet
99
100	end PartialGraph
101
102	/-- The relation symbols of partial graphs: edges, non-edges and one
103	unary symbol per color. -/
104	inductive Rel : ℕ → Type
105	\| edge : Rel 2
106	\| nonEdge : Rel 2
107	\| color (Y : ℕ) : Rel 1
108
109	/-- The language of partial graphs. -/
110	def language : Language :=
111	⟨fun _ => Empty, Rel⟩
112	deriving Language.IsRelational
113
114	/-- A partial graph as a relational structure. -/
115	@[implicit_reducible]
116	def PartialGraph.structure (G : PartialGraph V) : language.Structure V where
117	funMap f := isEmptyElim f
118	RelMap
119	\| .edge => fun x => G.edge.Adj (x 0) (x 1)
120	\| .nonEdge => fun x => G.nonEdge.Adj (x 0) (x 1)
121	\| .color Y => fun x => G.color (x 0) = Y
122
123	open Lax185574.Encoding in
124	/-- A partial graph on `Fin n` is encoded by the family of its colors,
125	then its edges and then its non-edges, each graph as in
126	`Lax185574.Encodings`. So the encoding is `n` and the `n` colors, then
127	`n` and for every vertex in order the set of its neighbors along edges,
128	then `n` and for every vertex the set of its neighbors along non-edges.
129	It is determined by the partial graph and has length O(‖G‖). Running
130	times are stated in terms of ‖G‖, which is only meaningful for an
131	encoding without padding. The edges and non-edges are relations, so the
132	encoding is not derived. -/
133	noncomputable instance {n : ℕ} : Encode (PartialGraph (Fin n)) where
134	encode G := encode (G.color, G.edge, G.nonEdge)
135
136	end Lax185574.PartialGraphs
137

defLax185574.ConstructionSequences

Construction sequences

merge_{P,Q}(G): P^H = P^G ∪ Q^G and Q^H = ∅, for P ≠ Q;
resolve⁺_{P,Q}(G): E(H) = E(G) ∪ (P^G Q^G ∖ N(G));
resolve⁻_{P,Q}(G): N(H) = N(G) ∪ (P^G Q^G ∖ E(G)).

Here P^G Q^G is the set of pairs xy of distinct vertices with x ∈ P^G and y ∈ Q^G. After either resolve, every pair in P^G Q^G is resolved.

1	import Lax185574.PartialGraphs
2
	… module docstring, 52 lines
55
56	namespace Lax185574.ConstructionSequences
57
58	open Lax185574.PartialGraphs
59
60	universe z
61
62	variable {V : Type z}
63
64	/-- The pairs `P^G Q^G`: distinct vertices, one of color `P` and the
65	other of color `Q`. -/
66	def between (G : PartialGraph V) (P Q : ℕ) : SimpleGraph V :=
67	SimpleGraph.fromRel fun x y => G.color x = P ∧ G.color y = Q
68
69	/-- `merge_{P,Q}(G)`: the vertices of color `Q` get color `P`. -/
70	def merge (G : PartialGraph V) (P Q : ℕ) : PartialGraph V :=
71	{ G with color := fun v => if G.color v = Q then P else G.color v }
72
73	/-- `resolve⁺_{P,Q}(G)`: the unresolved pairs in `P^G Q^G` become
74	edges. -/
75	def resolvePos (G : PartialGraph V) (P Q : ℕ) : PartialGraph V where
76	edge := G.edge ⊔ (between G P Q \ G.nonEdge)
77	nonEdge := G.nonEdge
78	disjoint := disjoint_sup_left.2 ⟨G.disjoint, disjoint_sdiff_self_left⟩
79	color := G.color
80
81	/-- `resolve⁻_{P,Q}(G)`: the unresolved pairs in `P^G Q^G` become
82	non-edges. -/
83	def resolveNeg (G : PartialGraph V) (P Q : ℕ) : PartialGraph V where
84	edge := G.edge
85	nonEdge := G.nonEdge ⊔ (between G P Q \ G.edge)
86	disjoint := disjoint_sup_right.2 ⟨G.disjoint, disjoint_sdiff_self_right⟩
87	color := G.color
88
89	/-- An initial partial graph: no resolved pairs, and every part is a
90	singleton. -/
91	def IsInitial (G : PartialGraph V) : Prop :=
92	G.edge = ⊥ ∧ G.nonEdge = ⊥ ∧ Function.Injective G.color
93
94	/-- `H` is obtained from `G` by one merge or one resolve. -/
95	def IsStep (G H : PartialGraph V) : Prop :=
96	∃ P Q : ℕ, (P ≠ Q ∧ H = merge G P Q) ∨ H = resolvePos G P Q ∨
97	H = resolveNeg G P Q
98
99	/-- `s` is a construction sequence of the graph `G`: it starts with an
100	initial partial graph, each entry is obtained from the previous one by
101	one merge or one resolve, and the last entry has a single part, the
102	edges of `G` as edges and the non-edges of `G` as non-edges. -/
103	def IsConstructionSequence (G : SimpleGraph V) (s : List (PartialGraph V)) :
104	Prop :=
105	∃ h : s ≠ [],
106	IsInitial (s.head h) ∧
107	(∀ (t : ℕ) (ht : t + 1 < s.length), IsStep s[t] s[t + 1]) ∧
108	(∀ u v : V, (s.getLast h).color u = (s.getLast h).color v) ∧
109	(s.getLast h).edge = G ∧ (s.getLast h).nonEdge = Gᶜ
110
111	open Lax185574.Encoding
112
113	/-- One step of a construction sequence. -/
114	inductive Step
115	/-- `merge_{P,Q}`. -/
116	\| merge (P Q : ℕ)
117	/-- `resolve⁺_{P,Q}`. -/
118	\| resolvePos (P Q : ℕ)
119	/-- `resolve⁻_{P,Q}`. -/
120	\| resolveNeg (P Q : ℕ)
121	deriving Encode
122
123	/-- The partial graph obtained by applying a step. -/
124	def apply (G : PartialGraph V) : Step → PartialGraph V
125	\| .merge P Q => merge G P Q
126	\| .resolvePos P Q => resolvePos G P Q
127	\| .resolveNeg P Q => resolveNeg G P Q
128
129	/-- The partial graph with no resolved pairs and the given colors. -/
130	def unresolved (color : V → ℕ) : PartialGraph V where
131	edge := ⊥
132	nonEdge := ⊥
133	disjoint := disjoint_bot_left
134	color := color
135
136	/-- A construction script on `Fin n`: the colors of the initial partial
137	graph, which has no resolved pairs, and the steps. -/
138	structure Script (n : ℕ) where
139	/-- The colors of the initial partial graph. -/
140	colors : Fin n → ℕ
141	/-- The steps, in order. -/
142	steps : List Step
143	deriving Encode
144
145	/-- The sequence produced by a script: the initial partial graph
146	followed by the results of the steps. -/
147	def Script.run {n : ℕ} (σ : Script n) : List (PartialGraph (Fin n)) :=
148	σ.steps.scanl apply (unresolved σ.colors)
149
150	/-- Every number in the encoding of the script `σ` is at most the
151	length of the encoding plus `n`. This holds when the colors of the
152	initial partial graph and of the steps are vertices. It lets an
153	algorithm pass the script on to another one, whose word length depends
154	on the numbers of its input. -/
155	def Script.HasSmallNumbers {n : ℕ} (σ : Script n) : Prop :=
156	∀ v ∈ encode σ, v ≤ (encode σ).length + n
157
158	/-- The list `y` encodes the sequence `s` of partial graphs on `n`
159	vertices: it is the encoding of a script that produces `s`. -/
160	def EncodesSequence {n : ℕ} (y : List ℕ) (s : List (PartialGraph (Fin n))) :
161	Prop :=
162	∃ σ : Script n, y = encode σ ∧ s = σ.run
163
164	end Lax185574.ConstructionSequences
165

defLax185574.ConstructionWidth

⊢Lax185574Proofs.ChainTheorem.exists_program_decreasingChain
- thm✓Lax710763.AlmostLinearNC
→
thm✓Lax185574.ChainTheorem
The statement for graphs, graph classes and $Algorithm.Computes$ , from the version for simple graphs applied to the class of the simple graphs of the members. The algorithm is the program with its exponent, the sequence of a graph is that of its simple graph, and the constant $c$ becomes $⌈c · 2^(3+δ)⌉$ , so that $c' · n^(3+δ) + c'$ bounds the time $⌊c · (n+1)^(3+δ)⌋$ .

thm✓Lax185574.TypeBound

lem✓Lax185574.TypeTreeSizes

lem✓Lax185574.ResolveLift

Lifting type trees through a resolve

|G|² · poly_{k,q}(M + T),

where

M = max_{a ∈ V(G)} ‖tree^G_{k,q}(a)‖, T = max_{a ∈ V(G)} |{tree^G_{k+i,q−i}(v̄) | 0 ≤ i ≤ q, ℓ ∈ [k+i], v̄ ∈ (Ball^H_{ρ⁺(k,q)}(a))^ℓ}|.

Each output tree has size poly_{k,q}(T).

1	import Lax185574.TypeTrees
2	import Lax185574.ConstructionSequences
3	import Lax185574.DistanceMatrix
4	import Lax185574.Algorithms
5
	… module docstring, 34 lines
40
41	namespace Lax185574.ResolveLift
42
43	open Lax185574.Encoding Lax185574.Algorithms
44	open Lax185574.PartialGraphs Lax185574.TypeTrees Lax185574.ConstructionSequences
45	open Lax185574.DistanceMatrix
46	open Lax3.DistFO (rhoMinus rhoPlus)
47
48	variable {n : ℕ}
49
50	/-- `resolve^±_{P,Q}(G)`, positive for `true`. -/
51	def resolveBy (G : PartialGraph (Fin n)) (s : Bool) (P Q : ℕ) : PartialGraph (Fin n) :=
52	if s then resolvePos G P Q else resolveNeg G P Q
53
54	/-- The parameter `T`: the largest number of type trees in `G` of
55	tuples from a ball of radius `ρ⁺(k, q)` in `H`, over all ranks
56	`(k+i, q−i)` and arities `ℓ ∈ [k+i]`. -/
57	noncomputable def treeCount (G H : PartialGraph (Fin n)) (k q : ℕ) : ℕ :=
58	Finset.univ.sup fun a : Fin n =>
59	Set.ncard {τ : TypeTree \| ∃ (i ℓ : ℕ) (v : Fin ℓ → Fin n), i ≤ q ∧ 1 ≤ ℓ ∧ ℓ ≤ k + i ∧
60	(∀ j, v j ∈ H.ball (rhoPlus k q) a) ∧ τ = tree G (k + i) (q - i) v}
61
62	/-- Resolve lift. One algorithm computes the partial graph `H` after
63	a resolve, its distance matrix and the type trees of all vertices in it,
64	from the partial graph `G` before, its distance matrix, `P`, `Q`, the
65	sign and its type trees, in time `O(n² · (M + T + 1)^a)`. Each new tree
66	has size `O((T + 1)^a)`. -/
67	axiom exists_program_resolveLift :
68	∃ A : Algorithm, ∀ k q : ℕ, ∃ c a : ℕ,
69	∀ (n : ℕ) (G : PartialGraph (Fin n)) (P Q : ℕ) (s : Bool), 1 ≤ k →
70	let H := resolveBy G s P Q
71	let T := treeCount G H k q
72	A.Computes c (G, distMatrix G, P, Q, s, family G k q) (H, distMatrix H, family H k q)
73	(n ^ 2 * (maxTreeSize G k q + T + 1) ^ a) ∧
74	∀ b : Fin n, (encode (tree H k q ![b])).length ≤ c * (T + 1) ^ a
75
76	end Lax185574.ResolveLift
77

defLax185574.GraphBalls

defLax185574.Partitions

Partitions, transversals and the partition into atomic types

For two partitions 𝒫, 𝒬 of the same set, 𝒫 ≼ 𝒬 says that 𝒫 refines 𝒬, that is, each part of 𝒫 is contained in some part of 𝒬. For a partition 𝒫 of V and X ⊆ V, X/𝒫 is the set of parts of 𝒫 that meet X. The part of 𝒫 containing an element v is 𝒫(v). Further, ≡_𝒫 is the equivalence relation on V whose classes are the parts of 𝒫. A transversal of 𝒫 is a set that contains exactly one vertex of every part.

For a graph G and S ⊆ V(G), two vertices u, v have the same atomic type over S if and only if either u = v, or u, v ∉ S and N(u) ∩ S = N(v) ∩ S. The partition into atomic types 𝒫_S partitions S into singletons and the vertices of V(G) ∖ S according to their neighborhoods in S.

1	import Lax185574.Encodings
2	import Mathlib.Data.Setoid.Basic
3	import Mathlib.Data.Set.Card
4	import Mathlib.Data.Fintype.Basic
5
	… module docstring, 38 lines
44
45	namespace Lax185574.Partitions
46
47	open Lax185574.Encoding
48
49	universe z
50
51	variable {V : Type z}
52
53	/-- `\|X/𝒫\|`: the number of parts of `P` that meet `X`. -/
54	noncomputable def partCount (P : Setoid V) (X : Set V) : ℕ :=
55	(Quotient.mk P '' X).ncard
56
57	/-- The part `𝒫(v)` of `P` that contains `v`. -/
58	def part (P : Setoid V) (v : V) : Set V := {u \| P u v}
59
60	/-- `T` is a transversal of `P`: every part of `P` contains exactly one
61	vertex of `T`. -/
62	def IsTransversal (P : Setoid V) (T : Set V) : Prop :=
63	∀ v : V, ∃! t : V, t ∈ T ∧ P t v
64
65	/-- The partition `𝒫_S` into atomic types over `S`: vertices of `S` are
66	singletons, and vertices outside `S` are grouped by their neighborhood
67	in `S`. -/
68	def atomicTypes (G : SimpleGraph V) (S : Set V) : Setoid V :=
69	Setoid.ker fun v => (S ∩ {v}, S ∩ G.neighborSet v)
70
71	/-- The parts of a partition of `Fin n`, as a finite set of finite
72	sets. -/
73	noncomputable def parts {n : ℕ} (P : Setoid (Fin n)) : Finset (Finset (Fin n)) :=
74	open Classical in Finset.univ.image fun v => Finset.univ.filter fun u => P u v
75
76	/-- A partition of `Fin n` is encoded by the finite set of its parts.
77	A setoid is a relation, so the encoding is not derived. -/
78	noncomputable instance {n : ℕ} : Encode (Setoid (Fin n)) where
79	encode P := encode (parts P)
80
81	end Lax185574.Partitions
82

defLax185574.MonadicDependence

defLax185574.VCDimension

lem✓Lax185574.NeighborhoodComplexityBound

obs✓Lax185574.BoundedVCClasses

defLax185574.FirstOrderTypes

Types of bounded quantifier rank

Let A be a structure and W a set of its elements. A formula with parameters from W is a formula in the signature of A expanded by a constant for every element of W. For a tuple v̄ ∈ V(A)^k and q ∈ ℕ, the type of quantifier rank q of v̄ over W, written tp_q(v̄/W), is the set of all formulas φ(x₁, …, x_k) with parameters from W and of quantifier rank at most q such that A ⊨ φ(v̄).

For sets X, Y of elements, Types_{k,q}(X/Y) = { tp_q(v̄/Y) : v̄ ∈ X^k } is the set of types realized by k-tuples from X. The notation omits /Y when Y is empty, and then the types are those without parameters, tp_q(v̄) and Types_{k,q}(X). The number of realized types |Types_{k,q}(X/Y)| is the quantity that the paper bounds throughout.

1	import Mathlib.ModelTheory.Satisfiability
2	import Mathlib.Data.Set.Card
3
	… module docstring, 48 lines
52
53	namespace Lax185574.FirstOrderTypes
54
55	open FirstOrder FirstOrder.Language
56
57	universe u v w z
58
59	variable {L : Language.{u, v}}
60
61	/-- The quantifier rank of a formula: the nesting depth of its
62	quantifiers. -/
63	def quantifierRank {α : Type w} : {n : ℕ} → L.BoundedFormula α n → ℕ
64	\| _, .falsum => 0
65	\| _, .equal _ _ => 0
66	\| _, .rel _ _ => 0
67	\| _, .imp φ ψ => max (quantifierRank φ) (quantifierRank ψ)
68	\| _, .all φ => quantifierRank φ + 1
69
70	variable {V : Type z}
71
72	section
73
74	variable [L.Structure V]
75
76	/-- The type `tp_q(v̄)` of quantifier rank `q` of the tuple `v`: the
77	formulas of quantifier rank at most `q`, without parameters, that hold
78	of `v`. -/
79	def rankType (q : ℕ) {k : ℕ} (v : Fin k → V) : Set (L.Formula (Fin k)) :=
80	{φ \| quantifierRank φ ≤ q ∧ φ.Realize v}
81
82	/-- `Types_{k,q}(X)`: the types of quantifier rank `q` of the `k`-tuples
83	from `X`. -/
84	def types (k q : ℕ) (X : Set V) : Set (Set (L.Formula (Fin k))) :=
85	rankType q '' {v : Fin k → V \| ∀ i, v i ∈ X}
86
87	/-- `\|Types_{k,q}(X)\|`: the number of types of quantifier rank `q`
88	realized by `k`-tuples from `X`. -/
89	noncomputable def typeCount (k q : ℕ) (X : Set V) : ℕ :=
90	(types (L := L) k q X).ncard
91
92	/-- The type `tp_q(v̄/W)` of quantifier rank `q` of the tuple `v` over
93	the parameter set `W`: the formulas of quantifier rank at most `q` with
94	parameters from `W` that hold of `v`. -/
95	def rankTypeOver (q : ℕ) (W : Set V) {k : ℕ} (v : Fin k → V) :
96	Set (L.Formula (Fin k ⊕ W)) :=
97	{φ \| quantifierRank φ ≤ q ∧ φ.Realize (Sum.elim v Subtype.val)}
98
99	/-- `Types_{k,q}(X/Y)`: the types of quantifier rank `q` over `Y` of the
100	`k`-tuples from `X`. -/
101	def typesOver (k q : ℕ) (X Y : Set V) : Set (Set (L.Formula (Fin k ⊕ Y))) :=
102	rankTypeOver q Y '' {v : Fin k → V \| ∀ i, v i ∈ X}
103
104	end
105
106	/-- `\|Types_{k,q}(X/Y)\|`: the number of types of quantifier rank `q` over
107	`Y` realized by `k`-tuples from `X`, in the structure `M`. -/
108	noncomputable def typeCountOver (M : L.Structure V) (k q : ℕ) (X Y : Set V) : ℕ :=
109	(@typesOver L V M k q X Y).ncard
110
111	end Lax185574.FirstOrderTypes
112

defLax185574.AtomicTypes

Atomic types of vertices and of pairs

1	import Lax185574.FirstOrderTypes
2	import Mathlib.ModelTheory.Graph
3
	… module docstring, 27 lines
31
32	namespace Lax185574.AtomicTypes
33
34	open FirstOrder FirstOrder.Language
35	open Lax185574.FirstOrderTypes
36
37	universe u
38
39	variable {V : Type u}
40
41	/-- `\|ATypes^G(X/Y)\|`: the number of atomic types over `Y`, in the graph
42	`G`, of the vertices of `X`. -/
43	noncomputable def atomicTypeCount (G : SimpleGraph V) (X Y : Set V) : ℕ :=
44	@typeCountOver Language.graph V G.structure 1 0 X Y
45
46	/-- The three atomic types of a pair of vertices in a graph, the set Π. -/
47	inductive PairType
48	/-- The type `x = y`. -/
49	\| eq
50	/-- The type `x ≠ y ∧ E(x, y)`. -/
51	\| adj
52	/-- The type `x ≠ y ∧ ¬E(x, y)`. -/
53	\| nonAdj
54	deriving DecidableEq
55
56	/-- There are three atomic types of pairs. -/
57	instance : Fintype PairType :=
58	⟨{.eq, .adj, .nonAdj}, fun x => by cases x <;> decide⟩
59
60	open Classical in
61	/-- The atomic type of the pair `(u, v)` in the graph `G`. -/
62	noncomputable def pairType (G : SimpleGraph V) (u v : V) : PairType :=
63	if u = v then .eq else if G.Adj u v then .adj else .nonAdj
64
65	/-- `atp(v/p̄)`, as an element of `Π^s`: its `i`-th component is the
66	atomic type of the pair `(v, pᵢ)`. -/
67	noncomputable def atomicTypeOver (G : SimpleGraph V) {s : ℕ} (p : Fin s → V)
68	(v : V) : Fin s → PairType :=
69	fun i => pairType G v (p i)
70
71	end Lax185574.AtomicTypes
72

defLax185574.GaifmanGraph

Gaifman graph, distances, balls and induced substructures

The Gaifman graph of a relational structure A with domain V has vertex set V. Two distinct elements are adjacent if they occur together in some tuple of some relation of A. For a structure with unary and binary relations, these are the pairs uv such that (u, v) or (v, u) lies in a binary relation. The distance dist^A(u, v) is the distance in the Gaifman graph, and Ball^A_r(ā) is the set of elements at distance at most r from some entry of the tuple ā.

For a set B of elements of a relational structure A, the induced substructure A[B] has domain B, and each relation of A is restricted to B. The paper uses A[B] without defining it.

1	import Mathlib.ModelTheory.Basic
2	import Mathlib.Combinatorics.SimpleGraph.Walk.Basic
3
	… module docstring, 25 lines
29
30	namespace Lax185574.GaifmanGraph
31
32	open FirstOrder FirstOrder.Language
33
34	universe u v z
35
36	variable {L : Language.{u, v}} {V : Type z} [L.Structure V]
37
38	variable (L) in
39	/-- The Gaifman graph: distinct elements are adjacent if they occur
40	together in a tuple of some relation. -/
41	def gaifmanGraph : SimpleGraph V :=
42	SimpleGraph.fromRel fun a b =>
43	∃ (l : ℕ) (R : L.Relations l) (x : Fin l → V),
44	Structure.RelMap R x ∧ a ∈ Set.range x ∧ b ∈ Set.range x
45
46	/-- The vertices `u` and `v` of the graph `G` are within distance `d`:
47	some walk from `u` to `v` has length at most `d`. -/
48	def WithinDist {W : Type*} (G : SimpleGraph W) (d : ℕ) (u v : W) : Prop :=
49	∃ p : G.Walk u v, p.length ≤ d
50
51	variable (L) in
52	/-- `Ball^A_r(ā)`: the elements within distance `r` of some entry of the
53	tuple `a` in the Gaifman graph. -/
54	def ball (r : ℕ) {k : ℕ} (a : Fin k → V) : Set V :=
55	{b \| ∃ i, WithinDist (gaifmanGraph L (V := V)) r (a i) b}
56
57	/-- The induced substructure `A[B]` of a relational structure: the
58	relations of `A`, restricted to `B`. -/
59	@[implicit_reducible]
60	def induced [L.IsRelational] (B : Set V) : L.Structure B where
61	funMap f := isEmptyElim f
62	RelMap R x := Structure.RelMap R (fun i => (x i : V))
63
64	end Lax185574.GaifmanGraph
65

defLax185574.Flips

Flips and flip metrics

For a graph G and a partition 𝒫 of V ≔ V(G), a 𝒫-flip of G is a graph H with V(H) = V such that for every pair X, Y ∈ 𝒫 (possibly X = Y), either H[X, Y] = G[X, Y] or H[X, Y] = Ḡ[X, Y]. If |𝒫| ≤ s, then H is an s-flip of G. The associated flip metric and its balls are

dist_𝒫(u, v) ≔ max { dist^H(u, v) : H is a 𝒫-flip of G }, Ball^𝒫_r(v) ≔ { u : dist_𝒫(u, v) ≤ r } = ⋂ { Ball^H_r(v) : H is a 𝒫-flip of G }.

As a shorthand, for a graph G and a set S ⊆ V(G), a 𝒫S-flip of G is called an S-flip, and dist_S^G ≔ dist{𝒫_S} and Ball^S_r ≔ Ball^{𝒫_S}_r. Here 𝒫_S is the partition into atomic types over S, see $Lax185574.AtomicTypes$ and $Lax185574.Partitions$ .

1	import Lax185574.Partitions
2	import Lax185574.GaifmanGraph
3
	… module docstring, 36 lines
40
41	namespace Lax185574.Flips
42
43	open Lax185574.Partitions Lax185574.GaifmanGraph
44
45	universe z
46
47	variable {V : Type z}
48
49	/-- `H` is a `𝒫`-flip of `G`: for every pair of parts `𝒫(a)`, `𝒫(b)`,
50	adjacency in `H` between distinct vertices of these parts either agrees
51	with adjacency in `G` throughout, or with non-adjacency in `G`
52	throughout. -/
53	def IsFlip (G : SimpleGraph V) (P : Setoid V) (H : SimpleGraph V) : Prop :=
54	∀ a b : V,
55	(∀ x y : V, P x a → P y b → x ≠ y → (H.Adj x y ↔ G.Adj x y)) ∨
56	(∀ x y : V, P x a → P y b → x ≠ y → (H.Adj x y ↔ ¬ G.Adj x y))
57
58	/-- `dist_𝒫(u, v) ≤ r`: in every `𝒫`-flip of `G`, some walk from `u`
59	to `v` has length at most `r`. -/
60	def FlipWithinDist (G : SimpleGraph V) (P : Setoid V) (r : ℕ) (u v : V) : Prop :=
61	∀ H : SimpleGraph V, IsFlip G P H → WithinDist H r u v
62
63	/-- `Ball^𝒫_r(v)`: the vertices within distance `r` of `v` in every
64	`𝒫`-flip of `G`. -/
65	def flipBall (G : SimpleGraph V) (P : Setoid V) (r : ℕ) (v : V) : Set V :=
66	{u \| FlipWithinDist G P r v u}
67
68	end Lax185574.Flips
69

defLax185574.ConstructionWidth

lem✓Lax185574.SeparatingTypesTuples

⊢Lax185574Proofs.TypeBound.typeCountOver_le
- thm✓Lax185574.ClosureTheoremTuples
- lem✓Lax185574.SeparatingTypesTuples
→
thm✓Lax185574.TypeBound
The proof in the paper, with the padding step replaced by a split of each tuple into its entries outside $U$ and its entries inside $U$ . Let $r = r(q)$ be the separation radius. For each $k' ≤ k$ , the closure theorem for tuples gives polynomially many $s$ -flips $H$ of $G$ such that every $k'$ -tuple outside $U$ is at distance more than $r$ from $U$ in one of them. A flip $H$ is undone by a toggle on at most $s$ parts, so the edges of $G$ are quantifier-free definable in $H$ expanded by the colors and by predicates for the parts, and the type of a tuple in this expansion $H⁺$ determines its type in $G⁺$ . A $k$ -tuple $v̄$ is a rearrangement of ā ū with ā outside $U$ and ū inside $U$ , and its type is determined by the type of ā ū and the positions. For fixed positions, ū, and $H$ , the tuples ā far from $U$ in $H$ realize at most $T(q, k', c + s)$ types in $H⁺$ . Summing over at most $2^k$ position sets, $(|U| + 1)^k$ tuples ū and the flips gives the bound, whose exponent does not depend on $c$ .

The argument is carried out for the graph classes of the archive and their monadic dependence, and transferred to the graph classes used here.

Lax Lean Archive

First-Order Model Checking on Monadically Dependent Graph Classes

Settings

Your comments

1	import Lax185574.DefinableFlips
2
	… module docstring, 16 lines
19
20	namespace Lax185574.DefinableFlipTransitivity
21
22	open Lax185574.DefinableFlips
23
24	universe u
25
26	/-- Transitivity of definable flips. An `s₂`-definable flip of an
27	`s₁`-definable flip of `G₀` is an `(s₁ + s₂)`-definable flip of `G₀`. -/
28	axiom isDefinableFlip_trans {V : Type u} {G₀ G₁ G₂ : SimpleGraph V}
29	{s₁ s₂ : ℕ} (h₁ : IsDefinableFlip G₀ s₁ G₁) (h₂ : IsDefinableFlip G₁ s₂ G₂) :
30	IsDefinableFlip G₀ (s₁ + s₂) G₂
31
32	end Lax185574.DefinableFlipTransitivity
33