Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31
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.

Erdős-Rado sunflower lemma: more than k!(r−1)k distinct k-sets contain an r-petal sunflower

Statement

Let k≥0 and r≥2. Every finite family F of distinct k-element sets satisfying

∣F∣>k!(r−1)k

contains an r-petal sunflower.

Facts & Assumptions

Given: Natural numbers k≥0 and r≥2, and a finite family F of distinct k-sets with ∣F∣>k!(r−1)k.

[L1]

For k≥1, a maximal disjoint subfamily either contains r members, forming an empty-core sunflower, or its union is a transversal of size at most k(r−1) (A maximal pairwise disjoint subfamily either supplies a sunflower or gives a small transversal for the whole uniform family).

[F1]

A sunflower is a family of distinct sets with one common pairwise intersection (Sunflowers, petals, and their common core).

[L2]

If f:A→B is a function between finite sets and ∣A∣>q∣B∣, then some fibre has more than q elements (If ∣A∣>k∣B∣ then every f:A→B has a fibre with more than k elements, and for nonempty B some fibre has at least ⌈∣A∣/∣B∣⌉ elements).

[L3]

0!=1 and k!=k(k−1)! for k≥1 (The factorial n! and the falling factorial nk‾, defined by recursion in N). Natural powers satisfy m0=1 and mσ(q)=mqm (Exponentiation of natural numbers, mn, and its agreement with the integer power in R); induction on N is valid (The principle of mathematical induction).

Proof

technique · induction
1.1

For k=0, there is only one 0-element set, so no family of distinct 0-sets satisfies ∣F∣>0!(r−1)0=1. The implication is therefore true.

baseL3
1.2

Assume the assertion for (k−1)-element sets, where k≥1, and let F satisfy the displayed bound for k.

ihL3
2.1

Choose a maximal pairwise disjoint subfamily G. If ∣G∣≥r, [L1] already supplies the required sunflower. Otherwise X=⋃G meets every member of F and ∣X∣≤k(r−1).

step 1.2L1choose
3.1

In the second case, let R={(F,x):F∈F, x∈F∩X} and project R to X. Every F∈F contributes at least one incidence, so ∣R∣≥∣F∣. Set q=(k−1)!(r−1)k−1. Since ∣F∣>k!(r−1)k=k(r−1)q and ∣X∣≤k(r−1), we have ∣R∣>q∣X∣. By [L2], some x∈X belongs to more than q members of F.

step 2.1L2L3
4.1

Remove x from those members. The resulting sets are distinct (k−1)-sets, so the induction hypothesis gives r of them forming a sunflower with core C. Restoring x gives r original members whose pairwise intersections are all C∪{x}.

step 3.1ihF1
5.1

The first case in step 2.1 and the construction in step 4.1 cover all possibilities, so F contains an r-petal sunflower.

step 2.1step 4.1discharge-induction∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

33 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