Lax3.ScatterSentences

Scatter sentences

concepts/Lax3/ScatterSentences.lean · lax-3

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

A set of vertices is r-scattered if its members have pairwise distance larger than r. A scatter sentence asserts that a distinguished r-scattered set of the vertices satisfying a one-variable formula β has at least t elements. Which scattered set is distinguished is the content of a scatter choice: for each graph, radius and vertex set it names a number that is the size of some inclusion-wise maximal r-scattered subset of that set. The maximum size of a scattered subset of the set, and the size the greedy process produces when it runs through the vertices in order and takes every vertex it can, are both scatter choices.

The locality theorem of $Lax3.Locality$ rewrites a formula into a boolean combination of local formulas and scatter sentences. Scatter sentences of distance rank (k, q) are those whose parameters obey the source's schedule: at most k + q witnesses, a local β of distance rank (k+i, q−i) for some 1 ≤ i ≤ q, and a radius between 4ρ⁻(k+i, q−i) and 9^(k+i)ρ⁻(k+i, q−i). The lower bound makes β semantically (r/4)-local, which is what the proof of the theorem consumes; the upper bound keeps the radius below ρ⁻(k, q), which is what keeps the rank from growing.

This is §2.1 of the source note (arXiv:2606.23180), specialized to the finite colored graphs of $Lax3.ColoredGraphs$ .

Lean source view on GitHub

1	import Lax3.DistFO
2	import Lax12.UniformQuasiWideness
3	import Mathlib.Data.Set.Card
4	import Mathlib.Order.Minimal
5
6	/-!
7	---
8	title: Scatter sentences
9	type: definition
10	---
11	A set of vertices is r-scattered if its members have pairwise
12	distance larger than r. A scatter sentence asserts that a
13	distinguished r-scattered set of the vertices satisfying a
14	one-variable formula β has at least t elements. Which scattered set
15	is distinguished is the content of a scatter choice: for each graph,
16	radius and vertex set it names a number that is the size of some
17	inclusion-wise maximal r-scattered subset of that set. The maximum
18	size of a scattered subset of the set, and the size the greedy process
19	produces when it runs through the vertices in order and takes every
20	vertex it can, are both scatter choices.
21
22	The locality theorem of `Lax3.Locality` rewrites a formula into a
23	boolean combination of local formulas and scatter sentences. Scatter
24	sentences of distance rank (k, q) are those whose parameters obey
25	the source's schedule: at most k + q witnesses, a local β of
26	distance rank (k+i, q−i) for some 1 ≤ i ≤ q, and a radius
27	between 4ρ⁻(k+i, q−i) and 9^(k+i)ρ⁻(k+i, q−i). The
28	lower bound makes β semantically (r/4)-local, which is what the proof
29	of the theorem consumes; the upper bound keeps the radius below
30	ρ⁻(k, q), which is what keeps the rank from growing.
31
32	This is §2.1 of the source note (arXiv:2606.23180), specialized to the
33	finite colored graphs of `Lax3.ColoredGraphs`.
34
35	# Formalization notes
36
37	The scatter choice is per graph, radius and vertex set; the source's is
38	per structure, radius and formula β. The two agree wherever a scatter
39	sentence is evaluated, since the vertex set involved is always
40	{a : β(a) holds}, and the coarser form is strictly stronger: it
41	forces the same value for two formulas defining the same set, and it is
42	uniform in the coloring, so a scatter value cannot change when colors
43	are added that β does not mention. Both are properties the algorithm
44	needs and neither is available from the source's form. The dependence
45	on the graph is genuine and stays.
46
47	"r-scattered" is Lax12's `DistIndependent`: a set is distance-r
48	independent in `G` when every walk between two distinct members is
49	longer than r, which is the source's "pairwise distance larger than
50	r" in the Gaifman graph, since the Gaifman graph of a colored graph
51	is the graph. It is used as it stands and not restated here.
52	Inclusion-wise maximality is mathlib's `Maximal`, over the property of
53	being a scattered subset of the given set.
54
55	Over `Fin n` every vertex set is finite, so the source's value ∞ — for
56	structures with arbitrarily large scattered subsets — cannot arise and
57	is not carried; `ScatterChoice.size` is ℕ-valued.
58
59	The distance rank of a scatter sentence is the source's condition
60	(2)/(eq:scatter-radius) verbatim, with the bound t ≤ k + q stated
61	alongside the radius window rather than in the surrounding prose.
62	Nothing here requires q ≥ 1: for q = 0 the condition 1 ≤ i ≤ q
63	is unsatisfiable, so no scatter sentence has distance rank (k, 0),
64	which is the source's convention made into a fact.
65	-/
66
67	namespace Lax3.ScatterSentences
68
69	open Lax3.ColoredGraphs Lax3.DistFO Lax12.UniformQuasiWideness
70
71	/-- A choice of scatter values: for every graph `G`, radius `r` and
72	vertex set `X`, a number `size G r X` which is the cardinality of some
73	inclusion-wise maximal `r`-scattered subset of `X`. This is the
74	source's "fix arbitrarily and once and for all a value `s`", made a
75	parameter: every statement about scatter sentences holds for every
76	choice. -/
77	structure ScatterChoice where
78	/-- The chosen scatter value of a graph, radius and vertex set. -/
79	size : ∀ {n : ℕ}, SimpleGraph (Fin n) → ℕ → Set (Fin n) → ℕ
80	/-- The chosen value is realized by an inclusion-wise maximal
81	`r`-scattered subset of `X`. -/
82	spec : ∀ {n : ℕ} (G : SimpleGraph (Fin n)) (r : ℕ) (X : Set (Fin n)),
83	∃ S : Set (Fin n), S ⊆ X ∧
84	Maximal (fun T => T ⊆ X ∧ DistIndependent G r T) S ∧ S.ncard = size G r X
85
86	/-- A scatter sentence: there is an `r`-scattered set of `t` vertices
87	satisfying the one-variable formula `β`, in the sense fixed by a
88	scatter choice. -/
89	structure ScatterSentence (L : ℕ) where
90	/-- The radius at which the witnesses are scattered. -/
91	r : ℕ
92	/-- The one-variable formula the witnesses satisfy. -/
93	β : DistFO L 1
94	/-- The number of witnesses demanded. -/
95	t : ℕ
96
97	variable {L n : ℕ}
98
99	/-- The scatter sentence holds in the colored graph `(G, col)` when the
100	chosen scatter value of the set defined by `β`, at radius `r`, is at
101	least `t`. -/
102	def ScatterSentence.Sat (choice : ScatterChoice) (G : SimpleGraph (Fin n))
103	(col : Coloring n L) (σ : ScatterSentence L) : Prop :=
104	σ.t ≤ choice.size G σ.r {a \| DistFO.Sat G col (fun _ => a) σ.β}
105
106	/-- The scatter sentence has distance rank `(k, q)`: it demands at most
107	`k + q` witnesses, and for some `1 ≤ i ≤ q` its formula `β` is local of
108	distance rank `(k + i, q - i)` and its radius lies in the source's
109	window `4ρ⁻(k + i, q - i) ≤ r ≤ 9 ^ (k + i) · ρ⁻(k + i, q - i)`. -/
110	def ScatterSentence.DRank (k q : ℕ) (σ : ScatterSentence L) : Prop :=
111	σ.t ≤ k + q ∧ ∃ i, 1 ≤ i ∧ i ≤ q ∧ DistFO.IsLocal σ.β ∧
112	DistFO.DRank (k + i) (q - i) σ.β ∧
113	4 * rhoMinus (k + i) (q - i) ≤ σ.r ∧ σ.r ≤ 9 ^ (k + i) * rhoMinus (k + i) (q - i)
114
115	end Lax3.ScatterSentences
116

