The Coffee Bean Problem: Exact Finite-n Optimality, Minimal-Cost Growth, and Monotone-Class Rigidity

A combinatorial optimization problem over graded families of nondecreasing labels. Every finite CBS has a rational label generating function G(q)=qP(q)/Q(q) with Q(q)=det(I−qT). For the coffee bean rule, breadth-first order is optimal for every n, with exact cost and multiplicity formulas; the minimum cost satisfies C_min(n,k) ~ (k/(k+1))(k!)^{1/k} n^{1+1/k}. Within the natural monotone class the coffee bean rule is uniquely characterized by Q(q)=(1−q)^k, P(q)=1, ρ(T)=1, and is extremal in cost and multiplicity. Companion Lean 4 development (asymptotic chain formalized, sorry-free): https://github.com/ycmath/cbs-lean. Deterministic verification scripts and run logs included. Submitted to the Electronic Journal of Combinatorics; this deposit is the preprint of record.