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 bounds and
Statement
For every finite simple graph ,
Both inequalities include the null graph, where all displayed quantities are .
Facts & Assumptions
Given: A finite simple graph and a proper -colouring .
Adjacent vertices receive different colours, and the fibres are the colour classes (Proper vertex colourings and chromatic number).
A clique has all pairs adjacent, an independent set has no adjacent pair, and and are the corresponding maximum cardinalities (Cliques, independent sets, clique number and independence number).
The cardinality of a finite disjoint union is the sum of the cardinalities of its blocks (The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition, clause 2).
Proof
If is a clique, then [L1] makes injective into the -element colour set, so ; maximizing over cliques gives .
Each colour class is independent, since two vertices in it have the same colour and therefore cannot be adjacent by [L1]; hence by [L2].
The colour classes are pairwise disjoint and have union , so [L3] and step 1.2 give .
Steps 1.1 and 2.1 prove the two claimed bounds, including the empty family of colour classes when .
Depends on
- Proper vertex colourings and chromatic number
- Cliques, independent sets, clique number and independence number
- The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$, and a sum over a finite index set splits along a partition
Used by
- A c-sparse set X satisfies α(G[X])≥|X|/(c|X|+1), and a c-dense set satisfies ω(G[X])≥|X|/(c|X|+1) Corollary
- An α-narrow graph has a clique or stable set of size at least |V(G)|^1/(2α) Corollary
- The polynomial Rödl property implies the Erdős–Hajnal property Corollary
- A large epsilon-restricted induced subgraph gives a polynomial clique or stable set Example
- Large induced subgraphs without a polynomial clique or stable set force complete or anticomplete blockades Lemma
- Every H-free graph has a homogeneous set of size at least 2^c√log₂ n Theorem
- Every H-free graph has a homogeneous set of size at least 2^c√log₂ n log₂ log₂ n Theorem
- Every perfect graph satisfies |V(G)|<=kappa(G) Theorem
- Leaf-reducible wonderful generalized nice finite families have the Erdős-Hajnal property Theorem
Dependency tree · two levels
24 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
- Bondy and Murty, Graph Theory, Stable Sets and Cliques (standard reference, not scraped)