Normal form for distance logic

Lax3.NormalForm · concepts/Lax3/NormalForm.lean · lax-3

proven

Loading review…

Natural Language Statement

Theorem

For q ≥ 1, every formula of distance logic of distance rank (k, q) is equivalent to a boolean combination of local formulas of distance rank (k, q) and explicit sentences "there are t vertices, pairwise at distance more than r, all satisfying β", where t ≤ k + q, the formula β is local of distance rank (k+1, q−1), the radius satisfies r ≤ ρ⁻(k, q), and β is semantically (r/4)-local. This is Corollary 7 of the source note (arXiv:2606.23180), the analogue for distance logic of Gaifman's normal form: it is the locality theorem of $Lax3.Locality$ with the scatter sentences written out in the logic itself.

The step from the theorem to the corollary is the maximum-size scatter choice: with it, "the distinguished maximal scattered set has at least t elements" says no more and no less than "some r-scattered set of t vertices satisfies β", and the latter is a sentence of distance logic. No choice appears in the statement below, because after that replacement there is nothing left for one to be attached to.

Concept map

7 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

- thm✓Lax3.Locality
→
thm✓Lax3.NormalForm
⊢Lax3Proofs.Assembly.normalForm

Lean source view on GitHub

Show types on hover

1	import Lax3.Locality
2	import Mathlib.Data.List.FinRange
3
4	/-!
5	---
6	title: Normal form for distance logic
7	type: theorem
8	---
9	For q ≥ 1, every formula of distance logic of distance rank
10	(k, q) is equivalent to a boolean combination of local formulas
11	of distance rank (k, q) and explicit sentences "there are t
12	vertices, pairwise at distance more than r, all satisfying β", where
13	t ≤ k + q, the formula β is local of distance rank
14	(k+1, q−1), the radius satisfies r ≤ ρ⁻(k, q), and β is
15	semantically (r/4)-local. This is Corollary 7 of the source note
16	(arXiv:2606.23180), the analogue for distance logic of Gaifman's
17	normal form: it is the locality theorem of `Lax3.Locality` with the
18	scatter sentences written out in the logic itself.
19
20	The step from the theorem to the corollary is the maximum-size scatter
21	choice: with it, "the distinguished maximal scattered set has at least
22	t elements" says no more and no less than "some r-scattered set of
23	t vertices satisfies β", and the latter is a sentence of distance
24	logic. No choice appears in the statement below, because after that
25	replacement there is nothing left for one to be attached to.
26
27	# Formalization notes
28
29	`scatterFml` is the source's sentence (3) written out. Its distance
30	condition is "larger than r", the negation of the binary distance
31	atom "at most r" — the strict inequality of the source has no atom
32	of its own and needs none. The empty conjunction is `verum`, a formula
33	that holds in every colored graph, so `scatterFml` is defined at every
34	`t` including `0`, where it is vacuously true, as the source's
35	sentence is. `verum` costs one unrestricted quantifier, which no
36	statement here notices: nothing constrains the distance rank of
37	`scatterFml` itself, and the rank conditions of the normal form are
38	conditions on the parameters `r`, `t`, β. Placing β at each bound
39	variable is what `DistFO.rename` is for.
40
41	The locality radius of β is `σ.r / 4` in ℕ, which rounds down. That
42	makes the claim slightly stronger than the source's real-valued r/4
43	and it is still sound: the radius window of a scatter sentence of
44	distance rank (k, q) guarantees 4ρ⁻(k+i, q−i) ≤ r, so
45	ρ⁻(k+i, q−i) ≤ ⌊r/4⌋, and β is semantically
46	ρ⁻(k+i, q−i)-local.
47
48	The boolean combination reuses the `BC` reification and the
49	`ScatterSentence` record of the locality concept as the carrier of the
50	parameter triple (r, t, β); here the record is only data — its
51	satisfaction is not used, each atom being evaluated through
52	`scatterFml` instead. Effectiveness is deliberately absent, for the
53	reasons recorded in `Lax3.Locality`.
54	-/
55
56	namespace Lax3.NormalForm
57
58	open Lax3.ColoredGraphs Lax3.DistFO Lax3.ScatterSentences Lax3.Locality
59
60	variable {L : ℕ}
61
62	/-- A formula that holds in every colored graph under every
63	environment: no vertex differs from itself. -/
64	def verum {k : ℕ} : DistFO L k :=
65	.not (.exU (.not (.eq (Fin.last k) (Fin.last k))))
66
67	/-- The conjunction of a list of formulas; the empty conjunction is
68	`verum`. -/
69	def conj {k : ℕ} : List (DistFO L k) → DistFO L k
70	\| [] => verum
71	\| φ :: φs => .and φ (conj φs)
72
73	/-- `k` unrestricted quantifiers in front of a formula with `k` free
74	variables, leaving a sentence. -/
75	def exUs : {k : ℕ} → DistFO L k → DistFO L 0
76	\| 0, φ => φ
77	\| _ + 1, φ => exUs (.exU φ)
78
79	/-- The source's scatter sentence written out in distance logic: there
80	are `t` vertices, pairwise at distance larger than `r`, each satisfying
81	`β`. Distance larger than `r` is the negation of the binary distance
82	atom of radius `r`, and `β` is placed at each bound variable by
83	renaming. -/
84	def scatterFml (r t : ℕ) (β : DistFO L 1) : DistFO L 0 :=
85	exUs (conj
86	(((List.finRange t).flatMap fun i =>
87	(List.finRange t).filterMap fun j =>
88	if i = j then none else some (DistFO.not (DistFO.distLe r i j))) ++
89	(List.finRange t).map fun i => rename (fun _ : Fin 1 => i) β))
90
91	/-- Normal form for distance logic (Corollary 7 of
92	arXiv:2606.23180). For `q ≥ 1`, every formula of distance rank `(k, q)`
93	is equivalent to a boolean combination of local formulas of distance
94	rank `(k, q)` and sentences `scatterFml r t β` — there are `t` vertices,
95	pairwise at distance larger than `r`, all satisfying `β` — where
96	`t ≤ k + q`, the formula `β` is local of distance rank `(k + 1, q - 1)`,
97	the radius satisfies `r ≤ ρ⁻(k, q)`, and `β` is semantically
98	`r / 4`-local. -/
99	axiom normalForm {k q : ℕ} (hq : 1 ≤ q) (φ : DistFO L k) (hφ : DistFO.DRank k q φ) :
100	∃ b : BC (DistFO L k ⊕ ScatterSentence L),
101	(∀ ψ : DistFO L k, Sum.inl ψ ∈ b.atoms → DistFO.IsLocal ψ ∧ DistFO.DRank k q ψ) ∧
102	(∀ σ : ScatterSentence L, Sum.inr σ ∈ b.atoms →
103	σ.t ≤ k + q ∧ DistFO.IsLocal σ.β ∧ DistFO.DRank (k + 1) (q - 1) σ.β ∧
104	σ.r ≤ rhoMinus k q ∧ DistFO.SemanticallyLocal (σ.r / 4) σ.β) ∧
105	∀ (n : ℕ) (G : SimpleGraph (Fin n)) (col : Coloring n L) (m : Fin k → Fin n),
106	DistFO.Sat G col m φ ↔
107	b.eval (Sum.elim (DistFO.Sat G col m)
108	(fun σ => DistFO.Sat G col Fin.elim0 (scatterFml σ.r σ.t σ.β)))
109
110	end Lax3.NormalForm
111

