Average-Rare Order Ideals in Functional Preorders

2025/11/25 by Masahiro Hachimori, Hachimori, Masahiro, Kenji Kashiwabara +1
Mathematics · Computer Science · #Commutative Algebra and Its Applications #Polynomial and algebraic computation #Rings, Modules, and Algebras

paper · pdf · doi:10.48550/arxiv.2511.19833

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.

Citations

• On the Averaging Problem of Ideal Families Related to Frankl's Conjecture with Formal Proof by Lean 4
• Improving the Lower Bound for the Union-closed Sets Conjecture via Conditionally IID Coupling
• Better bounds for the union-closed sets conjecture using the entropy approach
• Extension of a Method of Gilmer
• Improved Lower Bound for Frankl's Union-Closed Sets Conjecture
• A constant lower bound for the union-closed sets conjecture
• The journey of the union-closed sets conjecture

Related

• On the Averaging Problem of Ideal Families Related to Frankl's Conjecture with Formal Proof by Lean 4
• On Order Ideals of Minuscule Posets III: The CDE Property
• Low upper bounds of ideals
• The converse of a theorem by Bayer and Stillman
• Degree functions of graded families of ideals