Lax3.Locality

Locality theorem for distance logic

concepts/Lax3/Locality.lean · lax-3

proven

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax3.Locality

⊢Lax3Proofs.Assembly.locality

Theorem

Every formula of distance logic of distance rank (k, q) is equivalent to a boolean combination of local formulas and scatter sentences, all of distance rank (k, q). This is the locality theorem of the source note (arXiv:2606.23180, Theorem 1), in the spirit of Gaifman's locality theorem and of the locality theorem of Grohe, Kreutzer and Siebertz: unrestricted quantification is eliminated in favour of quantification inside a bounded neighborhood of the free variables, plus finitely many global assertions of the form "there are t pairwise far apart vertices satisfying β". What distinguishes this version, and what makes it usable, is that the rewriting does not increase the rank — and the rank it preserves, distance rank, controls the radii of everything the resulting formulas mention.

The theorem holds for every scatter choice; which one is fixed is invisible to the statement and decisive for the algorithm, which evaluates scatter sentences by running the greedy process. The companion statement $Lax3.NormalForm$ — the analogue of Gaifman's normal form — instantiates the maximum-size choice and writes the scatter sentences out in the logic itself.

Lean source view on GitHub

1	import Lax3.ScatterSentences
2
3	/-!
4	---
5	title: Locality theorem for distance logic
6	type: theorem
7	---
8	Every formula of distance logic of distance rank (k, q) is
9	equivalent to a boolean combination of local formulas and scatter
10	sentences, all of distance rank (k, q). This is the locality
11	theorem of the source note (arXiv:2606.23180, Theorem 1), in the spirit
12	of Gaifman's locality theorem and of the locality theorem of Grohe,
13	Kreutzer and Siebertz: unrestricted quantification is eliminated in
14	favour of quantification inside a bounded neighborhood of the free
15	variables, plus finitely many global assertions of the form "there are
16	t pairwise far apart vertices satisfying β". What distinguishes this
17	version, and what makes it usable, is that the rewriting does not
18	increase the rank — and the rank it preserves, distance rank, controls
19	the radii of everything the resulting formulas mention.
20
21	The theorem holds for every scatter choice; which one is fixed is
22	invisible to the statement and decisive for the algorithm, which
23	evaluates scatter sentences by running the greedy process. The
24	companion statement `Lax3.NormalForm` — the analogue of Gaifman's
25	normal form — instantiates the maximum-size choice and writes the
26	scatter sentences out in the logic itself.
27
28	# Formalization notes
29
30	The boolean combination is reified: `BC α` is the type of boolean
31	combinations of atoms drawn from `α`, with an evaluation map and a list
32	of the atoms occurring in it. That list is what carries the side
33	conditions of the theorem — "all of distance rank (k, q)" is a
34	statement about the atoms of the combination, and a bare `Prop`-level
35	equivalence could not express it. Atoms are the sum type of formulas
36	and scatter sentences, so one boolean combination mixes the two kinds
37	and `Sum.elim` supplies their two evaluations.
38
39	Effectiveness is not part of this claim: it asserts that the boolean
40	combination exists. `Lax3Proofs.LocalityFun.localityBC` consumes this
41	existential using `Classical.choose`, fixing one decomposition for the
42	scatter choice, formula and ranks before the input graph or environment
43	is supplied. Proof irrelevance makes that choice independent of the
44	rank witness. The model-checking schedule uses this fixed decomposition.
45	The headline theorem quantifies over the graph class, formula and
46	positive exponent, then asserts the existence of a word-RAM program and
47	time bounds that work for every input graph. This quantifier order lets
48	the decomposition be fixed with those parameters; it does not assert a
49	procedure that computes the program uniformly from them.
50
51	The statement is an `axiom` on this concept surface, discharged by
52	`Lax3Proofs.Assembly.locality` in the proofs package. The normal-form
53	corollary and the model-checking decomposition consume this concept
54	interface, whose proof is tracked as a separate dependency. The proofs
55	package also provides the chosen decomposition and its specifications
56	in `Lax3Proofs.LocalityFun` for consumers needing a fixed function.
57	-/
58
59	namespace Lax3.Locality
60
61	open Lax3.ColoredGraphs Lax3.DistFO Lax3.ScatterSentences
62
63	universe u
64
65	/-- Boolean combinations of atoms drawn from `α`. Disjunction and
66	implication are the usual abbreviations; the empty combination is
67	`tru`. -/
68	inductive BC (α : Type u) : Type u
69	/-- An atom. -/
70	\| atom (a : α) : BC α
71	/-- The empty combination, always true. -/
72	\| tru : BC α
73	/-- Negation. -/
74	\| not (b : BC α) : BC α
75	/-- Conjunction. -/
76	\| and (b c : BC α) : BC α
77
78	/-- The truth value of a boolean combination, given a truth value for
79	each atom. -/
80	def BC.eval {α : Type u} (v : α → Prop) : BC α → Prop
81	\| .atom a => v a
82	\| .tru => True
83	\| .not b => ¬ BC.eval v b
84	\| .and b c => BC.eval v b ∧ BC.eval v c
85
86	/-- The atoms occurring in a boolean combination, with multiplicity. -/
87	def BC.atoms {α : Type u} : BC α → List α
88	\| .atom a => [a]
89	\| .tru => []
90	\| .not b => BC.atoms b
91	\| .and b c => BC.atoms b ++ BC.atoms c
92
93	variable {L : ℕ}
94
95	/-- Locality theorem (Theorem 1 of arXiv:2606.23180). Fix a scatter
96	choice. Every formula of distance rank `(k, q)` is equivalent to a
97	boolean combination of local formulas of distance rank `(k, q)` and
98	scatter sentences of distance rank `(k, q)`: there is a boolean
99	combination whose formula atoms are all local of distance rank `(k, q)`,
100	whose scatter-sentence atoms all have distance rank `(k, q)`, and which
101	has the same truth value as the formula in every finite colored graph
102	under every environment. -/
103	axiom locality (choice : ScatterChoice) {k q : ℕ} (φ : DistFO L k)
104	(hφ : DistFO.DRank k q φ) :
105	∃ b : BC (DistFO L k ⊕ ScatterSentence L),
106	(∀ ψ : DistFO L k, Sum.inl ψ ∈ b.atoms → DistFO.IsLocal ψ ∧ DistFO.DRank k q ψ) ∧
107	(∀ σ : ScatterSentence L, Sum.inr σ ∈ b.atoms → σ.DRank k q) ∧
108	∀ (n : ℕ) (G : SimpleGraph (Fin n)) (col : Coloring n L) (m : Fin k → Fin n),
109	DistFO.Sat G col m φ ↔
110	b.eval (Sum.elim (DistFO.Sat G col m) (ScatterSentence.Sat choice G col))
111
112	end Lax3.Locality
113

