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.
Anticonnected block contraction turns an upside-down comb into a pure blockade
Statement
Let be a -free graph, let be an integer, and let . Suppose
is a -comb in with and for every . Suppose also that there is a vertex
that is complete to and anticomplete to . Then contains a pure -blockade.
Facts & Assumptions
Given: The graph , the integer , the set , the displayed comb, and the vertex satisfying the hypotheses above.
In the displayed comb, is complete to and anticomplete to for , while the blocks are pairwise disjoint and satisfy (Combs in a graph).
A set is an anticonnected component of precisely when it is the vertex set of a connected component of (Anticonnected graphs and anticonnected components).
Distinct anticonnected components of a graph are complete to one another (Distinct connected components are anticomplete, and distinct anticonnected components are complete).
A blockade is pure when every pair of distinct blocks is either complete or anticomplete (Complete, anticomplete, pure, weakly sparse, and -sparse blockades).
The graph has five vertices and four consecutive edges (Empty and complete graphs, complete bipartite graphs, and the convention that and have vertices).
Complementation exchanges edges and nonedges (Graph isomorphisms, automorphisms and graph complements).
Proof
Fix and put . Suppose first that every anticonnected component of has size less than . Partition the anticonnected components into a minimum number of unions , each of size less than , and order them by nondecreasing size. Since the parts cover , one has . Minimality gives for , and hence because . By [L1], the sets are pairwise complete. They therefore form a complete, hence pure, -blockade in . By [F1], , which proves the result in this case.
We may consequently assume that, for every , the graph has an anticonnected component with . Choose one such . Then , giving the required width bound for every chosen component.
Let , and suppose that some is mixed on . The sets of neighbours and nonneighbours of in are both nonempty. Since is connected, some edge of that complement crosses these two sets. Thus there are such that , , and .
Among the five vertices , the nonedges are exactly . Indeed, the hypotheses on determine its four incidences; [F1] determines the incidences from to and to ; and step 3.1 determines the three remaining incidences. Hence those four nonedges form the path , so these vertices induce by [F4] and [F5], contrary to the hypothesis on . Therefore no vertex of is mixed on .
Applying step 4.1 with both orders of shows that no vertex of either set is mixed on the other. If the pair had both an edge and a nonedge, then the vertices of would include one complete to and one anticomplete to ; every endpoint in of the cross-edge would then be mixed on , a contradiction. Thus is pure.
The sets are pairwise disjoint subsets of , have size at least by step 2.1, and every cross-pair is pure by step 5.1. Hence they form the required pure -blockade in .
Depends on
- Distinct connected components are anticomplete, and distinct anticonnected components are complete
- Anticonnected graphs and anticonnected components
- Combs in a graph
- Complete, anticomplete, pure, weakly sparse, and $x$-sparse blockades
- Graph isomorphisms, automorphisms and graph complements
- Empty and complete graphs, complete bipartite graphs, and the convention that $P_n$ and $C_n$ have $n$ vertices
Used by
Dependency tree · two levels
19 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 5.2.2 (standard reference, not scraped)