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.
Qid maximal blowup trichotomy
Statement
For a nonempty finite graph , and , there exist such that for every finite graph with and , where , at least one of the following holds:
- Some has and .
- .
- Disjoint have , , and is -sparse to in or .
Facts & Assumptions
Given: A fixed nonempty , , , and arbitrary in the stated ranges.
For every real , its unique integer part satisfies . (Integer part: for every real there is exactly one integer with ).
From Few induced copies exclude a fixed labelled blowup: If , no -blowup of exists in .
For a nonempty pattern with distinguished vertex , parameters , , and disjoint sets with at least nonneighbors in for every vertex of , , the local trichotomy gives a few- subset of of relative size at least , at least induced embeddings, or a pair of relative sizes at least with cross density at most . (Local special copy trichotomy).
From Qid fixed size density selection: Some -subset satisfies .
From Qid bipartite density trimming: If , then some with has for every .
Proof
If , take ; the count is . For , first prove the assertion when is an integer. Enlarge to a positive integer at least , using [F1]; proving the smaller copy threshold for this enlarged exponent implies the original first alternative. Set , for , , and . These are positive integers, for , and for : iterating gives .
If , choose a vertex . Of its neighbors and nonneighbors outside , one has size at least . That set is anticomplete to in one of the two graphs, proving the third alternative. Hence assume and all three alternatives fail for .
Let . The argument exceeds , so [F1] gives . Put , ; the reciprocal-integer assumption makes every an integer, and . Since , we have , whence . Failure of the count alternative and [F2] exclude a -blowup of .
A one-label subgraph of has a -blowup by taking any vertices. Among finitely many vertex subsets of admitting the specified blowup, take one of greatest size, say of size , with blocks . Choose and let . Outside , let contain vertices with at most neighbors if is an edge of , or at most nonneighbors otherwise. If , then give the third alternative. Thus every . Also . Consequently has size at least .
Write , , and . Then , , and . Fix and of size at least . If is a nonedge, apply [F3] to with its parameters , . Its nonneighbor hypothesis holds by the definition of . If is an edge, apply it to . Complementing both graphs preserves every induced embedding and the count of ; thus the same first two contradictions below apply in this case too.
The first outcome of [F3] would give a set of size at least with the forbidden few-copy property. For the second, : indeed and . Also and . Therefore its lower count is at least . Both outcomes are excluded. The third gives , of relative sizes at least , with cross density at most in the graph chosen in the previous step.
Because , [F4] chooses of exactly vertices without increasing its cross density to . Apply [F5] to to get of size at least , with degrees into at most . This is the required one-block processing step.
Process the labels in any fixed order, starting with and replacing by at each step. Before the last step its size is at least , so the preceding construction applies every time. Degree bounds into previously chosen survive restriction of their source set. The final has size at least : use and . Take of size .
For each , the bound from into implies cross density at most . Applying [F5] to supplies at least vertices with degree into at most ; take exactly that many as . The reverse degree bound into follows from the old bound into : it is at most . For two old labels, restricting the target from to changes the bound by a factor at most , giving in both directions. Thus these disjoint sets form a -blowup on , contrary to maximality. This proves the reciprocal-integer case.
For arbitrary allowed , put and . By [F1], , so and in particular . Apply the proved case at and take final , . Then , , , and -sparsity implies -sparsity. Each of the three alternatives therefore implies its required counterpart at , including the original unenlarged .
Source notes
Proof/convention locator: Bucic, Nguyen, Scott and Seymour, Induced subgraph density I, 4.3 complete proof.
Depends on
- Local special copy trichotomy
- Few induced copies exclude a fixed labelled blowup
- Good copy extension count
- Qid bipartite density trimming
- Qid fixed size density selection
- The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents
- Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$
Used by
Dependency tree · two levels
38 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)