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.
The path-plus-isolate co-Bird obstruction
Statement
Let be a finite simple co-Bird-free graph. Let be distinct vertices outside the indicated induced subgraph, with , and , and with complete to that subgraph. If induces the path and isolated vertex , then cannot be adjacent to and two consecutive vertices of the path and nonadjacent to the remaining endpoint.
Facts & Assumptions
The Bird graph and co-Bird supplies the following definition: The Bird graph is the graph on vertices with edge set So spans the bull, and is a new leaf attached to the horn vertex . The co-Bird graph is the complement of the Bird graph.
Edges between disjoint vertex sets; complete, anticomplete, pure and mixed pairs supplies the following definition: Let be a finite simple graph and let be disjoint. An edge between and is an edge with and . The pair is: - complete when every is adjacent to every ; - anticomplete when no is adjacent to any ; - pure when it is complete or anticomplete; and - mixed when it is neither complete nor anticomplete. Adjacency is the symmetric edge relation of (def-finite-simple-graph, def-graph-adjacency-incidence-neighbourhood-and-degree). If or , the pair is both complete and anticomplete, hence pure and not mixed.
-free and -free graphs under the induced-subgraph convention supplies the following definition: For finite graphs and , the graph is -free when has no induced copy of (def-induced-embedding-and-induced-copy). Equivalently, (def-induced-copy-number). For a family of finite graphs, a finite graph is -free when it is -free for every . Throughout this page, “free” always refers to induced subgraphs. It does not merely prohibit ordinary subgraph copies.
Proof
Given: The graph, vertices, sets and hypotheses in the statement.
Reverse the path if necessary to write the prohibited neighbourhood as . Completeness of and the prescribed path give exactly the edges on .
The six remaining pairs are . Under they map to .
These are exactly the six Bird edges; the other nine pairs are therefore exactly co-Bird edges. The induced copy is forbidden.
Depends on
Used by
Dependency tree · two levels
7 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–Zhou, Erdős–Hajnal beyond the five-vertex path, §6.2, Claim 6.5.1(2), Figure 9 (standard reference, not scraped)
- Diestel, Graph Theory, Chapter 1, §§1.1 and 1.4 (foundations) (standard reference, not scraped)