A Strict Bound for Nonempty Uncomplemented Strongly Incomparable Families

Let Bn = 2[n] be the Boolean lattice of subsets of [n] = {1, …, n}. A family A ⊆ Bn is uncomplemented if it contains no complementary pair {S, [n] ∖ S}, and two families Ai, Aj ⊆ Bn are strongly incomparable if no member of one is a subset of any member of the other. Peng, Yan, and Zhao recently proved that any t ≥ 2 mutually strongly incomparable, uncomplemented families in Bn have total size at most 2n−1, and conjectured (arXiv:2611.12199v1, Conjecture 4.3) that if t ≥ 3 and every family is nonempty, the maximum total size M(n,t) is 2n−1 − 1 for all n ≥ 3 and 3 ≤ t ≤ n. We resolve this conjecture by proving that ∑i=1t |Ai| ≤ 2n−1 − 1 for any t ≥ 3 nonempty, individually uncomplemented, pairwise strongly incomparable families in Bn. The proof combines Gladkov’s multiple-event Harris–Kleitman inequality with a new reflection inequality for upsets and a capacity bound for order-convex bands whose equality case forces the incomparable exterior to have a connected comparability graph. The upper bound, matching construction, and exact value M(n,t) = 2n−1 − 1 have also been formally verified in Lean 4. MSC 2020: Primary 05D05; Secondary 60C05, 06E30, 68V20. Files: The 11-page final manuscript is provided as Hilton_Nonempty_Strict_Bound_Final.pdf. Hilton_arXiv_Submission 2.0.zip contains the LaTeX manuscript, Lean 4 formalization, verification scripts, and supporting documentation and logs. Licensing: The manuscript, LaTeX text, and accompanying documentation are licensed under Creative Commons Attribution 4.0 International (CC BY 4.0). The Lean formalization and verification scripts are licensed under the Apache License, Version 2.0. Third-party dependencies retain their respective licenses.