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.
Complete or anticomplete blockade hypotheses force an -restricted induced subgraph
Statement
Let and . Let be a graph such that for every induced subgraph of with , there exists and a complete or anticomplete -blockade in . Then has an -restricted induced subgraph with at least vertices.
Facts & Assumptions
Given: The hypotheses of the statement.
Proof
Let be maximal subject to the existence of a pure blockade whose pattern graph is -free, every block has size at least , and . By A maximal pure blockade with large total -mass must already have at least blocks, one has .
By Pure blockades with -free patterns contain complete or anticomplete subblockades of square-root length, this blockade has a complete or anticomplete subblockade indexed by a set with . For each , choose with , and put . Then .
If the chosen subblockade is anticomplete, then every vertex of has neighbors in only inside , so its degree in is at most . Hence is -sparse, and therefore -restricted.
If the chosen subblockade is complete, then in the complement every vertex of has neighbors only inside , so the same estimate shows that is -sparse. Therefore is -dense, and again -restricted.
In either case has an -restricted induced subgraph on at least vertices, namely .
Depends on
- $c$-sparse, $c$-dense and $c$-restricted vertex sets
- Complete, anticomplete, pure, weakly sparse, and $x$-sparse blockades
- A maximal pure blockade with large total $a$-mass must already have at least $\epsilon^{-2}$ blocks
- Pure blockades with $P_4$-free patterns contain complete or anticomplete subblockades of square-root length
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
14 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, Theorem 7.4 (standard reference, not scraped)