Dev/MonadicDependence/SubdividedBicliqueRamsey/Full.lean

1	import Mathlib.Combinatorics.SimpleGraph.Copy
2	import Mathlib.Combinatorics.SimpleGraph.Bipartite
3	import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
4	import Mathlib.Combinatorics.SimpleGraph.Metric
5	import Mathlib.Data.Finset.Sort
6	import Mathlib.Order.Monotone.Basic
7	import Catalog.Sparsity.Preliminaries.Full
8	import Dev.MonadicDependence.Biclique.Full
9	import Dev.MonadicDependence.Subdivision.Full
10	import Dev.MonadicDependence.BipartiteRamsey.Full
11
12	namespace Dev.MonadicDependence.SubdividedBicliqueRamsey
13
14	open Dev.MonadicDependence.Biclique
15	open Dev.MonadicDependence.Subdivision
16
17	/-- Boolean masks for equality / adjacency patterns on
18	`(aᵢ, p_{i,j,0}, …, p_{i,j,r}, bⱼ)`, i.e. `(r + 3)`-tuples in the successor
19	case. -/
20	private abbrev AtomicMask (r : ℕ) : Type :=
21	Fin (r + 3) × Fin (r + 3) → Bool
22
23	/-- Encodes the atomic type of two `(r + 3)`-tuples by their equality and
24	adjacency masks. This is the finite color space fed into Bipartite Ramsey. -/
25	private abbrev AtomicType (r : ℕ) : Type :=
26	AtomicMask r × AtomicMask r
27
28	private noncomputable abbrev atomicTypeEquivFin (r : ℕ) :
29	AtomicType r ≃ Fin (Fintype.card (AtomicType r)) :=
30	Fintype.equivFin (AtomicType r)
31
32	private lemma atomicType_card_pos (r : ℕ) :
33	0 < Fintype.card (AtomicType r) := by
34	classical
35	refine Fintype.card_pos_iff.mpr ?_
36	exact ⟨(fun _ => false, fun _ => false)⟩
37
38	private theorem biclique_isContained_subdividedBiclique_zero (n : ℕ) :
39	(biclique n).IsContained (subdividedBiclique n 0) := by
40	refine ⟨⟨{ toFun := Sum.inl, map_rel' := ?_ }, Sum.inl_injective⟩⟩
41	intro x y hxy
42	rcases x with i \| j <;> rcases y with i' \| j' <;>
43	simp [biclique, subdividedBiclique] at hxy ⊢
44
45	private theorem subdividedBicliqueRamsey_zero :
46	∃ U : ℕ → ℕ, Monotone U ∧ (∀ N : ℕ, ∃ n : ℕ, N ≤ U n) ∧
47	∀ {V : Type} [DecidableEq V] [Fintype V]
48	(G : SimpleGraph V) (n : ℕ),
49	(subdividedBiclique n 0).IsContained G →
50	(biclique (U n)).IsContained G ∨
51	∃ r' : ℕ, 1 ≤ r' ∧ r' ≤ 0 ∧
52	(subdividedBiclique (U n) r').IsIndContained G := by
53	refine ⟨id, fun _ _ hmn => hmn, ?_, ?_⟩
54	· intro N
55	exact ⟨N, le_rfl⟩
56	· intro V _ _ G n hsub
57	left
58	exact (biclique_isContained_subdividedBiclique_zero n).trans hsub
59
60	private def leftRootVertex {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
61	{G : SimpleGraph V} {n : ℕ}
62	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (i : Fin n) : V :=
63	copy (.inl (.inl i))
64
65	private def rightRootVertex {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
66	{G : SimpleGraph V} {n : ℕ}
67	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (j : Fin n) : V :=
68	copy (.inl (.inr j))
69
70	private def pathVertex {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
71	{G : SimpleGraph V} {n : ℕ}
72	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
73	(i j : Fin n) (k : Fin (r + 1)) : V :=
74	copy (.inr ((i, j), k))
75
76	private def tupleVertexSet {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
77	{G : SimpleGraph V} {n : ℕ}
78	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
79	(i j : Fin n) : Set V :=
80	{v \| v = leftRootVertex copy i ∨ v = rightRootVertex copy j ∨
81	∃ k : Fin (r + 1), v = pathVertex copy i j k}
82
83	private def tupleInduced {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
84	{G : SimpleGraph V} {n : ℕ}
85	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
86	(i j : Fin n) : SimpleGraph {v // v ∈ tupleVertexSet copy i j} :=
87	G.induce (tupleVertexSet copy i j)
88
89	private theorem mem_tupleVertexSet_left {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
90	{G : SimpleGraph V} {n : ℕ}
91	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
92	(i j : Fin n) :
93	leftRootVertex copy i ∈ tupleVertexSet copy i j := by
94	simp [tupleVertexSet]
95
96	private theorem mem_tupleVertexSet_right {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
97	{G : SimpleGraph V} {n : ℕ}
98	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
99	(i j : Fin n) :
100	rightRootVertex copy j ∈ tupleVertexSet copy i j := by
101	simp [tupleVertexSet]
102
103	private theorem mem_tupleVertexSet_path {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
104	{G : SimpleGraph V} {n : ℕ}
105	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
106	(i j : Fin n) (k : Fin (r + 1)) :
107	pathVertex copy i j k ∈ tupleVertexSet copy i j := by
108	simp [tupleVertexSet]
109
110	private def tupleLeftRoot {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
111	{G : SimpleGraph V} {n : ℕ}
112	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
113	(i j : Fin n) : {v // v ∈ tupleVertexSet copy i j} :=
114	⟨leftRootVertex copy i, mem_tupleVertexSet_left copy i j⟩
115
116	private def tupleRightRoot {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
117	{G : SimpleGraph V} {n : ℕ}
118	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
119	(i j : Fin n) : {v // v ∈ tupleVertexSet copy i j} :=
120	⟨rightRootVertex copy j, mem_tupleVertexSet_right copy i j⟩
121
122	private def tuplePathVertex {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
123	{G : SimpleGraph V} {n : ℕ}
124	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
125	(i j : Fin n) (k : Fin (r + 1)) : {v // v ∈ tupleVertexSet copy i j} :=
126	⟨pathVertex copy i j k, mem_tupleVertexSet_path copy i j k⟩
127
128	private def tuplePathToRight {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
129	{G : SimpleGraph V} {n : ℕ}
130	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
131	(i j : Fin n) :
132	(k : ℕ) → (hk : k < r + 1) →
133	(tupleInduced copy i j).Walk
134	(tuplePathVertex copy i j ⟨k, hk⟩)
135	(tupleRightRoot copy i j)
136	\| k, hk =>
137	if hlast : k + 1 = r + 1 then
138	.cons
139	(by
140	have hk_eq : k = r := by omega
141	apply SimpleGraph.induce_adj.2
142	simpa [tuplePathVertex, tupleRightRoot, pathVertex, rightRootVertex] using
143	(copy.toHom.map_adj <\| by
144	simp [subdividedBiclique, hk_eq]))
145	.nil
146	else
147	let hk' : k + 1 < r + 1 := Nat.lt_of_le_of_ne (Nat.succ_le_of_lt hk) hlast
148	.cons
149	(by
150	apply SimpleGraph.induce_adj.2
151	simpa [tuplePathVertex, pathVertex] using
152	(copy.toHom.map_adj <\| by
153	simp [subdividedBiclique]))
154	(tuplePathToRight copy i j (k + 1) hk')
155	termination_by k => r + 1 - k
156	decreasing_by
157	omega
158
159	private def tupleWitnessWalk {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
160	{G : SimpleGraph V} {n : ℕ}
161	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
162	(i j : Fin n) :
163	(tupleInduced copy i j).Walk
164	(tupleLeftRoot copy i j)
165	(tupleRightRoot copy i j) :=
166	.cons
167	(by
168	apply SimpleGraph.induce_adj.2
169	simpa [tupleLeftRoot, tuplePathVertex, leftRootVertex, pathVertex] using
170	(copy.toHom.map_adj <\| by
171	simp [subdividedBiclique]))
172	(tuplePathToRight copy i j 0 (Nat.succ_pos r))
173
174	private def lastFin (n : ℕ) (hn : 1 ≤ n) : Fin n :=
175	⟨n - 1, Nat.sub_lt (Nat.lt_of_lt_of_le Nat.zero_lt_one hn) Nat.zero_lt_one⟩
176
177	private def firstFin (n : ℕ) (hn : 1 ≤ n) : Fin n :=
178	⟨0, hn⟩
179
180	/-- The degenerate two-point tuple sending both coordinates to `i`. Used to
181	probe the self atomic type of a single `(r + 2)`-tuple via the bipartite
182	Ramsey homogeneity statement. -/
183	private def diagPair {n : ℕ} (i : Fin n) : Fin 2 → Fin n :=
184	fun _ => i
185
186	private theorem orderType_diagPair {n : ℕ} (i : Fin n) :
187	Dev.MonadicDependence.BipartiteRamsey.orderType (diagPair i) =
188	fun _ => Ordering.eq := by
189	ext p
190	simp [diagPair, Dev.MonadicDependence.BipartiteRamsey.orderType]
191
192	/-- The `(r + 3)`-tuple `(aᵢ, p_{i,j,0}, …, p_{i,j,r}, bⱼ)` used for the
193	atomic-type coloring in the successor case. -/
194	private def atomicTuple {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
195	{G : SimpleGraph V} {n : ℕ}
196	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
197	(a b : Fin n) : Fin (r + 3) → V :=
198	fun t =>
199	if h : t.1 = 0 then
200	leftRootVertex copy a
201	else if hlast : t.1 = r + 2 then
202	rightRootVertex copy b
203	else
204	pathVertex copy a b
205	⟨t.1 - 1, by
206	have ht : t.1 < r + 3 := t.2
207	have hpos : 0 < t.1 := Nat.pos_of_ne_zero h
208	have hlt : t.1 < r + 2 := by omega
209	exact (Nat.sub_lt_iff_lt_add hpos).2 hlt⟩
210
211	private theorem atomicTuple_zero {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
212	{G : SimpleGraph V} {n : ℕ}
213	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
214	(a b : Fin n) :
215	atomicTuple copy a b 0 = leftRootVertex copy a := by
216	simp [atomicTuple]
217
218	private theorem atomicTuple_last {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
219	{G : SimpleGraph V} {n : ℕ}
220	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
221	(a b : Fin n) :
222	atomicTuple copy a b (lastFin (r + 3) (by omega)) = rightRootVertex copy b := by
223	have hne : ¬((lastFin (r + 3) (by omega) : Fin (r + 3)).1 = 0) := by
224	simp [lastFin]
225	have hlast :
226	(lastFin (r + 3) (by omega) : Fin (r + 3)).1 = r + 2 := by
227	simp [lastFin]
228	simp [atomicTuple, hlast]
229
230	private theorem atomicTuple_mem_tupleVertexSet {r : ℕ} {V : Type}
231	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
232	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
233	(a b : Fin n) (t : Fin (r + 3)) :
234	atomicTuple copy a b t ∈ tupleVertexSet copy a b := by
235	by_cases h0 : t.1 = 0
236	· simp [atomicTuple, h0, tupleVertexSet]
237	by_cases hlast : t.1 = r + 2
238	· simp [atomicTuple, hlast, tupleVertexSet]
239	· simp [atomicTuple, h0, hlast, tupleVertexSet]
240
241	/-- The labeled tuple graph on positions `0, …, r + 2`, where position `0`
242	is the left root, positions `1, …, r + 1` are the subdivision vertices, and
243	position `r + 2` is the right root. This is the discrete graph whose shortest
244	paths should eventually be transported across the Ramsey block. -/
245	private def tuplePositionGraph {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
246	{G : SimpleGraph V} {n : ℕ}
247	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
248	(a b : Fin n) : SimpleGraph (Fin (r + 3)) where
249	Adj s t := G.Adj (atomicTuple copy a b s) (atomicTuple copy a b t)
250	symm := by
251	intro s t h
252	exact G.symm h
253	loopless := ⟨fun s => by
254	simpa using G.loopless.irrefl (atomicTuple copy a b s)⟩
255
256	private noncomputable def atomicTypeOf {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
257	(G : SimpleGraph V) {n : ℕ}
258	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
259	(a : Fin 2 → Fin n) (b : Fin 2 → Fin n) : AtomicType r := by
260	classical
261	let t₀ := atomicTuple copy (a 0) (b 0)
262	let t₁ := atomicTuple copy (a 1) (b 1)
263	exact
264	(fun p => decide (t₀ p.1 = t₁ p.2),
265	fun p => decide (G.Adj (t₀ p.1) (t₁ p.2)))
266
267	/-- Step 3 coloring extracted from a subdivided-biclique witness. It records a
268	copy of the `subdividedBiclique n (r + 1)` inside `G`, and `c` is exactly the
269	finite encoding of the equality/adjacency masks between the two selected
270	root-plus-path tuples. -/
271	private structure HasAtomicTypeColoring (r : ℕ) {V : Type} [DecidableEq V] [Fintype V]
272	(G : SimpleGraph V) (n : ℕ)
273	(_hsub : (subdividedBiclique n (r + 1)).IsContained G)
274	(c : (Fin 2 → Fin n) → (Fin 2 → Fin n) → Fin (Fintype.card (AtomicType r))) where
275	copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G
276	color_eq : ∀ a b, c a b = atomicTypeEquivFin r (atomicTypeOf G copy a b)
277
278	/-- Packaged Step 5 data on a homogeneous Ramsey block.
279
280	At the current scaffold stage we expose the witness copy together with the
281	chosen shortest paths and the first genuine homogeneity consequence available
282	from the Ramsey block: every diagonal tuple `(aᵢ, p_{i,j,*}, bⱼ)` with
283	`i ∈ I`, `j ∈ J` has the same self atomic type. The eventual common-index
284	sequence can be extracted from this without changing consumers of the record. -/
285	private structure HasHomogeneousShortestPaths (r : ℕ) {V : Type}
286	[DecidableEq V] [Fintype V] (G : SimpleGraph V) (n : ℕ)
287	(_hsub : (subdividedBiclique n (r + 1)).IsContained G)
288	(_I _J : Finset (Fin n)) where
289	copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G
290	shortestPath :
291	∀ i j,
292	let H := tupleInduced copy i j
293	H.Path (tupleLeftRoot copy i j) (tupleRightRoot copy i j)
294	shortestPath_length_eq_dist : ∀ i j,
295	let H := tupleInduced copy i j
296	((shortestPath i j : H.Walk (tupleLeftRoot copy i j) (tupleRightRoot copy i j)).length) =
297	H.dist (tupleLeftRoot copy i j) (tupleRightRoot copy i j)
298	atomicType_eq_of_orderType :
299	∀ {a a' b b' : Fin 2 → Fin n},
300	(∀ i, a i ∈ _I) → (∀ i, a' i ∈ _I) →
301	(∀ j, b j ∈ _J) → (∀ j, b' j ∈ _J) →
302	Dev.MonadicDependence.BipartiteRamsey.orderType a =
303	Dev.MonadicDependence.BipartiteRamsey.orderType a' →
304	Dev.MonadicDependence.BipartiteRamsey.orderType b =
305	Dev.MonadicDependence.BipartiteRamsey.orderType b' →
306	atomicTypeOf G copy a b = atomicTypeOf G copy a' b'
307	diagonal_atomicType_eq :
308	∀ {i i' j j' : Fin n},
309	i ∈ _I → i' ∈ _I → j ∈ _J → j' ∈ _J →
310	atomicTypeOf G copy (diagPair i) (diagPair j) =
311	atomicTypeOf G copy (diagPair i') (diagPair j')
312
313	/-- Generic two-point tuple used to talk about ordered pairs of indices on a
314	Ramsey block. -/
315	private def pairTuple {n : ℕ} (x y : Fin n) : Fin 2 → Fin n
316	\| 0 => x
317	\| 1 => y
318
319	private theorem diagonal_left_right_adj_iff {r : ℕ} {V : Type}
320	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
321	{hsub : (subdividedBiclique n (r + 1)).IsContained G}
322	{I J : Finset (Fin n)}
323	(hpaths : HasHomogeneousShortestPaths r G n hsub I J)
324	{i i' j j' : Fin n}
325	(hi : i ∈ I) (hi' : i' ∈ I) (hj : j ∈ J) (hj' : j' ∈ J) :
326	G.Adj (leftRootVertex hpaths.copy i) (rightRootVertex hpaths.copy j) ↔
327	G.Adj (leftRootVertex hpaths.copy i') (rightRootVertex hpaths.copy j') := by
328	have hEq :=
329	hpaths.diagonal_atomicType_eq hi hi' hj hj'
330	let z : Fin (r + 3) := 0
331	let l : Fin (r + 3) := lastFin (r + 3) (by omega)
332	have hMask :
333	(atomicTypeOf G hpaths.copy (diagPair i) (diagPair j)).2 (z, l) =
334	(atomicTypeOf G hpaths.copy (diagPair i') (diagPair j')).2 (z, l) := by
335	exact congrArg (fun t => t.2 (z, l)) hEq
336	simp [atomicTypeOf, diagPair, z, l, atomicTuple_zero, atomicTuple_last] at hMask ⊢
337	exact hMask
338
339	private theorem atomicType_eq_iff_eq {r : ℕ} {V : Type}
340	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
341	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
342	{a a' b b' : Fin 2 → Fin n} {s t : Fin (r + 3)}
343	(hEq : atomicTypeOf G copy a b = atomicTypeOf G copy a' b') :
344	atomicTuple copy (a 0) (b 0) s = atomicTuple copy (a 1) (b 1) t ↔
345	atomicTuple copy (a' 0) (b' 0) s = atomicTuple copy (a' 1) (b' 1) t := by
346	have hMask :
347	(atomicTypeOf G copy a b).1 (s, t) =
348	(atomicTypeOf G copy a' b').1 (s, t) := by
349	exact congrArg (fun ty => ty.1 (s, t)) hEq
350	simpa [atomicTypeOf] using hMask
351
352	private theorem atomicType_eq_iff_adj {r : ℕ} {V : Type}
353	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
354	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
355	{a a' b b' : Fin 2 → Fin n} {s t : Fin (r + 3)}
356	(hEq : atomicTypeOf G copy a b = atomicTypeOf G copy a' b') :
357	G.Adj (atomicTuple copy (a 0) (b 0) s) (atomicTuple copy (a 1) (b 1) t) ↔
358	G.Adj (atomicTuple copy (a' 0) (b' 0) s) (atomicTuple copy (a' 1) (b' 1) t) := by
359	have hMask :
360	(atomicTypeOf G copy a b).2 (s, t) =
361	(atomicTypeOf G copy a' b').2 (s, t) := by
362	exact congrArg (fun ty => ty.2 (s, t)) hEq
363	simpa [atomicTypeOf] using hMask
364
365	private theorem diagonal_atomicTuple_eq_iff {r : ℕ} {V : Type}
366	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
367	{hsub : (subdividedBiclique n (r + 1)).IsContained G}
368	{I J : Finset (Fin n)}
369	(hpaths : HasHomogeneousShortestPaths r G n hsub I J)
370	{i i' j j' : Fin n}
371	(hi : i ∈ I) (hi' : i' ∈ I) (hj : j ∈ J) (hj' : j' ∈ J)
372	{s t : Fin (r + 3)} :
373	atomicTuple hpaths.copy i j s = atomicTuple hpaths.copy i j t ↔
374	atomicTuple hpaths.copy i' j' s = atomicTuple hpaths.copy i' j' t := by
375	exact atomicType_eq_iff_eq hpaths.copy (hpaths.diagonal_atomicType_eq hi hi' hj hj')
376
377	private theorem diagonal_atomicTuple_adj_iff {r : ℕ} {V : Type}
378	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
379	{hsub : (subdividedBiclique n (r + 1)).IsContained G}
380	{I J : Finset (Fin n)}
381	(hpaths : HasHomogeneousShortestPaths r G n hsub I J)
382	{i i' j j' : Fin n}
383	(hi : i ∈ I) (hi' : i' ∈ I) (hj : j ∈ J) (hj' : j' ∈ J)
384	{s t : Fin (r + 3)} :
385	G.Adj (atomicTuple hpaths.copy i j s) (atomicTuple hpaths.copy i j t) ↔
386	G.Adj (atomicTuple hpaths.copy i' j' s) (atomicTuple hpaths.copy i' j' t) := by
387	exact atomicType_eq_iff_adj hpaths.copy (hpaths.diagonal_atomicType_eq hi hi' hj hj')
388
389	private theorem pair_atomicType_eq {r : ℕ} {V : Type}
390	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
391	{hsub : (subdividedBiclique n (r + 1)).IsContained G}
392	{I J : Finset (Fin n)}
393	(hpaths : HasHomogeneousShortestPaths r G n hsub I J)
394	{i₀ i₁ i₀' i₁' j₀ j₁ j₀' j₁' : Fin n}
395	(hi : ∀ t, pairTuple i₀ i₁ t ∈ I)
396	(hi' : ∀ t, pairTuple i₀' i₁' t ∈ I)
397	(hj : ∀ t, pairTuple j₀ j₁ t ∈ J)
398	(hj' : ∀ t, pairTuple j₀' j₁' t ∈ J)
399	(hoti :
400	Dev.MonadicDependence.BipartiteRamsey.orderType (pairTuple i₀ i₁) =
401	Dev.MonadicDependence.BipartiteRamsey.orderType (pairTuple i₀' i₁'))
402	(hotj :
403	Dev.MonadicDependence.BipartiteRamsey.orderType (pairTuple j₀ j₁) =
404	Dev.MonadicDependence.BipartiteRamsey.orderType (pairTuple j₀' j₁')) :
405	atomicTypeOf G hpaths.copy (pairTuple i₀ i₁) (pairTuple j₀ j₁) =
406	atomicTypeOf G hpaths.copy (pairTuple i₀' i₁') (pairTuple j₀' j₁') := by
407	exact hpaths.atomicType_eq_of_orderType hi hi' hj hj' hoti hotj
408
409	private theorem pair_atomicTuple_adj_iff {r : ℕ} {V : Type}
410	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
411	{hsub : (subdividedBiclique n (r + 1)).IsContained G}
412	{I J : Finset (Fin n)}
413	(hpaths : HasHomogeneousShortestPaths r G n hsub I J)
414	{i₀ i₁ i₀' i₁' j₀ j₁ j₀' j₁' : Fin n}
415	(hi : ∀ t, pairTuple i₀ i₁ t ∈ I)
416	(hi' : ∀ t, pairTuple i₀' i₁' t ∈ I)
417	(hj : ∀ t, pairTuple j₀ j₁ t ∈ J)
418	(hj' : ∀ t, pairTuple j₀' j₁' t ∈ J)
419	(hoti :
420	Dev.MonadicDependence.BipartiteRamsey.orderType (pairTuple i₀ i₁) =
421	Dev.MonadicDependence.BipartiteRamsey.orderType (pairTuple i₀' i₁'))
422	(hotj :
423	Dev.MonadicDependence.BipartiteRamsey.orderType (pairTuple j₀ j₁) =
424	Dev.MonadicDependence.BipartiteRamsey.orderType (pairTuple j₀' j₁'))
425	{s t : Fin (r + 3)} :
426	G.Adj (atomicTuple hpaths.copy i₀ j₀ s) (atomicTuple hpaths.copy i₁ j₁ t) ↔
427	G.Adj (atomicTuple hpaths.copy i₀' j₀' s) (atomicTuple hpaths.copy i₁' j₁' t) := by
428	exact atomicType_eq_iff_adj hpaths.copy
429	(pair_atomicType_eq hpaths hi hi' hj hj' hoti hotj)
430
431	private theorem diagonal_tuplePositionGraph_eq {r : ℕ} {V : Type}
432	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
433	{hsub : (subdividedBiclique n (r + 1)).IsContained G}
434	{I J : Finset (Fin n)}
435	(hpaths : HasHomogeneousShortestPaths r G n hsub I J)
436	{i i' j j' : Fin n}
437	(hi : i ∈ I) (hi' : i' ∈ I) (hj : j ∈ J) (hj' : j' ∈ J) :
438	tuplePositionGraph hpaths.copy i j = tuplePositionGraph hpaths.copy i' j' := by
439	ext s t
440	exact diagonal_atomicTuple_adj_iff hpaths hi hi' hj hj'
441
442	private def leftRootEmbedding {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
443	{G : SimpleGraph V} {n : ℕ}
444	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) : Fin n ↪ V where
445	toFun := leftRootVertex copy
446	inj' := by
447	intro i i' h
448	have h' : copy (.inl (.inl i)) = copy (.inl (.inl i')) := by
449	simpa [leftRootVertex] using h
450	have hs : (.inl (.inl i) : SubdividedBicliqueVert n (r + 1)) =
451	.inl (.inl i') := copy.injective h'
452	simpa using hs
453
454	private def rightRootEmbedding {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
455	{G : SimpleGraph V} {n : ℕ}
456	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) : Fin n ↪ V where
457	toFun := rightRootVertex copy
458	inj' := by
459	intro j j' h
460	have h' : copy (.inl (.inr j)) = copy (.inl (.inr j')) := by
461	simpa [rightRootVertex] using h
462	have hs : (.inl (.inr j) : SubdividedBicliqueVert n (r + 1)) =
463	.inl (.inr j') := copy.injective h'
464	simpa using hs
465
466	/-- Embedding `Fin n ↪ V` that fixes a right-root `j` and an internal index `k`
467	and varies the left-root `i`, sending `i ↦ p_{i,j,k}`. Used in the D-3 biclique
468	packager when the cross-edge witness pins `j` and `k`. -/
469	private def pathLeftEmbedding {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
470	{G : SimpleGraph V} {n : ℕ}
471	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
472	(j : Fin n) (k : Fin (r + 1)) : Fin n ↪ V where
473	toFun := fun i => pathVertex copy i j k
474	inj' := by
475	intro i i' h
476	have h' : copy (.inr ((i, j), k)) = copy (.inr ((i', j), k)) := by
477	simpa [pathVertex] using h
478	have hs : (.inr ((i, j), k) : SubdividedBicliqueVert n (r + 1)) =
479	.inr ((i', j), k) := copy.injective h'
480	have h₁ : ((i, j), k) = ((i', j), k) := by simpa using hs
481	exact (Prod.mk.inj (Prod.mk.inj h₁).1).1
482
483	/-- Embedding `Fin n ↪ V` that fixes a left-root `i` and an internal index `k`
484	and varies the right-root `j`, sending `j ↦ p_{i,j,k}`. Used in the D-4 biclique
485	packager when the cross-edge witness pins `i` and `k`. -/
486	private def pathRightEmbedding {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
487	{G : SimpleGraph V} {n : ℕ}
488	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
489	(i : Fin n) (k : Fin (r + 1)) : Fin n ↪ V where
490	toFun := fun j => pathVertex copy i j k
491	inj' := by
492	intro j j' h
493	have h' : copy (.inr ((i, j), k)) = copy (.inr ((i, j'), k)) := by
494	simpa [pathVertex] using h
495	have hs : (.inr ((i, j), k) : SubdividedBicliqueVert n (r + 1)) =
496	.inr ((i, j'), k) := copy.injective h'
497	have h₁ : ((i, j), k) = ((i, j'), k) := by simpa using hs
498	exact (Prod.mk.inj (Prod.mk.inj h₁).1).2
499
500	private theorem biclique_isContained_of_completeRoots {r : ℕ} {V : Type}
501	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n m : ℕ}
502	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
503	(I J : Finset (Fin n)) (hIcard : m ≤ I.card) (hJcard : m ≤ J.card)
504	(hcomplete : ∀ i, i ∈ I → ∀ j, j ∈ J →
505	G.Adj (leftRootVertex copy i) (rightRootVertex copy j)) :
506	(biclique m).IsContained G := by
507	classical
508	obtain ⟨I', hI', hI'card⟩ := Finset.exists_subset_card_eq hIcard
509	obtain ⟨J', hJ', hJ'card⟩ := Finset.exists_subset_card_eq hJcard
510	rw [biclique, SimpleGraph.completeBipartiteGraph_isContained_iff]
511	refine ⟨I'.map (leftRootEmbedding copy), J'.map (rightRootEmbedding copy), ?_, ?_, ?_⟩
512	· simp [hI'card]
513	· simp [hJ'card]
514	· intro u hu v hv
515	rw [Finset.mem_coe, Finset.mem_map] at hu hv
516	rcases hu with ⟨i, hiI', rfl⟩
517	rcases hv with ⟨j, hjJ', rfl⟩
518	exact hcomplete i (hI' hiI') j (hJ' hjJ')
519
520	/-- Like `biclique_isContained_of_completeRoots`, but both biclique sides land
521	on the left-root vertex set. Used in the `{a_i}` clique halving (Block D-1):
522	splitting `I` into a "small half" `L` and a "large half" `R` with every
523	`a_i ∼ a_{i'}` edge present between them already witnesses a biclique. -/
524	private theorem biclique_isContained_of_leftLeftComplete {r : ℕ} {V : Type}
525	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n m : ℕ}
526	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
527	(L R : Finset (Fin n)) (hLcard : m ≤ L.card) (hRcard : m ≤ R.card)
528	(hcomplete : ∀ i, i ∈ L → ∀ i', i' ∈ R →
529	G.Adj (leftRootVertex copy i) (leftRootVertex copy i')) :
530	(biclique m).IsContained G := by
531	classical
532	obtain ⟨L', hL', hL'card⟩ := Finset.exists_subset_card_eq hLcard
533	obtain ⟨R', hR', hR'card⟩ := Finset.exists_subset_card_eq hRcard
534	rw [biclique, SimpleGraph.completeBipartiteGraph_isContained_iff]
535	refine ⟨L'.map (leftRootEmbedding copy), R'.map (leftRootEmbedding copy), ?_, ?_, ?_⟩
536	· simp [hL'card]
537	· simp [hR'card]
538	· intro u hu v hv
539	rw [Finset.mem_coe, Finset.mem_map] at hu hv
540	rcases hu with ⟨i, hiL', rfl⟩
541	rcases hv with ⟨i', hi'R', rfl⟩
542	exact hcomplete i (hL' hiL') i' (hR' hi'R')
543
544	/-- Symmetric to `biclique_isContained_of_leftLeftComplete`: clique on the
545	right roots `{b_j}` yields a biclique. Used in Block D-2. -/
546	private theorem biclique_isContained_of_rightRightComplete {r : ℕ} {V : Type}
547	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n m : ℕ}
548	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
549	(L R : Finset (Fin n)) (hLcard : m ≤ L.card) (hRcard : m ≤ R.card)
550	(hcomplete : ∀ j, j ∈ L → ∀ j', j' ∈ R →
551	G.Adj (rightRootVertex copy j) (rightRootVertex copy j')) :
552	(biclique m).IsContained G := by
553	classical
554	obtain ⟨L', hL', hL'card⟩ := Finset.exists_subset_card_eq hLcard
555	obtain ⟨R', hR', hR'card⟩ := Finset.exists_subset_card_eq hRcard
556	rw [biclique, SimpleGraph.completeBipartiteGraph_isContained_iff]
557	refine ⟨L'.map (rightRootEmbedding copy), R'.map (rightRootEmbedding copy), ?_, ?_, ?_⟩
558	· simp [hL'card]
559	· simp [hR'card]
560	· intro u hu v hv
561	rw [Finset.mem_coe, Finset.mem_map] at hu hv
562	rcases hu with ⟨j, hjL', rfl⟩
563	rcases hv with ⟨j', hj'R', rfl⟩
564	exact hcomplete j (hL' hjL') j' (hR' hj'R')
565
566	/-- General biclique packager: given two embeddings `fL, fR : Fin n ↪ V` and
567	finsets `L, R ⊆ Fin n` with `\|L\|, \|R\| ≥ m`, if `G` has every edge between
568	`fL '' L` and `fR '' R`, then `(biclique m).IsContained G`. Used by the
569	"one-axis-halved" Block D-3/D-4/D-5 cross-edge halving cases, where one
570	embedding is a root embedding and the other is a `pathLeftEmbedding` /
571	`pathRightEmbedding`. -/
572	private theorem biclique_isContained_of_complete {V : Type} [DecidableEq V]
573	[Fintype V] {G : SimpleGraph V} {n m : ℕ}
574	(fL fR : Fin n ↪ V) (L R : Finset (Fin n))
575	(hLcard : m ≤ L.card) (hRcard : m ≤ R.card)
576	(hcomplete : ∀ i, i ∈ L → ∀ i', i' ∈ R → G.Adj (fL i) (fR i')) :
577	(biclique m).IsContained G := by
578	classical
579	obtain ⟨L', hL', hL'card⟩ := Finset.exists_subset_card_eq hLcard
580	obtain ⟨R', hR', hR'card⟩ := Finset.exists_subset_card_eq hRcard
581	rw [biclique, SimpleGraph.completeBipartiteGraph_isContained_iff]
582	refine ⟨L'.map fL, R'.map fR, ?_, ?_, ?_⟩
583	· simp [hL'card]
584	· simp [hR'card]
585	· intro u hu v hv
586	rw [Finset.mem_coe, Finset.mem_map] at hu hv
587	rcases hu with ⟨i, hiL', rfl⟩
588	rcases hv with ⟨i', hi'R', rfl⟩
589	exact hcomplete i (hL' hiL') i' (hR' hi'R')
590
591	/-- Any two strictly-ordered pairs on `Fin n` carry the same `orderType`. -/
592	private theorem orderType_pairTuple_eq_of_lt {n : ℕ} {i i' i'' i''' : Fin n}
593	(hlt : i < i') (hlt' : i'' < i''') :
594	Dev.MonadicDependence.BipartiteRamsey.orderType (pairTuple i i') =
595	Dev.MonadicDependence.BipartiteRamsey.orderType (pairTuple i'' i''') := by
596	ext ⟨p, q⟩
597	fin_cases p <;> fin_cases q <;>
598	simp [Dev.MonadicDependence.BipartiteRamsey.orderType, pairTuple,
599	compare_lt_iff_lt.mpr hlt, compare_lt_iff_lt.mpr hlt',
600	compare_gt_iff_gt.mpr hlt, compare_gt_iff_gt.mpr hlt']
601
602	/-- Any two strictly-reverse-ordered pairs on `Fin n` carry the same
603	`orderType`. Companion to `orderType_pairTuple_eq_of_lt` for the `gt` case. -/
604	private theorem orderType_pairTuple_eq_of_gt {n : ℕ} {i i' i'' i''' : Fin n}
605	(hgt : i > i') (hgt' : i'' > i''') :
606	Dev.MonadicDependence.BipartiteRamsey.orderType (pairTuple i i') =
607	Dev.MonadicDependence.BipartiteRamsey.orderType (pairTuple i'' i''') := by
608	ext ⟨p, q⟩
609	fin_cases p <;> fin_cases q <;>
610	simp [Dev.MonadicDependence.BipartiteRamsey.orderType, pairTuple,
611	compare_lt_iff_lt.mpr hgt, compare_lt_iff_lt.mpr hgt',
612	compare_gt_iff_gt.mpr hgt, compare_gt_iff_gt.mpr hgt']
613
614	/-- `diagPair` and `pairTuple` agree on repeated arguments. -/
615	private theorem pairTuple_self_eq_diagPair {n : ℕ} (i : Fin n) :
616	pairTuple i i = diagPair i := by
617	funext t
618	fin_cases t <;> rfl
619
620	/-- First-m elements (smallest) of `I`, indexed by the order-embedding
621	`I.orderEmbOfFin rfl`. Requires `m ≤ \|I\|`. -/
622	private noncomputable def firstHalfFinset {n : ℕ} (I : Finset (Fin n))
623	{m : ℕ} (hm : m ≤ I.card) : Finset (Fin n) :=
624	(Finset.univ : Finset (Fin m)).map
625	(Fin.castLEEmb hm \|>.trans (I.orderEmbOfFin rfl).toEmbedding)
626
627	/-- Last-m elements (largest) of `I`. Requires `m ≤ \|I\|`. -/
628	private noncomputable def lastHalfFinset {n : ℕ} (I : Finset (Fin n))
629	{m : ℕ} (hm : m ≤ I.card) : Finset (Fin n) :=
630	(Finset.univ : Finset (Fin m)).map
631	((⟨fun k : Fin m => ⟨I.card - m + k.val, by omega⟩,
632	fun a b hab => by
633	have : (I.card - m) + a.val = (I.card - m) + b.val := by
634	simpa using congrArg Fin.val hab
635	exact Fin.ext (by omega)⟩ : Fin m ↪ Fin I.card).trans
636	(I.orderEmbOfFin rfl).toEmbedding)
637
638	private theorem firstHalfFinset_subset {n : ℕ} (I : Finset (Fin n)) {m : ℕ}
639	(hm : m ≤ I.card) : firstHalfFinset I hm ⊆ I := by
640	intro x hx
641	rw [firstHalfFinset, Finset.mem_map] at hx
642	obtain ⟨k, _, rfl⟩ := hx
643	exact Finset.orderEmbOfFin_mem I rfl _
644
645	private theorem lastHalfFinset_subset {n : ℕ} (I : Finset (Fin n)) {m : ℕ}
646	(hm : m ≤ I.card) : lastHalfFinset I hm ⊆ I := by
647	intro x hx
648	rw [lastHalfFinset, Finset.mem_map] at hx
649	obtain ⟨k, _, rfl⟩ := hx
650	exact Finset.orderEmbOfFin_mem I rfl _
651
652	private theorem firstHalfFinset_card {n : ℕ} (I : Finset (Fin n)) {m : ℕ}
653	(hm : m ≤ I.card) : (firstHalfFinset I hm).card = m := by
654	simp [firstHalfFinset]
655
656	private theorem lastHalfFinset_card {n : ℕ} (I : Finset (Fin n)) {m : ℕ}
657	(hm : m ≤ I.card) : (lastHalfFinset I hm).card = m := by
658	simp [lastHalfFinset]
659
660	private theorem firstHalfFinset_lt_lastHalfFinset {n : ℕ} (I : Finset (Fin n))
661	{m : ℕ} (h2m : 2 * m ≤ I.card)
662	{i i' : Fin n}
663	(hi : i ∈ firstHalfFinset I (by omega : m ≤ I.card))
664	(hi' : i' ∈ lastHalfFinset I (by omega : m ≤ I.card)) :
665	i < i' := by
666	rw [firstHalfFinset, Finset.mem_map] at hi
667	obtain ⟨k, _, rfl⟩ := hi
668	rw [lastHalfFinset, Finset.mem_map] at hi'
669	obtain ⟨k', _, rfl⟩ := hi'
670	apply (I.orderEmbOfFin rfl).strictMono
671	rw [Fin.lt_def]
672	simp only [Fin.castLEEmb_apply, Function.Embedding.coeFn_mk, Fin.val_castLE]
673	have hk : k.val < m := k.isLt
674	have hk' : k'.val < m := k'.isLt
675	omega
676
677	private noncomputable def shortestTuplePathData {r : ℕ} {V : Type}
678	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
679	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
680	(i j : Fin n) :
681	Σ' p : (tupleInduced copy i j).Path (tupleLeftRoot copy i j) (tupleRightRoot copy i j),
682	((p : (tupleInduced copy i j).Walk (tupleLeftRoot copy i j) (tupleRightRoot copy i j)).length) =
683	(tupleInduced copy i j).dist (tupleLeftRoot copy i j) (tupleRightRoot copy i j) := by
684	classical
685	let h := (tupleWitnessWalk copy i j).reachable.exists_path_of_dist
686	exact ⟨⟨Classical.choose h, (Classical.choose_spec h).1⟩, (Classical.choose_spec h).2⟩
687
688	private noncomputable def shortestTuplePath {r : ℕ} {V : Type}
689	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
690	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
691	(i j : Fin n) :
692	(tupleInduced copy i j).Path (tupleLeftRoot copy i j) (tupleRightRoot copy i j) :=
693	(shortestTuplePathData copy i j).1
694
695	private theorem shortestTuplePath_length_eq_dist {r : ℕ} {V : Type}
696	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
697	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
698	(i j : Fin n) :
699	((shortestTuplePath copy i j :
700	(tupleInduced copy i j).Walk (tupleLeftRoot copy i j) (tupleRightRoot copy i j)).length) =
701	(tupleInduced copy i j).dist (tupleLeftRoot copy i j) (tupleRightRoot copy i j) :=
702	(shortestTuplePathData copy i j).2
703
704	private noncomputable def ramseyBlockLeftEmbedding {m n : ℕ}
705	(I : Finset (Fin n)) (hIcard : m ≤ I.card) : Fin m ↪ Fin n :=
706	by
707	let hcard' : Fintype.card (Fin m) ≤ I.card := by simpa using hIcard
708	exact Classical.choose
709	(Function.Embedding.exists_of_card_le_finset (α := Fin m) (s := I) hcard')
710
711	private theorem ramseyBlockLeftEmbedding_mem {m n : ℕ}
712	(I : Finset (Fin n)) (hIcard : m ≤ I.card) (x : Fin m) :
713	ramseyBlockLeftEmbedding I hIcard x ∈ I :=
714	by
715	let hcard' : Fintype.card (Fin m) ≤ I.card := by simpa using hIcard
716	exact Classical.choose_spec
717	(Function.Embedding.exists_of_card_le_finset (α := Fin m) (s := I) hcard') ⟨x, rfl⟩
718
719	private noncomputable def ramseyBlockRightEmbedding {m n : ℕ}
720	(J : Finset (Fin n)) (hJcard : m ≤ J.card) : Fin m ↪ Fin n :=
721	by
722	let hcard' : Fintype.card (Fin m) ≤ J.card := by simpa using hJcard
723	exact Classical.choose
724	(Function.Embedding.exists_of_card_le_finset (α := Fin m) (s := J) hcard')
725
726	private theorem ramseyBlockRightEmbedding_mem {m n : ℕ}
727	(J : Finset (Fin n)) (hJcard : m ≤ J.card) (x : Fin m) :
728	ramseyBlockRightEmbedding J hJcard x ∈ J :=
729	by
730	let hcard' : Fintype.card (Fin m) ≤ J.card := by simpa using hJcard
731	exact Classical.choose_spec
732	(Function.Embedding.exists_of_card_le_finset (α := Fin m) (s := J) hcard') ⟨x, rfl⟩
733
734	private theorem subdividedBiclique_zero_isIndContained {r : ℕ} {V : Type}
735	[DecidableEq V] [Fintype V] (G : SimpleGraph V) :
736	(subdividedBiclique 0 (r + 1)).IsIndContained G := by
737	classical
738	letI : IsEmpty (SubdividedBicliqueVert 0 (r + 1)) := by
739	dsimp [SubdividedBicliqueVert]
740	infer_instance
741	exact SimpleGraph.IsIndContained.of_isEmpty
742
743	/-- The last position `r + 2` in `Fin (r + 3)`. Under `atomicTuple` this position
744	maps to the right root `bⱼ`. -/
745	private def positionLast (r : ℕ) : Fin (r + 3) := ⟨r + 2, by omega⟩
746
747	private theorem atomicTuple_positionLast {r : ℕ} {V : Type} [DecidableEq V]
748	[Fintype V] {G : SimpleGraph V} {n : ℕ}
749	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n) :
750	atomicTuple copy a b (positionLast r) = rightRootVertex copy b := by
751	simp [atomicTuple, positionLast]
752
753	private theorem atomicTuple_one {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
754	{G : SimpleGraph V} {n : ℕ}
755	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n) :
756	atomicTuple copy a b ⟨1, by omega⟩ = pathVertex copy a b ⟨0, by omega⟩ := by
757	simp [atomicTuple]
758
759	private theorem atomicTuple_intermediate {r : ℕ} {V : Type} [DecidableEq V]
760	[Fintype V] {G : SimpleGraph V} {n : ℕ}
761	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
762	{k : ℕ} (hk0 : k ≠ 0) (hklast : k ≠ r + 2) (hk : k < r + 3) :
763	atomicTuple copy a b ⟨k, hk⟩ =
764	pathVertex copy a b ⟨k - 1, by
765	have hpos : 0 < k := Nat.pos_of_ne_zero hk0
766	have hlt : k < r + 2 := lt_of_le_of_ne (by omega) hklast
767	omega⟩ := by
768	have hpos : 0 < k := Nat.pos_of_ne_zero hk0
769	have hlt : k < r + 2 := lt_of_le_of_ne (by omega) hklast
770	simp [atomicTuple, hk0, hklast]
771
772	/-- Convenient packaging of `atomicTuple_intermediate`: an internal index
773	`k : Fin (r + 1)` lifts to position `k.val + 1` in the `Fin (r + 3)`
774	atomic tuple, where it agrees with `pathVertex copy a b k`. Used in
775	Block D-3/D-4/D-5 to bridge `pathVertex`-stated cross-edge witnesses to
776	`pair_atomicTuple_adj_iff` queries. -/
777	private theorem atomicTuple_succ_eq_pathVertex {r : ℕ} {V : Type}
778	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
779	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
780	(k : Fin (r + 1)) :
781	atomicTuple copy a b ⟨k.val + 1, by have := k.isLt; omega⟩ =
782	pathVertex copy a b k := by
783	have hk0 : k.val + 1 ≠ 0 := by omega
784	have hklast : k.val + 1 ≠ r + 2 := by have := k.isLt; omega
785	have hk : k.val + 1 < r + 3 := by have := k.isLt; omega
786	have heq := atomicTuple_intermediate copy a b (k := k.val + 1) hk0 hklast hk
787	rw [heq]
788	congr 1
789
790	/-- Adjacency `s → s + 1` in the tuple position graph. Unfolds to a step along
791	the subdivided-biclique path and transports through `copy`. -/
792	private theorem tuplePositionGraph_step_adj {r : ℕ} {V : Type} [DecidableEq V]
793	[Fintype V] {G : SimpleGraph V} {n : ℕ}
794	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
795	(k : ℕ) (hk : k + 1 ≤ r + 2) :
796	(tuplePositionGraph copy a b).Adj ⟨k, by omega⟩ ⟨k + 1, by omega⟩ := by
797	show G.Adj (atomicTuple copy a b ⟨k, by omega⟩) (atomicTuple copy a b ⟨k + 1, by omega⟩)
798	by_cases hk0 : k = 0
799	· subst hk0
800	have h0 : atomicTuple copy a b (⟨0, by omega⟩ : Fin (r + 3)) = leftRootVertex copy a := by
801	simp [atomicTuple]
802	rw [h0, atomicTuple_one]
803	refine copy.toHom.map_adj ?_
804	show (subdividedBiclique n (r + 1)).Adj
805	(.inl (.inl a)) (.inr ((a, b), ⟨0, by omega⟩))
806	simp [subdividedBiclique]
807	by_cases hklast : k = r + 1
808	· subst hklast
809	have h1 : atomicTuple copy a b (⟨r + 1, by omega⟩ : Fin (r + 3)) =
810	pathVertex copy a b ⟨r, by omega⟩ := by
811	have := atomicTuple_intermediate (r := r) copy a b
812	(k := r + 1) (by omega) (by omega) (by omega)
813	simpa using this
814	have h2 : atomicTuple copy a b (⟨r + 1 + 1, by omega⟩ : Fin (r + 3)) =
815	rightRootVertex copy b := by
816	have : atomicTuple copy a b (positionLast r) = rightRootVertex copy b :=
817	atomicTuple_positionLast copy a b
818	simpa [positionLast] using this
819	rw [h1, h2]
820	refine copy.toHom.map_adj ?_
821	show (subdividedBiclique n (r + 1)).Adj
822	(.inr ((a, b), ⟨r, by omega⟩)) (.inl (.inr b))
823	simp [subdividedBiclique]
824	-- 0 < k < r + 1, so k + 1 < r + 2
825	have hkpos : 0 < k := Nat.pos_of_ne_zero hk0
826	have hksucc_ne_last : k + 1 ≠ r + 2 := by omega
827	have h1 : atomicTuple copy a b (⟨k, by omega⟩ : Fin (r + 3)) =
828	pathVertex copy a b ⟨k - 1, by omega⟩ :=
829	atomicTuple_intermediate (r := r) copy a b (k := k) hk0 (by omega) (by omega)
830	have h2 : atomicTuple copy a b (⟨k + 1, by omega⟩ : Fin (r + 3)) =
831	pathVertex copy a b ⟨k, by omega⟩ := by
832	have := atomicTuple_intermediate (r := r) copy a b
833	(k := k + 1) (by omega) hksucc_ne_last (by omega)
834	simpa using this
835	rw [h1, h2]
836	refine copy.toHom.map_adj ?_
837	show (subdividedBiclique n (r + 1)).Adj
838	(.inr ((a, b), ⟨k - 1, by omega⟩)) (.inr ((a, b), ⟨k, by omega⟩))
839	simp [subdividedBiclique]
840	omega
841
842	/-- Step-by-step walk `⟨k, _⟩ → ⟨k+1, _⟩ → ⋯ → positionLast r` in the tuple
843	position graph. -/
844	private def tuplePositionTailWalk {r : ℕ} {V : Type} [DecidableEq V] [Fintype V]
845	{G : SimpleGraph V} {n : ℕ}
846	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n) :
847	(k : ℕ) → (hk : k ≤ r + 2) →
848	(tuplePositionGraph copy a b).Walk ⟨k, by omega⟩ (positionLast r)
849	\| k, hk =>
850	if hlast : k = r + 2 then
851	(SimpleGraph.Walk.nil (G := tuplePositionGraph copy a b)
852	(u := positionLast r)).copy
853	(by apply Fin.ext; simp [positionLast, hlast]) rfl
854	else
855	have hk' : k + 1 ≤ r + 2 := Nat.lt_of_le_of_ne hk hlast
856	let hadj := tuplePositionGraph_step_adj copy a b k hk'
857	.cons hadj (tuplePositionTailWalk copy a b (k + 1) hk')
858	termination_by k _ => r + 2 - k
859
860	private theorem tuplePositionTailWalk_length {r : ℕ} {V : Type} [DecidableEq V]
861	[Fintype V] {G : SimpleGraph V} {n : ℕ}
862	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n) :
863	∀ (k : ℕ) (hk : k ≤ r + 2),
864	(tuplePositionTailWalk copy a b k hk).length = r + 2 - k := by
865	intro k hk
866	induction hd : r + 2 - k generalizing k with
867	\| zero =>
868	have hk_eq : k = r + 2 := by omega
869	unfold tuplePositionTailWalk
870	simp [hk_eq]
871	\| succ d ih =>
872	have hlast : k ≠ r + 2 := by omega
873	have hk' : k + 1 ≤ r + 2 := by omega
874	have hd' : r + 2 - (k + 1) = d := by omega
875	unfold tuplePositionTailWalk
876	rw [dif_neg hlast]
877	simp [SimpleGraph.Walk.length_cons, ih (k + 1) hk' hd']
878
879	/-- Explicit witness walk in `tuplePositionGraph copy a b` from position `0` to
880	`positionLast r`. Length exactly `r + 2`. -/
881	private def tuplePositionWitnessWalk {r : ℕ} {V : Type} [DecidableEq V]
882	[Fintype V] {G : SimpleGraph V} {n : ℕ}
883	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n) :
884	(tuplePositionGraph copy a b).Walk ⟨0, by omega⟩ (positionLast r) :=
885	tuplePositionTailWalk copy a b 0 (by omega)
886
887	private theorem tuplePositionWitnessWalk_length {r : ℕ} {V : Type} [DecidableEq V]
888	[Fintype V] {G : SimpleGraph V} {n : ℕ}
889	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n) :
890	(tuplePositionWitnessWalk copy a b).length = r + 2 := by
891	have := tuplePositionTailWalk_length (r := r) copy a b 0 (by omega)
892	simpa [tuplePositionWitnessWalk] using this
893
894	/-- Distance in `tuplePositionGraph copy a b` from `0` to `positionLast r` is
895	bounded above by `r + 2`, courtesy of `tuplePositionWitnessWalk`. -/
896	private theorem tuplePositionGraph_dist_le {r : ℕ} {V : Type} [DecidableEq V]
897	[Fintype V] {G : SimpleGraph V} {n : ℕ}
898	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n) :
899	(tuplePositionGraph copy a b).dist ⟨0, by omega⟩ (positionLast r) ≤ r + 2 := by
900	have h := SimpleGraph.dist_le (tuplePositionWitnessWalk copy a b)
901	rw [tuplePositionWitnessWalk_length] at h
902	exact h
903
904	/-- Under no direct `aᵢ bⱼ` edge, the positions `0` and `positionLast r` are not
905	directly adjacent in the tuple position graph, so their distance is at least
906	`2`. -/
907	private theorem tuplePositionGraph_one_lt_dist_of_no_direct {r : ℕ} {V : Type}
908	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
909	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
910	(hNoDirect : ¬ G.Adj (leftRootVertex copy a) (rightRootVertex copy b)) :
911	1 < (tuplePositionGraph copy a b).dist ⟨0, by omega⟩ (positionLast r) := by
912	have hne : (⟨0, by omega⟩ : Fin (r + 3)) ≠ positionLast r := by
913	intro h
914	have := congrArg Fin.val h
915	simp [positionLast] at this
916	have hnadj : ¬ (tuplePositionGraph copy a b).Adj ⟨0, by omega⟩ (positionLast r) := by
917	intro hadj
918	apply hNoDirect
919	have : G.Adj (atomicTuple copy a b ⟨0, by omega⟩) (atomicTuple copy a b (positionLast r)) :=
920	hadj
921	have h0 : atomicTuple copy a b (⟨0, by omega⟩ : Fin (r + 3)) = leftRootVertex copy a := by
922	simp [atomicTuple]
923	rw [h0, atomicTuple_positionLast] at this
924	exact this
925	have hreach : (tuplePositionGraph copy a b).Reachable ⟨0, by omega⟩ (positionLast r) :=
926	(tuplePositionWitnessWalk copy a b).reachable
927	exact hreach.one_lt_dist_of_ne_of_not_adj hne hnadj
928
929	/-- Internal length `r' := dist - 1` of the canonical shortest path in the base
930	tuple position graph. Under no direct edge, this lives in `[1, r + 1]`. -/
931	private noncomputable def canonicalInternalLength {r : ℕ} {V : Type}
932	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
933	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n) : ℕ :=
934	(tuplePositionGraph copy a b).dist ⟨0, by omega⟩ (positionLast r) - 1
935
936	private theorem canonicalInternalLength_le {r : ℕ} {V : Type} [DecidableEq V]
937	[Fintype V] {G : SimpleGraph V} {n : ℕ}
938	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n) :
939	canonicalInternalLength copy a b ≤ r + 1 := by
940	have := tuplePositionGraph_dist_le (r := r) copy a b
941	unfold canonicalInternalLength
942	omega
943
944	private theorem one_le_canonicalInternalLength_of_no_direct {r : ℕ} {V : Type}
945	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
946	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
947	(hNoDirect : ¬ G.Adj (leftRootVertex copy a) (rightRootVertex copy b)) :
948	1 ≤ canonicalInternalLength copy a b := by
949	have := tuplePositionGraph_one_lt_dist_of_no_direct (r := r) copy a b hNoDirect
950	unfold canonicalInternalLength
951	omega
952
953	/-- Chord-freeness of a shortest walk.
954
955	If `p : G.Walk u v` realises the distance `G.dist u v` and `i < j` are both
956	positions at most `p.length`, then `G.Adj (p.getVert i) (p.getVert j)` forces
957	`j = i + 1`. Contrapositively: distinct non-consecutive vertices of a shortest
958	walk are non-adjacent.
959
960	Proof. `p` is a path (by `Walk.isPath_of_length_eq_dist`), so its `getVert`
961	is injective on `[0, p.length]` and `length (takeUntil (getVert k))` equals
962	`k`. Splicing a hypothetical chord `hadj` into
963	`takeUntil i ++ cons hadj (dropUntil j)` yields a walk of length
964	`i + 1 + (p.length - j)`, which by `dist_le` dominates `p.length`. The
965	conclusion follows by arithmetic. -/
966	private theorem walk_noChord_of_length_eq_dist {V : Type*} {G : SimpleGraph V}
967	{u v : V} (p : G.Walk u v) (hlen : p.length = G.dist u v)
968	{i j : ℕ} (hi : i ≤ p.length) (hj : j ≤ p.length) (hlt : i < j)
969	(hadj : G.Adj (p.getVert i) (p.getVert j)) : j = i + 1 := by
970	classical
971	have hp : p.IsPath := p.isPath_of_length_eq_dist hlen
972	have hmem_i : p.getVert i ∈ p.support := p.getVert_mem_support i
973	have hmem_j : p.getVert j ∈ p.support := p.getVert_mem_support j
974	have hti_len : (p.takeUntil (p.getVert i) hmem_i).length = i := by
975	have h1 : (p.takeUntil (p.getVert i) hmem_i).length ≤ p.length :=
976	p.length_takeUntil_le hmem_i
977	have h2 : p.getVert (p.takeUntil (p.getVert i) hmem_i).length = p.getVert i :=
978	p.getVert_length_takeUntil hmem_i
979	exact hp.getVert_injOn h1 hi h2
980	have htj_len : (p.takeUntil (p.getVert j) hmem_j).length = j := by
981	have h1 : (p.takeUntil (p.getVert j) hmem_j).length ≤ p.length :=
982	p.length_takeUntil_le hmem_j
983	have h2 : p.getVert (p.takeUntil (p.getVert j) hmem_j).length = p.getVert j :=
984	p.getVert_length_takeUntil hmem_j
985	exact hp.getVert_injOn h1 hj h2
986	have hdj_len : (p.dropUntil (p.getVert j) hmem_j).length = p.length - j := by
987	have h := congr_arg SimpleGraph.Walk.length (p.take_spec hmem_j)
988	rw [SimpleGraph.Walk.length_append, htj_len] at h
989	omega
990	let q : G.Walk u v :=
991	(p.takeUntil (p.getVert i) hmem_i).append
992	((p.dropUntil (p.getVert j) hmem_j).cons hadj)
993	have hq_len : q.length = i + 1 + (p.length - j) := by
994	show ((p.takeUntil _ hmem_i).append
995	((p.dropUntil _ hmem_j).cons hadj)).length = _
996	rw [SimpleGraph.Walk.length_append, SimpleGraph.Walk.length_cons,
997	hti_len, hdj_len]
998	omega
999	have hdist_le : G.dist u v ≤ q.length := SimpleGraph.dist_le q
1000	rw [← hlen, hq_len] at hdist_le
1001	omega
1002
1003	/-- Canonical shortest walk from position `0` to `positionLast r` in the base
1004	tuple position graph, chosen noncomputably via `Reachable.exists_path_of_dist`
1005	applied to `tuplePositionWitnessWalk`. The walk is a path and its length equals
1006	`dist`. -/
1007	private noncomputable def canonicalShortestWalk {r : ℕ} {V : Type} [DecidableEq V]
1008	[Fintype V] {G : SimpleGraph V} {n : ℕ}
1009	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n) :
1010	(tuplePositionGraph copy a b).Walk ⟨0, by omega⟩ (positionLast r) :=
1011	((tuplePositionWitnessWalk copy a b).reachable.exists_path_of_dist).choose
1012
1013	private theorem canonicalShortestWalk_isPath {r : ℕ} {V : Type} [DecidableEq V]
1014	[Fintype V] {G : SimpleGraph V} {n : ℕ}
1015	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n) :
1016	(canonicalShortestWalk copy a b).IsPath :=
1017	(((tuplePositionWitnessWalk copy a b).reachable.exists_path_of_dist).choose_spec).1
1018
1019	private theorem canonicalShortestWalk_length_eq_dist {r : ℕ} {V : Type}
1020	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
1021	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n) :
1022	(canonicalShortestWalk copy a b).length =
1023	(tuplePositionGraph copy a b).dist ⟨0, by omega⟩ (positionLast r) :=
1024	(((tuplePositionWitnessWalk copy a b).reachable.exists_path_of_dist).choose_spec).2
1025
1026	/-- Under no direct `a-b` edge, the canonical shortest walk has length exactly
1027	`canonicalInternalLength + 1 = dist`. -/
1028	private theorem canonicalShortestWalk_length_eq_succ {r : ℕ} {V : Type}
1029	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
1030	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
1031	(hNoDirect : ¬ G.Adj (leftRootVertex copy a) (rightRootVertex copy b)) :
1032	(canonicalShortestWalk copy a b).length = canonicalInternalLength copy a b + 1 := by
1033	rw [canonicalShortestWalk_length_eq_dist]
1034	have hge : 1 < (tuplePositionGraph copy a b).dist ⟨0, by omega⟩ (positionLast r) :=
1035	tuplePositionGraph_one_lt_dist_of_no_direct copy a b hNoDirect
1036	unfold canonicalInternalLength
1037	omega
1038
1039	/-- The `k`-th canonical internal index on the base pair `(a, b)`. Defined as
1040	`(k + 1)`-th vertex of `canonicalShortestWalk`. Lives in `Fin (r + 3)`, i.e.
1041	as a tuple position. -/
1042	private noncomputable def canonicalInternalIndex {r : ℕ} {V : Type} [DecidableEq V]
1043	[Fintype V] {G : SimpleGraph V} {n : ℕ}
1044	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
1045	(k : Fin (canonicalInternalLength copy a b)) : Fin (r + 3) :=
1046	(canonicalShortestWalk copy a b).getVert (k.val + 1)
1047
1048	/-- Consecutive canonical internal indices are adjacent in the base tuple
1049	position graph. -/
1050	private theorem tuplePositionGraph_adj_canonicalInternalIndex_succ {r : ℕ}
1051	{V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
1052	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
1053	(hNoDirect : ¬ G.Adj (leftRootVertex copy a) (rightRootVertex copy b))
1054	(k : Fin (canonicalInternalLength copy a b))
1055	(hsucc : k.val + 1 < canonicalInternalLength copy a b) :
1056	(tuplePositionGraph copy a b).Adj
1057	(canonicalInternalIndex copy a b k)
1058	(canonicalInternalIndex copy a b ⟨k.val + 1, hsucc⟩) := by
1059	have hlen : (canonicalShortestWalk copy a b).length =
1060	canonicalInternalLength copy a b + 1 :=
1061	canonicalShortestWalk_length_eq_succ copy a b hNoDirect
1062	have hlt : k.val + 1 < (canonicalShortestWalk copy a b).length := by
1063	rw [hlen]; omega
1064	exact (canonicalShortestWalk copy a b).adj_getVert_succ hlt
1065
1066	/-- The position `0` is adjacent to the first canonical internal index. -/
1067	private theorem tuplePositionGraph_adj_zero_canonicalInternalIndex {r : ℕ}
1068	{V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
1069	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
1070	(hNoDirect : ¬ G.Adj (leftRootVertex copy a) (rightRootVertex copy b))
1071	(h : 0 < canonicalInternalLength copy a b) :
1072	(tuplePositionGraph copy a b).Adj ⟨0, by omega⟩
1073	(canonicalInternalIndex copy a b ⟨0, h⟩) := by
1074	have hlen : (canonicalShortestWalk copy a b).length =
1075	canonicalInternalLength copy a b + 1 :=
1076	canonicalShortestWalk_length_eq_succ copy a b hNoDirect
1077	have hlt : 0 < (canonicalShortestWalk copy a b).length := by
1078	rw [hlen]; omega
1079	have hadj := (canonicalShortestWalk copy a b).adj_getVert_succ hlt
1080	have h0 : (canonicalShortestWalk copy a b).getVert 0 = ⟨0, by omega⟩ := by
1081	simp
1082	simpa [canonicalInternalIndex, h0] using hadj
1083
1084	/-- The last canonical internal index is adjacent to `positionLast r`. -/
1085	private theorem tuplePositionGraph_adj_canonicalInternalIndex_last {r : ℕ}
1086	{V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
1087	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
1088	(hNoDirect : ¬ G.Adj (leftRootVertex copy a) (rightRootVertex copy b))
1089	(k : Fin (canonicalInternalLength copy a b))
1090	(hlast : k.val + 1 = canonicalInternalLength copy a b) :
1091	(tuplePositionGraph copy a b).Adj
1092	(canonicalInternalIndex copy a b k) (positionLast r) := by
1093	have hlen : (canonicalShortestWalk copy a b).length =
1094	canonicalInternalLength copy a b + 1 :=
1095	canonicalShortestWalk_length_eq_succ copy a b hNoDirect
1096	have hlt : k.val + 1 < (canonicalShortestWalk copy a b).length := by
1097	rw [hlen]; omega
1098	have hadj := (canonicalShortestWalk copy a b).adj_getVert_succ hlt
1099	have hend :
1100	(canonicalShortestWalk copy a b).getVert (k.val + 1 + 1) = positionLast r := by
1101	have hlen_le : (canonicalShortestWalk copy a b).length ≤ k.val + 1 + 1 := by
1102	rw [hlen]; omega
1103	exact (canonicalShortestWalk copy a b).getVert_of_length_le hlen_le
1104	have hval : k.val + 1 + 1 = (canonicalShortestWalk copy a b).length := by
1105	rw [hlen]; omega
1106	rw [canonicalInternalIndex]
1107	rw [show (canonicalShortestWalk copy a b).getVert (k.val + 1 + 1) = positionLast r from hend] at hadj
1108	exact hadj
1109
1110	/-- Canonical internal indices are distinct from the start position `0`. -/
1111	private theorem canonicalInternalIndex_ne_zero {r : ℕ} {V : Type} [DecidableEq V]
1112	[Fintype V] {G : SimpleGraph V} {n : ℕ}
1113	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
1114	(hNoDirect : ¬ G.Adj (leftRootVertex copy a) (rightRootVertex copy b))
1115	(k : Fin (canonicalInternalLength copy a b)) :
1116	canonicalInternalIndex copy a b k ≠ ⟨0, by omega⟩ := by
1117	have hp := canonicalShortestWalk_isPath (r := r) copy a b
1118	have hlen : (canonicalShortestWalk copy a b).length =
1119	canonicalInternalLength copy a b + 1 :=
1120	canonicalShortestWalk_length_eq_succ copy a b hNoDirect
1121	have hle : k.val + 1 ≤ (canonicalShortestWalk copy a b).length := by
1122	rw [hlen]; omega
1123	intro hEq
1124	have : (canonicalShortestWalk copy a b).getVert (k.val + 1) = ⟨0, by omega⟩ :=
1125	hEq
1126	have h := (hp.getVert_eq_start_iff hle).1 this
1127	omega
1128
1129	/-- Canonical internal indices are distinct from the end position `positionLast r`. -/
1130	private theorem canonicalInternalIndex_ne_last {r : ℕ} {V : Type} [DecidableEq V]
1131	[Fintype V] {G : SimpleGraph V} {n : ℕ}
1132	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
1133	(hNoDirect : ¬ G.Adj (leftRootVertex copy a) (rightRootVertex copy b))
1134	(k : Fin (canonicalInternalLength copy a b)) :
1135	canonicalInternalIndex copy a b k ≠ positionLast r := by
1136	have hp := canonicalShortestWalk_isPath (r := r) copy a b
1137	have hlen : (canonicalShortestWalk copy a b).length =
1138	canonicalInternalLength copy a b + 1 :=
1139	canonicalShortestWalk_length_eq_succ copy a b hNoDirect
1140	have hle : k.val + 1 ≤ (canonicalShortestWalk copy a b).length := by
1141	rw [hlen]; omega
1142	intro hEq
1143	have hv : (canonicalShortestWalk copy a b).getVert (k.val + 1) = positionLast r :=
1144	hEq
1145	have h := (hp.getVert_eq_end_iff hle).1 hv
1146	rw [hlen] at h
1147	omega
1148
1149	/-- The `val` of a canonical internal index is strictly positive. -/
1150	private theorem canonicalInternalIndex_val_pos {r : ℕ} {V : Type} [DecidableEq V]
1151	[Fintype V] {G : SimpleGraph V} {n : ℕ}
1152	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
1153	(hNoDirect : ¬ G.Adj (leftRootVertex copy a) (rightRootVertex copy b))
1154	(k : Fin (canonicalInternalLength copy a b)) :
1155	0 < (canonicalInternalIndex copy a b k).val := by
1156	have hne := canonicalInternalIndex_ne_zero (r := r) copy a b hNoDirect k
1157	rcases Nat.eq_zero_or_pos (canonicalInternalIndex copy a b k).val with h \| h
1158	· exfalso
1159	apply hne
1160	apply Fin.ext
1161	simp [h]
1162	· exact h
1163
1164	/-- The `val` of a canonical internal index is strictly less than `r + 2`, i.e.
1165	less than `positionLast r`. -/
1166	private theorem canonicalInternalIndex_val_lt {r : ℕ} {V : Type} [DecidableEq V]
1167	[Fintype V] {G : SimpleGraph V} {n : ℕ}
1168	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
1169	(hNoDirect : ¬ G.Adj (leftRootVertex copy a) (rightRootVertex copy b))
1170	(k : Fin (canonicalInternalLength copy a b)) :
1171	(canonicalInternalIndex copy a b k).val < r + 2 := by
1172	have hne := canonicalInternalIndex_ne_last (r := r) copy a b hNoDirect k
1173	have hlt : (canonicalInternalIndex copy a b k).val < r + 3 :=
1174	(canonicalInternalIndex copy a b k).isLt
1175	rcases Nat.lt_or_ge (canonicalInternalIndex copy a b k).val (r + 2) with h \| h
1176	· exact h
1177	· exfalso
1178	apply hne
1179	apply Fin.ext
1180	simp [positionLast]
1181	omega
1182
1183	/-- Canonical internal indices are injective in `k`. -/
1184	private theorem canonicalInternalIndex_injective {r : ℕ} {V : Type} [DecidableEq V]
1185	[Fintype V] {G : SimpleGraph V} {n : ℕ}
1186	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
1187	(hNoDirect : ¬ G.Adj (leftRootVertex copy a) (rightRootVertex copy b)) :
1188	Function.Injective (canonicalInternalIndex copy a b) := by
1189	have hp := canonicalShortestWalk_isPath (r := r) copy a b
1190	have hlen : (canonicalShortestWalk copy a b).length =
1191	canonicalInternalLength copy a b + 1 :=
1192	canonicalShortestWalk_length_eq_succ copy a b hNoDirect
1193	intro k₁ k₂ hEq
1194	have hk₁ : k₁.val + 1 ≤ (canonicalShortestWalk copy a b).length := by
1195	rw [hlen]; omega
1196	have hk₂ : k₂.val + 1 ≤ (canonicalShortestWalk copy a b).length := by
1197	rw [hlen]; omega
1198	have h := hp.getVert_injOn (by simpa using hk₁) (by simpa using hk₂) hEq
1199	apply Fin.ext
1200	omega
1201
1202	/-- Generalized atomic-tuple decoding: on positions strictly between `0` and
1203	`positionLast r`, `atomicTuple` lands in the path-vertex branch. -/
1204	private theorem atomicTuple_of_strict {r : ℕ} {V : Type} [DecidableEq V]
1205	[Fintype V] {G : SimpleGraph V} {n : ℕ}
1206	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
1207	(t : Fin (r + 3)) (hpos : 0 < t.val) (hlt : t.val < r + 2) :
1208	atomicTuple copy a b t = pathVertex copy a b ⟨t.val - 1, by omega⟩ :=
1209	atomicTuple_intermediate (r := r) copy a b (k := t.val)
1210	(by omega) (by omega) t.isLt
1211
1212	/-- Decoding `atomicTuple` at a canonical internal index. The canonical
1213	internal index lives strictly between `0` and `positionLast r`, so
1214	`atomicTuple` lands in the path-vertex branch regardless of the `(a', b')`
1215	tuple coordinates plugged in. -/
1216	private theorem atomicTuple_canonicalInternalIndex_eq {r : ℕ} {V : Type}
1217	[DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
1218	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G) (a b : Fin n)
1219	(hNoDirect : ¬ G.Adj (leftRootVertex copy a) (rightRootVertex copy b))
1220	(a' b' : Fin n) (k : Fin (canonicalInternalLength copy a b)) :
1221	atomicTuple copy a' b' (canonicalInternalIndex copy a b k) =
1222	pathVertex copy a' b'
1223	⟨(canonicalInternalIndex copy a b k).val - 1, by
1224	have h1 := canonicalInternalIndex_val_pos copy a b hNoDirect k
1225	have h2 := canonicalInternalIndex_val_lt copy a b hNoDirect k
1226	omega⟩ :=
1227	atomicTuple_of_strict copy a' b' (canonicalInternalIndex copy a b k)
1228	(canonicalInternalIndex_val_pos copy a b hNoDirect k)
1229	(canonicalInternalIndex_val_lt copy a b hNoDirect k)
1230
1231	/-- Candidate vertex map for the induced-copy embedding
1232	`subdividedBiclique (m + 1) (canonicalInternalLength copy i₀ j₀) ↪ V`.
1233
1234	Sends left/right roots of the target subdivided biclique to
1235	`leftRootVertex`/`rightRootVertex` at the Ramsey-block indices `eI i`, `eJ j`,
1236	and sends the `k`-th path vertex of the `(i, j)` diagonal to the `k`-th
1237	canonical internal-index position of the shortest path on the base diagonal
1238	`(i₀, j₀)` — decoded through the atomic-tuple encoding at `(eI i, eJ j)`. -/
1239	private noncomputable def candidateInducedMap
1240	{r : ℕ} {V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
1241	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
1242	{m : ℕ} (eI eJ : Fin (m + 1) ↪ Fin n) (i₀ j₀ : Fin n) :
1243	SubdividedBicliqueVert (m + 1) (canonicalInternalLength copy i₀ j₀) → V :=
1244	fun v =>
1245	match v with
1246	\| .inl (.inl i) => leftRootVertex copy (eI i)
1247	\| .inl (.inr j) => rightRootVertex copy (eJ j)
1248	\| .inr ((i, j), k) =>
1249	atomicTuple copy (eI i) (eJ j) (canonicalInternalIndex copy i₀ j₀ k)
1250
1251	@[simp] private theorem candidateInducedMap_inl_inl
1252	{r : ℕ} {V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
1253	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
1254	{m : ℕ} (eI eJ : Fin (m + 1) ↪ Fin n) (i₀ j₀ : Fin n) (i : Fin (m + 1)) :
1255	candidateInducedMap copy eI eJ i₀ j₀ (.inl (.inl i)) =
1256	leftRootVertex copy (eI i) := rfl
1257
1258	@[simp] private theorem candidateInducedMap_inl_inr
1259	{r : ℕ} {V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
1260	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
1261	{m : ℕ} (eI eJ : Fin (m + 1) ↪ Fin n) (i₀ j₀ : Fin n) (j : Fin (m + 1)) :
1262	candidateInducedMap copy eI eJ i₀ j₀ (.inl (.inr j)) =
1263	rightRootVertex copy (eJ j) := rfl
1264
1265	@[simp] private theorem candidateInducedMap_inr
1266	{r : ℕ} {V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
1267	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
1268	{m : ℕ} (eI eJ : Fin (m + 1) ↪ Fin n) (i₀ j₀ : Fin n)
1269	(i j : Fin (m + 1))
1270	(k : Fin (canonicalInternalLength copy i₀ j₀)) :
1271	candidateInducedMap copy eI eJ i₀ j₀ (.inr ((i, j), k)) =
1272	atomicTuple copy (eI i) (eJ j) (canonicalInternalIndex copy i₀ j₀ k) := rfl
1273
1274	/-- The candidate map evaluated on a subdivision vertex decodes to a
1275	`pathVertex` via `atomicTuple_canonicalInternalIndex_eq`. Convenient for
1276	reducing case analysis of injectivity and adjacency down to `copy`-level
1277	constructor equalities. -/
1278	private theorem candidateInducedMap_inr_eq_pathVertex
1279	{r : ℕ} {V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
1280	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
1281	{m : ℕ} (eI eJ : Fin (m + 1) ↪ Fin n) (i₀ j₀ : Fin n)
1282	(hNoDirect₀ : ¬ G.Adj (leftRootVertex copy i₀) (rightRootVertex copy j₀))
1283	(i j : Fin (m + 1))
1284	(k : Fin (canonicalInternalLength copy i₀ j₀)) :
1285	candidateInducedMap copy eI eJ i₀ j₀ (.inr ((i, j), k)) =
1286	pathVertex copy (eI i) (eJ j)
1287	⟨(canonicalInternalIndex copy i₀ j₀ k).val - 1, by
1288	have h1 := canonicalInternalIndex_val_pos copy i₀ j₀ hNoDirect₀ k
1289	have h2 := canonicalInternalIndex_val_lt copy i₀ j₀ hNoDirect₀ k
1290	omega⟩ := by
1291	show atomicTuple copy (eI i) (eJ j) (canonicalInternalIndex copy i₀ j₀ k) = _
1292	exact atomicTuple_canonicalInternalIndex_eq copy i₀ j₀ hNoDirect₀ (eI i) (eJ j) k
1293
1294	/-- The candidate map is injective, driven purely by `copy.injective`, the
1295	injectivity of `eI`, `eJ`, and `canonicalInternalIndex_injective`. No
1296	adjacency hypotheses are required. -/
1297	private theorem candidateInducedMap_injective
1298	{r : ℕ} {V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V} {n : ℕ}
1299	(copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G)
1300	{m : ℕ} (eI eJ : Fin (m + 1) ↪ Fin n) (i₀ j₀ : Fin n)
1301	(hNoDirect₀ : ¬ G.Adj (leftRootVertex copy i₀) (rightRootVertex copy j₀)) :
1302	Function.Injective (candidateInducedMap copy eI eJ i₀ j₀) := by
1303	intro u v huv
1304	-- Reduce every branch to an equality inside `SubdividedBicliqueVert n (r + 1)`
1305	-- under `copy`, then peel `copy.injective`, then `eI.injective` / `eJ.injective`
1306	-- or `canonicalInternalIndex_injective` as needed.
1307	have key :
1308	∀ {u v : SubdividedBicliqueVert (m + 1) (canonicalInternalLength copy i₀ j₀)},
1309	candidateInducedMap copy eI eJ i₀ j₀ u =
1310	candidateInducedMap copy eI eJ i₀ j₀ v → u = v := by
1311	intro u v huv
1312	have hPathDecode :
1313	∀ (i j : Fin (m + 1)) (k : Fin (canonicalInternalLength copy i₀ j₀)),
1314	candidateInducedMap copy eI eJ i₀ j₀ (.inr ((i, j), k)) =
1315	copy (.inr ((eI i, eJ j),
1316	⟨(canonicalInternalIndex copy i₀ j₀ k).val - 1, by
1317	have h1 := canonicalInternalIndex_val_pos copy i₀ j₀ hNoDirect₀ k
1318	have h2 := canonicalInternalIndex_val_lt copy i₀ j₀ hNoDirect₀ k
1319	omega⟩)) := by
1320	intro i j k
1321	have := candidateInducedMap_inr_eq_pathVertex copy eI eJ i₀ j₀ hNoDirect₀ i j k
1322	simpa [pathVertex] using this
1323	rcases u with ((i \| j) \| ⟨⟨i, j⟩, k⟩) <;>
1324	rcases v with ((i' \| j') \| ⟨⟨i', j'⟩, k'⟩) <;>
1325	simp only [candidateInducedMap_inl_inl, candidateInducedMap_inl_inr] at huv
1326	· -- left root = left root
1327	have hv : (Sum.inl (Sum.inl (eI i)) : SubdividedBicliqueVert n (r + 1)) =
1328	Sum.inl (Sum.inl (eI i')) :=
1329	copy.injective (by simpa [leftRootVertex] using huv)
1330	have : eI i = eI i' := by simpa using hv
1331	exact congrArg (fun x => (Sum.inl (Sum.inl x) : _)) (eI.injective this)
1332	· -- left root = right root: impossible
1333	exact absurd
1334	(copy.injective (by simpa [leftRootVertex, rightRootVertex] using huv))
1335	(by simp)
1336	· -- left root = path vertex: impossible
1337	rw [hPathDecode] at huv
1338	have hv := copy.injective (by simpa [leftRootVertex] using huv)
1339	simp at hv
1340	· -- right root = left root: impossible
1341	exact absurd
1342	(copy.injective (by simpa [leftRootVertex, rightRootVertex] using huv))
1343	(by simp)
1344	· -- right root = right root
1345	have hv : (Sum.inl (Sum.inr (eJ j)) : SubdividedBicliqueVert n (r + 1)) =
1346	Sum.inl (Sum.inr (eJ j')) :=
1347	copy.injective (by simpa [rightRootVertex] using huv)
1348	have : eJ j = eJ j' := by simpa using hv
1349	exact congrArg (fun x => (Sum.inl (Sum.inr x) : _)) (eJ.injective this)
1350	· -- right root = path vertex: impossible
1351	rw [hPathDecode] at huv
1352	have hv := copy.injective (by simpa [rightRootVertex] using huv)
1353	simp at hv
1354	· -- path vertex = left root: impossible
1355	rw [hPathDecode] at huv
1356	have hv := copy.injective (by simpa [leftRootVertex] using huv)
1357	simp at hv
1358	· -- path vertex = right root: impossible
1359	rw [hPathDecode] at huv
1360	have hv := copy.injective (by simpa [rightRootVertex] using huv)
1361	simp at hv
1362	· -- path vertex = path vertex
1363	rw [hPathDecode, hPathDecode] at huv
1364	have hv := copy.injective huv
1365	have hv' := Sum.inr.inj hv
1366	obtain ⟨hij, hk⟩ := Prod.mk.inj hv'
1367	obtain ⟨hi, hj⟩ := Prod.mk.inj hij
1368	have hi' := eI.injective hi
1369	have hj' := eJ.injective hj
1370	subst hi'; subst hj'
1371	have hk_val : (canonicalInternalIndex copy i₀ j₀ k).val - 1 =
1372	(canonicalInternalIndex copy i₀ j₀ k').val - 1 := by
1373	have := congrArg Fin.val hk
1374	simpa using this
1375	have hv1 := canonicalInternalIndex_val_pos copy i₀ j₀ hNoDirect₀ k
1376	have hv2 := canonicalInternalIndex_val_pos copy i₀ j₀ hNoDirect₀ k'
1377	have hidx :
1378	canonicalInternalIndex copy i₀ j₀ k =
1379	canonicalInternalIndex copy i₀ j₀ k' := by
1380	apply Fin.ext
1381	omega
1382	have := canonicalInternalIndex_injective copy i₀ j₀ hNoDirect₀ hidx
1383	subst this
1384	rfl
1385	exact key huv
1386
1387	/-- Proposition packaged by the remaining Step 5 argument after the direct
1388	`aᵢ bⱼ`-edge branch has been excluded.
1389
1390	At the current scaffold stage this is intentionally the exact existential
1391	statement consumed by the final theorem: the missing work is to extract a
1392	common shortest-path profile from the Ramsey block and turn the resulting
1393	cross-edge-free configuration into this induced-subdivision witness. -/
1394	private def CrossEdgeFreeData (r : ℕ) {V : Type} [DecidableEq V] [Fintype V]
1395	(G : SimpleGraph V) (U : ℕ → ℕ) (n : ℕ)
1396	(_hsub : (subdividedBiclique n (r + 1)).IsContained G)
1397	(_I _J : Finset (Fin n)) : Prop :=
1398	∃ r' : ℕ, 1 ≤ r' ∧ r' ≤ r + 1 ∧
1399	(subdividedBiclique (U n) r').IsIndContained G
1400
1401	/-- Remaining Step 5 scaffold: assuming the Ramsey block is cross-edge-free
1402	(no direct `aᵢ bⱼ` edges and no cross-root / cross-internal edges between
1403	different diagonals), extract the common shortest-path profile and package
1404	the resulting induced subdivided biclique witness.
1405
1406	Source-proof pairing: the five `hNo*Cross` hypotheses are the five
1407	"cross-edge-free" assumptions produced by the halving arguments in the
1408	Mählmann proof — `hNoAACross` and `hNoBBCross` come from the "both root
1409	sides are independent sets" reduction, and `hNoAQCross`, `hNoBQCross`,
1410	`hNoQQCross` are the three semi-induced-biclique halvings for internal-vs-
1411	root and internal-vs-internal cross edges. The caller
1412	(`homogeneousCaseSplit`) is responsible for producing these hypotheses
1413	from the Ramsey block (either directly or by branching to the biclique
1414	alternative). -/
1415	private theorem buildCrossEdgeFreeData (r : ℕ) {V : Type}
1416	[DecidableEq V] [Fintype V] (G : SimpleGraph V) (U : ℕ → ℕ) (n : ℕ)
1417	(hsub : (subdividedBiclique n (r + 1)).IsContained G)
1418	(I J : Finset (Fin n)) (hIcard : U n ≤ I.card) (hJcard : U n ≤ J.card)
1419	(hpaths : HasHomogeneousShortestPaths r G n hsub I J)
1420	(hNoDirectEdges :
1421	∀ i, i ∈ I → ∀ j, j ∈ J →
1422	¬ G.Adj (leftRootVertex hpaths.copy i) (rightRootVertex hpaths.copy j))
1423	(hNoAACross :
1424	∀ i, i ∈ I → ∀ i', i' ∈ I → i ≠ i' →
1425	¬ G.Adj (leftRootVertex hpaths.copy i) (leftRootVertex hpaths.copy i'))
1426	(hNoBBCross :
1427	∀ j, j ∈ J → ∀ j', j' ∈ J → j ≠ j' →
1428	¬ G.Adj (rightRootVertex hpaths.copy j) (rightRootVertex hpaths.copy j'))
1429	(hNoAQCross :
1430	∀ i, i ∈ I → ∀ i', i' ∈ I → i ≠ i' → ∀ j', j' ∈ J →
1431	∀ k : Fin (r + 1),
1432	¬ G.Adj (leftRootVertex hpaths.copy i)
1433	(pathVertex hpaths.copy i' j' k))
1434	(hNoBQCross :
1435	∀ j, j ∈ J → ∀ j', j' ∈ J → j ≠ j' → ∀ i', i' ∈ I →
1436	∀ k : Fin (r + 1),
1437	¬ G.Adj (rightRootVertex hpaths.copy j)
1438	(pathVertex hpaths.copy i' j' k))
1439	(hNoQQCross :
1440	∀ i, i ∈ I → ∀ i', i' ∈ I → ∀ j, j ∈ J → ∀ j', j' ∈ J →
1441	(i, j) ≠ (i', j') → ∀ k k' : Fin (r + 1),
1442	¬ G.Adj (pathVertex hpaths.copy i j k)
1443	(pathVertex hpaths.copy i' j' k')) :
1444	CrossEdgeFreeData r G U n hsub I J := by
1445	classical
1446	cases hUn : U n with
1447	\| zero =>
1448	refine ⟨1, by simp, by omega, ?_⟩
1449	rw [hUn]
1450	simpa using subdividedBiclique_zero_isIndContained (r := 0) G
1451	\| succ m =>
1452	let eI : Fin (Nat.succ m) ↪ Fin n := ramseyBlockLeftEmbedding I (by simpa [hUn] using hIcard)
1453	let eJ : Fin (Nat.succ m) ↪ Fin n := ramseyBlockRightEmbedding J (by simpa [hUn] using hJcard)
1454	have heI : ∀ x : Fin (Nat.succ m), eI x ∈ I := by
1455	intro x
1456	simpa [eI] using
1457	ramseyBlockLeftEmbedding_mem I (by simpa [hUn] using hIcard) x
1458	have heJ : ∀ x : Fin (Nat.succ m), eJ x ∈ J := by
1459	intro x
1460	simpa [eJ] using
1461	ramseyBlockRightEmbedding_mem J (by simpa [hUn] using hJcard) x
1462	let i₀ : Fin n := eI ⟨0, Nat.succ_pos m⟩
1463	let j₀ : Fin n := eJ ⟨0, Nat.succ_pos m⟩
1464	have hi₀ : i₀ ∈ I := heI ⟨0, Nat.succ_pos m⟩
1465	have hj₀ : j₀ ∈ J := heJ ⟨0, Nat.succ_pos m⟩
1466	have hNoDirect₀ :
1467	¬ G.Adj (leftRootVertex hpaths.copy i₀) (rightRootVertex hpaths.copy j₀) :=
1468	hNoDirectEdges i₀ hi₀ j₀ hj₀
1469	have hGraphEq :
1470	∀ {i j : Fin n}, i ∈ I → j ∈ J →
1471	tuplePositionGraph hpaths.copy i j = tuplePositionGraph hpaths.copy i₀ j₀ := by
1472	intro i j hi hj
1473	symm
1474	exact diagonal_tuplePositionGraph_eq hpaths hi₀ hi hj₀ hj
1475	-- The Step 5 internal path length `r' := dist - 1`, canonical on `(i₀, j₀)`.
1476	let r' : ℕ := canonicalInternalLength hpaths.copy i₀ j₀
1477	have hr'_pos : 1 ≤ r' :=
1478	one_le_canonicalInternalLength_of_no_direct hpaths.copy i₀ j₀ hNoDirect₀
1479	have hr'_le : r' ≤ r + 1 :=
1480	canonicalInternalLength_le hpaths.copy i₀ j₀
1481	-- The canonical shortest walk on `(i₀, j₀)` together with its internal
1482	-- position sequence is now entirely available as named API at this point.
1483	-- `canonicalShortestWalk hpaths.copy i₀ j₀` — a Walk in the base tuple
1484	-- position graph, with `.IsPath`, length `r' + 1`
1485	-- (`canonicalShortestWalk_length_eq_succ ... hNoDirect₀`).
1486	-- `canonicalInternalIndex hpaths.copy i₀ j₀ : Fin r' → Fin (r + 3)` —
1487	-- the ordered sequence `k₁, …, k_{r'}`, injective
1488	-- (`canonicalInternalIndex_injective`), strictly between `0` and
1489	-- `positionLast r` (`canonicalInternalIndex_val_pos/_lt`), adjacent
1490	-- consecutively and to the endpoints
1491	-- (`tuplePositionGraph_adj_canonicalInternalIndex_succ/_zero/_last`),
1492	-- and decoded by `atomicTuple` into path vertices via
1493	-- `atomicTuple_canonicalInternalIndex_eq`.
1494	have hlenCanon : (canonicalShortestWalk hpaths.copy i₀ j₀).length = r' + 1 :=
1495	canonicalShortestWalk_length_eq_succ hpaths.copy i₀ j₀ hNoDirect₀
1496	have hCanonPath : (canonicalShortestWalk hpaths.copy i₀ j₀).IsPath :=
1497	canonicalShortestWalk_isPath hpaths.copy i₀ j₀
1498	refine ⟨r', hr'_pos, hr'_le, ?_⟩
1499	rw [hUn]
1500	-- Package `candidateInducedMap` + `candidateInducedMap_injective` into a
1501	-- `SimpleGraph.Embedding (subdividedBiclique (m + 1) r') G`. The remaining
1502	-- work is exactly the `Adj ↔ Adj` direction.
1503	refine ⟨⟨⟨candidateInducedMap hpaths.copy eI eJ i₀ j₀,
1504	candidateInducedMap_injective hpaths.copy eI eJ i₀ j₀ hNoDirect₀⟩,
1505	?_⟩⟩
1506	-- Remaining gap: the `map_rel_iff'` clause of the `SimpleGraph.Embedding`.
1507	-- goal: ∀ {u v : SubdividedBicliqueVert (m + 1) r'},
1508	-- G.Adj (candidateInducedMap hpaths.copy eI eJ i₀ j₀ u)
1509	-- (candidateInducedMap hpaths.copy eI eJ i₀ j₀ v) ↔
1510	-- (subdividedBiclique (m + 1) r').Adj u v
1511	intro u v
1512	refine ⟨?mp, ?mpr⟩
1513	· -- `mp`: G-adjacency of the images forces adjacency in `subdividedBiclique`.
1514	--
1515	-- Block B (same diagonal, closed): non-adjacency of non-consecutive
1516	-- vertices on the canonical walk, by `walk_noChord_of_length_eq_dist`
1517	-- applied to `canonicalShortestWalk hpaths.copy i₀ j₀` (length = `dist`)
1518	-- and transported to `(eI i, eJ j)` via `hGraphEq`. Cross-root direct
1519	-- edges (a-b / b-a) are ruled out by `hNoDirectEdges`.
1520	--
1521	-- Block C (off-diagonal, closed): three cross-edge types —
1522	-- `a-a`/`b-b`, `a-q`/`b-q`/`q-a`/`q-b`, and `q-q` with
1523	-- `(i, j) ≠ (i', j')`. Each is now ruled out directly by one of the
1524	-- `hNo*Cross` hypotheses. Producing those hypotheses is now Block D,
1525	-- lifted to the caller `homogeneousCaseSplit`.
1526	intro h
1527	change G.Adj (candidateInducedMap hpaths.copy eI eJ i₀ j₀ u)
1528	(candidateInducedMap hpaths.copy eI eJ i₀ j₀ v) at h
1529	-- Transport: adjacency at any block pair equals adjacency at the base
1530	-- pair `(i₀, j₀)`.
1531	have hTransport :
1532	∀ (i j : Fin (m + 1)) {s t : Fin (r + 3)},
1533	(tuplePositionGraph hpaths.copy (eI i) (eJ j)).Adj s t →
1534	(tuplePositionGraph hpaths.copy i₀ j₀).Adj s t := by
1535	intro i j s t hadj
1536	exact hGraphEq (heI i) (heJ j) ▸ hadj
1537	-- Canonical-walk no-chord: positions in `tuplePositionGraph i₀ j₀` that
1538	-- are adjacent on the canonical shortest walk are forced to be
1539	-- consecutive walk positions.
1540	have hlenDist : (canonicalShortestWalk hpaths.copy i₀ j₀).length =
1541	(tuplePositionGraph hpaths.copy i₀ j₀).dist
1542	⟨0, by omega⟩ (positionLast r) :=
1543	canonicalShortestWalk_length_eq_dist hpaths.copy i₀ j₀
1544	have hStart :
1545	(canonicalShortestWalk hpaths.copy i₀ j₀).getVert 0 =
1546	(⟨0, by omega⟩ : Fin (r + 3)) := by
1547	simp
1548	have hEnd :
1549	(canonicalShortestWalk hpaths.copy i₀ j₀).getVert (r' + 1) =
1550	positionLast r := by
1551	rw [show r' + 1 = (canonicalShortestWalk hpaths.copy i₀ j₀).length
1552	from hlenCanon.symm]
1553	simp
1554	-- `noChord pos₁ pos₂`: if positions `pos₁ < pos₂` on the canonical walk
1555	-- are `tuplePositionGraph`-adjacent, then `pos₂ = pos₁ + 1`.
1556	have noChord :
1557	∀ {p₁ p₂ : ℕ}, p₁ < p₂ → p₂ ≤ r' + 1 →
1558	(tuplePositionGraph hpaths.copy i₀ j₀).Adj
1559	((canonicalShortestWalk hpaths.copy i₀ j₀).getVert p₁)
1560	((canonicalShortestWalk hpaths.copy i₀ j₀).getVert p₂) →
1561	p₂ = p₁ + 1 := by
1562	intro p₁ p₂ hlt hle hadj
1563	have hlen' : (canonicalShortestWalk hpaths.copy i₀ j₀).length =
1564	(tuplePositionGraph hpaths.copy i₀ j₀).dist ⟨0, by omega⟩
1565	(positionLast r) := hlenDist
1566	have hp1 : p₁ ≤ (canonicalShortestWalk hpaths.copy i₀ j₀).length := by
1567	rw [hlenCanon]; omega
1568	have hp2 : p₂ ≤ (canonicalShortestWalk hpaths.copy i₀ j₀).length := by
1569	rw [hlenCanon]; exact hle
1570	exact walk_noChord_of_length_eq_dist
1571	(canonicalShortestWalk hpaths.copy i₀ j₀) hlen' hp1 hp2 hlt hadj
1572	rcases u with ((i \| j) \| ⟨⟨i, j⟩, k⟩) <;>
1573	rcases v with ((i' \| j') \| ⟨⟨i', j'⟩, k'⟩) <;>
1574	dsimp only [candidateInducedMap] at h
1575	· -- `(a_i, a_{i'})`: `a`s form an independent set on the Ramsey block,
1576	-- so `hNoAACross` rules out any adjacency between two distinct left
1577	-- roots. Loop `i = i'` contradicts `G`'s irreflexivity.
1578	exfalso
1579	rcases eq_or_ne i i' with rfl \| hii
1580	· exact h.ne rfl
1581	· exact hNoAACross (eI i) (heI i) (eI i') (heI i')
1582	(fun heq => hii (eI.injective heq)) h
1583	· -- `(a_i, b_{j'})`: direct edge ruled out by `hNoDirectEdges`.
1584	exact absurd h (hNoDirectEdges (eI i) (heI i) (eJ j') (heJ j'))
1585	· -- `(a_i, q_{i', j', k'})`.
1586	by_cases hii : i = i'
1587	· -- Block B: same i. Force `k'.val = 0` via no-chord on canonical walk.
1588	subst hii
1589	-- Convert h to a `tuplePositionGraph (eI i) (eJ j')` adjacency at
1590	-- positions `0` and `canonicalInternalIndex i₀ j₀ k'`.
1591	have h0 : leftRootVertex hpaths.copy (eI i) =
1592	atomicTuple hpaths.copy (eI i) (eJ j') (⟨0, by omega⟩ : Fin (r + 3)) := by
1593	simp [atomicTuple]
1594	rw [h0] at h
1595	have hadjPair :
1596	(tuplePositionGraph hpaths.copy (eI i) (eJ j')).Adj
1597	⟨0, by omega⟩ (canonicalInternalIndex hpaths.copy i₀ j₀ k') := h
1598	have hadjBase :
1599	(tuplePositionGraph hpaths.copy i₀ j₀).Adj
1600	⟨0, by omega⟩ (canonicalInternalIndex hpaths.copy i₀ j₀ k') :=
1601	(hGraphEq (heI i) (heJ j')) ▸ hadjPair
1602	-- Apply no-chord with p₁ := 0, p₂ := k'.val + 1.
1603	have hadj' :
1604	(tuplePositionGraph hpaths.copy i₀ j₀).Adj
1605	((canonicalShortestWalk hpaths.copy i₀ j₀).getVert 0)
1606	((canonicalShortestWalk hpaths.copy i₀ j₀).getVert
1607	(k'.val + 1)) := by
1608	rw [hStart]
1609	show (tuplePositionGraph hpaths.copy i₀ j₀).Adj
1610	⟨0, by omega⟩ (canonicalInternalIndex hpaths.copy i₀ j₀ k')
1611	exact hadjBase
1612	have hk' : k'.val + 1 = 0 + 1 :=
1613	noChord (by omega) (by have := k'.isLt; omega) hadj'
1614	have hk'_zero : k'.val = 0 := by omega
1615	refine (SimpleGraph.fromRel_adj _ _ _).mpr ⟨?_, Or.inl ?_⟩
1616	· simp
1617	· exact ⟨rfl, hk'_zero⟩
1618	· -- Block C: i ≠ i', off-diagonal a-q. Rule out via `hNoAQCross`
1619	-- after decoding the atomicTuple into `pathVertex` at the canonical
1620	-- internal index.
1621	exfalso
1622	rw [atomicTuple_canonicalInternalIndex_eq hpaths.copy i₀ j₀
1623	hNoDirect₀ (eI i') (eJ j') k'] at h
1624	exact hNoAQCross (eI i) (heI i) (eI i') (heI i')
1625	(fun heq => hii (eI.injective heq)) (eJ j') (heJ j') _ h
1626	· -- `(b_j, a_{i'})`: direct edge ruled out by `hNoDirectEdges`.
1627	have h' := h.symm
1628	exact absurd h' (hNoDirectEdges (eI i') (heI i') (eJ j) (heJ j))
1629	· -- `(b_j, b_{j'})`: symmetric to `(a, a)`. Use `hNoBBCross` and
1630	-- irreflexivity.
1631	exfalso
1632	rcases eq_or_ne j j' with rfl \| hjj
1633	· exact h.ne rfl
1634	· exact hNoBBCross (eJ j) (heJ j) (eJ j') (heJ j')
1635	(fun heq => hjj (eJ.injective heq)) h
1636	· -- `(b_j, q_{i', j', k'})`.
1637	by_cases hjj : j = j'
1638	· -- Block B: same j. Force `k'.val = r' - 1` via no-chord.
1639	subst hjj
1640	have hLast : rightRootVertex hpaths.copy (eJ j) =
1641	atomicTuple hpaths.copy (eI i') (eJ j) (positionLast r) :=
1642	(atomicTuple_positionLast hpaths.copy (eI i') (eJ j)).symm
1643	rw [hLast] at h
1644	have hadjPair :
1645	(tuplePositionGraph hpaths.copy (eI i') (eJ j)).Adj
1646	(positionLast r) (canonicalInternalIndex hpaths.copy i₀ j₀ k') := h
1647	have hadjBase :
1648	(tuplePositionGraph hpaths.copy i₀ j₀).Adj
1649	(positionLast r) (canonicalInternalIndex hpaths.copy i₀ j₀ k') :=
1650	(hGraphEq (heI i') (heJ j)) ▸ hadjPair
1651	-- Apply no-chord with p₁ := k'.val + 1, p₂ := r' + 1.
1652	have hadj' :
1653	(tuplePositionGraph hpaths.copy i₀ j₀).Adj
1654	((canonicalShortestWalk hpaths.copy i₀ j₀).getVert
1655	(k'.val + 1))
1656	((canonicalShortestWalk hpaths.copy i₀ j₀).getVert
1657	(r' + 1)) := by
1658	rw [hEnd]
1659	show (tuplePositionGraph hpaths.copy i₀ j₀).Adj
1660	(canonicalInternalIndex hpaths.copy i₀ j₀ k') (positionLast r)
1661	exact hadjBase.symm
1662	have hk' : r' + 1 = k'.val + 1 + 1 :=
1663	noChord (by have := k'.isLt; omega) (by omega) hadj'
1664	have hk'_eq : k'.val = r' - 1 := by omega
1665	refine (SimpleGraph.fromRel_adj _ _ _).mpr ⟨?_, Or.inl ?_⟩
1666	· simp
1667	· exact ⟨rfl, hk'_eq⟩
1668	· -- Block C: j ≠ j', off-diagonal b-q. Rule out via `hNoBQCross`
1669	-- after decoding the atomicTuple into `pathVertex`.
1670	exfalso
1671	rw [atomicTuple_canonicalInternalIndex_eq hpaths.copy i₀ j₀
1672	hNoDirect₀ (eI i') (eJ j') k'] at h
1673	exact hNoBQCross (eJ j) (heJ j) (eJ j') (heJ j')
1674	(fun heq => hjj (eJ.injective heq)) (eI i') (heI i') _ h
1675	· -- `(q_{i, j, k}, a_{i'})`: symmetric to `(a, q)`.
1676	by_cases hii : i = i'
1677	· subst hii
1678	have h0 : leftRootVertex hpaths.copy (eI i) =
1679	atomicTuple hpaths.copy (eI i) (eJ j) (⟨0, by omega⟩ : Fin (r + 3)) := by
1680	simp [atomicTuple]
1681	rw [h0] at h
1682	have hadjPair :
1683	(tuplePositionGraph hpaths.copy (eI i) (eJ j)).Adj
1684	(canonicalInternalIndex hpaths.copy i₀ j₀ k) ⟨0, by omega⟩ := h
1685	have hadjBase :
1686	(tuplePositionGraph hpaths.copy i₀ j₀).Adj
1687	⟨0, by omega⟩ (canonicalInternalIndex hpaths.copy i₀ j₀ k) :=
1688	((hGraphEq (heI i) (heJ j)) ▸ hadjPair).symm
1689	have hadj' :
1690	(tuplePositionGraph hpaths.copy i₀ j₀).Adj
1691	((canonicalShortestWalk hpaths.copy i₀ j₀).getVert 0)
1692	((canonicalShortestWalk hpaths.copy i₀ j₀).getVert
1693	(k.val + 1)) := by
1694	rw [hStart]
1695	show (tuplePositionGraph hpaths.copy i₀ j₀).Adj
1696	⟨0, by omega⟩ (canonicalInternalIndex hpaths.copy i₀ j₀ k)
1697	exact hadjBase
1698	have hk : k.val + 1 = 0 + 1 :=
1699	noChord (by omega) (by have := k.isLt; omega) hadj'
1700	have hk_zero : k.val = 0 := by omega
1701	refine (SimpleGraph.fromRel_adj _ _ _).mpr ⟨?_, Or.inr ?_⟩
1702	· simp
1703	· exact ⟨rfl, hk_zero⟩
1704	· -- Block C: i ≠ i', off-diagonal q-a. Symmetric to `(a, q)`; flip `h`
1705	-- and apply `hNoAQCross`.
1706	exfalso
1707	rw [atomicTuple_canonicalInternalIndex_eq hpaths.copy i₀ j₀
1708	hNoDirect₀ (eI i) (eJ j) k] at h
1709	exact hNoAQCross (eI i') (heI i') (eI i) (heI i)
1710	(fun heq => hii (eI.injective heq).symm) (eJ j) (heJ j) _ h.symm
1711	· -- `(q_{i, j, k}, b_{j'})`: symmetric to `(b, q)`.
1712	by_cases hjj : j = j'
1713	· subst hjj
1714	have hLast : rightRootVertex hpaths.copy (eJ j) =
1715	atomicTuple hpaths.copy (eI i) (eJ j) (positionLast r) :=
1716	(atomicTuple_positionLast hpaths.copy (eI i) (eJ j)).symm
1717	rw [hLast] at h
1718	have hadjPair :
1719	(tuplePositionGraph hpaths.copy (eI i) (eJ j)).Adj
1720	(canonicalInternalIndex hpaths.copy i₀ j₀ k) (positionLast r) := h
1721	have hadjBase :
1722	(tuplePositionGraph hpaths.copy i₀ j₀).Adj
1723	(positionLast r) (canonicalInternalIndex hpaths.copy i₀ j₀ k) :=
1724	((hGraphEq (heI i) (heJ j)) ▸ hadjPair).symm
1725	have hadj' :
1726	(tuplePositionGraph hpaths.copy i₀ j₀).Adj
1727	((canonicalShortestWalk hpaths.copy i₀ j₀).getVert
1728	(k.val + 1))
1729	((canonicalShortestWalk hpaths.copy i₀ j₀).getVert
1730	(r' + 1)) := by
1731	rw [hEnd]
1732	show (tuplePositionGraph hpaths.copy i₀ j₀).Adj
1733	(canonicalInternalIndex hpaths.copy i₀ j₀ k) (positionLast r)
1734	exact hadjBase.symm
1735	have hk : r' + 1 = k.val + 1 + 1 :=
1736	noChord (by have := k.isLt; omega) (by omega) hadj'
1737	have hk_eq : k.val = r' - 1 := by omega
1738	refine (SimpleGraph.fromRel_adj _ _ _).mpr ⟨?_, Or.inr ?_⟩
1739	· simp
1740	· exact ⟨rfl, hk_eq⟩
1741	· -- Block C: j ≠ j', off-diagonal q-b. Symmetric to `(b, q)`; flip `h`
1742	-- and apply `hNoBQCross`.
1743	exfalso
1744	rw [atomicTuple_canonicalInternalIndex_eq hpaths.copy i₀ j₀
1745	hNoDirect₀ (eI i) (eJ j) k] at h
1746	exact hNoBQCross (eJ j') (heJ j') (eJ j) (heJ j)
1747	(fun heq => hjj (eJ.injective heq).symm) (eI i) (heI i) _ h.symm
1748	· -- `(q_{i, j, k}, q_{i', j', k'})`.
1749	by_cases hij : (i, j) = (i', j')
1750	· -- Block B: same diagonal. Force `k.val + 1 = k'.val` (or vice versa)
1751	-- via no-chord on canonical walk.
1752	obtain ⟨hii, hjj⟩ := Prod.mk.inj hij
1753	subst hii; subst hjj
1754	have hadjPair :
1755	(tuplePositionGraph hpaths.copy (eI i) (eJ j)).Adj
1756	(canonicalInternalIndex hpaths.copy i₀ j₀ k)
1757	(canonicalInternalIndex hpaths.copy i₀ j₀ k') := h
1758	have hadjBase :
1759	(tuplePositionGraph hpaths.copy i₀ j₀).Adj
1760	(canonicalInternalIndex hpaths.copy i₀ j₀ k)
1761	(canonicalInternalIndex hpaths.copy i₀ j₀ k') :=
1762	(hGraphEq (heI i) (heJ j)) ▸ hadjPair
1763	rcases lt_trichotomy k.val k'.val with hlt \| heq \| hgt
1764	· -- k.val < k'.val: forces k'.val = k.val + 1.
1765	have hadj' :
1766	(tuplePositionGraph hpaths.copy i₀ j₀).Adj
1767	((canonicalShortestWalk hpaths.copy i₀ j₀).getVert
1768	(k.val + 1))
1769	((canonicalShortestWalk hpaths.copy i₀ j₀).getVert
1770	(k'.val + 1)) := hadjBase
1771	have hkk : k'.val + 1 = k.val + 1 + 1 :=
1772	noChord (by omega) (by have := k'.isLt; omega) hadj'
1773	have hkk' : k.val + 1 = k'.val := by omega
1774	refine (SimpleGraph.fromRel_adj _ _ _).mpr ⟨?_, Or.inl ?_⟩
1775	· intro hcontra
1776	have := Sum.inr.inj hcontra
1777	have hkeq : k = k' := (Prod.mk.inj this).2
1778	omega
1779	· exact ⟨rfl, hkk'⟩
1780	· -- k.val = k'.val: contradicts loopless of tuplePositionGraph.
1781	exfalso
1782	have hkeq : k = k' := Fin.ext heq
1783	subst hkeq
1784	exact hadjBase.ne rfl
1785	· -- k.val > k'.val: symmetric — forces k.val = k'.val + 1.
1786	have hadj' :
1787	(tuplePositionGraph hpaths.copy i₀ j₀).Adj
1788	((canonicalShortestWalk hpaths.copy i₀ j₀).getVert
1789	(k'.val + 1))
1790	((canonicalShortestWalk hpaths.copy i₀ j₀).getVert
1791	(k.val + 1)) := hadjBase.symm
1792	have hkk : k.val + 1 = k'.val + 1 + 1 :=
1793	noChord (by omega) (by have := k.isLt; omega) hadj'
1794	have hkk' : k'.val + 1 = k.val := by omega
1795	refine (SimpleGraph.fromRel_adj _ _ _).mpr ⟨?_, Or.inr ?_⟩
1796	· intro hcontra
1797	have := Sum.inr.inj hcontra
1798	have hkeq : k = k' := (Prod.mk.inj this).2
1799	omega
1800	· exact ⟨rfl, hkk'⟩
1801	· -- Block C: off-diagonal q-q. Decode both atomicTuples into
1802	-- `pathVertex`s and rule out via `hNoQQCross`.
1803	exfalso
1804	rw [atomicTuple_canonicalInternalIndex_eq hpaths.copy i₀ j₀
1805	hNoDirect₀ (eI i) (eJ j) k,
1806	atomicTuple_canonicalInternalIndex_eq hpaths.copy i₀ j₀
1807	hNoDirect₀ (eI i') (eJ j') k'] at h
1808	have hne : (eI i, eJ j) ≠ (eI i', eJ j') := by
1809	intro heq
1810	obtain ⟨hi, hj⟩ := Prod.mk.inj heq
1811	exact hij (by rw [eI.injective hi, eJ.injective hj])
1812	exact hNoQQCross (eI i) (heI i) (eI i') (heI i')
1813	(eJ j) (heJ j) (eJ j') (heJ j') hne _ _ h
1814	· -- `mpr` = Block A (no halving): adjacency in
1815	-- `subdividedBiclique (m + 1) r'` is realised by G.
1816	--
1817	-- 9-case analysis on `u`, `v`. After `simp [subdividedBiclique] at h`,
1818	-- the two trivial diagonals (`(aᵢ, aᵢ')` and `(bⱼ, bⱼ')`) close
1819	-- automatically; the cross-root case (`aᵢ ∼ bⱼ`) forces `r' = 0`,
1820	-- contradicting `hr'_pos`; the remaining five cases use one of the
1821	-- three canonical-walk adjacency lemmas transported from `(i₀, j₀)`
1822	-- to `(eI i, eJ j)` via `hGraphEq`.
1823	intro h
1824	-- Transport: adjacency in the base tuple position graph equals
1825	-- adjacency at any block pair. Uses `hGraphEq` via rewriting.
1826	have hTransport :
1827	∀ (i j : Fin (m + 1)) {s t : Fin (r + 3)},
1828	(tuplePositionGraph hpaths.copy i₀ j₀).Adj s t →
1829	(tuplePositionGraph hpaths.copy (eI i) (eJ j)).Adj s t := by
1830	intro i j s t hadj
1831	have hEq :
1832	tuplePositionGraph hpaths.copy i₀ j₀ =
1833	tuplePositionGraph hpaths.copy (eI i) (eJ j) :=
1834	(hGraphEq (heI i) (heJ j)).symm
1835	exact hEq ▸ hadj
1836	rcases u with ((i \| j) \| ⟨⟨i, j⟩, k⟩) <;>
1837	rcases v with ((i' \| j') \| ⟨⟨i', j'⟩, k'⟩) <;>
1838	simp [subdividedBiclique] at h
1839	· -- `(aᵢ, bⱼ')`: would need `r' = 0`, contradicting `hr'_pos`.
1840	exfalso; omega
1841	· -- `(aᵢ, p_{i', j', k'})`: `i = i'` and `k'.val = 0`.
1842	-- Use `tuplePositionGraph_adj_zero_canonicalInternalIndex` at
1843	-- `(i₀, j₀)`, transported to `(eI i, eJ j')`.
1844	obtain ⟨hii, hk0⟩ := h
1845	subst hii
1846	have hk_eq : k' = (⟨0, hr'_pos⟩ : Fin r') := Fin.ext hk0
1847	have hAdj0 := tuplePositionGraph_adj_zero_canonicalInternalIndex
1848	hpaths.copy i₀ j₀ hNoDirect₀ hr'_pos
1849	have hAdjPair := hTransport i j' hAdj0
1850	have h0 : atomicTuple hpaths.copy (eI i) (eJ j')
1851	(⟨0, by omega⟩ : Fin (r + 3)) =
1852	leftRootVertex hpaths.copy (eI i) := by
1853	simp [atomicTuple]
1854	show G.Adj (leftRootVertex hpaths.copy (eI i))
1855	(atomicTuple hpaths.copy (eI i) (eJ j')
1856	(canonicalInternalIndex hpaths.copy i₀ j₀ k'))
1857	rw [hk_eq, ← h0]
1858	exact hAdjPair
1859	· -- `(bⱼ, aᵢ')`: would need `r' = 0`, contradicting `hr'_pos`.
1860	exfalso; omega
1861	· -- `(bⱼ, p_{i', j', k'})`: `j = j'` and `k'.val = r' - 1`.
1862	-- Use `tuplePositionGraph_adj_canonicalInternalIndex_last` at
1863	-- `(i₀, j₀)`, transported to `(eI i', eJ j)`, then flip.
1864	obtain ⟨hjj, hkR⟩ := h
1865	subst hjj
1866	have hk_eq : k' = (⟨r' - 1, by omega⟩ : Fin r') := Fin.ext hkR
1867	have hsucc : (⟨r' - 1, by omega⟩ : Fin r').val + 1 = r' := by
1868	show (r' - 1) + 1 = r'
1869	omega
1870	have hAdjLast := tuplePositionGraph_adj_canonicalInternalIndex_last
1871	hpaths.copy i₀ j₀ hNoDirect₀ ⟨r' - 1, by omega⟩ hsucc
1872	have hAdjPair := hTransport i' j hAdjLast
1873	have hLast : atomicTuple hpaths.copy (eI i') (eJ j) (positionLast r) =
1874	rightRootVertex hpaths.copy (eJ j) :=
1875	atomicTuple_positionLast hpaths.copy (eI i') (eJ j)
1876	show G.Adj (rightRootVertex hpaths.copy (eJ j))
1877	(atomicTuple hpaths.copy (eI i') (eJ j)
1878	(canonicalInternalIndex hpaths.copy i₀ j₀ k'))
1879	rw [hk_eq, ← hLast]
1880	exact hAdjPair.symm
1881	· -- `(p_{i, j, k}, aᵢ')`: symmetric to the `(a, p)` case.
1882	obtain ⟨hii, hk0⟩ := h
1883	subst hii
1884	have hk_eq : k = (⟨0, hr'_pos⟩ : Fin r') := Fin.ext hk0
1885	have hAdj0 := tuplePositionGraph_adj_zero_canonicalInternalIndex
1886	hpaths.copy i₀ j₀ hNoDirect₀ hr'_pos
1887	have hAdjPair := hTransport i' j hAdj0
1888	have h0 : atomicTuple hpaths.copy (eI i') (eJ j)
1889	(⟨0, by omega⟩ : Fin (r + 3)) =
1890	leftRootVertex hpaths.copy (eI i') := by
1891	simp [atomicTuple]
1892	show G.Adj (atomicTuple hpaths.copy (eI i') (eJ j)
1893	(canonicalInternalIndex hpaths.copy i₀ j₀ k))
1894	(leftRootVertex hpaths.copy (eI i'))
1895	rw [hk_eq, ← h0]
1896	exact hAdjPair.symm
1897	· -- `(p_{i, j, k}, bⱼ')`: symmetric to the `(b, p)` case.
1898	obtain ⟨hjj, hkR⟩ := h
1899	subst hjj
1900	have hk_eq : k = (⟨r' - 1, by omega⟩ : Fin r') := Fin.ext hkR
1901	have hsucc : (⟨r' - 1, by omega⟩ : Fin r').val + 1 = r' := by
1902	show (r' - 1) + 1 = r'
1903	omega
1904	have hAdjLast := tuplePositionGraph_adj_canonicalInternalIndex_last
1905	hpaths.copy i₀ j₀ hNoDirect₀ ⟨r' - 1, by omega⟩ hsucc
1906	have hAdjPair := hTransport i j' hAdjLast
1907	have hLast : atomicTuple hpaths.copy (eI i) (eJ j') (positionLast r) =
1908	rightRootVertex hpaths.copy (eJ j') :=
1909	atomicTuple_positionLast hpaths.copy (eI i) (eJ j')
1910	show G.Adj (atomicTuple hpaths.copy (eI i) (eJ j')
1911	(canonicalInternalIndex hpaths.copy i₀ j₀ k))
1912	(rightRootVertex hpaths.copy (eJ j'))
1913	rw [hk_eq, ← hLast]
1914	exact hAdjPair
1915	· -- `(p_{i, j, k}, p_{i', j', k'})`: same diagonal, consecutive
1916	-- `k`. Use `tuplePositionGraph_adj_canonicalInternalIndex_succ`.
1917	obtain ⟨_, hrel⟩ := h
1918	rcases hrel with ⟨⟨hii, hjj⟩, hkk⟩ \| ⟨⟨hii, hjj⟩, hkk⟩
1919	· -- `k.val + 1 = k'.val`
1920	subst hii; subst hjj
1921	have hsucc : k.val + 1 < r' := by
1922	have := k'.isLt
1923	omega
1924	have hk'_eq : k' = (⟨k.val + 1, hsucc⟩ : Fin r') :=
1925	Fin.ext hkk.symm
1926	have hAdjSucc := tuplePositionGraph_adj_canonicalInternalIndex_succ
1927	hpaths.copy i₀ j₀ hNoDirect₀ k hsucc
1928	have hAdjPair := hTransport i j hAdjSucc
1929	show G.Adj (atomicTuple hpaths.copy (eI i) (eJ j)
1930	(canonicalInternalIndex hpaths.copy i₀ j₀ k))
1931	(atomicTuple hpaths.copy (eI i) (eJ j)
1932	(canonicalInternalIndex hpaths.copy i₀ j₀ k'))
1933	rw [hk'_eq]
1934	exact hAdjPair
1935	· -- `k'.val + 1 = k.val`; symmetric (`i' = i`, `j' = j`).
1936	subst hii; subst hjj
1937	have hsucc : k'.val + 1 < r' := by
1938	have := k.isLt
1939	omega
1940	have hk_eq : k = (⟨k'.val + 1, hsucc⟩ : Fin r') :=
1941	Fin.ext hkk.symm
1942	have hAdjSucc := tuplePositionGraph_adj_canonicalInternalIndex_succ
1943	hpaths.copy i₀ j₀ hNoDirect₀ k' hsucc
1944	have hAdjPair := hTransport i' j' hAdjSucc
1945	show G.Adj (atomicTuple hpaths.copy (eI i') (eJ j')
1946	(canonicalInternalIndex hpaths.copy i₀ j₀ k))
1947	(atomicTuple hpaths.copy (eI i') (eJ j')
1948	(canonicalInternalIndex hpaths.copy i₀ j₀ k'))
1949	rw [hk_eq]
1950	exact hAdjPair.symm
1951
1952	private theorem bipartiteHomogeneity (r : ℕ) :
1953	∃ U : ℕ → ℕ, Monotone U ∧ (∀ N : ℕ, ∃ n : ℕ, N ≤ U n) ∧
1954	∀ (n : ℕ)
1955	(c : (Fin 2 → Fin n) → (Fin 2 → Fin n) → Fin (Fintype.card (AtomicType r))),
1956	∃ I J : Finset (Fin n),
1957	U n ≤ I.card ∧ U n ≤ J.card ∧
1958	∃ f : (Fin 2 × Fin 2 → Ordering) →
1959	(Fin 2 × Fin 2 → Ordering) → Fin (Fintype.card (AtomicType r)),
1960	∀ (a : Fin 2 → Fin n) (b : Fin 2 → Fin n),
1961	(∀ i, a i ∈ I) → (∀ j, b j ∈ J) →
1962	c a b = f (Dev.MonadicDependence.BipartiteRamsey.orderType a)
1963	(Dev.MonadicDependence.BipartiteRamsey.orderType b) := by
1964	simpa [AtomicType] using Dev.MonadicDependence.BipartiteRamsey.bipartiteRamsey
1965	(Fintype.card (AtomicType r)) 2 2
1966	(atomicType_card_pos r)
1967
1968	private noncomputable def buildAtomicTypeColoring (r : ℕ) {V : Type}
1969	[DecidableEq V] [Fintype V]
1970	(G : SimpleGraph V) (n : ℕ)
1971	(hsub : (subdividedBiclique n (r + 1)).IsContained G) :
1972	Σ c : (Fin 2 → Fin n) → (Fin 2 → Fin n) → Fin (Fintype.card (AtomicType r)),
1973	HasAtomicTypeColoring r G n hsub c := by
1974	classical
1975	let copy : SimpleGraph.Copy (subdividedBiclique n (r + 1)) G := Classical.choice hsub
1976	refine ⟨fun a b => atomicTypeEquivFin r (atomicTypeOf G copy a b), ?_⟩
1977	exact { copy := copy, color_eq := fun _ _ => rfl }
1978
1979	private noncomputable def extractHomogeneousShortestPaths (r : ℕ) {V : Type}
1980	[DecidableEq V] [Fintype V] (G : SimpleGraph V) (n : ℕ)
1981	(hsub : (subdividedBiclique n (r + 1)).IsContained G)
1982	(I J : Finset (Fin n))
1983	(c : (Fin 2 → Fin n) → (Fin 2 → Fin n) → Fin (Fintype.card (AtomicType r)))
1984	(hc : HasAtomicTypeColoring r G n hsub c)
1985	(f : (Fin 2 × Fin 2 → Ordering) →
1986	(Fin 2 × Fin 2 → Ordering) → Fin (Fintype.card (AtomicType r)))
1987	(_hf : ∀ (a : Fin 2 → Fin n) (b : Fin 2 → Fin n),
1988	(∀ i, a i ∈ I) → (∀ j, b j ∈ J) →
1989	c a b = f (Dev.MonadicDependence.BipartiteRamsey.orderType a)
1990	(Dev.MonadicDependence.BipartiteRamsey.orderType b)) :
1991	HasHomogeneousShortestPaths r G n hsub I J := by
1992	have hdiag_color :
1993	∀ {i i' j j' : Fin n},
1994	i ∈ I → i' ∈ I → j ∈ J → j' ∈ J →
1995	c (diagPair i) (diagPair j) = c (diagPair i') (diagPair j') := by
1996	intro i i' j j' hi hi' hj hj'
1997	rw [_hf (diagPair i) (diagPair j) (by intro a; simp [diagPair, hi])
1998	(by intro b; simp [diagPair, hj])]
1999	rw [_hf (diagPair i') (diagPair j') (by intro a; simp [diagPair, hi'])
2000	(by intro b; simp [diagPair, hj'])]
2001	simp [orderType_diagPair]
2002	exact
2003	{ copy := hc.copy
2004	shortestPath := fun i j => shortestTuplePath hc.copy i j
2005	shortestPath_length_eq_dist := fun i j => shortestTuplePath_length_eq_dist hc.copy i j
2006	atomicType_eq_of_orderType := by
2007	intro a a' b b' ha ha' hb hb' hota hotb
2008	apply (atomicTypeEquivFin r).injective
2009	rw [← hc.color_eq a b, ← hc.color_eq a' b']
2010	rw [_hf a b ha hb, _hf a' b' ha' hb']
2011	simp [hota, hotb]
2012	diagonal_atomicType_eq := by
2013	intro i i' j j' hi hi' hj hj'
2014	apply (atomicTypeEquivFin r).injective
2015	rw [← hc.color_eq (diagPair i) (diagPair j)]
2016	rw [← hc.color_eq (diagPair i') (diagPair j')]
2017	exact hdiag_color hi hi' hj hj' }
2018
2019	private theorem homogeneousCaseSplit (r : ℕ) {V : Type} [DecidableEq V] [Fintype V]
2020	(G : SimpleGraph V) (U : ℕ → ℕ) (n : ℕ)
2021	(hsub : (subdividedBiclique n (r + 1)).IsContained G)
2022	(I J : Finset (Fin n)) (hIcard : 2 * U n ≤ I.card) (hJcard : 2 * U n ≤ J.card)
2023	(hpaths : HasHomogeneousShortestPaths r G n hsub I J) :
2024	(biclique (U n)).IsContained G ∨ CrossEdgeFreeData r G U n hsub I J := by
2025	classical
2026	have hIcard' : U n ≤ I.card := by omega
2027	have hJcard' : U n ≤ J.card := by omega
2028	by_cases hU : U n = 0
2029	· -- `biclique 0` is the empty graph, trivially contained.
2030	left
2031	rw [hU]
2032	refine biclique_isContained_of_leftLeftComplete hpaths.copy
2033	(∅ : Finset (Fin n)) (∅ : Finset (Fin n)) ?_ ?_ ?_
2034	· simp
2035	· simp
2036	· intro i hi _ _
2037	exact absurd hi (Finset.notMem_empty _)
2038	· have hUpos : 0 < U n := Nat.pos_of_ne_zero hU
2039	-- Pick reference elements for the adjacency-homogeneity transports.
2040	have hIne : I.Nonempty := Finset.card_pos.mp (by omega)
2041	have hJne : J.Nonempty := Finset.card_pos.mp (by omega)
2042	obtain ⟨iStar, hiStar⟩ := hIne
2043	obtain ⟨jStar, hjStar⟩ := hJne
2044	by_cases hEdge :
2045	∃ i, i ∈ I ∧ ∃ j, j ∈ J ∧
2046	G.Adj (leftRootVertex hpaths.copy i) (rightRootVertex hpaths.copy j)
2047	· -- Case A: direct `aᵢ–bⱼ` edge. Full `I × J` is a biclique.
2048	left
2049	rcases hEdge with ⟨i₀, hi₀, j₀, hj₀, hAdj₀⟩
2050	refine biclique_isContained_of_completeRoots hpaths.copy I J hIcard' hJcard' ?_
2051	intro i hi j hj
2052	exact (diagonal_left_right_adj_iff hpaths hi hi₀ hj hj₀).2 hAdj₀
2053	· have hNoDirect : ∀ i, i ∈ I → ∀ j, j ∈ J →
2054	¬ G.Adj (leftRootVertex hpaths.copy i) (rightRootVertex hpaths.copy j) := by
2055	intro i hi j hj hij
2056	exact hEdge ⟨i, hi, j, hj, hij⟩
2057	by_cases hAA :
2058	∃ i, i ∈ I ∧ ∃ i', i' ∈ I ∧ i ≠ i' ∧
2059	G.Adj (leftRootVertex hpaths.copy i) (leftRootVertex hpaths.copy i')
2060	· -- Block D-1: an `aᵢ ∼ aᵢ'` cross edge exists. By orderType
2061	-- homogeneity, every strictly-ordered pair `(i, i')` in `I × I` has
2062	-- the same adjacency. Halve `I` into its smallest / largest `U n`
2063	-- elements and package via `biclique_isContained_of_leftLeftComplete`.
2064	left
2065	obtain ⟨iW₀, hiW₀, iW₁, hiW₁, hneW, hAdjW⟩ := hAA
2066	-- WLOG the witnessed pair is strictly ordered.
2067	have hWit : ∃ x y, x ∈ I ∧ y ∈ I ∧ x < y ∧
2068	G.Adj (leftRootVertex hpaths.copy x) (leftRootVertex hpaths.copy y) := by
2069	rcases lt_or_gt_of_ne hneW with h \| h
2070	· exact ⟨iW₀, iW₁, hiW₀, hiW₁, h, hAdjW⟩
2071	· exact ⟨iW₁, iW₀, hiW₁, hiW₀, h, hAdjW.symm⟩
2072	obtain ⟨xW, yW, hxW, hyW, hltW, hAdjW⟩ := hWit
2073	-- Halves of `I`.
2074	refine biclique_isContained_of_leftLeftComplete hpaths.copy
2075	(firstHalfFinset I hIcard') (lastHalfFinset I hIcard')
2076	(by rw [firstHalfFinset_card]) (by rw [lastHalfFinset_card]) ?_
2077	intro i hiL i' hi'R
2078	have hiI : i ∈ I := firstHalfFinset_subset I hIcard' hiL
2079	have hi'I : i' ∈ I := lastHalfFinset_subset I hIcard' hi'R
2080	have hlt : i < i' := firstHalfFinset_lt_lastHalfFinset I hIcard hiL hi'R
2081	have hOtI := orderType_pairTuple_eq_of_lt hltW hlt
2082	have hPair := pair_atomicTuple_adj_iff hpaths
2083	(i₀ := xW) (i₁ := yW) (i₀' := i) (i₁' := i')
2084	(j₀ := jStar) (j₁ := jStar) (j₀' := jStar) (j₁' := jStar)
2085	(s := 0) (t := 0)
2086	(by intro t; fin_cases t <;> simp [pairTuple, hxW, hyW])
2087	(by intro t; fin_cases t <;> simp [pairTuple, hiI, hi'I])
2088	(by intro t; fin_cases t <;> simp [pairTuple, hjStar])
2089	(by intro t; fin_cases t <;> simp [pairTuple, hjStar])
2090	hOtI rfl
2091	rw [atomicTuple_zero, atomicTuple_zero, atomicTuple_zero, atomicTuple_zero] at hPair
2092	exact hPair.mp hAdjW
2093	· have hNoAA : ∀ i, i ∈ I → ∀ i', i' ∈ I → i ≠ i' →
2094	¬ G.Adj (leftRootVertex hpaths.copy i) (leftRootVertex hpaths.copy i') := by
2095	intro i hi i' hi' hne hij
2096	exact hAA ⟨i, hi, i', hi', hne, hij⟩
2097	by_cases hBB :
2098	∃ j, j ∈ J ∧ ∃ j', j' ∈ J ∧ j ≠ j' ∧
2099	G.Adj (rightRootVertex hpaths.copy j) (rightRootVertex hpaths.copy j')
2100	· -- Block D-2: symmetric to D-1 on `J`.
2101	left
2102	obtain ⟨jW₀, hjW₀, jW₁, hjW₁, hneW, hAdjW⟩ := hBB
2103	have hWit : ∃ x y, x ∈ J ∧ y ∈ J ∧ x < y ∧
2104	G.Adj (rightRootVertex hpaths.copy x) (rightRootVertex hpaths.copy y) := by
2105	rcases lt_or_gt_of_ne hneW with h \| h
2106	· exact ⟨jW₀, jW₁, hjW₀, hjW₁, h, hAdjW⟩
2107	· exact ⟨jW₁, jW₀, hjW₁, hjW₀, h, hAdjW.symm⟩
2108	obtain ⟨xW, yW, hxW, hyW, hltW, hAdjW⟩ := hWit
2109	refine biclique_isContained_of_rightRightComplete hpaths.copy
2110	(firstHalfFinset J hJcard') (lastHalfFinset J hJcard')
2111	(by rw [firstHalfFinset_card]) (by rw [lastHalfFinset_card]) ?_
2112	intro j hjL j' hj'R
2113	have hjJ : j ∈ J := firstHalfFinset_subset J hJcard' hjL
2114	have hj'J : j' ∈ J := lastHalfFinset_subset J hJcard' hj'R
2115	have hlt : j < j' := firstHalfFinset_lt_lastHalfFinset J hJcard hjL hj'R
2116	have hOtJ := orderType_pairTuple_eq_of_lt hltW hlt
2117	have hPair := pair_atomicTuple_adj_iff hpaths
2118	(i₀ := iStar) (i₁ := iStar) (i₀' := iStar) (i₁' := iStar)
2119	(j₀ := xW) (j₁ := yW) (j₀' := j) (j₁' := j')
2120	(s := lastFin (r + 3) (by omega)) (t := lastFin (r + 3) (by omega))
2121	(by intro t; fin_cases t <;> simp [pairTuple, hiStar])
2122	(by intro t; fin_cases t <;> simp [pairTuple, hiStar])
2123	(by intro t; fin_cases t <;> simp [pairTuple, hxW, hyW])
2124	(by intro t; fin_cases t <;> simp [pairTuple, hjJ, hj'J])
2125	rfl hOtJ
2126	rw [atomicTuple_last, atomicTuple_last, atomicTuple_last, atomicTuple_last] at hPair
2127	exact hPair.mp hAdjW
2128	· have hNoBB : ∀ j, j ∈ J → ∀ j', j' ∈ J → j ≠ j' →
2129	¬ G.Adj (rightRootVertex hpaths.copy j) (rightRootVertex hpaths.copy j') := by
2130	intro j hj j' hj' hne hij
2131	exact hBB ⟨j, hj, j', hj', hne, hij⟩
2132	by_cases hAQ :
2133	∃ i, i ∈ I ∧ ∃ i', i' ∈ I ∧ i ≠ i' ∧ ∃ j', j' ∈ J ∧
2134	∃ k : Fin (r + 1), G.Adj (leftRootVertex hpaths.copy i)
2135	(pathVertex hpaths.copy i' j' k)
2136	· -- Block D-3: an `aᵢ ∼ p_{i', j', k}` cross-edge exists with `i ≠ i'`.
2137	-- Halve `I`; orderType-homogeneity propagates the witness adjacency
2138	-- across the halves to give a biclique on `(leftRoot, pathLeft)`.
2139	left
2140	obtain ⟨iW, hiWI, i'W, hi'WI, hneW, j'W, hj'WJ, kW, hAdjW⟩ := hAQ
2141	-- Helper: position `kW.val + 1` in `Fin (r + 3)`.
2142	have hkLt : kW.val + 1 < r + 3 := by have := kW.isLt; omega
2143	rcases lt_or_gt_of_ne hneW with hltW \| hgtW
2144	· -- `iW < i'W`: leftRoot side = firstHalf, pathLeft side = lastHalf.
2145	refine biclique_isContained_of_complete (G := G)
2146	(leftRootEmbedding hpaths.copy)
2147	(pathLeftEmbedding hpaths.copy j'W kW)
2148	(firstHalfFinset I hIcard') (lastHalfFinset I hIcard')
2149	(by rw [firstHalfFinset_card]) (by rw [lastHalfFinset_card]) ?_
2150	intro i hiL i' hi'R
2151	have hiI : i ∈ I := firstHalfFinset_subset I hIcard' hiL
2152	have hi'I : i' ∈ I := lastHalfFinset_subset I hIcard' hi'R
2153	have hlt : i < i' := firstHalfFinset_lt_lastHalfFinset I hIcard hiL hi'R
2154	have hOtI := orderType_pairTuple_eq_of_lt hltW hlt
2155	have hPair := pair_atomicTuple_adj_iff hpaths
2156	(i₀ := iW) (i₁ := i'W) (i₀' := i) (i₁' := i')
2157	(j₀ := j'W) (j₁ := j'W) (j₀' := j'W) (j₁' := j'W)
2158	(s := 0) (t := ⟨kW.val + 1, hkLt⟩)
2159	(by intro t; fin_cases t <;> simp [pairTuple, hiWI, hi'WI])
2160	(by intro t; fin_cases t <;> simp [pairTuple, hiI, hi'I])
2161	(by intro t; fin_cases t <;> simp [pairTuple, hj'WJ])
2162	(by intro t; fin_cases t <;> simp [pairTuple, hj'WJ])
2163	hOtI rfl
2164	rw [atomicTuple_zero, atomicTuple_zero,
2165	atomicTuple_succ_eq_pathVertex, atomicTuple_succ_eq_pathVertex] at hPair
2166	exact hPair.mp hAdjW
2167	· -- `iW > i'W`: leftRoot side = lastHalf, pathLeft side = firstHalf.
2168	refine biclique_isContained_of_complete (G := G)
2169	(leftRootEmbedding hpaths.copy)
2170	(pathLeftEmbedding hpaths.copy j'W kW)
2171	(lastHalfFinset I hIcard') (firstHalfFinset I hIcard')
2172	(by rw [lastHalfFinset_card]) (by rw [firstHalfFinset_card]) ?_
2173	intro i hiR i' hi'L
2174	have hiI : i ∈ I := lastHalfFinset_subset I hIcard' hiR
2175	have hi'I : i' ∈ I := firstHalfFinset_subset I hIcard' hi'L
2176	have hgt : i > i' := firstHalfFinset_lt_lastHalfFinset I hIcard hi'L hiR
2177	have hOtI := orderType_pairTuple_eq_of_gt hgtW hgt
2178	have hPair := pair_atomicTuple_adj_iff hpaths
2179	(i₀ := iW) (i₁ := i'W) (i₀' := i) (i₁' := i')
2180	(j₀ := j'W) (j₁ := j'W) (j₀' := j'W) (j₁' := j'W)
2181	(s := 0) (t := ⟨kW.val + 1, hkLt⟩)
2182	(by intro t; fin_cases t <;> simp [pairTuple, hiWI, hi'WI])
2183	(by intro t; fin_cases t <;> simp [pairTuple, hiI, hi'I])
2184	(by intro t; fin_cases t <;> simp [pairTuple, hj'WJ])
2185	(by intro t; fin_cases t <;> simp [pairTuple, hj'WJ])
2186	hOtI rfl
2187	rw [atomicTuple_zero, atomicTuple_zero,
2188	atomicTuple_succ_eq_pathVertex, atomicTuple_succ_eq_pathVertex] at hPair
2189	exact hPair.mp hAdjW
2190	· have hNoAQCross : ∀ i, i ∈ I → ∀ i', i' ∈ I → i ≠ i' → ∀ j', j' ∈ J →
2191	∀ k : Fin (r + 1),
2192	¬ G.Adj (leftRootVertex hpaths.copy i)
2193	(pathVertex hpaths.copy i' j' k) := by
2194	intro i hi i' hi' hne j' hj' k hadj
2195	exact hAQ ⟨i, hi, i', hi', hne, j', hj', k, hadj⟩
2196	by_cases hBQ :
2197	∃ j, j ∈ J ∧ ∃ j', j' ∈ J ∧ j ≠ j' ∧ ∃ i', i' ∈ I ∧
2198	∃ k : Fin (r + 1), G.Adj (rightRootVertex hpaths.copy j)
2199	(pathVertex hpaths.copy i' j' k)
2200	· -- Block D-4: symmetric to D-3, halving `J`.
2201	left
2202	obtain ⟨jW, hjWJ, j'W, hj'WJ, hneW, i'W, hi'WI, kW, hAdjW⟩ := hBQ
2203	have hkLt : kW.val + 1 < r + 3 := by have := kW.isLt; omega
2204	rcases lt_or_gt_of_ne hneW with hltW \| hgtW
2205	· -- `jW < j'W`.
2206	refine biclique_isContained_of_complete (G := G)
2207	(rightRootEmbedding hpaths.copy)
2208	(pathRightEmbedding hpaths.copy i'W kW)
2209	(firstHalfFinset J hJcard') (lastHalfFinset J hJcard')
2210	(by rw [firstHalfFinset_card]) (by rw [lastHalfFinset_card]) ?_
2211	intro j hjL j' hj'R
2212	have hjJ : j ∈ J := firstHalfFinset_subset J hJcard' hjL
2213	have hj'J : j' ∈ J := lastHalfFinset_subset J hJcard' hj'R
2214	have hlt : j < j' := firstHalfFinset_lt_lastHalfFinset J hJcard hjL hj'R
2215	have hOtJ := orderType_pairTuple_eq_of_lt hltW hlt
2216	have hPair := pair_atomicTuple_adj_iff hpaths
2217	(i₀ := i'W) (i₁ := i'W) (i₀' := i'W) (i₁' := i'W)
2218	(j₀ := jW) (j₁ := j'W) (j₀' := j) (j₁' := j')
2219	(s := lastFin (r + 3) (by omega)) (t := ⟨kW.val + 1, hkLt⟩)
2220	(by intro t; fin_cases t <;> simp [pairTuple, hi'WI])
2221	(by intro t; fin_cases t <;> simp [pairTuple, hi'WI])
2222	(by intro t; fin_cases t <;> simp [pairTuple, hjWJ, hj'WJ])
2223	(by intro t; fin_cases t <;> simp [pairTuple, hjJ, hj'J])
2224	rfl hOtJ
2225	rw [atomicTuple_last, atomicTuple_last,
2226	atomicTuple_succ_eq_pathVertex, atomicTuple_succ_eq_pathVertex] at hPair
2227	exact hPair.mp hAdjW
2228	· -- `jW > j'W`.
2229	refine biclique_isContained_of_complete (G := G)
2230	(rightRootEmbedding hpaths.copy)
2231	(pathRightEmbedding hpaths.copy i'W kW)
2232	(lastHalfFinset J hJcard') (firstHalfFinset J hJcard')
2233	(by rw [lastHalfFinset_card]) (by rw [firstHalfFinset_card]) ?_
2234	intro j hjR j' hj'L
2235	have hjJ : j ∈ J := lastHalfFinset_subset J hJcard' hjR
2236	have hj'J : j' ∈ J := firstHalfFinset_subset J hJcard' hj'L
2237	have hgt : j > j' := firstHalfFinset_lt_lastHalfFinset J hJcard hj'L hjR
2238	have hOtJ := orderType_pairTuple_eq_of_gt hgtW hgt
2239	have hPair := pair_atomicTuple_adj_iff hpaths
2240	(i₀ := i'W) (i₁ := i'W) (i₀' := i'W) (i₁' := i'W)
2241	(j₀ := jW) (j₁ := j'W) (j₀' := j) (j₁' := j')
2242	(s := lastFin (r + 3) (by omega)) (t := ⟨kW.val + 1, hkLt⟩)
2243	(by intro t; fin_cases t <;> simp [pairTuple, hi'WI])
2244	(by intro t; fin_cases t <;> simp [pairTuple, hi'WI])
2245	(by intro t; fin_cases t <;> simp [pairTuple, hjWJ, hj'WJ])
2246	(by intro t; fin_cases t <;> simp [pairTuple, hjJ, hj'J])
2247	rfl hOtJ
2248	rw [atomicTuple_last, atomicTuple_last,
2249	atomicTuple_succ_eq_pathVertex, atomicTuple_succ_eq_pathVertex] at hPair
2250	exact hPair.mp hAdjW
2251	· have hNoBQCross : ∀ j, j ∈ J → ∀ j', j' ∈ J → j ≠ j' → ∀ i', i' ∈ I →
2252	∀ k : Fin (r + 1),
2253	¬ G.Adj (rightRootVertex hpaths.copy j)
2254	(pathVertex hpaths.copy i' j' k) := by
2255	intro j hj j' hj' hne i' hi' k hadj
2256	exact hBQ ⟨j, hj, j', hj', hne, i', hi', k, hadj⟩
2257	by_cases hQQ :
2258	∃ i, i ∈ I ∧ ∃ i', i' ∈ I ∧ ∃ j, j ∈ J ∧ ∃ j', j' ∈ J ∧
2259	(i, j) ≠ (i', j') ∧ ∃ k k' : Fin (r + 1),
2260	G.Adj (pathVertex hpaths.copy i j k)
2261	(pathVertex hpaths.copy i' j' k')
2262	· -- Block D-5: a `p_{i,j,k} ∼ p_{i',j',k'}` cross-edge exists with
2263	-- `(i, j) ≠ (i', j')`. Two subcases on which coordinate differs.
2264	left
2265	obtain ⟨iW, hiWI, i'W, hi'WI, jW, hjWJ, j'W, hj'WJ,
2266	hneW, kW, k'W, hAdjW⟩ := hQQ
2267	have hkLt : kW.val + 1 < r + 3 := by have := kW.isLt; omega
2268	have hk'Lt : k'W.val + 1 < r + 3 := by have := k'W.isLt; omega
2269	by_cases hiNe : iW = i'W
2270	· -- Subcase: `iW = i'W`, so `jW ≠ j'W`. Halve `J`.
2271	subst hiNe
2272	have hjNe : jW ≠ j'W := by
2273	intro h
2274	apply hneW
2275	rw [h]
2276	rcases lt_or_gt_of_ne hjNe with hltW \| hgtW
2277	· refine biclique_isContained_of_complete (G := G)
2278	(pathRightEmbedding hpaths.copy iW kW)
2279	(pathRightEmbedding hpaths.copy iW k'W)
2280	(firstHalfFinset J hJcard') (lastHalfFinset J hJcard')
2281	(by rw [firstHalfFinset_card]) (by rw [lastHalfFinset_card]) ?_
2282	intro j hjL j' hj'R
2283	have hjJ : j ∈ J := firstHalfFinset_subset J hJcard' hjL
2284	have hj'J : j' ∈ J := lastHalfFinset_subset J hJcard' hj'R
2285	have hlt : j < j' := firstHalfFinset_lt_lastHalfFinset J hJcard hjL hj'R
2286	have hOtJ := orderType_pairTuple_eq_of_lt hltW hlt
2287	have hPair := pair_atomicTuple_adj_iff hpaths
2288	(i₀ := iW) (i₁ := iW) (i₀' := iW) (i₁' := iW)
2289	(j₀ := jW) (j₁ := j'W) (j₀' := j) (j₁' := j')
2290	(s := ⟨kW.val + 1, hkLt⟩) (t := ⟨k'W.val + 1, hk'Lt⟩)
2291	(by intro t; fin_cases t <;> simp [pairTuple, hiWI])
2292	(by intro t; fin_cases t <;> simp [pairTuple, hiWI])
2293	(by intro t; fin_cases t <;> simp [pairTuple, hjWJ, hj'WJ])
2294	(by intro t; fin_cases t <;> simp [pairTuple, hjJ, hj'J])
2295	rfl hOtJ
2296	rw [atomicTuple_succ_eq_pathVertex, atomicTuple_succ_eq_pathVertex,
2297	atomicTuple_succ_eq_pathVertex, atomicTuple_succ_eq_pathVertex] at hPair
2298	exact hPair.mp hAdjW
2299	· refine biclique_isContained_of_complete (G := G)
2300	(pathRightEmbedding hpaths.copy iW kW)
2301	(pathRightEmbedding hpaths.copy iW k'W)
2302	(lastHalfFinset J hJcard') (firstHalfFinset J hJcard')
2303	(by rw [lastHalfFinset_card]) (by rw [firstHalfFinset_card]) ?_
2304	intro j hjR j' hj'L
2305	have hjJ : j ∈ J := lastHalfFinset_subset J hJcard' hjR
2306	have hj'J : j' ∈ J := firstHalfFinset_subset J hJcard' hj'L
2307	have hgt : j > j' := firstHalfFinset_lt_lastHalfFinset J hJcard hj'L hjR
2308	have hOtJ := orderType_pairTuple_eq_of_gt hgtW hgt
2309	have hPair := pair_atomicTuple_adj_iff hpaths
2310	(i₀ := iW) (i₁ := iW) (i₀' := iW) (i₁' := iW)
2311	(j₀ := jW) (j₁ := j'W) (j₀' := j) (j₁' := j')
2312	(s := ⟨kW.val + 1, hkLt⟩) (t := ⟨k'W.val + 1, hk'Lt⟩)
2313	(by intro t; fin_cases t <;> simp [pairTuple, hiWI])
2314	(by intro t; fin_cases t <;> simp [pairTuple, hiWI])
2315	(by intro t; fin_cases t <;> simp [pairTuple, hjWJ, hj'WJ])
2316	(by intro t; fin_cases t <;> simp [pairTuple, hjJ, hj'J])
2317	rfl hOtJ
2318	rw [atomicTuple_succ_eq_pathVertex, atomicTuple_succ_eq_pathVertex,
2319	atomicTuple_succ_eq_pathVertex, atomicTuple_succ_eq_pathVertex] at hPair
2320	exact hPair.mp hAdjW
2321	· -- Subcase: `iW ≠ i'W`. Halve `I`.
2322	rcases lt_or_gt_of_ne hiNe with hltW \| hgtW
2323	· refine biclique_isContained_of_complete (G := G)
2324	(pathLeftEmbedding hpaths.copy jW kW)
2325	(pathLeftEmbedding hpaths.copy j'W k'W)
2326	(firstHalfFinset I hIcard') (lastHalfFinset I hIcard')
2327	(by rw [firstHalfFinset_card]) (by rw [lastHalfFinset_card]) ?_
2328	intro i hiL i' hi'R
2329	have hiI : i ∈ I := firstHalfFinset_subset I hIcard' hiL
2330	have hi'I : i' ∈ I := lastHalfFinset_subset I hIcard' hi'R
2331	have hlt : i < i' := firstHalfFinset_lt_lastHalfFinset I hIcard hiL hi'R
2332	have hOtI := orderType_pairTuple_eq_of_lt hltW hlt
2333	have hPair := pair_atomicTuple_adj_iff hpaths
2334	(i₀ := iW) (i₁ := i'W) (i₀' := i) (i₁' := i')
2335	(j₀ := jW) (j₁ := j'W) (j₀' := jW) (j₁' := j'W)
2336	(s := ⟨kW.val + 1, hkLt⟩) (t := ⟨k'W.val + 1, hk'Lt⟩)
2337	(by intro t; fin_cases t <;> simp [pairTuple, hiWI, hi'WI])
2338	(by intro t; fin_cases t <;> simp [pairTuple, hiI, hi'I])
2339	(by intro t; fin_cases t <;> simp [pairTuple, hjWJ, hj'WJ])
2340	(by intro t; fin_cases t <;> simp [pairTuple, hjWJ, hj'WJ])
2341	hOtI rfl
2342	rw [atomicTuple_succ_eq_pathVertex, atomicTuple_succ_eq_pathVertex,
2343	atomicTuple_succ_eq_pathVertex, atomicTuple_succ_eq_pathVertex] at hPair
2344	exact hPair.mp hAdjW
2345	· refine biclique_isContained_of_complete (G := G)
2346	(pathLeftEmbedding hpaths.copy jW kW)
2347	(pathLeftEmbedding hpaths.copy j'W k'W)
2348	(lastHalfFinset I hIcard') (firstHalfFinset I hIcard')
2349	(by rw [lastHalfFinset_card]) (by rw [firstHalfFinset_card]) ?_
2350	intro i hiR i' hi'L
2351	have hiI : i ∈ I := lastHalfFinset_subset I hIcard' hiR
2352	have hi'I : i' ∈ I := firstHalfFinset_subset I hIcard' hi'L
2353	have hgt : i > i' := firstHalfFinset_lt_lastHalfFinset I hIcard hi'L hiR
2354	have hOtI := orderType_pairTuple_eq_of_gt hgtW hgt
2355	have hPair := pair_atomicTuple_adj_iff hpaths
2356	(i₀ := iW) (i₁ := i'W) (i₀' := i) (i₁' := i')
2357	(j₀ := jW) (j₁ := j'W) (j₀' := jW) (j₁' := j'W)
2358	(s := ⟨kW.val + 1, hkLt⟩) (t := ⟨k'W.val + 1, hk'Lt⟩)
2359	(by intro t; fin_cases t <;> simp [pairTuple, hiWI, hi'WI])
2360	(by intro t; fin_cases t <;> simp [pairTuple, hiI, hi'I])
2361	(by intro t; fin_cases t <;> simp [pairTuple, hjWJ, hj'WJ])
2362	(by intro t; fin_cases t <;> simp [pairTuple, hjWJ, hj'WJ])
2363	hOtI rfl
2364	rw [atomicTuple_succ_eq_pathVertex, atomicTuple_succ_eq_pathVertex,
2365	atomicTuple_succ_eq_pathVertex, atomicTuple_succ_eq_pathVertex] at hPair
2366	exact hPair.mp hAdjW
2367	· have hNoQQCross : ∀ i, i ∈ I → ∀ i', i' ∈ I → ∀ j, j ∈ J → ∀ j', j' ∈ J →
2368	(i, j) ≠ (i', j') → ∀ k k' : Fin (r + 1),
2369	¬ G.Adj (pathVertex hpaths.copy i j k)
2370	(pathVertex hpaths.copy i' j' k') := by
2371	intro i hi i' hi' j hj j' hj' hne k k' hadj
2372	exact hQQ ⟨i, hi, i', hi', j, hj, j', hj', hne, k, k', hadj⟩
2373	right
2374	exact buildCrossEdgeFreeData r G U n hsub I J hIcard' hJcard' hpaths
2375	hNoDirect hNoAA hNoBB hNoAQCross hNoBQCross hNoQQCross
2376
2377	private theorem crossEdgeFreeGivesInducedSubdivision (r : ℕ) {V : Type}
2378	[DecidableEq V] [Fintype V] (G : SimpleGraph V) (U : ℕ → ℕ) (n : ℕ)
2379	(hsub : (subdividedBiclique n (r + 1)).IsContained G)
2380	(I J : Finset (Fin n)) (_hIcard : U n ≤ I.card) (_hJcard : U n ≤ J.card)
2381	(hfree : CrossEdgeFreeData r G U n hsub I J) :
2382	∃ r' : ℕ, 1 ≤ r' ∧ r' ≤ r + 1 ∧
2383	(subdividedBiclique (U n) r').IsIndContained G := by
2384	exact hfree
2385
2386	private theorem subdividedBicliqueRamsey_succ (r : ℕ) :
2387	∃ U : ℕ → ℕ, Monotone U ∧ (∀ N : ℕ, ∃ n : ℕ, N ≤ U n) ∧
2388	∀ {V : Type} [DecidableEq V] [Fintype V]
2389	(G : SimpleGraph V) (n : ℕ),
2390	(subdividedBiclique n (r + 1)).IsContained G →
2391	(biclique (U n)).IsContained G ∨
2392	∃ r' : ℕ, 1 ≤ r' ∧ r' ≤ r + 1 ∧
2393	(subdividedBiclique (U n) r').IsIndContained G := by
2394	classical
2395	-- Outside-in `c(r)` absorption (cf. handshake `architectural decision`):
2396	-- every Block D cross-edge halving is pre-paid by dividing the inner Ramsey
2397	-- bound `U_bip` by 2. Only one halving fires per run (the first cross case
2398	-- that holds returns a biclique of half-size; otherwise `CrossEdgeFreeData`
2399	-- consumes the full block), so `c(r) = 2` suffices.
2400	obtain ⟨U, hUmono, hUunb, hRamsey⟩ := bipartiteHomogeneity r
2401	let U' : ℕ → ℕ := fun n => U n / 2
2402	refine ⟨U', ?_, ?_, ?_⟩
2403	· intro a b hab
2404	exact Nat.div_le_div_right (hUmono hab)
2405	· intro N
2406	obtain ⟨n, hn⟩ := hUunb (2 * N)
2407	refine ⟨n, ?_⟩
2408	show N ≤ U n / 2
2409	omega
2410	· intro V _ _ G n hsub
2411	obtain ⟨c, hc⟩ := buildAtomicTypeColoring r G n hsub
2412	obtain ⟨I, J, hIcard, hJcard, f, hf⟩ := hRamsey n c
2413	have hpaths : HasHomogeneousShortestPaths r G n hsub I J :=
2414	extractHomogeneousShortestPaths r G n hsub I J c hc f hf
2415	have hIcard2 : 2 * U' n ≤ I.card := by
2416	show 2 * (U n / 2) ≤ I.card
2417	have h2 : 2 * (U n / 2) ≤ U n := Nat.mul_div_le (U n) 2
2418	omega
2419	have hJcard2 : 2 * U' n ≤ J.card := by
2420	show 2 * (U n / 2) ≤ J.card
2421	have h2 : 2 * (U n / 2) ≤ U n := Nat.mul_div_le (U n) 2
2422	omega
2423	rcases homogeneousCaseSplit r G U' n hsub I J hIcard2 hJcard2 hpaths with hBiclique \| hfree
2424	· exact Or.inl hBiclique
2425	· have hIcard1 : U' n ≤ I.card := by omega
2426	have hJcard1 : U' n ≤ J.card := by omega
2427	exact Or.inr
2428	(crossEdgeFreeGivesInducedSubdivision r G U' n hsub I J hIcard1 hJcard1 hfree)
2429
2430	/-- Mählmann Lemma 13.8. -/
2431	theorem subdividedBicliqueRamsey (r : ℕ) :
2432	∃ U : ℕ → ℕ, Monotone U ∧ (∀ N : ℕ, ∃ n : ℕ, N ≤ U n) ∧
2433	∀ {V : Type} [DecidableEq V] [Fintype V]
2434	(G : SimpleGraph V) (n : ℕ),
2435	(subdividedBiclique n r).IsContained G →
2436	(biclique (U n)).IsContained G ∨
2437	∃ r' : ℕ, 1 ≤ r' ∧ r' ≤ r ∧
2438	(subdividedBiclique (U n) r').IsIndContained G := by
2439	cases r with
2440	\| zero =>
2441	exact subdividedBicliqueRamsey_zero
2442	\| succ r =>
2443	exact subdividedBicliqueRamsey_succ r
2444
2445	end Dev.MonadicDependence.SubdividedBicliqueRamsey
2446