4 Layer L1b: permutation sums
The paper’s core analytic-combinatorial machine (§5.4): the balance between logarithmic losses and factorial gains, in the pure word model (DESIGN.md §5.5).
Words are maps \(w\colon \mathrm{Fin}\, m \to \mathcal{L}\) with prescribed fiber sizes; \(\mathrm{wordSum}\) sums a functional over them, and the definitional ledger is \(\mathrm{paperSum} := \big(\prod _{\mathfrak l} m_{\mathfrak l}!\big) \cdot \mathrm{wordSum}\). Paper-facing statements use \(\mathrm{paperSum}\) on the left with the paper’s right-hand sides verbatim; proofs manipulate \(\mathrm{wordSum}\). Includes the no-adjacent-equal-letters and primitivity predicates on words, and the labeled-arrangement fiber-count lemma (\(\# \{ \text{labeled arrangements inducing } w\} = \prod _{\mathfrak l} m_{\mathfrak l}!\)).
For \(\tau \)-separated points \(x_1,\dots ,x_n \in \mathbb {T}^4\): \(\sum _{\pi \in S_n}\prod _{j=1}^{n-1} \lvert x_{\pi (j)} - x_{\pi (j+1)}\rvert ^{-2} \le C^n (n!)^{1/2}\tau ^{-2(n-1)}\), via the iterated local inequality (1.15).
Dyadic packing shells, last-index peeling over injective tuples, central-binomial factorial comparison.
For \(A, B \subseteq \mathbb {Z}^4\) with separations \(M, N\) and \(P = \lvert A\rvert M^4\), \(Q = \lvert B\rvert N^4\): the bilinear bound (5.58) with right-hand side \(\lvert A\rvert ^{1/2}M^{-2}\, \lvert B\rvert ^{1/2}N^{-2} \min \big(1, (Q/P)^{1/4}\big)\), by dyadic shell counting.
Single-\(y\) bound (5.63) by near/far case analysis; the three-case \(y\)-summation (5.65)–(5.67); \(Q \le P\) assembly and the min-combination with the weak bound.
Leaf types, \(\gamma ^2_{\mathfrak n}\), \(\gamma ^\infty _{\mathfrak n}\), and the power-counting identity (5.31).
The estimate (5.39) for word sums with a skipped set \(O\) (\(\mathrm{paperSum}\) normalization; no primitivity assumed): scale classification \(\sigma _1,\sigma _2,\sigma _3\), outer \(\boldsymbol {X}\)-sum (5.76)–(5.86), inner \(\pi \)-sum (5.87)–(5.98) via the local inequalities (5.90)–(5.92). Formalization makes explicit the inclusive-ancestor constant in (5.69) and uses the exponent \(2(m_{\mathfrak l}-2)\) in both simple-leaf products of (5.83); see docs/PAPER_NOTES.md.
The generalized estimate (5.33) with compound leaves under (5.32), constants \(C_0 {\gt} 1000\), \(D = e^{C_0^{10}}\). Proof by induction on the tree: choose the lowest branching node satisfying (5.40); collapse its subtree to a compound leaf via the word-level collapse equivalence \(\pi \leftrightarrow (\pi _1, O, \pi _2)\); comparability (5.41); factor bookkeeping (5.42)–(5.48), with the \(((s+1)!)^{-1}\) of (5.45)(i) supplied by the ledger 13.
The estimate (5.15): \(\mathrm{paperSum}\) of the inverse-square chain weights is bounded by \(C^n \sum _{W\subseteq \mathcal{B}\setminus \{ \mathfrak r\} } (n - \lvert W\rvert )!\, \prod (m_{\mathfrak l}!)^{1/2}\cdots \) — the log-loss/factorial-gain balance. Derived from 18 by merging adjacent equal copies ((5.34)–(5.37)); the constants \(C_0, D\) are discharged here.
The (5.1)-form lattice estimate from 12 and 19: geometric \((N_{\mathfrak n})\)-summation (5.16)–(5.17), the endpoint refinement \(\min (\lvert W\rvert + 1, n-2)\), and the elementary inequality \((n-s)!\, \lvert \log \varepsilon \rvert ^{\min (s+1,n-2)} \le C^n\lvert \log \varepsilon \rvert ^{n-2}\). Consumed by 26 through the discretization interface 25.