exists_family_card_six_no_three_petal_sunflower
There is a finite family F of six 2-element subsets of a 6-element ground set (namely the six edges of two disjoint triangles) such that no 3-element subfamily of F is a sunflower with any kernel: for every G ⊆ F with |G| = 3 and every set C, G is not a sunflower with kernel C. Since |F| = 6 > 2!·2 = 4, this shows that the folklore threshold k!·s is not a valid bound in the sunflower lemma; the threshold must grow as k!·s^k.
Statement
theorem exists_family_card_six_no_three_petal_sunflower :
∃ F : Finset (Finset (Fin 6)), (∀ A ∈ F, A.card = 2) ∧ F.card = 6 ∧
(∀ G ⊆ F, G.card = 3 → ∀ C, ¬ IsSunflower G C)- Source
- Counterexample recorded when the KB node exists_isSunflower_of_card_gt_factorial_mul was refuted (two disjoint triangles = 6 edges, a 2-uniform family with no 3-petal sunflower); it is the sanity witness for the corrected node exists_isSunflower_of_card_gt_factorial_mul_pow.
- Verified
- 10 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Built on 1
- IsSunflowerA finite family F of finite sets is a sunflower (a delta-system) with kernel C if every member of F contains C and any two distinct…
Read back from the Lean
There exists a finite family F of finite subsets of the 6-element set Fin 6 such that: 1. every member A of F has exactly 2 elements (A.card = 2); 2. F itself has exactly 6 members (F.card = 6); 3. for every subfamily G ⊆ F with exactly 3 members, and for every finite set C of vertices of Fin 6, it is NOT the case that G is a sunflower with kernel C. Clause 3 uses the knowledge-base predicate IsSunflower G C, whose body is: (∀ A ∈ G, C ⊆ A) ∧ (∀ A ∈ G, ∀ B ∈ G, A ≠ B → A ∩ B = C). So "G is a sunflower with kernel C" means: C is contained in every petal of G, and any two distinct petals of G have intersection exactly C. Clause 3 says this fails for every possible kernel C. So in ordinary terms: the declaration asserts the existence of a 6-edge set (each edge a 2-element subset of a 6-vertex set) whose every 3-edge subfamily fails to be a sunflower — i.e. a set of 6 pairs on 6 points in which no 3 of the pairs have a common kernel. Since distinct 2-element sets meet in at most one point, the forbidden configurations are exactly: three pairwise disjoint pairs (kernel ∅), and three pairs sharing one common point with otherwise disjoint endpoints (kernel a single vertex). Quantifier form (explicit order): ∃ F, (∀ A, A ∈ F → A.card = 2) ∧ F.card = 6 ∧ (∀ G, G ⊆ F → G.card = 3 → ∀ C, ¬ IsSunflower G C). The hypotheses are bundled as conjuncts of an existential, not as separate premises.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- Two disjoint triangles give six 2-element sets with no 3-petal sunflower, refuting the folklore threshold k!·s for the sunflower lemma. -/ theorem exists_family_card_six_no_three_petal_sunflower : ∃ F : Finset (Finset (Fin 6)), (∀ A ∈ F, A.card = 2) ∧ F.card = 6 ∧ (∀ G ⊆ F, G.card = 3 → ∀ C, ¬ IsSunflower G C) := by refine ⟨{{0,1},{1,2},{0,2},{3,4},{4,5},{3,5}}, ?_, ?_, ?_⟩ · decide · decide · intro G hGF hG3 C hC have hpair : ∀ a ∈ ({{0,1},{1,2},{0,2},{3,4},{4,5},{3,5}} : Finset (Finset (Fin 6))), ∀ b ∈ ({{0,1},{1,2},{0,2},{3,4},{4,5},{3,5}} : Finset (Finset (Fin 6))), ∀ d ∈ ({{0,1},{1,2},{0,2},{3,4},{4,5},{3,5}} : Finset (Finset (Fin 6))), a ≠ b → a ≠ d → b ≠ d → ¬(a ∩ b = a ∩ d ∧ a ∩ b = b ∩ d) := by decide obtain ⟨a, b, d, hab, had, hbd, hGeq⟩ := Finset.card_eq_three.mp hG3 have ha : a ∈ G := by rw [hGeq]; simp have hb : b ∈ G := by rw [hGeq]; simp have hd : d ∈ G := by rw [hGeq]; simp have h1 : a ∩ b = C := hC.2 a ha b hb hab have h2 : a ∩ d = C := hC.2 a ha d hd had have h3 : b ∩ d = C := hC.2 b hb d hd hbd exact hpair a (hGF ha) b (hGF hb) d (hGF hd) hab had hbd ⟨by rw [h1, h2], by rw [h1, h3]⟩