Formalization notes

The scatter choice is per graph, radius and vertex set; the source's is per structure, radius and formula β. The two agree wherever a scatter sentence is evaluated, since the vertex set involved is always {a : β(a) holds}, and the coarser form is strictly stronger: it forces the same value for two formulas defining the same set, and it is uniform in the coloring, so a scatter value cannot change when colors are added that β does not mention. Both are properties the algorithm needs and neither is available from the source's form. The dependence on the graph is genuine and stays.

"r-scattered" is Lax12's $DistIndependent$ : a set is distance-r independent in $G$ when every walk between two distinct members is longer than r, which is the source's "pairwise distance larger than r" in the Gaifman graph, since the Gaifman graph of a colored graph is the graph. It is used as it stands and not restated here. Inclusion-wise maximality is mathlib's $Maximal$ , over the property of being a scattered subset of the given set.

Over $Fin n$ every vertex set is finite, so the source's value ∞ — for structures with arbitrarily large scattered subsets — cannot arise and is not carried; $ScatterChoice.size$ is ℕ-valued.

The distance rank of a scatter sentence is the source's condition (2)/(eq:scatter-radius) verbatim, with the bound t ≤ k + q stated alongside the radius window rather than in the surrounding prose. Nothing here requires q ≥ 1: for q = 0 the condition 1 ≤ i ≤ q is unsatisfiable, so no scatter sentence has distance rank (k, 0), which is the source's convention made into a fact.

Builds on

Used by

Lax3.Locality

From Mathlib

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

Scatter sentences

Flags

Flag this concept