feat: Add statements for degree sequences in triangle-free graphs #343
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mo271
reviewed
Jul 9, 2025
Paul-Lez
reviewed
Jul 9, 2025
|
|
||
| variable (d : ℕ → ℕ) (n k r : ℕ) | ||
|
|
||
| /-- **Lemma 1 (a)** -/ |
There was a problem hiding this comment.
I think it will be helpful to also have an informal version of this lemma in the docstring (and similarly for the ones below)
Paul-Lez
reviewed
Jul 14, 2025
|
|
||
| section lemmas | ||
|
|
||
| variable (d : ℕ → ℕ) (n k r : ℕ) |
There was a problem hiding this comment.
Here the paper also assumes that d is nondecreasing, that all terms are positive and that no three terms are equal.
Comment on lines
+118
to
+114
| def degreeSequenceCompact (G : SimpleGraph α) [DecidableRel G.Adj] : Prop := | ||
| IsCompactSequence fun k => (degreeSequence G).getD k 0 |
There was a problem hiding this comment.
Here you'll run into trouble because the compactness is only meant to hold for small k (for large k, you will have d_{k+2} - d_k = 0). One way out of this would be to define an IsCompactSequenceOn predicate, which takes as extra parameter a set, and states that the sequence is compact for inputs from that set.
This commit introduces the formal statements (definitions, lemmas, and theorems) from the paper "Degree sequences in triangle-free graphs" by P. Erdős, S. Fajtlowicz, and W. Staton. The work was published in Discrete Mathematics, Volume 92, Issues 1–3, in November 1991, pages 85-88. This initial commit lays the groundwork for the formal proofs of the paper's results. The paper answers of the Grafitti conjectures. Grafitti conjectures apperead in this repository in the directory FormalConjectures/WrittenOnTheWallII.
henrykmichalewski
force-pushed
the
erdos-graffiti-conjecture
branch
from
2ba0365 to
eaa6e78
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This commit introduces the formal statements (definitions, lemmas, and theorems) from the paper "Degree sequences in triangle-free graphs" by P. Erdős, S. Fajtlowicz, and W. Staton.
The work was published in Discrete Mathematics, Volume 92, Issues 1–3, in November 1991, pages 85-88.
The paper answers one of the Graffiti conjectures. Graffiti conjectures appeared in this repository in the directory FormalConjectures/WrittenOnTheWallII.