Australasian Journal of Combinatorics 96 (2026), 319-334.
Average-rare order ideals in functional preorders
by Masahiro Hachimori and Kenji Kashiwabara
Abstract
We prove that for the preorder induced by a function $f:V\rightarrow V$, the family of all order ideals is average-rare, that is, its normalized degree sum 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.