Frankl’s Union-Closed Sets Conjecture

A Lean 4 formalization scaffold for Frankl’s union-closed sets conjecture.

The Conjecture

For every finite nontrivial union-closed family of finite sets, some element belongs to at least half of the member-sets.

In Lean, a family is represented as Finset (Finset α), and the half-bound is written without division:

F.card ≤ 2 * memberCount x F

Current Formalized Territory

The project proves the classical small-set cases and several local pieces of the (now-paused) entropy-transport attack.

• Singleton case. If a union-closed family contains {x}, then the map A ↦ insert x A injects the member-sets omitting x into the member-sets containing x; hence x occurs in at least half the family.
• Doubleton case. If a union-closed family contains {a, b} with a ≠ b, then a or b occurs in at least half the family. Partition the family by the membership pattern of a and b; the map A ↦ insert a (insert b A) injects the (a∉, b∉) block into the (a∈, b∈) block, and a short counting argument shows a or b must be abundant (Frankl.isFranklElement_left_or_right_of_pair_mem).

These are the standard “a member-set of size ≤ 2 forces the conjecture” results (Bruhn–Schaudt survey); they are formalized as known territory, independent of the entropy program.

• Twin-free reduction (Frankl.FamilyTwinFree). Elements i, j are twins if every member contains both or neither. Deleting one twin — F ↦ F.image (·.erase j) — preserves union-closure (isUnionClosed_image_erase), the family size, and every non-j element’s count, and transports a Frankl element back to F (franklConjectureFor_of_erase_twin). So the conjecture reduces to twin-free (separating) families. Sorry-free, axiom-clean.

Lattice (Poonen) reformulation

Frankl.Lattice states the equivalent lattice form (Poonen 1992): every finite lattice L with |L| ≥ 2 has a join-irreducible element j (Mathlib’s SupIrred) below at most half of the elements, 2 * |{x : j ≤ x}| ≤ |L| (FranklLattice). Two known classes are proved completely and sorry-free:

• Distributive lattices (franklLattice_of_distribLattice), by an elementary Birkhoff-free argument: a maximal join-irreducible j with the map x ↦ ⨆ {y ≤ x : ¬ j ≤ y} injects the up-set of j into its complement. Finite chains follow (franklLattice_of_linearOrder).
• Lattices with a left-modular coatom (franklLattice_of_leftModular_coatom, Woodroofe) — the “master” case covering modular, dually (lower) semimodular, and supersolvable lattices. Pick a join-irreducible x ⊄ m; since the coatom m satisfies x ⊔ m = ⊤, the map α ↦ m ⊓ α injects ↑x into its complement (injective by left-modularity x ⊔ m ⊓ α = (x ⊔ m) ⊓ α).
• Modular lattices (franklLattice_of_modular, Abe–Nakano) follow as a corollary: every element of a modular lattice is left-modular, and a finite nontrivial lattice has a coatom. This strictly generalises the distributive case.
• Large-coatom-ideal lattices (franklLattice_of_large_coatom_ideal), found while attacking the open frontier: if some coatom m lies above at least half the elements then any join-irreducible x ⊄ m satisfies ↑x ⊆ L ∖ ↓m, so |↑x| ≤ |L|/2. No modularity needed; incomparable to the modular case. Its engine two_mul_card_upset_le_of_disjoint_finset (any finset disjoint from ↑x of size ≥ |↑x| certifies x) underlies the experimental condition (★) explored in research/lattice_frankl_attack.md — which survives all testing but is not a proof.

Poonen’s equivalence is fully proved: franklConjecture_iff_franklLattice shows FranklConjecture ↔ FranklLattice (sorry-free, axiom-clean).

• Forward (franklConjecture_imp_franklLattice): given a finite lattice L, the members f a = {j join-irreducible : ¬ j ≤ a} (a ∈ L) form a union-closed family on the join-irreducibles whose Frankl element is a join-irreducible j₀ with 2 |↑j₀| ≤ |L|.
• Reverse (franklLattice_imp_franklConjecture, in Frankl.LatticeReverse): given a union-closed family F (with ∅ ∈ F), the poset (F, ⊆) is a finite lattice; a meet-irreducible m has a least strict upper bound m⁺, and any x ∈ m⁺ ∖ m makes m the largest x-free member, so ↓m is exactly the x-free members. The dual lattice bound 2 |↓m| ≤ |F| then makes x abundant. Supporting results: InfIrred.exists_least_gt (a meet-irreducible in a finite lattice has a unique upper cover) and ucLattice (the lattice structure on a union-closed family).

The meet-irreducible (dual) form FranklLatticeMeet — the formulation Poonen proved equivalent to the conjecture — is shown equivalent to FranklLattice by order duality (franklLattice_iff_franklLatticeMeet). The semimodular/modular/geometric lattice cases are future work.

Reduction to indecomposables (Frankl.LatticeProduct): a join-irreducible witness in one factor lifts to a product — if 2|↑j₁| ≤ |L₁| then 2|↑(j₁,⊥)| ≤ |L₁ × L₂|, since ↑(j₁,⊥) ≃ ↑j₁ × L₂ (franklLattice_witness_prod_left, franklLattice_prod_left). Hence a nontrivial direct product is automatically a Frankl lattice, and by induction on Nat.card the conjecture reduces to the directly-indecomposable lattices (Boolean lattices, being products of two-element chains, are handled for free). This is a structural reduction, obtained without any local witness-selection — see research/frankl_negative_space_round.md.

