2 Layer L0: combinatorics
Pairings of finite index sets, interval structure, primitivity, and the elementary counting lemmas of the paper’s §5.4.2. Everything here is mathlib-level combinatorics with no analytic content.
A partial pairing \(\kappa \) of a finite index set \(A\) is a partition of a subset \(P \subseteq A\) into disjoint two-element subsets (pairs); \(S = A \setminus P\) is the set of single indices. If \(S = \varnothing \), \(\kappa \) is a full pairing.
For a linearly ordered finite index set: subintervals \([a,b]\); a subinterval \(B\) is fully paired under \(\kappa \) if \(\kappa \) induces a full pairing on \(B\); \(\kappa \) is primitive if no proper subinterval is fully paired. The L0 API also provides: the induced pairing after removing a fully paired subinterval (paper Def. 3.1(2a)), the smallest-leftmost fully paired subinterval selector with its uniqueness lemma, and enumeration finsets for fixed index sets (needs of 44 and §4.1).
The number of plane rooted trees with \(r\) leaves in which every internal node has at least two children is at most \(C^r\) for an explicit absolute constant \(C\). Such trees have at most \(2r-1\) vertices; the balanced-parentheses serialization injects them into Dyck-type words of bounded length, giving an explicit \(C\).
Prefix-code cancellation for the serialization key; injection into bounded binary words.
A family of positive integers is lacunary if every dyadic window \([X, 2X]\) contains \(O(1)\) of its members.
For every \(\alpha {\gt} 1\) there is \(\beta = \beta (\alpha )\) with \(\binom {m+n}{m} \le \alpha ^m \beta ^n\); the multinomial analogue (paper (5.50)); and the lacunary version (paper (5.51)) with a uniform \(C^{n_1+\dots +n_r}\) bound.
Binomial theorem term bound; exact-telescoping multinomial recursion; dyadic pigeonhole and sorted rearrangement for the lacunary case.
For \(\theta {\gt} 0\) and \(m \le n\): \(\sum _{1\le z_1,\dots ,z_m\le n}\prod _{j=1}^{m-1} \min \big(1, 2^{-\theta (z_j - z_{j+1})}\big) \le C(\theta )^n\); the dyadic version (paper (5.56)); and the variants skipping at most 100 factors.
Truncated drops with a strictly monotone reindexing into binomial counts; rank replacement for the dyadic version; block splitting for the skip variant.