Lax3.NormalForm

Normal form for distance logic

concepts/Lax3/NormalForm.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.

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

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.

Lean source view on GitHub

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

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