How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
In a regular pair, fewer than vertices have too small a degree into a large subset, and fewer than have too large a degree
Statement
Suppose is an -regular pair of density , and satisfies . Then fewer than vertices have and fewer than vertices have
Facts & Assumptions
Given: An -regular pair of density and a set with .
Every , with and satisfies (-regular pairs and self-regular vertex sets).
Proof
Let be the set of all with and let be the set of all with . Suppose, for contradiction, that .
Summing degrees over gives , hence . Since and , this contradicts [L1]. Therefore .
Assume likewise that . Summing degrees over gives , and the same two size conditions again contradict [L1]. Therefore .
Both exceptional sets therefore have size strictly below , which is the Statement.
Depends on
Used by
- Deleting the high-degree vertices of a γ-self-regular set of density d leaves more than (1-γ) of it, and that remainder is ((d+γ)/(1-γ))-sparse Lemma
- Deleting the low-degree vertices of a γ-self-regular set of density d leaves more than (1-γ) of it, and that remainder is ((1-d+2γ)/(1-γ))-dense Lemma
- Counting lemma: regular dense pairs contain many part-respecting copies of every fixed graph Theorem
- Triangle counting lemma for three pairwise regular vertex sets Theorem
Dependency tree · two levels
2 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Y. Zhao, Graph Theory and Additive Combinatorics, Lemma 2.2.3 (standard reference, not scraped)