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.
Property (*) for a finite graph family
Definition
Let be a finite family of finite graphs. We say that has property if there exist constants such that the following holds for every -free graph , where is the family of graph complements (Graph isomorphisms, automorphisms and graph complements) (-free and -free graphs under the induced-subgraph convention).
Suppose there is an -comb in (Combs in a graph) with , and suppose there is a vertex such that is complete to and anticomplete to . Then at least one of the following holds:
- has a clique or stable set of size at least (Cliques, stable sets, the clique number and stability number );
- has a complete or anticomplete -blockade for some real , where the real length threshold means that the blockade's integral length is at least (Blockades, their length, their width, and their support, Complete, anticomplete, pure, weakly sparse, and -sparse blockades);
- has a pure -blockade.
This condition records exactly the three ways the special-vertex comb trigger can terminate the second sparsification round.
Depends on
- Cliques, stable sets, the clique number $\omega(G)$ and stability number $\alpha(G)$
- Combs in a graph
- Blockades, their length, their width, and their support
- Complete, anticomplete, pure, weakly sparse, and $x$-sparse blockades
- Graph isomorphisms, automorphisms and graph complements
- $H$-free and $\mathcal F$-free graphs under the induced-subgraph convention
Used by
- A four-tooth comb with a special vertex realizes the trigger configuration for property (*) Example
- The third outcome of property (*) gives a pure four-blockade Example
- Property (*) and leaf reducibility yield five comb outcomes in a restricted graph Lemma
- Property (*) and leaf reducibility imply generalized niceness Theorem
Dependency tree · two levels
18 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
- Shenwei Huang, Yiao Ju, and Yidong Zhou, Erdős-Hajnal beyond the five-vertex path, Section 1.4 (standard reference, not scraped)