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 random-colouring proof of
Example
For every natural , a uniformly random red-blue colouring of the edges of a suitable complete graph proves the strict diagonal Ramsey bound
Facts & Assumptions
Given: A natural and .
A uniform red-blue edge colouring is equivalently (The Erdős-Rényi finite random graph ).
Prescribing edge colours has probability (A prescribed set of present and absent edges in has product probability).
Probability of a finite union is at most the sum of its event probabilities, complements have complementary probabilities, and positive probability yields a witness (The finite union bound, Normalization, nonnegativity, monotonicity, complements, and differences in a finite probability space, An event of positive probability in a finite probability space is nonempty).
is the least order forcing a monochromatic -clique, and the published theorem states the same strict bound (The off-diagonal Ramsey number as the least with , for positive , Erdős's finite counting bound for every ).
Binomial coefficients have the factorial formula, and is the integer part of (The set of -element subsets and the binomial coefficient , for ; hence , the quotient is a natural number, and , The factorial and the falling factorial , defined by recursion in , Rational powers of a positive base, Monotonicity of and of , Integer part: for every real there is exactly one integer with ).
Verification
Construct the random colouring by colouring every edge independently and uniformly red or blue. A fixed -set is monochromatic with probability .
The union bound over all -sets gives failure probability at most .
At , . If for , then because . Hence the final bound in step 2.1 is less than for every .
By [L3] a colouring with no monochromatic -set exists on vertices, so . Since is an integer and , this implies and agrees with [L4].
Depends on
- The Erdős-Rényi finite random graph $G(n,p)$
- A prescribed set of present and absent edges in $G(n,p)$ has product probability
- Normalization, nonnegativity, monotonicity, complements, and differences in a finite probability space
- The finite union bound
- An event of positive probability in a finite probability space is nonempty
- The off-diagonal Ramsey number $R(s,t)$ as the least $N$ with $N\to(s,t)^2$, for positive $s,t$
- Erdős's finite counting bound $R(k,k)>2^{k/2}$ for every $k\ge3$
- The set $[A]^{k}$ of $k$-element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$
- $\binom{n}{k}\,k!\,(n-k)! = n!$ for $k \le n$; hence $\binom{n}{k}\,k! = n^{\underline{k}}$, the quotient $n!/(k!(n-k)!)$ is a natural number, and $\binom{n}{k} = \binom{n}{n-k}$
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
- Rational powers $a^r$ of a positive base
- Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$
- Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 135 results over 30 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
- J. Matousek and J. Vondrak, The Probabilistic Method, Section 2.1 (standard reference, not scraped)