Boolean antichains of intermediate size in the Tamari lattice

The Tamari lattice construction, checked against the source's own drawings and its own statistics: |Tₘ| = cₘ for 2 <= m <= 9, the greatest element is above all cₘ elements and the least below all of them (so the indexing is a linear extension), |cov(1)| = m-1, the qₘ-fibre through the greatest element has exactly m elements, and exactly cₘ - cₘ₋₁ elements are not the greatest in their fibre

Loc. cit. Theorem thm:mainₜhm_for_Booleanₗattices reproduced: the number of Boolean antichains of size k in the Boolean lattice Bₙ is the Stirling number S(n+1,k+1), all 21 entries for 2 <= n <= 6, and there is none of size n+1

The partition lattice table: |Cₖ(Pₙ)| for 3 <= n <= 6 and every k. The maximal-size entries 3, 16, 125, 1296 are the source's nⁿ⁻²; the intermediate entries – |C₂(P₅)| = 620, |C₃(P₅)| = 670, |C₂(P₆)| = 9750, |C₃(P₆)| = 24050, |C₄(P₆)| = 11595 – are in neither the source nor OEIS

The table the source's Question asks for: |Cₖ(Tₘ)|, the number of Boolean antichains of size k in the Tamari lattice Tₘ, for 2 <= m <= 8 and every k, computed from the definition verbatim (every pair of subsets). The k = 2 column is 2, 21, 167, 1248, 9330, 71247 and the k = 3 column is 5, 106, 1579, 20870, 263823

The two membership tests agree: the reduced test, which enumerates only the partitions C u c = T u A u B, returns the same count vector as the literal definition on Tₘ for 2 <= m <= 9, on Bₙ for n <= 6 and on Pₙ for n <= 6 – COVERAGE NARROWED 2026-08-29: formal agreement is Tamari-only

Loc. cit. prop: BooleanAreValid, verified exhaustively for 2 <= m <= 9: every Boolean antichain of Tₘ has at most one element that is not the greatest element of its qₘ-fibre, and the Boolean antichains all of whose elements are fibre maxima are exactly the fₘ₋₁-images of the Boolean antichains of Tₘ₋₁, size for size

The refined split, 2 <= m <= 9: for every size k, how many Boolean antichains of Tₘ have exactly one element off its qₘ-fibre maximum, and how many of those have that element in the fibre through the greatest element. Against the naive count (m-1)*|Cₖ₋₁(Tₘ₋₁)| the latter is exact for k <= 2 and strictly smaller from k = 3 on

|Cₖ(T₉)| = 1, 4861, 558963, 3288908, 4632944, 2360907, 505701, 45838, 1430, 0 – the table at the kernel-bound frontier, from the definition verbatim

Negative controls: the source's own worked counterexample in T₄ – w = (x1((x2(x3x4))x5)), a = ((x1(x2x3))(x4x5)), b = ((x1x2)(x3(x4x5))) – has all three pairs Boolean and all three pairwise joins equal to the top, yet the triple is not Boolean; the count of merely-pairwise-joining subsets differs from the Boolean-antichain count in Tₘ from m = 4 on while coinciding at every size in the distributive Bₙ; and |C₅(T₆)| is neither 41 nor 43, and T₆ has no Boolean antichain of size 6

Cost profile and the parked frontier: T₉ costs 8.71 s and 195 MB in C and 197 s and 1.89 GB under native_decide in Lean; T₁0 costs 429 s and 2.31 GB in C and yields the row 1, 16795, 4505098, 40990121, 83309281, 61023464, 19526769, 2923896, 198458, 4862; T₁1 is over the cap at 27.6 GB of meet and join tables. Two Lean-side facts against what the C profile predicts: the partition-reduced membership test does 8.1x fewer join tests and is 15x faster in C but costs the SAME in Lean (231 s against 226 s at T₉), and the meet/join tables are 34% of the C bill but only a few percent of the Lean one (three T₉ searches off one Ctx take 517 s against about 3 x 197 s for three that each build their own). Plus: native_decide counts heartbeats against its own evaluation – the literal T₈ count passes at the 200,000 default in 7.0 s while the identical statement at T₉ exhausts 2,000,000 after 740 s and fails with 'timeout at isDefEq', which reads exactly like an elaborator blow-up and is not one