Formalizing Structural Graph Theory in Lean 4

Dev/MonadicDependence/WeaklySparseMonDepIsNowhereDense/Full.lean
1import Mathlib.Data.Fintype.Pigeonhole
2import Mathlib.Order.Interval.Finset.Basic
3import Mathlib.Order.Interval.Finset.Nat
4import Catalog.Sparsity.Preliminaries.Full
5import Dev.MonadicDependence.WeaklySparse.Full
6import Dev.MonadicDependence.MonadicDependence.Full
7import Dev.MonadicDependence.NowhereDense.Full
8import Dev.MonadicDependence.Biclique.Full
9import Dev.MonadicDependence.Subdivision.Full
10import Dev.MonadicDependence.Flip.Full
11import Dev.MonadicDependence.StarCrossing.Full
12import Dev.MonadicDependence.SubdividedBicliqueRamsey.Full
13
14namespace Dev.MonadicDependence.WeaklySparseMonDepIsNowhereDense
15
16open Catalog.Sparsity.Preliminaries
17open Dev.MonadicDependence.WeaklySparse
18open Dev.MonadicDependence.MonadicDependence
19open Dev.MonadicDependence.NowhereDense
20open Dev.MonadicDependence.Biclique
21open Dev.MonadicDependence.Subdivision
22open Dev.MonadicDependence.Flip
23open Dev.MonadicDependence.StarCrossing
24open Dev.MonadicDependence.SubdividedBicliqueRamsey
25
26/-- With the empty layer relation `F = ⊥` the flip operation returns the
27original graph. Used in Step 3b to identify the unflipped star
28`r'`-crossing with a flipped one. -/
29lemma flip_bot {V α : Type*} (G : SimpleGraph V) (κ : V → α) :
30 flip G κ (⊥ : α → α → Prop) (fun _ _ h => h) = G := by
31 ext u v
32 change (u ≠ v ∧ (G.Adj u v ↔ ¬ (⊥ : α → α → Prop) (κ u) (κ v))) ↔ G.Adj u v
33 refine ⟨fun ⟨_, hiff⟩ => hiff.mpr (id : ¬ False), fun h => ⟨G.ne_of_adj h, ?_⟩⟩
34 exact ⟨fun _ hbot => hbot, fun _ => h⟩
35
36/-!
37### Step 1 helper: an `r`-subdivided biclique of order `⌊N/2⌋` is contained
38as a subgraph in the `r`-subdivided clique of order `N`.
39
40The embedding sends the left roots to `{0, …, ⌊N/2⌋ - 1}`, the right roots
41to `{⌊N/2⌋, …, 2⌊N/2⌋ - 1}`, and path vertices to the corresponding
42subdivision paths of the ordered edges `(leftFin i, rightFin j)` (well-defined
43because `leftFin i < rightFin j` whenever both are in range). The map is an
44injective graph homomorphism into the subdivided clique; the subdivided
45clique has *additional* edges (subdivision paths within each half, plus, for
46`r = 0`, every pair of principals adjacent) which are tolerated because
47`IsContained` is non-induced.
48
49Filling in the mechanical case analysis for `bicliqueHomToClique.map_rel'`
50and full injectivity is left as a sub-`sorry` pending a dedicated Close
51session; the top-level structure of the rest of the proof depends only on
52the statement of this lemma.
53-/
54
55/-- Left-half embedding `Fin (N/2) ↪ Fin N`: `i ↦ i`. -/
56private def leftFin (N : ℕ) (i : Fin (N / 2)) : Fin N :=
57 ⟨i.val, lt_of_lt_of_le i.isLt (Nat.div_le_self N 2)⟩
58
59/-- Right-half embedding `Fin (N/2) ↪ Fin N`: `j ↦ ⌊N/2⌋ + j`. -/
60private def rightFin (N : ℕ) (j : Fin (N / 2)) : Fin N :=
61 ⟨N / 2 + j.val, by
62 have h1 : j.val < N / 2 := j.isLt
63 have h2 : N / 2 * 2 ≤ N := Nat.div_mul_le_self N 2
64 omega⟩
65
66private lemma leftFin_val (N : ℕ) (i : Fin (N / 2)) :
67 (leftFin N i).val = i.val := rfl
68
69private lemma rightFin_val (N : ℕ) (j : Fin (N / 2)) :
70 (rightFin N j).val = N / 2 + j.val := rfl
71
72private lemma leftFin_lt_rightFin (N : ℕ) (i j : Fin (N / 2)) :
73 (leftFin N i).val < (rightFin N j).val := by
74 simp only [leftFin_val, rightFin_val]
75 have := i.isLt; omega
76
77private lemma leftFin_ne_rightFin (N : ℕ) (i j : Fin (N / 2)) :
78 leftFin N i ≠ rightFin N j := fun h => by
79 have h' : (leftFin N i).val = (rightFin N j).val := by rw [h]
80 simp only [leftFin_val, rightFin_val] at h'
81 have := i.isLt
82 omega
83
84private lemma leftFin_injective (N : ℕ) : Function.Injective (leftFin N) := by
85 intro i j h
86 apply Fin.ext
87 have h' : (leftFin N i).val = (leftFin N j).val := by rw [h]
88 simpa [leftFin_val] using h'
89
90private lemma rightFin_injective (N : ℕ) : Function.Injective (rightFin N) := by
91 intro i j h
92 apply Fin.ext
93 have h' : (rightFin N i).val = (rightFin N j).val := by rw [h]
94 simpa [rightFin_val] using h'
95
96/-- Vertex embedding `SubdividedBicliqueVert (N/2) r → SubdividedCliqueVert N r`. -/
97private def bicliqueVertToClique (N r : ℕ) :
98 SubdividedBicliqueVert (N / 2) r → SubdividedCliqueVert N r
99 | .inl (.inl i) => .inl (leftFin N i)
100 | .inl (.inr j) => .inl (rightFin N j)
101 | .inr ⟨⟨i, j⟩, k⟩ =>
102 .inr ⟨⟨(leftFin N i, rightFin N j), leftFin_lt_rightFin N i j⟩, k⟩
103
104private lemma bicliqueVertToClique_injective (N r : ℕ) :
105 Function.Injective (bicliqueVertToClique N r) := by
106 intro u v heq
107 rcases u with (iU | jU) | ⟨⟨iU, jU⟩, kU⟩ <;>
108 rcases v with (iV | jV) | ⟨⟨iV, jV⟩, kV⟩ <;>
109 dsimp only [bicliqueVertToClique] at heq
110 · exact congrArg (fun x => (Sum.inl (Sum.inl x) : SubdividedBicliqueVert (N/2) r))
111 (leftFin_injective N (Sum.inl.inj heq))
112 · exact absurd (Sum.inl.inj heq) (leftFin_ne_rightFin N _ _)
113 · cases heq
114 · exact absurd (Sum.inl.inj heq).symm (leftFin_ne_rightFin N _ _)
115 · exact congrArg (fun x => (Sum.inl (Sum.inr x) : SubdividedBicliqueVert (N/2) r))
116 (rightFin_injective N (Sum.inl.inj heq))
117 · cases heq
118 · cases heq
119 · cases heq
120 · have h := Sum.inr.inj heq
121 -- h : ((⟨(leftFin iU, rightFin jU), _⟩ : _ × _), kU)
122 -- = ((⟨(leftFin iV, rightFin jV), _⟩ : _ × _), kV)
123 obtain ⟨hSub, hk⟩ := Prod.mk.inj h
124 -- hSub : ⟨(leftFin iU, rightFin jU), _⟩ = ⟨(leftFin iV, rightFin jV), _⟩
125 have hpair : (leftFin N iU, rightFin N jU) = (leftFin N iV, rightFin N jV) :=
126 Subtype.ext_iff.mp hSub
127 obtain ⟨hil, hir⟩ := Prod.mk.inj hpair
128 have hi : iU = iV := leftFin_injective N hil
129 have hj : jU = jV := rightFin_injective N hir
130 subst hi; subst hj; subst hk; rfl
131
132/-- Adjacency-preserving hom induced by `bicliqueVertToClique`. -/
133private def bicliqueHomToClique (N r : ℕ) :
134 subdividedBiclique (N / 2) r →g subdividedClique N r where
135 toFun := bicliqueVertToClique N r
136 map_rel' := by
137 intro u v huv
138 rw [subdividedBiclique, SimpleGraph.fromRel_adj] at huv
139 rw [subdividedClique, SimpleGraph.fromRel_adj]
140 obtain ⟨hne, hor⟩ := huv
141 refine ⟨fun h => hne (bicliqueVertToClique_injective N r h), ?_⟩
142 rcases u with (iU | jU) | ⟨⟨iU, jU⟩, kU⟩ <;>
143 rcases v with (iV | jV) | ⟨⟨iV, jV⟩, kV⟩ <;>
144 dsimp only [bicliqueVertToClique] at *
145 · -- (L iU, L iV): biclique hor is `False ∨ False`
146 exact (hor.elim id id).elim
147 · -- (L iU, R jV): biclique hor is `r = 0 ∨ False`; clique goal is `r = 0 ∨ r = 0`
148 rcases hor with h | h
149 · exact Or.inl h
150 · exact h.elim
151 · -- (L iU, P iV jV kV): biclique hor is `(iU = iV ∧ kV = 0) ∨ False`;
152 -- clique goal is (iU,jU,kV)-relation on principal vs path
153 rcases hor with ⟨hii, hk⟩ | h
154 · exact Or.inl (Or.inl ⟨by rw [hii], hk⟩)
155 · exact h.elim
156 · -- (R jU, L iV): biclique hor is `False ∨ r = 0`; clique goal `r = 0 ∨ r = 0`
157 rcases hor with h | h
158 · exact h.elim
159 · exact Or.inr h
160 · -- (R jU, R jV): biclique hor `False ∨ False`
161 exact (hor.elim id id).elim
162 · -- (R jU, P iV jV kV): biclique hor is `(jU = jV ∧ kV = r-1) ∨ False`
163 rcases hor with ⟨hjj, hk⟩ | h
164 · exact Or.inl (Or.inr ⟨by rw [hjj], hk⟩)
165 · exact h.elim
166 · -- (P iU jU kU, L iV): biclique hor is `False ∨ (iV = iU ∧ kU = 0)`
167 rcases hor with h | ⟨hii, hk⟩
168 · exact h.elim
169 · exact Or.inr (Or.inl ⟨by rw [hii], hk⟩)
170 · -- (P iU jU kU, R jV): biclique hor is `False ∨ (jV = jU ∧ kU = r-1)`
171 rcases hor with h | ⟨hjj, hk⟩
172 · exact h.elim
173 · exact Or.inr (Or.inr ⟨by rw [hjj], hk⟩)
174 · -- (P iU jU kU, P iV jV kV): biclique hor
175 -- is `((iU,jU) = (iV,jV) ∧ kU+1=kV) ∨ ((iV,jV) = (iU,jU) ∧ kV+1=kU)`
176 rcases hor with ⟨hij, hk⟩ | ⟨hij, hk⟩
177 · refine Or.inl ⟨?_, hk⟩
178 obtain ⟨hii, hjj⟩ := Prod.mk.inj hij
179 apply Subtype.ext
180 simp only [hii, hjj]
181 · refine Or.inr ⟨?_, hk⟩
182 obtain ⟨hii, hjj⟩ := Prod.mk.inj hij
183 apply Subtype.ext
184 simp only [hii, hjj]
185
186/-- Step 1 helper: an `r`-subdivided biclique of order `⌊N/2⌋` is contained
187as a subgraph in the `r`-subdivided clique of order `N`. -/
188lemma subdividedBiclique_isContained_subdividedClique (N r : ℕ) :
189 (subdividedBiclique (N / 2) r).IsContained (subdividedClique N r) :=
190 ⟨(bicliqueHomToClique N r).toCopy (bicliqueVertToClique_injective N r)⟩
191
192/-!
193### r=0 helper: the biclique `K_{⌊N/2⌋, ⌊N/2⌋}` is a subgraph of the
194`0`-subdivided clique of order `N`.
195-/
196
197private def bicliqueVertToCliqueZero (N : ℕ) :
198 (Fin (N / 2) ⊕ Fin (N / 2)) → SubdividedCliqueVert N 0
199 | .inl i => .inl (leftFin N i)
200 | .inr j => .inl (rightFin N j)
201
202private lemma bicliqueVertToCliqueZero_injective (N : ℕ) :
203 Function.Injective (bicliqueVertToCliqueZero N) := by
204 intro u v heq
205 rcases u with iU | jU <;> rcases v with iV | jV <;>
206 simp only [bicliqueVertToCliqueZero] at heq
207 · exact congrArg Sum.inl (leftFin_injective N (Sum.inl.inj heq))
208 · exact absurd (Sum.inl.inj heq) (leftFin_ne_rightFin N _ _)
209 · exact absurd (Sum.inl.inj heq).symm (leftFin_ne_rightFin N _ _)
210 · exact congrArg Sum.inr (rightFin_injective N (Sum.inl.inj heq))
211
212private def bicliqueHomToCliqueZero (N : ℕ) :
213 biclique (N / 2) →g subdividedClique N 0 where
214 toFun := bicliqueVertToCliqueZero N
215 map_rel' := by
216 intro u v huv
217 rcases u with iU | jU <;> rcases v with iV | jV
218 · exact absurd huv (by simp [biclique, completeBipartiteGraph])
219 · refine ⟨fun h => leftFin_ne_rightFin N _ _ (Sum.inl.inj h), ?_⟩
220 exact Or.inl (by show (0 : ℕ) = 0; rfl)
221 · refine ⟨fun h => (leftFin_ne_rightFin N _ _) (Sum.inl.inj h).symm, ?_⟩
222 exact Or.inl (by show (0 : ℕ) = 0; rfl)
223 · exact absurd huv (by simp [biclique, completeBipartiteGraph])
224
225/-- A biclique of order `⌊N/2⌋` is contained as a subgraph in the
226`0`-subdivided clique of order `N`. -/
227lemma biclique_isContained_subdividedClique_zero (N : ℕ) :
228 (biclique (N / 2)).IsContained (subdividedClique N 0) :=
229 ⟨(bicliqueHomToCliqueZero N).toCopy (bicliqueVertToCliqueZero_injective N)⟩
230
231/-!
232### Helper: biclique-mono.
233`biclique k ⊑ biclique m` whenever `k ≤ m`.
234-/
235
236lemma biclique_isContained_biclique_of_le {k m : ℕ} (h : k ≤ m) :
237 (biclique k).IsContained (biclique m) := by
238 -- `Fin k ↪ Fin m` via `Fin.castLE` gives a hom of complete bipartite graphs.
239 refine ⟨?_⟩
240 refine
241 { toHom :=
242 { toFun := fun v =>
243 match v with
244 | .inl i => .inl (Fin.castLE h i)
245 | .inr j => .inr (Fin.castLE h j)
246 map_rel' := by
247 intro u v huv
248 rcases u with iU | jU <;> rcases v with iV | jV <;>
249 simp_all [biclique, completeBipartiteGraph] }
250 injective' := ?_ }
251 intro u v heq
252 rcases u with iU | jU <;> rcases v with iV | jV
253 · have h := Sum.inl.inj heq
254 exact congrArg (fun x => (Sum.inl x : Fin k ⊕ Fin k))
255 (Fin.ext (by simpa using congrArg (Fin.val : Fin m → ℕ) h))
256 · cases heq
257 · cases heq
258 · have h := Sum.inr.inj heq
259 exact congrArg (fun x => (Sum.inr x : Fin k ⊕ Fin k))
260 (Fin.ext (by simpa using congrArg (Fin.val : Fin m → ℕ) h))
261
262/-!
263### Helper: induced biclique mono.
264`subdividedBiclique k r ⊴ subdividedBiclique m r` whenever `k ≤ m`, via
265the obvious inclusion `Fin.castLE` on each coordinate.
266-/
267
268private lemma subdividedBiclique_isIndContained_of_le {k m r : ℕ} (h : k ≤ m) :
269 (subdividedBiclique k r).IsIndContained (subdividedBiclique m r) := by
270 refine ⟨{
271 toFun := fun v => match v with
272 | .inl (.inl i) => .inl (.inl (Fin.castLE h i))
273 | .inl (.inr j) => .inl (.inr (Fin.castLE h j))
274 | .inr ⟨⟨i, j⟩, k'⟩ => .inr ⟨⟨Fin.castLE h i, Fin.castLE h j⟩, k'⟩
275 inj' := by
276 intro u v heq
277 rcases u with (iU | jU) | ⟨⟨iU, jU⟩, kU⟩ <;>
278 rcases v with (iV | jV) | ⟨⟨iV, jV⟩, kV⟩ <;>
279 simp_all [Fin.ext_iff]
280 map_rel_iff' := by
281 intro u v
282 simp only [subdividedBiclique, SimpleGraph.fromRel_adj]
283 rcases u with (iU | jU) | ⟨⟨iU, jU⟩, kU⟩ <;>
284 rcases v with (iV | jV) | ⟨⟨iV, jV⟩, kV⟩ <;>
285 simp_all [Fin.ext_iff, Prod.ext_iff]
286 }⟩
287
288/-!
289### Main theorem.
290
291Negate `IsNowhereDense`, extract the bad `r`, then case on `r = 0` vs
292`r ≥ 1`. The `r = 0` branch uses `biclique_isContained_subdividedClique_zero`
293and immediately contradicts weak sparseness. The `r ≥ 1` branch goes
294through `subdividedBicliqueRamsey` and pigeonhole.
295-/
296
297/-- Mählmann Lemma 13.7: weakly sparse + monadically dependent ⇒
298nowhere dense (local sense). -/
299theorem weaklySparseMonDepIsNowhereDense (C : GraphClass) :
300 IsWeaklySparse C → IsMonadicallyDependent C → IsNowhereDense C := by
301 rintro ⟨kWS, hWS⟩ hMD
302 by_contra hNotND
303 -- Unfold and negate `IsNowhereDense`. Package all implicit instance
304 -- binders explicitly in the resulting existential.
305 have hBad : ∃ r : ℕ, ∀ N : ℕ, ∃ (V : Type) (_ : DecidableEq V)
306 (_ : Fintype V) (G : SimpleGraph V),
307 C G ∧ (subdividedClique N r).IsContained G := by
308 classical
309 by_contra hGood
310 apply hNotND
311 intro r
312 by_contra hNoN
313 apply hGood
314 refine ⟨r, ?_⟩
315 intro N
316 by_contra hNoWitness
317 apply hNoN
318 refine ⟨N, ?_⟩
319 intro V _ _ G hCG hContained
320 exact hNoWitness ⟨V, inferInstance, inferInstance, G, hCG, hContained⟩
321 obtain ⟨r, hr⟩ := hBad
322 -- `r = 0` branch: biclique contradiction.
323 rcases Nat.eq_zero_or_pos r with hr0 | hrPos
324 · subst hr0
325 -- For N = 2 * kWS + 1 we get a subdivided clique of order N with r=0;
326 -- this contains the biclique of order (N/2) ≥ kWS; contradicts weak
327 -- sparseness.
328 obtain ⟨V, instD, instF, G, hCG, hContained⟩ := hr (2 * kWS + 1)
329 have hContBiclique : (biclique ((2 * kWS + 1) / 2)).IsContained G :=
330 (biclique_isContained_subdividedClique_zero (2 * kWS + 1)).trans hContained
331 have hDiv : (2 * kWS + 1) / 2 = kWS := by omega
332 rw [hDiv] at hContBiclique
333 exact hWS G hCG hContBiclique
334 -- `r ≥ 1`: apply Ramsey.
335 -- For every `n`, the subdivided biclique of order `n` is contained
336 -- in some `G ∈ C`.
337 have hBiclique : ∀ n : ℕ, ∃ (V : Type) (_ : DecidableEq V)
338 (_ : Fintype V) (G : SimpleGraph V),
339 C G ∧ (subdividedBiclique n r).IsContained G := by
340 intro n
341 obtain ⟨V, instD, instF, G, hCG, hContained⟩ := hr (2 * n + 1)
342 refine ⟨V, instD, instF, G, hCG, ?_⟩
343 have hDiv : (2 * n + 1) / 2 = n := by omega
344 have step := subdividedBiclique_isContained_subdividedClique (2 * n + 1) r
345 rw [hDiv] at step
346 exact step.trans hContained
347 -- Apply `subdividedBicliqueRamsey`.
348 obtain ⟨U, _hUmono, hUunb, hRamsey⟩ := subdividedBicliqueRamsey r
349 -- Build the alternative at every `n`.
350 have hAlt : ∀ n : ℕ, ∃ (V : Type) (_ : DecidableEq V)
351 (_ : Fintype V) (G : SimpleGraph V), C G ∧
352 ((biclique (U n)).IsContained G ∨
353 ∃ r' : ℕ, 1 ≤ r' ∧ r' ≤ r ∧
354 (subdividedBiclique (U n) r').IsIndContained G) := by
355 intro n
356 obtain ⟨V, instD, instF, G, hCG, hContained⟩ := hBiclique n
357 exact ⟨V, instD, instF, G, hCG, hRamsey G n hContained⟩
358 -- Pigeonhole on the two top-level alternatives: either the biclique
359 -- alternative occurs for arbitrarily large `U n`, or the induced-biclique
360 -- alternative does; in the latter case, pigeonhole again on `Fin r`.
361 by_cases hBranch1 : ∀ M : ℕ, ∃ n : ℕ, M ≤ U n ∧
362 ∃ (V : Type) (_ : DecidableEq V) (_ : Fintype V) (G : SimpleGraph V),
363 C G ∧ (biclique (U n)).IsContained G
364 · -- Step 3a: biclique alternative → weak-sparseness contradiction.
365 obtain ⟨n, hUn, V, instD, instF, G, hCG, hContained⟩ := hBranch1 kWS
366 have : (biclique kWS).IsContained G :=
367 (biclique_isContained_biclique_of_le hUn).trans hContained
368 exact hWS G hCG this
369 · -- Branch 1 fails: then for some threshold `M₀`, no `n` with
370 -- `U n ≥ M₀` lands in the biclique alternative. Hence for every
371 -- larger target there is a new `n` landing in the induced-biclique
372 -- alternative. Pigeonhole on `Fin r` to fix a single `r' ∈ [r]`.
373 push_neg at hBranch1
374 obtain ⟨M₀, hM₀⟩ := hBranch1
375 -- For each `m ≥ M₀` choose an `n` with `U n ≥ m` exhibiting an induced
376 -- `r'`-biclique alternative (`r' ∈ [r]`), then pigeonhole on `r'`.
377 -- Combine into: there is a single `r' ∈ [r]` such that for every `m`
378 -- there is some `G ∈ C` containing an induced `r'`-subdivided biclique
379 -- of order ≥ `m`.
380 have hIndUnb : ∃ r' : ℕ, 1 ≤ r' ∧ r' ≤ r ∧ ∀ m : ℕ,
381 ∃ (V : Type) (_ : DecidableEq V) (_ : Fintype V) (G : SimpleGraph V),
382 C G ∧ ∃ n : ℕ, m ≤ n ∧ (subdividedBiclique n r').IsIndContained G := by
383 classical
384 haveI : NeZero r := ⟨Nat.one_le_iff_ne_zero.mp hrPos⟩
385 -- For each `M`, choose an index `n` with `U n ≥ max M M₀`, apply `hAlt`,
386 -- rule out the biclique alternative via `hM₀`, extract `r'(M) ∈ Fin r`.
387 have step : ∀ M : ℕ, ∃ (r' : Fin r) (n : ℕ),
388 M ≤ U n ∧
389 ∃ (V : Type) (_ : DecidableEq V) (_ : Fintype V) (G : SimpleGraph V),
390 C G ∧ (subdividedBiclique (U n) (r'.val + 1)).IsIndContained G := by
391 intro M
392 obtain ⟨n, hn⟩ := hUunb (max M M₀)
393 have hnM : M ≤ U n := (le_max_left _ _).trans hn
394 have hnM₀ : M₀ ≤ U n := (le_max_right _ _).trans hn
395 obtain ⟨V, instD, instF, G, hCG, hAltCase⟩ := hAlt n
396 rcases hAltCase with hbc | ⟨r', hr'1, hr'r, hIC⟩
397 · exfalso
398 exact (hM₀ n hnM₀ V instD instF G hCG).false hbc.some
399 · refine ⟨⟨r' - 1, by omega⟩, n, hnM, V, instD, instF, G, hCG, ?_⟩
400 have : r' - 1 + 1 = r' := by omega
401 rw [this]; exact hIC
402 -- Extract the r'-choice as a function ℕ → Fin r.
403 choose rChoice nChoice hChoice using step
404 -- Pigeonhole: some r₀ has infinite preimage under rChoice.
405 obtain ⟨r₀, hr₀inf⟩ := Finite.exists_infinite_fiber rChoice
406 refine ⟨r₀.val + 1, by omega, by omega, ?_⟩
407 intro m
408 -- Use that the preimage is infinite to find M ≥ m with rChoice M = r₀.
409 have hSetInf : (rChoice ⁻¹' {r₀}).Infinite := Set.infinite_coe_iff.mp hr₀inf
410 obtain ⟨M, hMmem, hMlt⟩ := hSetInf.exists_gt m
411 have hMeq : rChoice M = r₀ := hMmem
412 obtain ⟨hMbd, V, instD, instF, G, hCG, hICM⟩ := hChoice M
413 refine ⟨V, instD, instF, G, hCG, U (nChoice M), ?_, ?_⟩
414 · exact le_trans hMlt.le hMbd
415 · rw [← hMeq]; exact hICM
416 obtain ⟨r', hr'1, hr'r, hInd⟩ := hIndUnb
417 -- Step 3b: apply monadic dependence at `r'`.
418 obtain ⟨kMD, hMD'⟩ := hMD r' hr'1
419 -- Pick `m = kMD` and get an induced subdivided biclique of order `≥ kMD`.
420 obtain ⟨V, instD, instF, G, hCG, n, hnBound, hContained⟩ := hInd kMD
421 -- An induced subdivided biclique of order `n ≥ kMD` contains one of
422 -- order `kMD` (also induced).
423 have hContainedKMD :
424 (subdividedBiclique kMD r').IsIndContained G :=
425 (subdividedBiclique_isIndContained_of_le hnBound).trans hContained
426 -- The star `r'`-crossing is by definition `subdividedBiclique`, so the
427 -- induced subgraph is a flipped star `r'`-crossing with `F = ⊥`.
428 have hStar : (flip (starCrossing kMD r') layer
429 (⊥ : Fin (r' + 2) → Fin (r' + 2) → Prop) (fun _ _ h => h)).IsIndContained G := by
430 have : flip (starCrossing kMD r') layer
431 (⊥ : Fin (r' + 2) → Fin (r' + 2) → Prop) (fun _ _ h => h) =
432 subdividedBiclique kMD r' := by
433 simpa [starCrossing] using flip_bot (subdividedBiclique kMD r') layer
434 rw [this]
435 exact hContainedKMD
436 -- Contradiction with monadic dependence.
437 exact (hMD' G hCG).1 _ _ hStar
438
439end Dev.MonadicDependence.WeaklySparseMonDepIsNowhereDense
440