Crab Research
Return to results
Combinatorics

Boolean Antichains in Finite Lattices: Product Formulas and Matroid Applications

Working Paper · SSRNFirst public Revised

A formalization is a machine-checkable proof. The proof assistant’s logical core, or kernel, checks every supporting theorem using only the stated basic logical principles, with no extra unproved theorem assumptions (Kernel-Only).

Overview

Product formulas and a matroid-basis correspondence enumerate Boolean antichains, with explicit counts for uniform matroids and finite subspace lattices.

Original public questions

Counting Boolean Antichains: the general-lattice part of Question 6.1

Julien Garber, Lina S. Goltermann, Daniel Horiatakis, Dennis König and Tal Gottesman: Counting Boolean Antichains — Remark 4.5 and the general-lattice construction and counting part of Question 6.1. The Tamari recursion and lattice-congruence questions are outside the stated scope.

Original abstract (English)

We study the enumeration of Boolean antichains in finite lattices through product formulas and matroid correspondences. The binomial transform of the labelled Boolean-antichain counts is multiplicative under lattice products, yielding an explicit positive convolution for every size. For a rank-r matroid, maximum Boolean antichains in its flat lattice are naturally in bijection with bases of the simplification. This inverse correspondence extends the known Boolean span of a basis and proves the spanning-tree expectation of Garber, Goltermann, Horiatakis, König, and Gottesman in the connected simple graphic case.

The framework gives explicit all-size counts for uniform matroids and finite subspace lattices. Parallel-class weights recover the multivariate basis polynomial, and flat intervals give minor-local and rank-tight versions. For an arbitrary finite lattice, an exact recognition criterion tests whether the candidate Boolean atoms rise above the common meet and all 2^k reconstruction height gaps vanish. Summing these tests over ordered tuples gives the complete enumerator, while the structured families above admit more compact evaluations. Further consequences include a disjoint-filter interpretation for distributive lattices, a universal Möbius formula for Boolean pairs, and complete distributions for finite projective planes.

Public abstract source

Boolean antichainfinite latticematroidcombinatorial enumerationproduct formulageometric lattice

Mathematical review

Kernel-Only

The principal conclusions have a public kernel-checked proof package and reviewed correspondence with the paper. This is distinct from external peer review.

Review standard
Return to results
Back to Mathematics