Nine composed theorems, machine-checked

A composed theorem is a cross-paper result that exists in no single paper: the graph's typed preconditions expose when a lemma proved in one lineage applies, verbatim, to an architecture from another lineage with no citation path between them. Source claims enter Lean as named axioms, anchor-cited to the file:line in the papers that prove them; explicitly argued bridging assumptions are likewise named axioms; the composed statements are then proved from those axioms — so the composition itself is machine-checked (core Lean 4.32.1, no mathlib, sorry-free at the composition layer, with per-theorem #print axioms audits). Nine composed theorems hold under this regime — one from round 1, eight from round 2 — and two of their predicted separations (S5 state tracking; mod-3 counting) were validated by a cheap falsification harness. Full narrative in preprint §7.

In plain terms, the nine:

1. AT-2 — Attention-graph reachability is provably insufficient for inner-product search: under OVC, any network on PowerAttention's power-of-2 graph needs Ω̃(n^1−o(1)) layers for BigBird's minimum-inner-product task, though one full-attention layer solves it.
2. AT2-KV-1 — Every prefix-decided KV eviction/merging policy is a streaming algorithm; BalanceKV's INDEX lower bound then forces a linear-in-n cache-budget floor in the high-accuracy retrieval regime.
3. AT2-KV-4 — Under the matching-window assumption, a content-oblivious sliding-window cache with budget B ≥ L is deterministically lossless for COPY; L separates eviction-safe from eviction-hard inputs.
4. AT2-KV-6 — Under Scissorhands' power-law attention-weight model (k > 3), vAttention's verified sampling budget is O(1), independent of context length — a statement in neither paper.
5. AT2-LG-3 — No diagonal-real finite-precision linear RNN, any depth or width, can count modulo 3 — while the same class provably implements in-context gradient descent.
6. AT2-LG-4 — Spectral-filtering (STU) networks are in L-uniform TC⁰: the literature's strongest length-generalization guarantee coexists with conditional S5 impossibility.
7. AT2-LG-6 — Any looped transformer with Periodic+Local per-pass computation needs Ω(n/log n) passes to copy n tokens.
8. AT2-LG-7 — Full-coverage length generalization is class-relative: from identical S5 coverage data, Householder-product linear RNNs provably generalize; diagonal/gated SSMs (conditionally) contain no solution.
9. F2 — No-free-lunch: no linear-RNN/SSM class is both regular-language complete and in L-uniform TC⁰ unless TC⁰ = NC¹; classes with only nonnegative real transition spectra are unconditionally incomplete.

A tenth composition (AT-3: SMYRF's exactness-assumption triple must fail on worst-case inputs under OVC) is machine-checked but rests on two explicitly accepted readings; it is counted separately as proof-complete-modulo-bridges. The Lean stage also corrected two defects in our own proof dossiers — formalization was not stenography.