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.
Kővári–Sós–Turán: exact bipartite and ordinary-graph upper bounds for excluding
Statement
For and ,
Consequently every -vertex ordinary graph containing no satisfies
and therefore
For , the first inequality reads .
Facts & Assumptions
Given: The hypotheses and notation of the statement above.
For a bipartite graph with parts of sizes containing no oriented with its vertices on the -side, the common-neighbour count is at most ; for nonnegative integer degrees of total with , smoothing gives the lower bound (The Kővári–Sós–Turán common-neighbour count and the discrete convexity lower bound for degree sums).
In , the -vertex part of the forbidden lies on the left and the -vertex part lies on the right (The Zarankiewicz number for a forbidden in a bipartite graph).
means an eventual constant upper bound, means , and subscripts permit the constants and thresholds to depend on those parameters (Edge density and the asymptotic notations , , , and for extremal functions).
Proof
Let in the bipartite problem. If or , then and the first bound is immediate. Assume . If , the bound is again immediate. Otherwise the preceding lemma gives . Taking nonnegative th roots and rearranging yields .
For an ordinary -free graph on vertices, form a bipartite incidence graph between two copies of its vertex set, joining the left copy of to the right copy of exactly when is an edge. It is oriented--free and has edges. Apply step 1.1 with and divide by .
The displayed ordinary bound is , since its linear term has no larger order. At , step 1.1 uses the same algebra and gives the stated exact specialization.
Depends on
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 25 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Yufei Zhao, Graph Theory and Additive Combinatorics (standard reference, not scraped)