A Macaulay-Type Lower Bound for Nested Multichains and Lecture Hall Polytopes

Macaulay's theorem bounds the growth of the Hilbert function of a standard graded algebra from above: H(d+1) ≤ H(d)^ . We prove lower bounds of the same type for a natural combinatorial family. Let A_1 ⊆ A_2 ⊆ ... be finite subsets of a totally ordered set and let h(D) count the multichains q_1 ≤ ... ≤ q_D with q_i ∈ A_i. Then h(D+1) ≥ h(D)^ for every D ≥ 1, with equality throughout when all A_i coincide. More precisely, for D ≥ 2, if h(D) = C(n+D-1, D) - c with 0 ≤ c < C(n+D-2, D-1), then h(D+1) ≥ C(n+D, D+1) - c^ : measured against a polynomial ring, the deficit grows at most at Macaulay's rate one degree lower. This complement bound is strictly stronger than the first bound except at binomial values, which characterizes the equality cases, and it is best possible for D = 2. Both bounds hold for chains with any prescribed pattern of strict and weak inequalities; for strict chains they give the Kruskal–Katona analogue h^<(D+1) ≥ h^<(D)^(D) and its complement form. The proofs are a short induction whose essential feature is that nested sequences are closed under deleting their largest elements, and the complement bound is the fixed point of that induction. Through order embeddings by ceilings and floors, the lattice-point counts of s-lecture hall polytopes with s nondecreasing, with weak or strict inequalities, satisfy the same bounds as the dimension grows. For width-normalized (coffee-bean) label systems this gives a short proof of coffee-bean maximality for all k at once and a quantitative version: the shortfall below the coffee-bean count grows at most at Macaulay's rate one degree lower. Examples show that each hypothesis is needed; joins and disjoint unions of chains fail. Files: manuscript PDF; LaTeX source; reverse_macaulay_scripts.zip (exact-integer Python scripts for every numerical statement, including the scripts of the independent referee passes). Lean 4 formalization: cbs-lean release v1.2.0 (doi:10.5281/zenodo.23374238; all versions doi:10.5281/zenodo.22070763) formalizes Lemmas 2.1–2.3 (Lemma 2.1(a) in its one-term form), Theorems 3.1 and 3.4 with their equality cases, Corollary 3.3, Definition 4.1 and Lemma 4.2(a),(b) together with the inequality of (c), identity (2) and Theorem 4.3 for every word (hence Corollary 4.4), the Macaulay inequalities of Corollary 6.1, Lemma 7.1 for k_1 = 1, and Corollary 7.2. Not formalized: Lemma 2.4 and the results that use it, the equality case of Lemma 4.2(c), Proposition 4.8, and the word and complement forms of Corollary 6.1. AI assistance: exploration, numerical experiments and drafting were carried out with the assistance of Claude (Anthropic). Four independent AI referee passes re-derived the proofs and reran the computations. The author checked all statements and takes full responsibility for them.