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.
Local special copy trichotomy
Statement
Let be a nonempty finite graph, , , , and . Let and let be disjoint vertex subsets of a finite graph , such that every has at least nonneighbors in . At least one of the following holds:
- Some has and .
- .
- Some , have , and .
Integer powers use the empty-function convention .
Facts & Assumptions
Given: as in the statement, with the stated nonneighbor bound.
From The set of functions between finite sets is finite, with : Then is finite and ,
For finite sets and a relation , . (Double counting: for a relation between finite sets).
Proof
If , the second lower bound is zero. If and , it is also zero. If , then even when is empty. Hence assume nonempty and , and that the first and second alternatives both fail.
List the edges at as , and let retain precisely the first of them, with all other adjacencies unchanged. Count special induced embeddings of taking to and other labels to ; denote the number by . For each , its nonneighbor set has . Failure of the first alternative gives at least embeddings of there. Extending by and summing disjoint fibres by [F2] yields , where .
Failure of the second alternative gives , since . Thus and there is a first with . Its predecessor satisfies , since and . Also .
Put . For each induced embedding of into , let contain the valid images of for . Let contain the valid images of for , using this intermediate graph, not . Let and count respectively nonedges and edges between . The only remaining pair is : a nonedge completes and an edge completes . Conversely every special embedding restricts to exactly one such . Therefore [F2] gives and .
There are at most possible by [F1]. Discard those with . Their total is at most , so the retained family has total at least . If every retained had , summing would give , impossible. Some retained therefore has .
For this , . Since and , this implies and . Moreover . Set , . These satisfy the third alternative and complete the proof.
Source notes
Proof/convention locator: Bucic, Nguyen, Scott and Seymour, Induced subgraph density I, 3.1 complete proof.
Depends on
- Induced copy density and homogeneous restriction parameter
- Few induced copies exclude a fixed labelled blowup
- Double counting: $\sum_{x \in X}\lvert R_x\rvert = \lvert R\rvert = \sum_{y \in Y}\lvert R^y\rvert$ for a relation between finite sets
- The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $\lvert A^{B}\rvert = \lvert A\rvert^{\lvert B\rvert}$
- The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents
Used by
Dependency tree · two levels
28 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
- Bucic, Nguyen, Scott and Seymour, Induced subgraph density I (standard reference, not scraped)