Lax57.GraphDefinitions

Finite graph notions for the five-vertex path theorem

concepts/Lax57/GraphDefinitions.lean · lax-57

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

This module defines the five-vertex path $P_5$ , its complement (the house), and the notions of sparsity, restrictedness, and blockades used throughout the formalization. For a positive integer $E$ , $ESparse$ means maximum degree at most $|G|/E$ , while $WeaklyESparse$ is the corresponding edge-density condition with its denominator cleared.

Lean source view on GitHub

1	import Lax54.GraphDefinitions
2	import Mathlib.Combinatorics.SimpleGraph.Density
3	import Mathlib.Combinatorics.SimpleGraph.Hasse
4
5	/-!
6	---
7	title: Finite graph notions for the five-vertex path theorem
8	type: definition
9	---
10	This module defines the five-vertex path $P_5$ , its complement (the house),
11	and the notions of sparsity, restrictedness, and blockades used throughout
12	the formalization. For a positive integer $E$ , `ESparse` means maximum degree
13	at most $\|G\|/E$ , while `WeaklyESparse` is the corresponding edge-density
14	condition with its denominator cleared.
15	-/
16
17	open Finset
18	open scoped SimpleGraph
19
20	namespace Lax57.GraphDefinitions
21
22	universe u
23
24	/-- The path on five vertices. -/
25	abbrev P5 : SimpleGraph (Fin 5) := SimpleGraph.pathGraph 5
26
27	/-- The house graph, namely the complement of the five-vertex path. -/
28	abbrev House : SimpleGraph (Fin 5) := P5ᶜ
29
30	/-- A graph has no induced copy of the five-vertex path. -/
31	def IsP5Free {V : Type u} (G : SimpleGraph V) : Prop :=
32	¬ P5 ⊴ G
33
34	/-- A graph has no induced copy of the house. -/
35	def IsHouseFree {V : Type u} (G : SimpleGraph V) : Prop :=
36	¬ House ⊴ G
37
38	/-- The largest cardinality of a clique or stable set. -/
39	noncomputable abbrev homogeneousNumber {V : Type u} (G : SimpleGraph V) : ℕ :=
40	Lax54.GraphDefinitions.homogeneousNumber G
41
42	/-- The product of the clique and independence numbers. -/
43	noncomputable abbrev kappa {V : Type u} (G : SimpleGraph V) : ℕ :=
44	Lax54.GraphDefinitions.kappa G
45
46	/-- `q`-criticality for the product `ω(G)α(G)`. -/
47	abbrev IsQCritical {V : Type u} [Fintype V] (q : ℕ) (G : SimpleGraph V) : Prop :=
48	Lax54.GraphDefinitions.IsQCritical q G
49
50	/-- The neighbors of `v` lying in a prescribed finite set. -/
51	def neighborsIn {V : Type u} [DecidableEq V] (G : SimpleGraph V)
52	[DecidableRel G.Adj] (A : Finset V) (v : V) : Finset V :=
53	A.filter fun x ↦ G.Adj v x
54
55	/-- `B` is `1/E`-sparse to `A`, with the denominator cleared. -/
56	def ESparseTo {V : Type u} [DecidableEq V] (G : SimpleGraph V)
57	[DecidableRel G.Adj] (E : ℕ) (B A : Finset V) : Prop :=
58	∀ b ∈ B, E * (neighborsIn G A b).card ≤ A.card
59
60	/-- The pair `(A,B)` has edge density at most `1/E`. -/
61	def WeaklyESparse {V : Type u} [DecidableEq V] (G : SimpleGraph V)
62	[DecidableRel G.Adj] (E : ℕ) (A B : Finset V) : Prop :=
63	E * (G.interedges A B).card ≤ A.card * B.card
64
65	/-- The graph induced by `A` has maximum degree at most `\|A\|/E`. -/
66	def ESparse {V : Type u} [DecidableEq V] (G : SimpleGraph V)
67	[DecidableRel G.Adj] (E : ℕ) (A : Finset V) : Prop :=
68	∀ v : {x : V // x ∈ A}, E * (G.induce (A : Set V)).degree v ≤ A.card
69
70	/-- One of the two complementary graphs induced by `A` is `1/E`-sparse. -/
71	def ERestricted {V : Type u} [DecidableEq V] (G : SimpleGraph V)
72	[DecidableRel G.Adj] (E : ℕ) (A : Finset V) : Prop :=
73	ESparse G E A ∨ ESparse Gᶜ E A
74
75	/-- A sequence of pairwise disjoint vertex blocks. -/
76	structure Blockade {V : Type u} [DecidableEq V] (k : ℕ) where
77	block : Fin k → Finset V
78	disjoint : ∀ {i j : Fin k}, i ≠ j → Disjoint (block i) (block j)
79
80	/-- Every two different blocks are complete to one another. -/
81	def Blockade.IsComplete {V : Type u} [DecidableEq V] {k : ℕ}
82	(G : SimpleGraph V) (B : Blockade (V := V) k) : Prop :=
83	∀ {i j : Fin k}, i ≠ j →
84	∀ x ∈ B.block i, ∀ y ∈ B.block j, G.Adj x y
85
86	/-- Every two different blocks are anticomplete to one another. -/
87	def Blockade.IsAnticomplete {V : Type u} [DecidableEq V] {k : ℕ}
88	(G : SimpleGraph V) (B : Blockade (V := V) k) : Prop :=
89	∀ {i j : Fin k}, i ≠ j →
90	∀ x ∈ B.block i, ∀ y ∈ B.block j, ¬ G.Adj x y
91
92	/-- Each pair of blocks is either complete or anticomplete. -/
93	def Blockade.IsPure {V : Type u} [DecidableEq V] {k : ℕ}
94	(G : SimpleGraph V) (B : Blockade (V := V) k) : Prop :=
95	∀ {i j : Fin k}, i ≠ j →
96	((∀ x ∈ B.block i, ∀ y ∈ B.block j, G.Adj x y) ∨
97	(∀ x ∈ B.block i, ∀ y ∈ B.block j, ¬ G.Adj x y))
98
99	/-- A complete or anticomplete blockade. -/
100	def Blockade.IsUniform {V : Type u} [DecidableEq V] {k : ℕ}
101	(G : SimpleGraph V) (B : Blockade (V := V) k) : Prop :=
102	B.IsComplete G ∨ B.IsAnticomplete G
103
104	/-- The directed vertexwise sparsity condition of the paper. -/
105	def Blockade.IsESparse {V : Type u} [DecidableEq V] {k : ℕ}
106	(G : SimpleGraph V) [DecidableRel G.Adj] (E : ℕ)
107	(B : Blockade (V := V) k) : Prop :=
108	∀ {i j : Fin k}, i < j → ESparseTo G E (B.block j) (B.block i)
109
110	/-- Each pair is complete or weakly `1/E`-sparse. -/
111	def Blockade.IsSemisparse {V : Type u} [DecidableEq V] {k : ℕ}
112	(G : SimpleGraph V) [DecidableRel G.Adj] (E : ℕ)
113	(B : Blockade (V := V) k) : Prop :=
114	∀ {i j : Fin k}, i ≠ j →
115	((∀ x ∈ B.block i, ∀ y ∈ B.block j, G.Adj x y) ∨
116	WeaklyESparse G E (B.block i) (B.block j))
117
118	/-- All blocks have size at least `\|V(G)\| / loss`. -/
119	def Blockade.HasWidthLoss {V : Type u} [Fintype V] [DecidableEq V]
120	{k : ℕ} (B : Blockade (V := V) k) (loss : ℕ) : Prop :=
121	∀ i : Fin k, Fintype.card V ≤ loss * (B.block i).card
122
123	/-- Every block lies in a prescribed ambient vertex set. -/
124	def Blockade.IsInside {V : Type u} [DecidableEq V] {k : ℕ}
125	(B : Blockade (V := V) k) (S : Finset V) : Prop :=
126	∀ i : Fin k, B.block i ⊆ S
127
128	/-- A uniform blockade with polynomial width and controlled length. -/
129	def HasUniformBlockade {V : Type u} [Fintype V] [DecidableEq V]
130	(G : SimpleGraph V) (E a : ℕ) : Prop :=
131	∃ (k : ℕ) (B : Blockade (V := V) k),
132	2 ≤ k ∧ k ≤ E ∧ B.IsUniform G ∧ B.HasWidthLoss (k ^ a)
133
134	end Lax57.GraphDefinitions
135

Builds on

Lax54.GraphDefinitions

Used by

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

Finite graph notions for the five-vertex path theorem

Flags

Flag this concept