Show Proof

Formalization notes

$scatterFml$ is the source's sentence (3) written out. Its distance condition is "larger than r", the negation of the binary distance atom "at most r" — the strict inequality of the source has no atom of its own and needs none. The empty conjunction is $verum$ , a formula that holds in every colored graph, so $scatterFml$ is defined at every $t$ including $0$ , where it is vacuously true, as the source's sentence is. $verum$ costs one unrestricted quantifier, which no statement here notices: nothing constrains the distance rank of $scatterFml$ itself, and the rank conditions of the normal form are conditions on the parameters $r$ , $t$ , β. Placing β at each bound variable is what $DistFO.rename$ is for.

The locality radius of β is $σ.r / 4$ in ℕ, which rounds down. That makes the claim slightly stronger than the source's real-valued r/4 and it is still sound: the radius window of a scatter sentence of distance rank (k, q) guarantees 4ρ⁻(k+i, q−i) ≤ r, so ρ⁻(k+i, q−i) ≤ ⌊r/4⌋, and β is semantically ρ⁻(k+i, q−i)-local.

The boolean combination reuses the $BC$ reification and the $ScatterSentence$ record of the locality concept as the carrier of the parameter triple (r, t, β); here the record is only data — its satisfaction is not used, each atom being evaluated through $scatterFml$ instead. Effectiveness is deliberately absent, for the reasons recorded in $Lax3.Locality$ .

Builds on

Lax3.Locality

Used by

none

From Mathlib

Mathlib.Data.List.FinRange

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Normal form for distance logic

Flags

Flag this concept

Natural Language Statement

Theorem

Lean source view on GitHub

Discussion

Settings

Your comments