Alphabeta MathHow 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.
The pattern of the terminal -overlap quotient is -free
Statement
In a co--free graph, the pattern graph of a terminal pure iterated -overlap quotient is -free.
Facts & Assumptions
Given: A terminal pure quotient blockade in a co--free graph.
A pattern edge means its two nonempty blocks are complete; a pattern nonedge means they are anticomplete (The pattern graph of a pure blockade).
Every initial induced lies wholly in one initial overlap class, and quotienting only merges blocks (The -overlap blockade and its iterated mixed quotients).
Proof
Suppose the pattern contains an induced , and choose one vertex from each of its eleven corresponding nonempty blocks. By [F1], the selected vertices induce in the ambient graph.
If the pattern contains an induced co-, selecting one vertex from each of its six blocks and using [F1] similarly induces co- in the ambient graph, contradicting co--freeness.
The eleven selected vertices lie in distinct terminal blocks. But [F2] says the vertices of every induced must already lie in one initial overlap class and hence in one terminal block, a contradiction.
Neither forbidden induced graph occurs in the pattern.
Depends on
- The $H_5$-overlap blockade and its iterated mixed quotients
- Iterated mixed quotients of an $H_5$-overlap blockade terminate at a pure blockade
- The pattern graph of a pure blockade
- The graphs $H_0,H_1,\ldots,H_5$
- The $E$-graph and co-$E$
- 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
- Huang, Ju, and Zhou, Erdős-Hajnal beyond the five-vertex path, Lemma 6.4(2.2) (standard reference, not scraped)