Boolean Antichains in Finite Lattices: Complete Classification, Product Structure, and Matroid Applications

Garber, Goltermann, Horiatakis, König, and Gottesman asked for constructions and counts of Boolean antichains in geometric lattices and proposed a spanning-tree correspondence for graphic matroids. We answer the graphic expectation and the general-lattice construction question in greater generality by classifying Boolean antichains of every size in every finite lattice. For an ordered family, intersecting all but one member produces candidate Boolean atoms. The family is Boolean precisely when those atoms rise above the common meet and all 2^k reconstruction height gaps vanish. This gives an exact finite formula for the complete enumerator. Its binomial transform is multiplicative under lattice products, equivalently giving an explicit positive convolution.

For a rank-r matroid, maximum Boolean antichains in the flat lattice are naturally in bijection with bases of the simplification. For graphs this gives spanning forests and specializes to the proposed spanning-tree bijection in the connected simple case. Retaining parallel classes recovers the multivariate basis polynomial, while flat intervals give minor-local and rank-tight versions. The framework also yields explicit all-size formulas for uniform matroids, complete classifications for finite distributive and subspace lattices, a universal Möbius formula for Boolean pairs, and complete distributions for finite projective planes.

The Lean 4 sources, theorem map, verification instructions, and finite regression scripts are available at github.com/crabsatellite/matroid-boolean-antichains.