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.
A sparse graph has a prescribed-size induced subgraph of bounded maximum degree
Statement
Let be a finite graph with at most
edges, where . If is an integer with , then there exists with such that the induced subgraph has maximum degree at most .
Facts & Assumptions
Given: A finite graph , a real , and an integer with , such that has at most edges.
Proof
If , then any single vertex set works, because a one-vertex graph has maximum degree .
If , then has no edges, so any -vertex set has maximum degree . Hence we may assume from now on that and . Average the edge count over all -vertex subsets . Some such satisfies , because the expected edge count in a random -subset is exactly the global edge count multiplied by the probability that both endpoints of a given edge are chosen.
In this chosen set , fewer than vertices have degree greater than . Otherwise at least vertices would contribute more than each to the degree sum, giving , contrary to step 1.2.
Delete all vertices of whose degree in exceeds . By step 2.1 at least vertices remain; choose any of them and call the resulting set . Every vertex of has degree at most its degree in , so .
This has the required size and degree bound.
Used by
Dependency tree · 0 levels
Nothing. This result depends on no other item in the library.
Sources
- Maria Chudnovsky, Alex Scott, Paul Seymour, and Sophie Spirkl, Erdős-Hajnal for graphs with no 5-hole, Theorem 4.2 (standard reference, not scraped)