TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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\ge0$ and $r\ge2$ . Every finite family $\mathcal F$ of distinct $k$ -element sets satisfying

$|\mathcal F|>k!(r-1)^k$

contains an $r$ -petal sunflower.

Facts & Assumptions

Given: Natural numbers $k\ge0$ and $r\ge2$ , and a finite family $\mathcal F$ of distinct $k$ -sets with $|\mathcal F|>k!(r-1)^k$ .

[L1]

For $k\ge1$ , 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\to B$ is a function between finite sets and $|A|>q|B|$ , then some fibre has more than $q$ elements (If $\lvert A\rvert > k\lvert B\rvert$ then every $f : A \to B$ has a fibre with more than $k$ elements, and for nonempty $B$ some fibre has at least $\lceil \lvert A\rvert / \lvert B\rvert\rceil$ elements).

[L3]

$0!=1$ and $k!=k(k-1)!$ for $k\ge1$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $\mathbb{N}$ ). Natural powers satisfy $m^0=1$ and $m^{\sigma(q)}=m^q m$ (Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $\mathbb{R}$ ); induction on $\mathbb 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 $|\mathcal F|>0!(r-1)^0=1$ . The implication is therefore true.

baseL3

1.2

Assume the assertion for $(k-1)$ -element sets, where $k\ge1$ , and let $\mathcal F$ satisfy the displayed bound for $k$ .

ihL3

2.1

Choose a maximal pairwise disjoint subfamily $\mathcal G$ . If $|\mathcal G|\ge r$ , [L1] already supplies the required sunflower. Otherwise $X=\bigcup\mathcal G$ meets every member of $\mathcal F$ and $|X|\le k(r-1)$ .

step 1.2L1choose

3.1

In the second case, let $\mathcal R=\{(F,x):F\in\mathcal F,\ x\in F\cap X\}$ and project $\mathcal R$ to $X$ . Every $F\in\mathcal F$ contributes at least one incidence, so $|\mathcal R|\ge|\mathcal F|$ . Set $q=(k-1)!(r-1)^{k-1}$ . Since $|\mathcal F|>k!(r-1)^k=k(r-1)q$ and $|X|\le k(r-1)$ , we have $|\mathcal R|>q|X|$ . By [L2], some $x\in X$ belongs to more than $q$ members of $\mathcal 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\cup\{x\}$ .

step 3.1ihF1

5.1

The first case in step 2.1 and the construction in step 4.1 cover all possibilities, so $\mathcal 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 71 results over 20 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

Sunflower (mathematics) (Wikipedia) (standard reference, not scraped)

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