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.
An iterative sparsification step for sparse -free graphs
Statement
Put . Let , and let be a -sparse -free graph with . Then at least one of the following holds:
- for some , there is a pure in ; or
- for some , there is an -sparse in .
Facts & Assumptions
Given: The constant , a parameter , and a -sparse -free graph with .
Lemma 5.4 of Nguyen, Scott, and Seymour's cited paper gives the displayed two outcomes with these constants and exponents. Its statement prints before is bound; the proof shows that the intended hypothesis is by using it to deduce .
The source proof chooses a minimal threshold , applies its preceding three-outcome sparse-blockade lemma, and rules out the deeper-sparsification branch by minimality. The remaining branches give the pure blockade in outcome 1 or the -sparse blockade in outcome 2.
Proof
Apply the corrected, well-formed reading of the cited source lemma recorded in [F1]. Its two alternatives are exactly outcomes 1 and 2, and [F2] records the minimal-threshold argument establishing them.
Therefore the present statement follows.
Depends on
- An $x$-sparse blockade iteration yields further sparsification or a pure blockade
- Rödl: for every $H$ and every $\epsilon\in(0,\tfrac12)$ there is $\delta>0$ such that every nonempty $H$-free graph has an $\epsilon$-restricted vertex set of size at least $\delta|V(G)|$
- A set is $c$-sparse in $G$ exactly when it is $c$-dense in $\overline G$, so $c$-restrictedness is complement-invariant
- $c$-sparse, $c$-dense and $c$-restricted vertex sets
- Blockades, their length, their width, and their support
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
16 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
- Tung Nguyen, Alex Scott, and Paul Seymour, Induced subgraph density. VII. The five-vertex path, Lemma 5.4 (standard reference, not scraped)