Alphabeta Math
LemmaStatement: 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.

A maximal pairwise disjoint subfamily either supplies a sunflower or gives a small transversal for the whole uniform family

Statement

Let k≥1k\ge1, let F\mathcal F be a finite family of distinct kk-element sets, and let r≥2r\ge2. If G⊆F\mathcal G\subseteq\mathcal F is maximal among pairwise disjoint subfamilies, then either ∣G∣≥r|\mathcal G|\ge r, in which case F\mathcal F contains an rr-petal sunflower with empty core, or

X:=⋃G∈GGX:=\bigcup_{G\in\mathcal G}G

meets every member of F\mathcal F and has cardinality at most k(r−1)k(r-1).

Facts & Assumptions

Given: A natural k≥1k\ge1, a finite family F\mathcal F of distinct kk-sets, a natural r≥2r\ge2, and a maximal pairwise disjoint subfamily G\mathcal G.

[F1]

Pairwise disjoint distinct sets form a sunflower with empty core (Sunflowers, petals, and their common core).

[F2]

Subsets of finite sets are finite, and a finite disjoint union has cardinality equal to the sum of the cardinalities of its members (The cardinality ∣A∣\lvert A\rvert of a finite set, A subset of a finite set is finite, with ∣B∣≤∣A∣\lvert B\rvert \le \lvert A\rvert, and equality holds if and only if B=AB = A, The sum rule: a finite disjoint union is finite with ∣A∪B∣=∣A∣+∣B∣\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert and ∣⋃i∈IAi∣=∑i∈I∣Ai∣\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).

Proof

technique · direct
1.1

If ∣G∣≥r|\mathcal G|\ge r, any rr members of G\mathcal G are pairwise disjoint and therefore form an rr-petal sunflower with empty core.

givenF1
1.2

Suppose ∣G∣≤r−1|\mathcal G|\le r-1 and put X=⋃G∈GGX=\bigcup_{G\in\mathcal G}G. Since the members of G\mathcal G are disjoint kk-sets, ∣X∣=k∣G∣≤k(r−1)|X|=k|\mathcal G|\le k(r-1).

givenF2
2.1

Every F∈FF\in\mathcal F meets XX. Otherwise FF would be disjoint from every G∈GG\in\mathcal G, so G∪{F}\mathcal G\cup\{F\} would be a larger pairwise disjoint subfamily, contradicting maximality.

step 1.2given
3.1

Thus the first case gives an empty-core sunflower, while the second gives a transversal XX of size at most k(r−1)k(r-1) meeting every member of F\mathcal F.

step 1.1step 1.2step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

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