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.
A wonderful anticonnected complete-or-sparse blockade yields a restricted subgraph or a large anticomplete pair
Statement
Let be a wonderful finite family, and let be a witness for wonderfulness. Let and let be a -sparse -free graph. Suppose that
is a blockade in such that:
- ;
- all blocks have the same size ;
- every block is anticonnected;
- every distinct pair is either complete or mutually -sparse;
- the support satisfies .
Then one of the following holds:
- has a -restricted induced subgraph with at least vertices; or
- there exist disjoint sets with , , and anticomplete to .
Facts & Assumptions
Given: The wonderful family , its witness exponent , the parameter , the -sparse graph , and the blockade satisfying hypotheses 1-5.
The definition of wonderfulness applied to yields either a -restricted induced subgraph of size at least , or an index such that at most vertices in have between and neighbours in (Wonderful finite graph families).
A -sparse graph has maximum degree at most on its full vertex set (-sparse, -dense and -restricted vertex sets).
A pair is anticomplete exactly when it has no cross-edges (Edges between disjoint vertex sets; complete, anticomplete, pure and mixed pairs).
Proof
Proof technique: apply wonderfulness and then count the outside vertices that still see a chosen block.
Apply [L1] to the blockade . If it yields a -restricted induced subgraph on at least vertices, then outcome 1 of the present lemma holds immediately.
We may therefore assume that [L1] yields an index for which at most vertices outside are mixed on . Let be that exceptional set of mixed outside vertices. Every outside vertex with a neighbour in but not in has at least neighbours in . Since every vertex of has total degree at most by [L2], the number of outside vertices with at least neighbours in is at most .
Let be the set of vertices in that have no neighbours in , and let . By step 2.1, . By construction there are no edges between and , so [L3] gives that is anticomplete to . Because all blocks have size , we also have . Thus outcome 2 holds.
Steps 1.1 and 3.1 prove that one of the two stated outcomes must occur.
Depends on
- Wonderful finite graph families
- Anticonnected graphs and anticonnected components
- Blockades, their length, their width, and their support
- $c$-sparse, $c$-dense and $c$-restricted vertex sets
- Sparsity of one vertex set to another, and weak sparsity of a pair
- Edges between disjoint vertex sets; complete, anticomplete, pure and mixed pairs
Used by
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, Claim 7.1.2 (standard reference, not scraped)
- Shenwei Huang, Yiao Ju, and Yidong Zhou, Erdos-Hajnal beyond the five-vertex path, proof of Lemma 3.1 (standard reference, not scraped)