Formalizing Structural Graph Theory in Lean 4

Dev/MonadicDependence/NowhereDenseBridge/Full.lean
1import Catalog.Sparsity.Preliminaries.Full
2import Catalog.Sparsity.NowhereDense.Full
3import Catalog.Sparsity.ShallowMinor.Full
4import Catalog.Sparsity.ShallowTopologicalMinor.Full
5import Catalog.Sparsity.Ramsey.Full
6import Catalog.Sparsity.MulticolorRamsey.Full
7import Dev.MonadicDependence.NowhereDense.Full
8import Dev.MonadicDependence.Subdivision.Full
9
10namespace Dev.MonadicDependence.NowhereDenseBridge
11
12open Catalog.Sparsity.Preliminaries
13open Catalog.Sparsity.ShallowMinor
14open Catalog.Sparsity.ShallowTopologicalMinor
15open Dev.MonadicDependence.Subdivision
16
17/-- Adjacency between two consecutive subdivision vertices on the same
18oriented edge of `subdividedClique N r`. -/
19private lemma subdividedClique_adj_subdivision
20 {N r : ℕ} (e : {p : Fin N × Fin N // p.1 < p.2})
21 (k k' : Fin r) (h : k.val + 1 = k'.val) :
22 (subdividedClique N r).Adj
23 (Sum.inr ⟨e, k⟩ : SubdividedCliqueVert N r)
24 (Sum.inr ⟨e, k'⟩ : SubdividedCliqueVert N r) := by
25 refine ⟨fun heq => ?_, Or.inl ⟨rfl, h⟩⟩
26 simp only [Sum.inr.injEq, Prod.mk.injEq] at heq
27 have : k.val = k'.val := congrArg Fin.val heq.2
28 omega
29
30/-- Adjacency between the last subdivision vertex of an oriented edge and
31its head principal vertex. -/
32private lemma subdividedClique_adj_principal_right
33 {N r : ℕ} (e : {p : Fin N × Fin N // p.1 < p.2})
34 (k : Fin r) (hk : k.val = r - 1) :
35 (subdividedClique N r).Adj
36 (Sum.inr ⟨e, k⟩ : SubdividedCliqueVert N r)
37 (Sum.inl e.1.2 : SubdividedCliqueVert N r) := by
38 refine ⟨?_, Or.inr (Or.inr ⟨rfl, hk⟩)⟩
39 intro heq; nomatch heq
40
41/-- Adjacency between the tail principal vertex of an oriented edge and
42its first subdivision vertex. -/
43private lemma subdividedClique_adj_principal_left
44 {N r : ℕ} (e : {p : Fin N × Fin N // p.1 < p.2})
45 (k : Fin r) (hk : k.val = 0) :
46 (subdividedClique N r).Adj
47 (Sum.inl e.1.1 : SubdividedCliqueVert N r)
48 (Sum.inr ⟨e, k⟩ : SubdividedCliqueVert N r) := by
49 refine ⟨?_, Or.inl (Or.inl ⟨rfl, hk⟩)⟩
50 intro heq; nomatch heq
51
52/-- The tail segment of a subdivided-clique edge path, starting at the
53subdivision vertex indexed by `k` and ending at the head principal
54vertex. -/
55private def subdivisionTailWalk :
56 {N : ℕ} → {r : ℕ} → (e : {p : Fin N × Fin N // p.1 < p.2}) → (k : Fin r) →
57 (subdividedClique N r).Walk (Sum.inr ⟨e, k⟩) (Sum.inl e.1.2)
58 | _, 0, _, k => k.elim0
59 | N, r' + 1, e, k =>
60 Fin.reverseInduction
61 (motive := fun (k : Fin (r' + 1)) =>
62 (subdividedClique N (r' + 1)).Walk
63 (Sum.inr ⟨e, k⟩ : SubdividedCliqueVert N (r' + 1))
64 (Sum.inl e.1.2))
65 (SimpleGraph.Walk.cons
66 (subdividedClique_adj_principal_right e (Fin.last r') rfl)
67 SimpleGraph.Walk.nil)
68 (fun i w =>
69 SimpleGraph.Walk.cons
70 (subdividedClique_adj_subdivision e i.castSucc i.succ rfl)
71 w)
72 k
73
74private lemma subdivisionTailWalk_length
75 {N r : ℕ} (e : {p : Fin N × Fin N // p.1 < p.2}) (k : Fin r) :
76 (subdivisionTailWalk e k).length = r - k.val := by
77 match r, k with
78 | r' + 1, k =>
79 induction k using Fin.reverseInduction with
80 | last =>
81 simp [subdivisionTailWalk]
82 | cast i ih =>
83 simp [subdivisionTailWalk] at ih ⊢
84 have hi : i.val < r' := i.isLt
85 omega
86
87private lemma mem_subdivisionTailWalk_support
88 {N r : ℕ} (e : {p : Fin N × Fin N // p.1 < p.2}) (k : Fin r)
89 {x : SubdividedCliqueVert N r}
90 (hx : x ∈ (subdivisionTailWalk e k).support) :
91 x = .inl e.1.2 ∨ ∃ j : Fin r, k.val ≤ j.val ∧ x = .inr ⟨e, j⟩ := by
92 revert x
93 match r, k with
94 | r' + 1, k =>
95 induction k using Fin.reverseInduction with
96 | last =>
97 intro x hx
98 simp [subdivisionTailWalk] at hx
99 rcases hx with rfl | rfl
100 · exact Or.inr ⟨Fin.last r', le_rfl, rfl⟩
101 · exact Or.inl rfl
102 | cast i ih =>
103 intro x hx
104 simp [subdivisionTailWalk] at hx
105 rcases hx with rfl | hx
106 · exact Or.inr ⟨i.castSucc, le_rfl, rfl⟩
107 · rcases ih hx with h | ⟨j, hj, hxj⟩
108 · exact Or.inl h
109 · refine Or.inr ⟨j, ?_, hxj⟩
110 have : i.castSucc.val + 1 = i.succ.val := rfl
111 omega
112
113private lemma subdivisionTailWalk_isPath
114 {N r : ℕ} (e : {p : Fin N × Fin N // p.1 < p.2}) (k : Fin r) :
115 (subdivisionTailWalk e k).IsPath := by
116 match r, k with
117 | r' + 1, k =>
118 induction k using Fin.reverseInduction with
119 | last =>
120 simp [subdivisionTailWalk]
121 | cast i ih =>
122 simp [subdivisionTailWalk]
123 refine ⟨ih, ?_⟩
124 intro hmem
125 rcases mem_subdivisionTailWalk_support e i.succ hmem with h | ⟨j, hj, hxj⟩
126 · nomatch h
127 · simp only [Sum.inr.injEq, Prod.mk.injEq] at hxj
128 have hval : i.castSucc.val = j.val := congrArg Fin.val hxj.2
129 have hi : i.castSucc.val + 1 = i.succ.val := rfl
130 omega
131
132/-- The canonical routed walk along the subdivided edge corresponding to
133`e`. -/
134private def forwardSubdivisionWalk :
135 {N : ℕ} → {r : ℕ} → (e : {p : Fin N × Fin N // p.1 < p.2}) →
136 (subdividedClique N r).Walk (Sum.inl e.1.1) (Sum.inl e.1.2)
137 | _, 0, e =>
138 SimpleGraph.Walk.cons
139 (show (subdividedClique _ 0).Adj (Sum.inl e.1.1) (Sum.inl e.1.2) from
140 ⟨fun heq => absurd (Sum.inl.inj heq) (Fin.ne_of_lt e.2),
141 Or.inl rfl⟩)
142 SimpleGraph.Walk.nil
143 | _, r' + 1, e =>
144 SimpleGraph.Walk.cons
145 (subdividedClique_adj_principal_left e (⟨0, Nat.succ_pos _⟩ : Fin (r' + 1)) rfl)
146 (subdivisionTailWalk e (⟨0, Nat.succ_pos _⟩ : Fin (r' + 1)))
147
148private lemma forwardSubdivisionWalk_length
149 {N r : ℕ} (e : {p : Fin N × Fin N // p.1 < p.2}) :
150 (@forwardSubdivisionWalk N r e).length = r + 1 := by
151 match r with
152 | 0 => simp [forwardSubdivisionWalk]
153 | r' + 1 =>
154 simp [forwardSubdivisionWalk, subdivisionTailWalk_length]
155
156private lemma forwardSubdivisionWalk_isPath
157 {N r : ℕ} (e : {p : Fin N × Fin N // p.1 < p.2}) :
158 (@forwardSubdivisionWalk N r e).IsPath := by
159 match r with
160 | 0 =>
161 simp [forwardSubdivisionWalk]
162 exact Fin.ne_of_lt e.2
163 | r' + 1 =>
164 simp [forwardSubdivisionWalk]
165 refine ⟨subdivisionTailWalk_isPath e _, ?_⟩
166 intro hmem
167 rcases mem_subdivisionTailWalk_support e _ hmem with h | ⟨j, _, hxj⟩
168 · exact absurd (Sum.inl.inj h) (Fin.ne_of_lt e.2)
169 · nomatch hxj
170
171private noncomputable def completeEdgeOrient
172 {N : ℕ} (e : (SimpleGraph.completeGraph (Fin N)).edgeSet) :
173 {p : Fin N × Fin N // p.1 < p.2} := by
174 have hne : e.1.out.1 ≠ e.1.out.2 := by
175 have heMem : s(e.1.out.1, e.1.out.2) ∈ (SimpleGraph.completeGraph (Fin N)).edgeSet := by
176 rw [Sym2.mk, e.1.out_eq]
177 exact e.2
178 have heAdj : (SimpleGraph.completeGraph (Fin N)).Adj e.1.out.1 e.1.out.2 := by
179 rwa [SimpleGraph.mem_edgeSet] at heMem
180 exact (SimpleGraph.top_adj _ _).mp heAdj
181 by_cases h : e.1.out.1 < e.1.out.2
182 · exact ⟨(e.1.out.1, e.1.out.2), h⟩
183 · exact ⟨(e.1.out.2, e.1.out.1), lt_of_le_of_ne (le_of_not_gt h) hne.symm⟩
184
185private lemma completeEdgeOrient_spec
186 {N : ℕ} (e : (SimpleGraph.completeGraph (Fin N)).edgeSet) :
187 s((completeEdgeOrient e).1.1, (completeEdgeOrient e).1.2) = (e : Sym2 (Fin N)) := by
188 by_cases h : e.1.out.1 < e.1.out.2
189 · simp [completeEdgeOrient, h, Sym2.mk, e.1.out_eq]
190 · simp [completeEdgeOrient, h, Sym2.eq_swap, Sym2.mk, e.1.out_eq]
191
192private noncomputable def completeEdgeTail
193 {N : ℕ} (e : (SimpleGraph.completeGraph (Fin N)).edgeSet) : Fin N :=
194 (completeEdgeOrient e).1.1
195
196private lemma completeEdgeTail_mem
197 {N : ℕ} (e : (SimpleGraph.completeGraph (Fin N)).edgeSet) :
198 completeEdgeTail e ∈ (e : Sym2 (Fin N)) := by
199 refine ⟨(completeEdgeOrient e).1.2, ?_⟩
200 simpa [completeEdgeTail] using (completeEdgeOrient_spec e).symm
201
202private noncomputable def completeEdgeHead
203 {N : ℕ} (e : (SimpleGraph.completeGraph (Fin N)).edgeSet) : Fin N :=
204 Sym2.Mem.other (completeEdgeTail_mem e)
205
206private lemma completeEdgeHead_eq
207 {N : ℕ} (e : (SimpleGraph.completeGraph (Fin N)).edgeSet) :
208 completeEdgeHead e = (completeEdgeOrient e).1.2 := by
209 have hmem : completeEdgeHead e ∈ (e : Sym2 (Fin N)) := by
210 exact Sym2.other_mem (completeEdgeTail_mem e)
211 have hmem' : completeEdgeHead e ∈
212 s((completeEdgeOrient e).1.1, (completeEdgeOrient e).1.2) := by
213 simpa [completeEdgeOrient_spec e] using hmem
214 have hne : completeEdgeHead e ≠ completeEdgeTail e := by
215 simpa [completeEdgeHead] using
216 (SimpleGraph.completeGraph (Fin N)).edge_other_ne e.2 (completeEdgeTail_mem e)
217 have hcases : completeEdgeHead e = completeEdgeTail e ∨
218 completeEdgeHead e = (completeEdgeOrient e).1.2 := by
219 simpa [completeEdgeTail] using (Sym2.mem_iff.mp hmem')
220 exact hcases.resolve_left hne
221
222private noncomputable def completeEdgeWalk
223 {N r : ℕ} (e : (SimpleGraph.completeGraph (Fin N)).edgeSet) :
224 (subdividedClique N r).Walk
225 (Sum.inl (completeEdgeTail e))
226 (Sum.inl (Sym2.Mem.other (completeEdgeTail_mem e))) := by
227 exact (forwardSubdivisionWalk (completeEdgeOrient e)).copy rfl
228 (congrArg Sum.inl (completeEdgeHead_eq e).symm)
229
230/-- Every vertex on the canonical subdivided-edge walk lies either at one
231endpoint or on the subdivision chain of that same edge. -/
232private lemma mem_forwardSubdivisionWalk_support
233 {N r : ℕ} (e : {p : Fin N × Fin N // p.1 < p.2})
234 {x : SubdividedCliqueVert N r}
235 (hx : x ∈ (forwardSubdivisionWalk e).support) :
236 x = .inl e.1.1 ∨ x = .inl e.1.2 ∨ ∃ k : Fin r, x = .inr ⟨e, k⟩ := by
237 match r with
238 | 0 =>
239 simp [forwardSubdivisionWalk] at hx
240 rcases hx with rfl | rfl
241 · exact Or.inl rfl
242 · exact Or.inr (Or.inl rfl)
243 | r' + 1 =>
244 simp [forwardSubdivisionWalk] at hx
245 rcases hx with rfl | hx
246 · exact Or.inl rfl
247 · rcases mem_subdivisionTailWalk_support e _ hx with h | ⟨j, _, hj⟩
248 · exact Or.inr (Or.inl h)
249 · exact Or.inr (Or.inr ⟨j, hj⟩)
250
251/-- Forward-direction helper: a subgraph copy of an `r`-subdivided clique
252of order `N` induces a depth-`⌈r/2⌉` shallow topological minor model of
253`K_N`. The eventual Close session should build the explicit routed paths
254along the subdivision edges. -/
255private theorem subdividedClique_isShallowTopologicalMinor
256 {V : Type} [DecidableEq V] [Fintype V] (G : SimpleGraph V)
257 (N r : ℕ) (hContain : (subdividedClique N r).IsContained G) :
258 IsShallowTopologicalMinor (SimpleGraph.completeGraph (Fin N)) G ((r + 1) / 2) := by
259 rcases hContain with ⟨copy⟩
260 let model :
261 ShallowTopologicalMinorModel
262 (SimpleGraph.completeGraph (Fin N))
263 G
264 ((r + 1) / 2) :=
265 { branchVertex :=
266 ⟨fun i => copy (Sum.inl i), fun _ _ h => Sum.inl.inj (copy.injective h)⟩
267 edgeTail := completeEdgeTail
268 edgeTail_mem := completeEdgeTail_mem
269 edgePath := fun e => (completeEdgeWalk e).map copy.toHom
270 edgePath_isPath := by
271 intro e
272 exact SimpleGraph.Walk.map_isPath_of_injective copy.injective
273 (by simpa [completeEdgeWalk] using
274 (forwardSubdivisionWalk_isPath (completeEdgeOrient e)))
275 edgePath_length := by
276 intro e
277 calc
278 ((completeEdgeWalk e).map copy.toHom).length = r + 1 := by
279 simp [completeEdgeWalk, forwardSubdivisionWalk_length]
280 _ ≤ 2 * ((r + 1) / 2) + 1 := by omega
281 edgePath_interior_avoids_branch := by
282 intro e x hx htail hhead w
283 rw [SimpleGraph.Walk.support_map] at hx
284 rcases List.mem_map.mp hx with ⟨y, hy, rfl⟩
285 have hy' : y ∈ (forwardSubdivisionWalk (completeEdgeOrient e)).support := by
286 simpa [completeEdgeWalk] using hy
287 rcases mem_forwardSubdivisionWalk_support (e := completeEdgeOrient e) hy' with
288 htail' | hhead' | ⟨k, hk⟩
289 · exact (htail (by simpa [completeEdgeWalk] using congrArg copy htail')).elim
290 · have hheadEq :
291 copy (Sum.inl (completeEdgeOrient e).1.2) =
292 copy (Sum.inl (Sym2.Mem.other (completeEdgeTail_mem e))) := by
293 rw [← completeEdgeHead_eq e]
294 rfl
295 exact (hhead ((congrArg copy hhead').trans hheadEq)).elim
296 · intro hw
297 have : (Sum.inr ⟨completeEdgeOrient e, k⟩ : SubdividedCliqueVert N r) = Sum.inl w := by
298 exact hk.symm.trans (copy.injective hw)
299 nomatch this
300 edgePath_interior_disjoint := by
301 intro e e' x hne hx hx' htail hhead htail' hhead'
302 rw [SimpleGraph.Walk.support_map] at hx hx'
303 rcases List.mem_map.mp hx with ⟨y, hy, rfl⟩
304 rcases List.mem_map.mp hx' with ⟨y', hy', hyy'⟩
305 have hy0 : y ∈ (forwardSubdivisionWalk (completeEdgeOrient e)).support := by
306 simpa [completeEdgeWalk] using hy
307 have hy0' : y' ∈ (forwardSubdivisionWalk (completeEdgeOrient e')).support := by
308 simpa [completeEdgeWalk] using hy'
309 rcases mem_forwardSubdivisionWalk_support (e := completeEdgeOrient e) hy0 with
310 hxTail | hxHead | ⟨k, hk⟩
311 · exact (htail (by simpa [completeEdgeWalk] using congrArg copy hxTail)).elim
312 · have hheadEq :
313 copy (Sum.inl (completeEdgeOrient e).1.2) =
314 copy (Sum.inl (Sym2.Mem.other (completeEdgeTail_mem e))) := by
315 rw [← completeEdgeHead_eq e]
316 rfl
317 exact (hhead ((congrArg copy hxHead).trans hheadEq)).elim
318 · rcases mem_forwardSubdivisionWalk_support (e := completeEdgeOrient e') hy0' with
319 hxTail' | hxHead' | ⟨k', hk'⟩
320 · exact (htail' (hyy'.symm.trans (by simpa [completeEdgeWalk] using congrArg copy hxTail'))).elim
321 · have hheadEq' :
322 copy (Sum.inl (completeEdgeOrient e').1.2) =
323 copy (Sum.inl (Sym2.Mem.other (completeEdgeTail_mem e'))) := by
324 rw [← completeEdgeHead_eq e']
325 rfl
326 exact (hhead' (hyy'.symm.trans ((congrArg copy hxHead').trans hheadEq'))).elim
327 · have horient :
328 completeEdgeOrient e = completeEdgeOrient e' := by
329 have hyy : y = y' := copy.injective hyy'.symm
330 have hpair :
331 (⟨completeEdgeOrient e, k⟩ : {p : Fin N × Fin N // p.1 < p.2} × Fin r) =
332 ⟨completeEdgeOrient e', k'⟩ := by
333 exact Sum.inr.inj (hk.symm.trans (hyy.trans hk'))
334 exact congrArg Prod.fst hpair
335 apply hne
336 apply Subtype.ext
337 have hsym :
338 s((completeEdgeOrient e).1.1, (completeEdgeOrient e).1.2) =
339 s((completeEdgeOrient e').1.1, (completeEdgeOrient e').1.2) := by
340 simpa using
341 congrArg (fun z : {p : Fin N × Fin N // p.1 < p.2} => s(z.1.1, z.1.2)) horient
342 calc
343 (e : Sym2 (Fin N)) = s((completeEdgeOrient e).1.1, (completeEdgeOrient e).1.2) :=
344 (completeEdgeOrient_spec e).symm
345 _ = s((completeEdgeOrient e').1.1, (completeEdgeOrient e').1.2) := hsym
346 _ = (e' : Sym2 (Fin N)) := completeEdgeOrient_spec e' }
347 exact ⟨model⟩
348
349/-- Shallow-minor nowhere denseness implies the local subdivided-clique
350formulation. This is the linear parameter translation
351`N_r := ω_{⌈r/2⌉}(C) + 1`. -/
352private theorem catalog_nowhereDense_to_dev_nowhereDense
353 (C : GraphClass)
354 (hCat : Catalog.Sparsity.NowhereDense.IsNowhereDense C) :
355 Dev.MonadicDependence.NowhereDense.IsNowhereDense C := by
356 intro r
357 rcases hCat ((r + 1) / 2) with ⟨t, ht⟩
358 refine ⟨t + 1, ?_⟩
359 intro V _ _ G hCG hContain
360 have hTop :
361 IsShallowTopologicalMinor (SimpleGraph.completeGraph (Fin (t + 1))) G ((r + 1) / 2) :=
362 subdividedClique_isShallowTopologicalMinor G (t + 1) r hContain
363 exact ht G hCG (shallowTopologicalMinor_toShallowMinor hTop)
364
365/-- Step 1 data for the backward direction: starting from a shallow minor
366model of `K_{t+1}`, record the centre-to-centre candidate walks obtained
367by concatenating the branch-radius walks with the bridge edge. Each walk
368has length at most `2 d + 1`. -/
369private structure CandidatePathData {V : Type} (G : SimpleGraph V) (d t : ℕ) where
370 model : ShallowMinorModel (SimpleGraph.completeGraph (Fin (t + 1))) G d
371 /-- For every pair of distinct clique vertices `i ≠ j`, a walk in `G`
372 between the corresponding branch-set centres. -/
373 candidateWalk : ∀ {i j : Fin (t + 1)}, i ≠ j →
374 G.Walk (model.center i) (model.center j)
375 /-- Each candidate walk has length at most `2 d + 1`. -/
376 candidateWalk_length_le : ∀ {i j : Fin (t + 1)} (h : i ≠ j),
377 (candidateWalk h).length ≤ 2 * d + 1
378
379/-- Step 2 data: after a multicolour Ramsey pass, all candidate paths on a
380subclique `subclique` of size at least `m` share a common length
381`commonLength ≤ 2d + 1`.
382
383`hasCommonLengthWalk` is stated existentially (rather than fixing
384`candidateWalk` itself) so that we can symmetrise the orientation: for a
385subclique edge `{i, j}`, the common-length walk is realised by whichever of
386`candidateWalk (i ≠ j)` or the reverse of `candidateWalk (j ≠ i)` matches
387the Ramsey-monochromatic colour. Step 1 makes no symmetry guarantee
388between `candidateWalk h` and `candidateWalk h.symm`, and the existential
389form keeps Step 1 unchanged.
390
391The size parameter `m` records the lower bound on the monochromatic
392subclique produced by `multicolorRamsey`. It threads through downstream
393steps so that Step 6 can pick a final `t` large enough to contradict the
394local nowhere-dense hypothesis. -/
395private structure UniformLengthData {V : Type} (G : SimpleGraph V) (d t m : ℕ)
396 extends CandidatePathData G d t where
397 subclique : Finset (Fin (t + 1))
398 subclique_card_ge : m ≤ subclique.card
399 commonLength : ℕ
400 commonLength_le : commonLength ≤ 2 * d + 1
401 hasCommonLengthWalk : ∀ {i j : Fin (t + 1)},
402 i ∈ subclique → j ∈ subclique → i ≠ j →
403 ∃ w : G.Walk (model.center i) (model.center j), w.length = commonLength
404
405/-- Step 3 data: after the iterative two-colour Ramsey refinement, the
406branching pattern at every interior level is canonical on the surviving
407subclique. Concretely:
408
409* `canonicalWalk` fixes a specific common-length walk between subclique
410 centres, chosen via `Classical.choose` on the inherited
411 `hasCommonLengthWalk` existential so that the rest of the scaffold can
412 talk about concrete vertices of the walk.
413* `patternShared i h` is the shared/disjoint flag at focus vertex `i` and
414 interior level `h`: `true` means all canonical walks from `center i`
415 pass through the same `h`-th vertex on the subclique, `false` means the
416 `h`-th vertices are pairwise distinct as the other endpoint varies.
417 Values outside the relevant range (`h ≥ commonLength`) are unspecified
418 and the spec fields take no view of them. -/
419private structure CanonicalPatternData {V : Type} (G : SimpleGraph V) (d t m : ℕ)
420 extends UniformLengthData G d t m where
421 /-- A concrete walk of length `commonLength` between the branch-set centres
422 of any two distinct subclique vertices. Chosen to realise the inherited
423 `hasCommonLengthWalk` existential. -/
424 canonicalWalk : ∀ {i j : Fin (t + 1)},
425 i ∈ subclique → j ∈ subclique → i ≠ j →
426 G.Walk (model.center i) (model.center j)
427 /-- Each canonical walk has length exactly `commonLength`. -/
428 canonicalWalk_length : ∀ {i j : Fin (t + 1)}
429 (hi : i ∈ subclique) (hj : j ∈ subclique) (hij : i ≠ j),
430 (canonicalWalk hi hj hij).length = commonLength
431 /-- Branching-pattern bit: for each focus vertex `i` and level `h`,
432 `patternShared i h = true` means "all canonical walks from `center i`
433 share the `h`-th vertex on the subclique", `false` means "they have
434 pairwise distinct `h`-th vertices". Levels `h ≥ commonLength` are
435 unconstrained. -/
436 patternShared : Fin (t + 1) → ℕ → Bool
437 /-- Spec for the "shared" bit: if `patternShared i h = true`, then for any
438 two other subclique vertices `j`, `k`, the `h`-th vertices of the
439 canonical walks `center i → center j` and `center i → center k` agree. -/
440 patternShared_shared : ∀ {i j k : Fin (t + 1)}
441 (hi : i ∈ subclique) (hj : j ∈ subclique) (hk : k ∈ subclique)
442 (hij : i ≠ j) (hik : i ≠ k)
443 {h : ℕ}, h < commonLength → patternShared i h = true →
444 (canonicalWalk hi hj hij).getVert h =
445 (canonicalWalk hi hk hik).getVert h
446 /-- Spec for the "disjoint" bit: if `patternShared i h = false`, then for
447 any two distinct other subclique vertices `j ≠ k`, the `h`-th vertices of
448 the canonical walks `center i → center j` and `center i → center k`
449 differ. -/
450 patternShared_disjoint : ∀ {i j k : Fin (t + 1)}
451 (hi : i ∈ subclique) (hj : j ∈ subclique) (hk : k ∈ subclique)
452 (hij : i ≠ j) (hik : i ≠ k) (_hjk : j ≠ k)
453 {h : ℕ}, h < commonLength → patternShared i h = false →
454 (canonicalWalk hi hj hij).getVert h ≠
455 (canonicalWalk hi hk hik).getVert h
456
457/-- Step 4 data: after the shared prefixes/suffixes have been trimmed and any
458residual interior collisions cleaned up, we have, on the surviving subclique,
459a new system of internally disjoint walks of uniform length `trimmedLength + 1`
460between trimmed centres `c_i' ∈ B_i`, with `trimmedLength ≤ 2d`.
461
462The interior-disjointness spec is stated so that Step 5 can assemble a
463`subdividedClique`-shaped subgraph copy: interiors of distinct trimmed walks
464are entirely disjoint, and no interior vertex of a walk coincides with any
465trimmed centre (other than the walk's own endpoints). -/
466private structure TrimmedPathData {V : Type} (G : SimpleGraph V) (d t m : ℕ)
467 extends CanonicalPatternData G d t m where
468 /-- Uniform internal-path length, `ℓ' ≤ 2d`. -/
469 trimmedLength : ℕ
470 trimmedLength_le : trimmedLength ≤ 2 * d
471 /-- Trimmed centre `c_i'` at the tip of `i`'s shared prefix. Lies in the
472 branch set `B_i` of the minor model for every subclique vertex `i`. -/
473 trimmedCenter : Fin (t + 1) → V
474 trimmedCenter_mem : ∀ {i : Fin (t + 1)},
475 i ∈ subclique → trimmedCenter i ∈ model.branchSet i
476 /-- Trimmed walk between the trimmed centres of two distinct subclique
477 vertices, of uniform length `trimmedLength + 1`. -/
478 trimmedWalk : ∀ {i j : Fin (t + 1)},
479 i ∈ subclique → j ∈ subclique → i ≠ j →
480 G.Walk (trimmedCenter i) (trimmedCenter j)
481 trimmedWalk_length : ∀ {i j : Fin (t + 1)}
482 (hi : i ∈ subclique) (hj : j ∈ subclique) (hij : i ≠ j),
483 (trimmedWalk hi hj hij).length = trimmedLength + 1
484 trimmedWalk_isPath : ∀ {i j : Fin (t + 1)}
485 (hi : i ∈ subclique) (hj : j ∈ subclique) (hij : i ≠ j),
486 (trimmedWalk hi hj hij).IsPath
487 /-- Centre-avoidance: no vertex of any trimmed walk equals any trimmed
488 centre of the subclique, except at the walk's two own endpoints. -/
489 trimmedWalk_avoids_centres : ∀ {i j k : Fin (t + 1)}
490 (hi : i ∈ subclique) (hj : j ∈ subclique) (_hk : k ∈ subclique)
491 (hij : i ≠ j) {v : V},
492 v ∈ (trimmedWalk hi hj hij).support →
493 v = trimmedCenter k → k = i ∨ k = j
494 /-- Pairwise interior-disjointness: if a vertex lies on two trimmed walks
495 indexed by distinct unordered pairs, it must already be one of the two
496 endpoints of the first walk (and hence, by centre-avoidance on the other
497 walk, also an endpoint of the second — the shared endpoint case). -/
498 trimmedWalk_interior_disjoint : ∀ {i j i' j' : Fin (t + 1)}
499 (hi : i ∈ subclique) (hj : j ∈ subclique) (hij : i ≠ j)
500 (hi' : i' ∈ subclique) (hj' : j' ∈ subclique) (hi'j' : i' ≠ j')
501 (_hpair_ne : s(i, j) ≠ s(i', j'))
502 {v : V},
503 v ∈ (trimmedWalk hi hj hij).support →
504 v ∈ (trimmedWalk hi' hj' hi'j').support →
505 v = trimmedCenter i ∨ v = trimmedCenter j
506
507/-- Step 5 data: the cleaned path system has been packaged as a subgraph copy
508of a subdivided clique in `G`. The subdivision order is at least `m`, which
509is what Step 6 eventually inverts against the local nowhere-dense bound. -/
510private structure CleanSubdivisionData {V : Type} (G : SimpleGraph V) (d t m : ℕ)
511 extends TrimmedPathData G d t m where
512 subdivisionOrder : ℕ
513 subdivisionOrder_ge : m ≤ subdivisionOrder
514 contained : (subdividedClique subdivisionOrder trimmedLength).IsContained G
515
516/-- Backward direction, Step 1: from a shallow minor model, build the
517centre-to-centre candidate paths of length at most `2d + 1`. -/
518private noncomputable def backward_step1_candidate_paths
519 {V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V}
520 {d t : ℕ}
521 (hMinor : IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) G d) :
522 CandidatePathData G d t := by
523 classical
524 let model := hMinor.some
525 have hwalk : ∀ {i j : Fin (t + 1)}, i ≠ j →
526 ∃ w : G.Walk (model.center i) (model.center j), w.length ≤ 2 * d + 1 := by
527 intro i j hij
528 have hadj : (SimpleGraph.completeGraph (Fin (t + 1))).Adj i j :=
529 (SimpleGraph.top_adj i j).mpr hij
530 obtain ⟨x, hx, y, hy, hxy⟩ := model.branchEdge i j hadj
531 obtain ⟨pxi, _, hxilen, _⟩ := model.branchRadius i x hx
532 obtain ⟨pyj, _, hyjlen, _⟩ := model.branchRadius j y hy
533 refine ⟨pxi.append (SimpleGraph.Walk.cons hxy pyj.reverse), ?_⟩
534 simp [SimpleGraph.Walk.length_append, SimpleGraph.Walk.length_cons,
535 SimpleGraph.Walk.length_reverse]
536 omega
537 exact
538 { model := model
539 candidateWalk := fun {_ _} h => (hwalk h).choose
540 candidateWalk_length_le := fun {_ _} h => (hwalk h).choose_spec }
541
542/-- Backward direction, Step 2: multicolour Ramsey normalises the candidate
543path lengths. We apply `Catalog.Sparsity.MulticolorRamsey.multicolorRamsey`
544to the colouring `{i, j} ↦ min ((candidateWalk (i ≠ j)).length)
545((candidateWalk (j ≠ i)).length)`, with all colours targeting a
546monochromatic subclique of size `m`. The hypothesis `hThresh` asserts that
547the Ramsey threshold fits into `t + 1`, so Ramsey fires and the output
548carries a subclique of size at least `m`. The final `t` / `m` choice is
549deferred to `backward_step6_extract_bound`. -/
550private noncomputable def backward_step2_uniform_length
551 {V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V}
552 {d t m : ℕ}
553 (hStep1 : CandidatePathData G d t)
554 (hThresh :
555 (Catalog.Sparsity.MulticolorRamsey.multicolorRamsey
556 (List.replicate (2 * d + 2) m)
557 List.replicate_succ_ne_nil).choose ≤ t + 1) :
558 UniformLengthData G d t m := by
559 classical
560 -- Symmetric length function on ordered pairs; clamp to `Fin (2d + 2)`.
561 let lenFn : Fin (t + 1) → Fin (t + 1) → ℕ := fun i j =>
562 if h : i = j then 0
563 else min (hStep1.candidateWalk h).length
564 (hStep1.candidateWalk (Ne.symm h)).length
565 have lenFn_le : ∀ i j, lenFn i j ≤ 2 * d + 1 := by
566 intro i j
567 change (if h : i = j then 0 else _) ≤ _
568 by_cases h : i = j
569 · simp [h]
570 · rw [dif_neg h]
571 have h1 := hStep1.candidateWalk_length_le h
572 have h2 := hStep1.candidateWalk_length_le (Ne.symm h)
573 omega
574 have lenFn_symm : ∀ i j, lenFn i j = lenFn j i := by
575 intro i j
576 change (if h : i = j then 0 else _) = (if h : j = i then 0 else _)
577 by_cases h : i = j
578 · subst h; rfl
579 · have h' : j ≠ i := Ne.symm h
580 rw [dif_neg h, dif_neg h']
581 exact Nat.min_comm _ _
582 -- `multicolorRamsey` demands colours in `Fin sizes.length`. With
583 -- `sizes := List.replicate (2 d + 2) m`, `sizes.length` is propositionally
584 -- but not definitionally `2 d + 2`, so the colour function is typed in
585 -- `Fin sizes.length` and we bridge via `List.length_replicate`.
586 let colourFn : Sym2 (Fin (t + 1)) →
587 Fin (List.replicate (2 * d + 2) m).length :=
588 Sym2.lift
589 ⟨fun i j => ⟨lenFn i j, by
590 rw [List.length_replicate]
591 exact Nat.lt_succ_of_le (lenFn_le i j)⟩,
592 fun i j => Fin.ext (lenFn_symm i j)⟩
593 -- `multicolorRamsey` lives in `Prop`; the target type `UniformLengthData`
594 -- is a `Type`, so destructuring via `obtain` would fail with
595 -- `Exists.casesOn can only eliminate into Prop`. Use `Classical.choose`
596 -- instead, mirroring the Step 1 idiom for `IsShallowMinor`.
597 let hRam :=
598 Catalog.Sparsity.MulticolorRamsey.multicolorRamsey
599 (List.replicate (2 * d + 2) m)
600 List.replicate_succ_ne_nil
601 have hcard : hRam.choose ≤ Fintype.card (Fin (t + 1)) := by
602 simpa [Fintype.card_fin] using hThresh
603 let hRamOut := hRam.choose_spec hcard colourFn
604 let i_ram : Fin (List.replicate (2 * d + 2) m).length := hRamOut.choose
605 let hS := hRamOut.choose_spec
606 let S : Finset (Fin (t + 1)) := hS.choose
607 have hSpair : (↑S : Set (Fin (t + 1))).Pairwise
608 (fun u v => colourFn s(u, v) = i_ram) :=
609 hS.choose_spec.2
610 have hSgeM : m ≤ S.card := by
611 have hsize : (List.replicate (2 * d + 2) m).get i_ram ≤ S.card :=
612 hS.choose_spec.1
613 -- `get` of a replicated list is the replicated value.
614 have hi_lt : i_ram.val < 2 * d + 2 := by
615 have := i_ram.isLt
616 simpa [List.length_replicate] using this
617 have hget : (List.replicate (2 * d + 2) m).get i_ram = m := by
618 simp [List.get_eq_getElem, List.getElem_replicate]
619 rw [hget] at hsize
620 exact hsize
621 refine
622 { toCandidatePathData := hStep1
623 subclique := S
624 subclique_card_ge := hSgeM
625 commonLength := i_ram.val
626 commonLength_le := by
627 have hi := i_ram.isLt
628 have hLen : (List.replicate (2 * d + 2) m).length = 2 * d + 2 :=
629 List.length_replicate
630 omega
631 hasCommonLengthWalk := ?_ }
632 intro a b ha hb hab
633 have haSet : a ∈ (↑S : Set (Fin (t + 1))) := by simpa using ha
634 have hbSet : b ∈ (↑S : Set (Fin (t + 1))) := by simpa using hb
635 have hcol : colourFn s(a, b) = i_ram := hSpair haSet hbSet hab
636 have hval : lenFn a b = i_ram.val := by
637 have hv := congrArg Fin.val hcol
638 simpa [colourFn, Sym2.lift_mk] using hv
639 have hlen : min (hStep1.candidateWalk hab).length
640 (hStep1.candidateWalk (Ne.symm hab)).length = i_ram.val := by
641 have : lenFn a b = min (hStep1.candidateWalk hab).length
642 (hStep1.candidateWalk (Ne.symm hab)).length := by
643 change (if h : a = b then 0 else _) = _
644 rw [dif_neg hab]
645 rw [this] at hval
646 exact hval
647 rcases Nat.le_total (hStep1.candidateWalk hab).length
648 (hStep1.candidateWalk (Ne.symm hab)).length with hle | hle
649 · refine ⟨hStep1.candidateWalk hab, ?_⟩
650 rw [Nat.min_eq_left hle] at hlen
651 exact hlen
652 · refine ⟨(hStep1.candidateWalk (Ne.symm hab)).reverse, ?_⟩
653 rw [SimpleGraph.Walk.length_reverse]
654 rw [Nat.min_eq_right hle] at hlen
655 exact hlen
656
657/-- Non-emptiness helper for Step 3's Ramsey sizes list: the list is
658`List.replicate K m` with `K` positive. -/
659private lemma step3_sizes_ne_nil (d t m : ℕ) :
660 List.replicate
661 (Fintype.card (Fin (t + 1) → Fin (2 * d + 1) → Bool)) m ≠ [] := by
662 rw [ne_eq, List.replicate_eq_nil_iff]
663 exact Fintype.card_ne_zero
664
665/-- Backward direction, Step 3: iterative two-colour Ramsey normalises the
666shared-prefix/shared-suffix branching pattern.
667
668`hThresh3` bounds the threshold returned by multicolour Ramsey applied with
669`(t+1)*(2d+1)`-bit colours (one bit per focus vertex, interior level).
670Combined with the inherited `m ≤ hStep2.subclique.card`, it guarantees the
671Ramsey call fires on the subclique's subtype. The Ramsey-monochromatic
672colour then reads off the canonical branching pattern: for each focus
673vertex `i` in the refined subclique and each interior level `h`, either all
674canonical walks from `center i` share the same `h`-th vertex on the refined
675subclique, or they have pairwise distinct `h`-th vertices. -/
676private noncomputable def backward_step3_canonical_pattern
677 {V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V}
678 {d t m : ℕ}
679 (hStep2 : UniformLengthData G d t m)
680 (hThresh3 :
681 (Catalog.Sparsity.MulticolorRamsey.multicolorRamsey
682 (List.replicate
683 (Fintype.card (Fin (t + 1) → Fin (2 * d + 1) → Bool)) m)
684 (step3_sizes_ne_nil d t m)).choose ≤ m) :
685 CanonicalPatternData G d t m := by
686 classical
687 -- Shorthand for hStep2's subclique.
688 let S₂ : Finset (Fin (t + 1)) := hStep2.subclique
689 -- Pick concrete walks from the inherited existential.
690 let walk : ∀ {i j : Fin (t + 1)},
691 i ∈ S₂ → j ∈ S₂ → i ≠ j →
692 G.Walk (hStep2.model.center i) (hStep2.model.center j) :=
693 fun hi hj hij => (hStep2.hasCommonLengthWalk hi hj hij).choose
694 have walk_length : ∀ {i j : Fin (t + 1)} (hi : i ∈ S₂) (hj : j ∈ S₂)
695 (hij : i ≠ j),
696 (walk hi hj hij).length = hStep2.commonLength :=
697 fun hi hj hij => (hStep2.hasCommonLengthWalk hi hj hij).choose_spec
698 -- Colour type for the Step-3 Ramsey: one Bool per (focus vertex, level).
699 let ColourT : Type := Fin (t + 1) → Fin (2 * d + 1) → Bool
700 let K : ℕ := Fintype.card ColourT
701 let sizes : List ℕ := List.replicate K m
702 -- Raw colour: given two subclique vertices `a ≠ b`, for each `(i, h)` the
703 -- bit says whether the `h`-th vertex of walk `i → a` equals walk `i → b`
704 -- at position `h`. When `i ∈ {a, b}` or `i ∉ S₂` we return `true`
705 -- (the branch is irrelevant; chosen so the raw function is symmetric in
706 -- `a, b`).
707 let rawBit : ↥S₂ → ↥S₂ → ColourT := fun a b i h =>
708 if hia : i = a.val then true
709 else if hib : i = b.val then true
710 else if hi : i ∈ S₂ then
711 decide ((walk hi a.property hia).getVert h.val =
712 (walk hi b.property hib).getVert h.val)
713 else true
714 have rawBit_sym : ∀ a b, rawBit a b = rawBit b a := by
715 intro a b
716 funext i h
717 show (if hia : i = a.val then (true : Bool)
718 else if hib : i = b.val then (true : Bool)
719 else if hi : i ∈ S₂ then
720 decide ((walk hi a.property hia).getVert h.val =
721 (walk hi b.property hib).getVert h.val)
722 else (true : Bool)) =
723 (if hia : i = b.val then (true : Bool)
724 else if hib : i = a.val then (true : Bool)
725 else if hi : i ∈ S₂ then
726 decide ((walk hi b.property hia).getVert h.val =
727 (walk hi a.property hib).getVert h.val)
728 else (true : Bool))
729 by_cases hia : i = a.val
730 · by_cases hib : i = b.val
731 · rw [dif_pos hia, dif_pos hib]
732 · rw [dif_pos hia, dif_neg hib, dif_pos hia]
733 · by_cases hib : i = b.val
734 · rw [dif_neg hia, dif_pos hib, dif_pos hib]
735 · by_cases hi : i ∈ S₂
736 · rw [dif_neg hia, dif_neg hib, dif_pos hi,
737 dif_neg hib, dif_neg hia, dif_pos hi]
738 congr 1
739 exact propext eq_comm
740 · rw [dif_neg hia, dif_neg hib, dif_neg hi,
741 dif_neg hib, dif_neg hia, dif_neg hi]
742 -- Sym2-lifted colour on subclique pairs.
743 let colourFn : Sym2 ↥S₂ → ColourT := Sym2.lift ⟨rawBit, rawBit_sym⟩
744 -- We need `colourFn` typed as `Sym2 ↥S₂ → Fin sizes.length`. Bridge via
745 -- `Fintype.truncEquivFin` and `List.length_replicate`.
746 let equivCol : ColourT ≃ Fin K := (Fintype.truncEquivFin ColourT).out
747 have sizes_length : sizes.length = K := List.length_replicate
748 let finColourFn : Sym2 ↥S₂ → Fin sizes.length := fun p =>
749 Fin.cast sizes_length.symm (equivCol (colourFn p))
750 -- Apply the multicolour Ramsey.
751 have hRam_le : (Catalog.Sparsity.MulticolorRamsey.multicolorRamsey
752 sizes (step3_sizes_ne_nil d t m)).choose ≤ Fintype.card (↥S₂) := by
753 rw [Fintype.card_coe]
754 exact hThresh3.trans hStep2.subclique_card_ge
755 let hRam := Catalog.Sparsity.MulticolorRamsey.multicolorRamsey
756 sizes (step3_sizes_ne_nil d t m)
757 let hOut := hRam.choose_spec hRam_le finColourFn
758 let c_ram : Fin sizes.length := hOut.choose
759 let hOut2 := hOut.choose_spec
760 let T : Finset ↥S₂ := hOut2.choose
761 have hT_card : sizes.get c_ram ≤ T.card := hOut2.choose_spec.1
762 have hT_pair : (↑T : Set ↥S₂).Pairwise
763 (fun u v => finColourFn s(u, v) = c_ram) := hOut2.choose_spec.2
764 -- `sizes.get c_ram = m` since all entries of `sizes` are `m`.
765 have h_get_eq_m : sizes.get c_ram = m := by
766 have hi_lt : c_ram.val < K := by
767 simpa [sizes_length] using c_ram.isLt
768 simp [sizes, List.get_eq_getElem, List.getElem_replicate]
769 rw [h_get_eq_m] at hT_card
770 -- Refined subclique in `Fin (t + 1)`.
771 let S₃ : Finset (Fin (t + 1)) := T.image Subtype.val
772 have hS₃_sub : ∀ {x}, x ∈ S₃ → x ∈ S₂ := by
773 intro x hx
774 rcases Finset.mem_image.mp hx with ⟨⟨y, hy⟩, _, rfl⟩
775 exact hy
776 have hS₃_card : m ≤ S₃.card := by
777 rw [show S₃.card = T.card from Finset.card_image_of_injective _ Subtype.val_injective]
778 exact hT_card
779 -- The monochromatic colour tuple, pulled back through `equivCol`.
780 let patternCol : ColourT := equivCol.symm (Fin.cast sizes_length c_ram)
781 -- Pattern on arbitrary levels: use the Ramsey colour bit for `h < 2*d+1`,
782 -- and `true` elsewhere (vacuous; only `h < commonLength ≤ 2*d+1` is used).
783 let patternShared : Fin (t + 1) → ℕ → Bool := fun i h =>
784 if h_lt : h < 2 * d + 1 then patternCol i ⟨h, h_lt⟩ else true
785 -- Key bridging fact: for two distinct elements `j ≠ k` of `T` (as
786 -- subclique members), the raw colour at position `(i, h)` equals the
787 -- monochromatic pattern bit `patternCol i h`.
788 have colour_eq : ∀ {j k : ↥S₂}, j ∈ T → k ∈ T → j ≠ k →
789 rawBit j k = patternCol := by
790 intro j k hj hk hjk
791 have hpair : finColourFn s(j, k) = c_ram := hT_pair hj hk hjk
792 have hcol_eq : colourFn s(j, k) = patternCol := by
793 have hrev : equivCol (colourFn s(j, k)) = Fin.cast sizes_length c_ram := by
794 have := congrArg (Fin.cast sizes_length) hpair
795 simpa [finColourFn, Fin.cast_cast] using this
796 have := congrArg equivCol.symm hrev
797 simpa [patternCol] using this
798 simpa [colourFn, Sym2.lift_mk] using hcol_eq
799 -- Build the shared spec.
800 have shared_spec : ∀ {i j k : Fin (t + 1)}
801 (hi : i ∈ S₃) (hj : j ∈ S₃) (hk : k ∈ S₃)
802 (hij : i ≠ j) (hik : i ≠ k) {h : ℕ}, h < hStep2.commonLength →
803 patternShared i h = true →
804 (walk (hS₃_sub hi) (hS₃_sub hj) hij).getVert h =
805 (walk (hS₃_sub hi) (hS₃_sub hk) hik).getVert h := by
806 intro i j k hi hj hk hij hik h hh_lt hpat
807 -- Case split j = k (trivial) vs j ≠ k (use Ramsey monochromaticity).
808 by_cases hjk : j = k
809 · subst hjk; rfl
810 -- `hh_lt : h < commonLength ≤ 2*d+1`, so patternShared unfolds to patternCol.
811 have hh_lt_all : h < 2 * d + 1 :=
812 lt_of_lt_of_le hh_lt hStep2.commonLength_le
813 have hpat_col : patternCol i ⟨h, hh_lt_all⟩ = true := by
814 change (if h_lt : h < 2 * d + 1 then patternCol i ⟨h, h_lt⟩
815 else (true : Bool)) = true at hpat
816 rwa [dif_pos hh_lt_all] at hpat
817 -- Extract ⟨j, _⟩, ⟨k, _⟩ ∈ T. j, k ∈ S₃ means their "upgraded" versions are in T.
818 rcases Finset.mem_image.mp hj with ⟨jT, hjT, hjeq⟩
819 rcases Finset.mem_image.mp hk with ⟨kT, hkT, hkeq⟩
820 subst hjeq
821 subst hkeq
822 have hj_ne_k : jT ≠ kT := by
823 intro heq; apply hjk; exact congrArg Subtype.val heq
824 -- Apply colour_eq: rawBit jT kT = patternCol, in particular at (i, ⟨h, hh_lt_all⟩).
825 have hbit : rawBit jT kT i ⟨h, hh_lt_all⟩ = patternCol i ⟨h, hh_lt_all⟩ := by
826 rw [colour_eq hjT hkT hj_ne_k]
827 rw [hpat_col] at hbit
828 -- Unfold rawBit at the (i, ⟨h, hh_lt_all⟩) arguments with i ≠ jT.val, i ≠ kT.val,
829 -- i ∈ S₂ (via hi ∈ S₃ ⇒ S₂).
830 have hi_S₂ : i ∈ S₂ := hS₃_sub hi
831 have hi_ne_j : i ≠ jT.val := hij
832 have hi_ne_k : i ≠ kT.val := hik
833 simp only [rawBit] at hbit
834 rw [dif_neg hi_ne_j, dif_neg hi_ne_k, dif_pos hi_S₂] at hbit
835 have : decide
836 ((walk hi_S₂ jT.property hi_ne_j).getVert h =
837 (walk hi_S₂ kT.property hi_ne_k).getVert h) = true := hbit
838 exact of_decide_eq_true this
839 have disjoint_spec : ∀ {i j k : Fin (t + 1)}
840 (hi : i ∈ S₃) (hj : j ∈ S₃) (hk : k ∈ S₃)
841 (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k)
842 {h : ℕ}, h < hStep2.commonLength → patternShared i h = false →
843 (walk (hS₃_sub hi) (hS₃_sub hj) hij).getVert h ≠
844 (walk (hS₃_sub hi) (hS₃_sub hk) hik).getVert h := by
845 intro i j k hi hj hk hij hik hjk h hh_lt hpat
846 have hh_lt_all : h < 2 * d + 1 :=
847 lt_of_lt_of_le hh_lt hStep2.commonLength_le
848 have hpat_col : patternCol i ⟨h, hh_lt_all⟩ = false := by
849 change (if h_lt : h < 2 * d + 1 then patternCol i ⟨h, h_lt⟩
850 else (true : Bool)) = false at hpat
851 rwa [dif_pos hh_lt_all] at hpat
852 rcases Finset.mem_image.mp hj with ⟨jT, hjT, hjeq⟩
853 rcases Finset.mem_image.mp hk with ⟨kT, hkT, hkeq⟩
854 subst hjeq
855 subst hkeq
856 have hj_ne_k : jT ≠ kT := by
857 intro heq; apply hjk; exact congrArg Subtype.val heq
858 have hbit : rawBit jT kT i ⟨h, hh_lt_all⟩ = patternCol i ⟨h, hh_lt_all⟩ := by
859 rw [colour_eq hjT hkT hj_ne_k]
860 rw [hpat_col] at hbit
861 have hi_S₂ : i ∈ S₂ := hS₃_sub hi
862 have hi_ne_j : i ≠ jT.val := hij
863 have hi_ne_k : i ≠ kT.val := hik
864 simp only [rawBit] at hbit
865 rw [dif_neg hi_ne_j, dif_neg hi_ne_k, dif_pos hi_S₂] at hbit
866 exact of_decide_eq_false hbit
867 -- Package the data.
868 refine
869 { toUniformLengthData :=
870 { toCandidatePathData := hStep2.toCandidatePathData
871 subclique := S₃
872 subclique_card_ge := hS₃_card
873 commonLength := hStep2.commonLength
874 commonLength_le := hStep2.commonLength_le
875 hasCommonLengthWalk := fun hi hj hij =>
876 hStep2.hasCommonLengthWalk (hS₃_sub hi) (hS₃_sub hj) hij }
877 canonicalWalk := fun hi hj hij => walk (hS₃_sub hi) (hS₃_sub hj) hij
878 canonicalWalk_length := fun hi hj hij =>
879 walk_length (hS₃_sub hi) (hS₃_sub hj) hij
880 patternShared := patternShared
881 patternShared_shared := @shared_spec
882 patternShared_disjoint := @disjoint_spec }
883
884/-- Backward direction, Step 4: cut the shared prefixes and suffixes,
885perform one more Ramsey round on interior collisions, and produce the
886system of internally disjoint trimmed walks required by Step 5.
887
888Currently an open scaffold leaf; see `formalization-notes.md` under "Step 4
889(trimming)" for the proof plan. The design of `TrimmedPathData` above
890matches what `backward_step5_build_subdivision` needs to assemble an
891`IsContained` witness: uniform-length walks between branch-set-anchored
892centres, pairwise interior-disjoint, each a path. -/
893private noncomputable def backward_step4_trim_paths
894 {V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V}
895 {d t m : ℕ}
896 (hStep3 : CanonicalPatternData G d t m) :
897 TrimmedPathData G d t m := by
898 sorry
899
900/-- Backward direction, Step 5: package the cleaned path system as a
901subdivided-clique subgraph. -/
902private noncomputable def backward_step5_build_subdivision
903 {V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V}
904 {d t m : ℕ}
905 (hStep4 : TrimmedPathData G d t m) :
906 CleanSubdivisionData G d t m := by
907 sorry
908
909/-- Backward direction, Step 6: choose a Ramsey threshold `t(d)` and a
910subdivision-order target `m` so that any cleaned Step-5 subdivision witness
911of order `≥ m` contradicts the local nowhere-dense hypothesis. The
912`hThresh` field feeds Step 2's multicolour-Ramsey threshold; `hThresh3`
913similarly feeds Step 3's branching-pattern Ramsey. This is where the
914six-step scaffold collapses back to the catalog bound
915`HasShallowCliqueBound C d t(d)`. -/
916private theorem backward_step6_extract_bound
917 (C : GraphClass)
918 (hDev : Dev.MonadicDependence.NowhereDense.IsNowhereDense C)
919 (d : ℕ) :
920 ∃ (t m : ℕ),
921 (Catalog.Sparsity.MulticolorRamsey.multicolorRamsey
922 (List.replicate (2 * d + 2) m)
923 List.replicate_succ_ne_nil).choose ≤ t + 1 ∧
924 (Catalog.Sparsity.MulticolorRamsey.multicolorRamsey
925 (List.replicate
926 (Fintype.card (Fin (t + 1) → Fin (2 * d + 1) → Bool)) m)
927 (step3_sizes_ne_nil d t m)).choose ≤ m ∧
928 ∀ {V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V},
929 C G → CleanSubdivisionData G d t m → False := by
930 sorry
931
932/-- Local subdivided-clique nowhere denseness implies the catalog shallow-
933minor formulation. The Ramsey bookkeeping is split into six helper steps
934matching `formalization-notes.md`. -/
935private theorem dev_nowhereDense_to_catalog_nowhereDense
936 (C : GraphClass)
937 (hDev : Dev.MonadicDependence.NowhereDense.IsNowhereDense C) :
938 Catalog.Sparsity.NowhereDense.IsNowhereDense C := by
939 intro d
940 rcases backward_step6_extract_bound C hDev d with
941 ⟨t, m, hThresh, hThresh3, hStep6⟩
942 refine ⟨t, ?_⟩
943 intro V _ _ G hCG hMinor
944 let step1 : CandidatePathData G d t := backward_step1_candidate_paths hMinor
945 let step2 : UniformLengthData G d t m :=
946 backward_step2_uniform_length step1 hThresh
947 let step3 : CanonicalPatternData G d t m :=
948 backward_step3_canonical_pattern step2 hThresh3
949 let step4 : TrimmedPathData G d t m := backward_step4_trim_paths step3
950 let step5 : CleanSubdivisionData G d t m :=
951 backward_step5_build_subdivision step4
952 exact hStep6 hCG step5
953
954/-- Folklore equivalence between the local and shallow-minor
955formulations of nowhere-denseness. See `Contract.lean` for the
956statement-level discussion and `formalization-notes.md` for the
957proof strategy. -/
958theorem nowhereDenseBridge (C : GraphClass) :
959 Dev.MonadicDependence.NowhereDense.IsNowhereDense C ↔
960 Catalog.Sparsity.NowhereDense.IsNowhereDense C := by
961 constructor
962 · exact dev_nowhereDense_to_catalog_nowhereDense C
963 · exact catalog_nowhereDense_to_dev_nowhereDense C
964
965end Dev.MonadicDependence.NowhereDenseBridge
966