← All papers
Average-Rare Order Ideals in Functional Preorders
math.CO
Nov 25, 2025 · v1
TL;DR
All theorems on average-rarity of order-ideal families of functional preorders are machine-checked in Lean 4 with definitions added to mathlib4.
Abstract
We prove that for the preorder induced by a function f: V -> V, the family of all order ideals is average-rare, that is, its normalized degree sum (nds) is nonpositive. As a base case in our reduction, we establish the same result for functional partial orders (or rooted forests). We also propose a conjecture related to Frankl's Conjecture. All proofs have been formally verified in the proof assistant Lean 4.
Problem
Frankl's Conjecture concerns the existence of rare vertices in union-closed set families. Whether the family of all order ideals in a functional preorder satisfies the average-rarity condition (a stronger property implying the conjecture) was unresolved.
Approach
The authors prove that for the preorder induced by a function f: V -> V, the family of all order ideals is average-rare (normalized degree sum is nonpositive). They reduce the general case to functional partial orders (rooted forests) as a base case. All proofs are formally verified in Lean 4.
Results
The average-rarity result is established for all functional preorders, verified in Lean 4. The authors also propose a new conjecture related to Frankl's Conjecture.