Reduction along a cut element (Frankl.LatticeCut): a cut element c (comparable to every element) splits L vertically into ↓c and the filter ↑c = Set.Ici c. A join-irreducible Frankl witness of ↑c lifts to L (franklLattice_witness_of_cut): such a witness j is ≠ c (so it is join-irreducible in L too — its lower covers all lie ≥ c by the cut property), its up-set is unchanged (↑j ≃ ↑j ∩ ↑c), and |↑c| ≤ |L|. Hence the conjecture also reduces to the vertically-indecomposable lattices; combined with the product reduction, to those that are both directly and vertically indecomposable.

Relatively-complemented atoms (Frankl.LatticeRelComplement). The mechanism behind the geometric-lattice case, isolated with no semimodularity:

• franklLattice_witness_of_atom_relComplemented — if a is an atom and every x ≥ a has a relative complement of a in [⊥, x] (a ⊓ y = ⊥, a ⊔ y = x), then a is a join-irreducible Frankl witness (2|↑a| ≤ |L|). Proof: x ↦ y injects ↑a into its complement (a ≰ y, and x = a ⊔ y recovers x).
• franklLattice_witness_of_atom_complementedModular — a concrete instantiation: complemented modular lattices are relatively complemented (IsModularLattice.exists_disjoint_and_sup_eq), so every atom is a witness.

This captures the operative content of the geometric (atomistic upper-semimodular) case verified in research/frankl_negative_space_round.md.

Geometric lattices (Frankl.LatticeGeometric) — the genuinely new, non-modular semimodular case, built on the relative-complement mechanism. Since Mathlib v4.28.0 has no semimodular/geometric-lattice class, the geometric lattice is given by the two elementary axioms that define it:

• hsm upper-semimodularity (covering form): p ⊓ q ⋖ p → q ⋖ p ⊔ q;
• hat atomisticity (usable form): below any x ≰ z lies an atom c ≤ x, c ≰ z.

From these, atom_exchange_of_semimodular derives the matroid exchange property, exists_relComplement_of_geometric derives relative complementation by a maximal-element argument, and franklLattice_witness_of_atom_geometric concludes that every atom is a Frankl witness (2|↑a| ≤ |L|). These axioms hold for every geometric lattice — partition lattices Πₙ, subspace lattices, and any atomistic modular lattice — so this covers the non-modular geometric lattices that the modular case (franklLattice_of_modular) misses. All sorry-free and axiom-clean.

Concrete instance & the modular bridge (Frankl.GeometricInstances). The powerset lattice Finset α is exhibited as a concrete geometric lattice: atomistic_finset discharges hat (via Finset.not_subset and singleton atoms), upperSemimodular_finset discharges hsm (via the powerset cover characterisation), and franklLattice_witness_singleton_finset instantiates the abstract theorem — every singleton {a} is a Frankl witness in Finset α — proving the geometric hypotheses are non-vacuous. Separately, isUpperSemimodular_of_modular shows every modular lattice satisfies hsm (via the diamond order-iso infIccOrderIsoIccSup, which preserves CovBy), connecting the geometric axiom to Mathlib’s IsModularLattice.

Extremal / balanced families (Frankl.Coatom)

A self-contained study of every-half families — union-closed families in which every ground element lies in exactly half the member-sets (2 * memberCount x F = |F|), the set-side image of the Frankl-extremal case (see research/frankl_tight_boolean.md). All sorry-free and axiom-clean.

• Coatom lemma (coatom_mem_of_everyHalf_twinFree): a twin-free every-half union-closed family contains every coatom (familyUnion F).erase i. The member-subfamilies {A ∈ F : i ∈ A} are distinct (twin-free) and all of size |F|/2 (every-half), hence pairwise incomparable; so for i ≠ j some member separates them, and the union of all i-avoiding members is exactly U ∖ {i}. Supporting: biUnion_id_mem_of_nonempty_subset and the incomparability lemma exists_mem_of_everyHalf_twinFree.
• Field-of-sets characterization (everyHalf_field_iff_powerset): a nonempty twin-free family that is both union- and intersection-closed and every-half is exactly the full power set (familyUnion F).powerset. Forward direction is the coatom-lemma payoff (intersection-closure generates every subset from the coatoms); the reverse (isEveryHalf_powerset &c.) shows the power set realizes all hypotheses, so Frankl’s ½ bound is sharp — attained with equality at every element. Dropping intersection-closure is exactly the open, conjecture-equivalent residual.

The active research program is tracked in research/checklist.md. It focuses on formalizing the Gilmer/AHS entropy hinge, testing a coupled-OR replacement, and migrating stable finite certificates into Lean.

Structure

Building

lake update && lake build

The top-level open conjecture file intentionally contains one sorry; all supporting modules listed above are closed.

Research Artifacts

Lightweight Verification

python3 -m py_compile research/gilmer_ahs_verification.py research/window_experiment.py
python3 research/gilmer_ahs_verification.py --check-ahs-certificate research/ahs_hinge_certificate.json
python3 research/window_experiment.py --check-center-certificate research/center_generation_certificate.json
python3 research/window_experiment.py --check-tc-summary research/tc_exact_n4_size7_summary.json
python3 research/window_experiment.py --campaign frontier-shadow
lake build

Named computational campaigns can be listed with:

python3 research/window_experiment.py --list-campaigns

The same lightweight suite is available as:

research/lightweight_checks.sh