Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Averaging Problem of Ideal Families Related to Frankl's Conjecture with Formal Proof by Lean 4

Masahiro Hachimori, Kenji Kashiwabara

TL;DR

This work addresses Frankl's union-closed conjecture via its intersection-closed form by analyzing average rarity through the normalized degree sum $\mathrm{NDS}(\mathcal{F})$. It proves that every ideal family on a nonempty finite ground set $U$ has $\mathrm{NDS}(\mathcal{F}) \le 0$, hence is average rare, using induction on $|U|$ and minor operations (deletion, contraction, trace). A key lemma ensures the existence of a rare vertex in any ideal family, which anchors the inductive step and enables case distinctions based on vertex degree. The paper also formalizes the entire argument in Lean 4, with implementations and proofs publicly available, illustrating the role of formal methods in validating intricate combinatorial reasoning. The results open avenues to extend average-rarity analyses to broader intersection-closed classes and demonstrate the practical integration of proof assistants in combinatorics research.

Abstract

Frankl's conjecture, also known as the union-closed sets conjecture, can be equivalently expressed in terms of intersection-closed set families by considering the complements of sets. It posits that any family of sets closed under intersections, and containing both the ground set and the empty set, must have a ``rare vertex'' -- a vertex belonging to at most half of the members of the family. The concept of \emph{average rarity} describes a set family where the average degree of all the elements is at most half of the number of its members. Average rarity is a stronger property that implies the existence of a rare vertex. This paper focuses on ideal families, which are set families that are downward-closed (except the ground set) and include the ground set. We present a proof that the normalized degree sum of any ideal family is non-positive, which is equivalent to saying that every ideal family satisfies the average rarity condition. This proof is formalized and verified using the Lean 4 theorem prover.

On the Averaging Problem of Ideal Families Related to Frankl's Conjecture with Formal Proof by Lean 4

TL;DR

This work addresses Frankl's union-closed conjecture via its intersection-closed form by analyzing average rarity through the normalized degree sum . It proves that every ideal family on a nonempty finite ground set has , hence is average rare, using induction on and minor operations (deletion, contraction, trace). A key lemma ensures the existence of a rare vertex in any ideal family, which anchors the inductive step and enables case distinctions based on vertex degree. The paper also formalizes the entire argument in Lean 4, with implementations and proofs publicly available, illustrating the role of formal methods in validating intricate combinatorial reasoning. The results open avenues to extend average-rarity analyses to broader intersection-closed classes and demonstrate the practical integration of proof assistants in combinatorics research.

Abstract

Frankl's conjecture, also known as the union-closed sets conjecture, can be equivalently expressed in terms of intersection-closed set families by considering the complements of sets. It posits that any family of sets closed under intersections, and containing both the ground set and the empty set, must have a ``rare vertex'' -- a vertex belonging to at most half of the members of the family. The concept of \emph{average rarity} describes a set family where the average degree of all the elements is at most half of the number of its members. Average rarity is a stronger property that implies the existence of a rare vertex. This paper focuses on ideal families, which are set families that are downward-closed (except the ground set) and include the ground set. We present a proof that the normalized degree sum of any ideal family is non-positive, which is equivalent to saying that every ideal family satisfies the average rarity condition. This proof is formalized and verified using the Lean 4 theorem prover.

Paper Structure

This paper contains 20 sections, 8 theorems, 30 equations.

Table of Contents

  1. Introduction
  2. Frankl's conjecture
  3. Averaging approach to Frankl's conjecture
  4. Formalization of the theorem
  5. Mathematical preliminaries
  6. Intersection-closed families, rarity, and average rarity
  7. Ideal families
  8. Minors of ideal families
  9. Deletion minor: ${\mathcal{F}}.{\rm del}\,{v}$
  10. Contraction minor: ${\mathcal{F}}.\text{cont}\,{v}$
  11. Trace minor: ${\mathcal{F}}.{\rm trace}\,{v}$
  12. Examples
  13. Ground set with two vertices
  14. Ground set with three vertices
  15. Ideal family with a vertex of degree 1 and a large hyperedge
  16. ...and 5 more sections

Key Result

Lemma 2.1

If a set family $\mathcal{F}$ satisfies the average rarity condition, $\mathcal{F}$ has a rare vertex.

Theorems & Definitions (18)

  • Definition 2.1: Intersection-closed family
  • Definition 2.2: Degree of a vertex
  • Definition 2.3: Rare vertex
  • Conjecture 2.1
  • Definition 2.4: Normalized degree sum
  • Lemma 2.1
  • Definition 2.5: Ideal family
  • Lemma 2.2
  • proof
  • Lemma 2.3
  • ...and 8 more