Rank rigidity from a sharp chain bound
Abstract
A colouring attaining the trivial monochromatic chain bound in an odd Boolean lattice is constant on each rank, and its ranks split equally between the two colours.
Theorem 1.1 (Equal-rank sets have equal colours).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/ErdosUlam/SublatticeRankRigidity.rank_rigidity (✓ std3). ∎
Source. Repository-derived.
Commentary.
Every maximal chain has n plus one members. Its two colour classes are sublattices whenever nonempty, so the assumed upper bound forces each colour to occur exactly (n plus one) divided by two times. For a set C and distinct points x and y outside C, enumerate C first, then x and y, then the remaining points. Reversing x and y produces two maximal chains which differ only at rank |C| plus one. Balance forces C union {x} and C union {y} to have the same colour. For equal-size A and B, choose x in A outside B and y in B outside A and exchange them. The number of points of A outside B decreases by one. Induction connects A to B.
Theorem 1.2 (The prefix ranks split equally).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/ErdosUlam/SublatticeRankRigidity.balanced_prefixes (✓ std3). ∎
Source. Repository-derived.
Commentary.
The standard prefix chain consists of the subsets with elements less than r, for r from zero through n. Distinct ranks give distinct sets. The assumed upper bound applies to either colour class of this chain. Their cardinalities sum to the even number n plus one, and neither exceeds half that number, so both equal half.