Show Proof

Formalization notes

The boolean combination is reified: $BC α$ is the type of boolean combinations of atoms drawn from $α$ , with an evaluation map and a list of the atoms occurring in it. That list is what carries the side conditions of the theorem — "all of distance rank (k, q)" is a statement about the atoms of the combination, and a bare $Prop$ -level equivalence could not express it. Atoms are the sum type of formulas and scatter sentences, so one boolean combination mixes the two kinds and $Sum.elim$ supplies their two evaluations.

Effectiveness is not part of this claim: it asserts that the boolean combination exists. $Lax3Proofs.LocalityFun.localityBC$ consumes this existential using $Classical.choose$ , fixing one decomposition for the scatter choice, formula and ranks before the input graph or environment is supplied. Proof irrelevance makes that choice independent of the rank witness. The model-checking schedule uses this fixed decomposition. The headline theorem quantifies over the graph class, formula and positive exponent, then asserts the existence of a word-RAM program and time bounds that work for every input graph. This quantifier order lets the decomposition be fixed with those parameters; it does not assert a procedure that computes the program uniformly from them.

The statement is an $axiom$ on this concept surface, discharged by $Lax3Proofs.Assembly.locality$ in the proofs package. The normal-form corollary and the model-checking decomposition consume this concept interface, whose proof is tracked as a separate dependency. The proofs package also provides the chosen decomposition and its specifications in $Lax3Proofs.LocalityFun$ for consumers needing a fixed function.

Builds on

Lax3.ScatterSentences

Used by

Lax3.NormalForm

From Mathlib

none

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