# A Joint Formal–Empirical Knowledge Graph of the Efficient-Sequence-Model Literature, and What Auditing It Mechanically Reveals

**PaperGraph (working name) — draft v0.1, 2026-07-25**

---

## Abstract

We built a knowledge graph over 600 arXiv papers on efficient attention and long-context
sequence models in which both layers of each paper — the theorems and the tables — are
extracted into typed, provenance-anchored form and cross-linked: 119,486 empirical result
tuples (each anchored to a file:line in the paper's LaTeX source and gated by adversarial
verification), 760 typed theoretical claims, and 660 compile-checked Lean 4 statements of
those claims. Because theory and evidence live in one queryable structure, questions that
previously required weeks of reading become mechanical queries, and we report four findings
obtained that way. (i) The subfield's theory and experiments are largely decoupled: of the
326 in-scope formal claims (complexity, approximation, expressivity), 292 — 90% — are never
empirically tested, a rate essentially unchanged as the corpus grew from 220 to 600 papers.
(ii) An audit evaluating each quantitative guarantee's own formula at its paper's deployed
configuration finds systematic divergence between what is certified and what is run: in the
claim-level round, 29 of 157 auditable claims (18%) are deployed strictly outside their
certified regimes, 87 (55%) are not evaluable at all (unpinned constants, unrecorded premise
parameters), and several prominent methods deploy a variant their theorem does not cover —
in some cases a variant the paper's own ablation shows to be worse. (iii) Contradiction
mining over the fused graph surfaces cross-paper baseline forks (three circulating
generations of "the S4 baseline"; a 22-point spread in "the BigBird baseline"), roughly 15
papers with provable internal defects including a mechanically verifiable transposed
citation, and one formal contradiction: FlashAttention's IO-optimality claim is refuted in
the small-cache regime by a later paper's constructive algorithm. (iv) The graph's typed
preconditions support machine-proposed compositions of theorems across papers with no
citation path: nine composed theorems (one from round 1, eight from round 2) are
machine-checked in Lean — the formalization step itself caught and repaired two defects in
our own proof dossiers — and a cheap falsification harness validated two predicted
separations (S5 state tracking; mod-3 counting) at toy scale. We take the audit results to
be a property of the field's publishing conventions, not of any individual paper: nothing
here impugns the empirical contributions of the audited work, and the corpus also contains
papers whose theory–deployment hygiene is essentially complete.

---

## 1. Introduction

The efficient-attention literature maintains two parallel discourses. One proves theorems:
approximation guarantees with explicit feature counts, IO lower bounds, circuit-class
memberships, copying-capacity bounds. The other runs benchmarks: LRA, WikiText-103,
LongBench, needle retrieval. The two are written into the same papers, but they interact
far less than the papers' framing suggests. A guarantee's preconditions — a norm bound, a
feature-count formula, a projection-dimension schedule — are stated once, in notation, and
then the experiments proceed at whatever configuration trains well. Whether the deployed
configuration satisfies the theorem's hypotheses is a question of arithmetic that, as far
as we can tell, essentially nobody performs: not authors, not reviewers, not readers. The
arithmetic is not hard; it is merely tedious, scattered across appendices, and unrewarded.

Our claim is that this audit becomes mechanical once the literature is represented at the
right resolution. We built that representation for one subfield: a joint formal–empirical
knowledge graph in which every extracted number is one click from the LaTeX it came from,
every theorem is a typed claim with explicit preconditions (and, where possible, a
compiling Lean statement), and results are linked to the claims they test. Formal-only
graphs exist for pure mathematics (the mathlib dependency graph); a crude empirical shadow
exists for benchmarks (Papers with Code). The joint graph is where the value is, because
the interesting failures are precisely at the interface: claims nothing tests, deployments
nothing certifies, baselines that silently fork.

The retrieval use of such a graph ("every empirical test of sub-quadratic-attention
quality claims, with contradictions highlighted") is the obvious one, and we ship it. But
the design goal is generation: the graph should propose experiments and theorems. Typed
preconditions expose when a lemma proved for architecture family A applies, verbatim, to
architecture family B in a different lineage with no citation path — a composition a human
reader would need to hold two subliteratures in mind to notice. Gap queries enumerate
claims no experiment touches. Contradiction mining ranks places where theory or evidence
must give. The north star, stated in our project specification before any of the work
below, is one novel, validated result that provably came from graph structure rather than
from a human reading papers. The composed theorems and validation runs of §7 are the
current state of that programme.

This paper describes the graph (§2–3) and four findings (§4–7), then limitations (§8). All
numbers are reproducible from the repository's data files; we cite source anchors
(arXiv id, file:line) throughout.

---

## 2. Corpus and pipeline

The corpus is 600 arXiv papers on efficient attention, state-space models, long-context
architectures, KV-cache compression, and the associated theory (screened from 777
candidates; 597 parsed with zero failures — we work from LaTeX source, not PDF). The
pipeline, in order:

**Structure parse.** Sections, theorem environments, tables, and citation keys, each with
a file:line anchor. A gold-set audit on six seed papers (Performer, Linear Transformers,
RetNet, FlashAttention, Longformer, Mamba) found theorem-block extraction exact on all six
(23/23 blocks) and table extraction at 70 parsed against 66 ground truth (4 spurious, 2
missed) before fixes; the main defect classes (nested tabular bodies, title macros) were
fixed and re-verified.

**Result extraction with an adversarial gate.** LLM extractors emit result tuples (model,
dataset, metric, value, config notes) from tables and text; each tuple then faces
independent verifier votes (two votes in the widened round) attempting refutation before
it may enter the graph. Corpus-wide, 119,486 tuples were accepted and 6,963 refuted — a
5.5% rejection rate at the gate. The refutation discipline is deliberately conservative:
unstated metrics or datasets, unnamed systems, by-construction baselines, bound cells
(">1000"), and footnote-approximated values are refuted, not guessed. Zero schema
violations; every tuple carries provenance (paper, table index, file:line anchor, caption,
extractor, verifier votes).

**Conservative entity resolution.** Model, dataset, and metric vocabularies are clustered
into canonical entities with versioned SAME_AS verdicts rather than destructive merges. At
the 220-paper stage: 3,870 model names → 3,686 clusters, 1,416 dataset names → 1,290,
822 metric names → 653, with exact partitions, no duplicate aliases, and count
conservation over all 37,028 tuples then in the graph. Size variants are kept separate;
case-collision traps (CrossFormer the vision model vs Crossformer the time-series model)
were manually split; false-positive joins (SparseK ≠ sparseKT) were explicitly rejected at
adjudication. The resolution increment for the widened corpus (4,215 model, 1,830 dataset,
682 metric names) was in progress at the time of writing.

**Typed claims.** Every theorem-bearing paper's theorem blocks are extracted into typed
claims: kind (complexity_bound, approximation_error, expressivity, impossibility,
equivalence, ...), a plain restatement faithfulness-checked against the LaTeX, objects,
bound, preconditions, anchor. Round 1 produced 455 claims from all 46 theorem-bearing
papers (631 theorem blocks; unintelligible blocks recorded as skips with reasons, never
guessed); the widened corpus added 108 theory papers (25 off-domain pure-mathematics
papers gated out) for 760 claims total across 154 papers — 133 expressivity, 109
complexity_bound, 88 equivalence, 84 approximation_error, 42 impossibility, with the
remainder in smaller kinds.

**Compile-checked Lean tier.** Each claim gets an autoformalization attempt into Lean 4
(4.32.1, core only, no mathlib): abstract preambles, the paper's preconditions as
hypotheses, and a sorry proof — the statements compile, the papers' proofs are not
re-verified (§8). All 660 statements across 121 papers compile with zero failures; 100
round-1 claims are marked not_formalizable with reasons. Formalization earned its keep
beyond the composition work of §7: writing hypotheses explicitly surfaced
implicit-hypothesis debt in the literature — papers omitting conditions their theorems
need (exact Taylor expansion, power-series representability, positivity constraints,
exactness conjuncts), each flagged in the Lean file headers and fed into the audit.

**Fusion and store.** TESTS edges link results to the claims they probe, with
support/contradict/mixed verdicts; the verdict discipline never links quality metrics to
complexity claims, and zero-edge papers are documented rather than force-linked. The graph
carries 55 verified claim-level edges (31 same-paper, 24 cross-paper via the
entity-resolved joins) with 398 result links; verdicts: 46 supports, 7 mixed, 1
contradicts, 1 inconclusive. An ABLATES layer aggregates 4,798 same-table
model-vs-Transformer-class comparisons across 25 architecture families. Everything loads
into a single SQLite store.

Corpus statistics:

| Quantity | Value |
|---|---|
| Papers (screened → in corpus → parsed) | 777 → 600 → 597 |
| Accepted result tuples | 119,486 |
| Tuples refuted at the adversarial gate | 6,963 (5.5%) |
| Typed claims (papers with claims) | 760 (154) |
| Compiled Lean 4 statements (papers) | 660 (121), 0 compile failures |
| Entity clusters at the 220-paper stage (models / datasets / metrics) | 3,686 / 1,290 / 653 |
| Claim-level fusion edges (same-paper / cross-paper) | 55 (31 / 24), 398 result links |
| ABLATES comparisons (families) | 4,798 (25) |
| Demo-scope claims: probed / never tested | 34 / 292 (of 326) |

---

## 3. Finding 1: the theory–empirics gap is large and scale-stable

The demo query asks: of the sub-quadratic-attention claims in scope (kinds complexity,
approximation, expressivity), which are empirically probed at all?

At 220 papers, 178 claims were in scope and 158 (89%) were never tested by their own
papers. Enriching the graph with cross-paper TESTS edges — other papers' experiments
probing a claim, joinable only because entity resolution exists — raised the probed count
to 34, leaving 144 (81%) untested by anyone in the corpus.

At 600 papers the in-scope set grew to 326 claims; the probed count is unchanged at 34,
leaving 292 (90%) untested. (The probed count is inherited from the 220-paper edge layer:
fusion-edge enrichment over the widened corpus awaits the in-progress entity-resolution
increment, so 90% is the current upper estimate of the gap; new edges can only lower it,
and at the previous ratio would lower it to roughly the same 80–90% band.) Among the 34
probed claims, 1 is contradicted and 6 have mixed or inconclusive evidence.

The point is not that any single claim ought to have been tested — many are asymptotic
statements with no finite content to test (§5 quantifies this). The point is that the
untested surface is now an enumerated, provenance-linked list rather than a vague
suspicion, and that its relative size did not shrink when the corpus nearly tripled. The
theory and the experiments of this subfield are, to first order, produced independently.

---

## 4. Finding 2: the scope audit — certified versus deployed

### 4.1 Method

For each paper we (1) keep only quantitative guarantees: explicit constants or rates tying
a resource parameter (features m, projection dimension k, cache budget B, sample count) to
a tolerance or failure probability; (2) recover the deployed parameter values from the
extracted results' config notes and from the source tarballs; (3) evaluate the bound's own
formula at the deployed values. Verdicts: **inside** (deployment satisfies the certified
preconditions), **outside** (deployment provably violates them), **not evaluable** (the
formula cannot be evaluated at any deployed configuration — unpinned constants, asymptotic
conditions, or premise parameters never recorded). Where a paper's constants exist only in
its proofs, we use the proof-pinned constants and say so.

Round 1 audited 43 papers at paper level: batch A (20 papers) 2 inside / 6 outside / 12
not evaluable; batch B (23 papers) 5 inside / 1 outside / 17 not evaluable. Round 2, over
the widened corpus, re-ran the audit at claim level: **157 auditable claims across 71
papers — 41 inside (26%), 29 outside (18%), 87 not evaluable (55%)**.

Three things should be said before the details. First, this is an audit of scope hygiene,
not of correctness or good faith: no audited theorem is claimed to be wrong (with one
exception, treated as a contradiction in §5), and the papers' empirical contributions
stand on their own. Second, the failure mode is structural — the certified regime and the
efficient operating regime often cannot coincide, and saying so plainly would cost the
papers little. Third, the corpus contains model citizens (§4.6) proving the standard is
attainable.

### 4.2 The empty-regime and never-runs patterns: Linformer and Performer

**Linformer** (2006.04768) carries the subfield's canonical "linear attention preserves
quality" theorems. Theorem 1's proof selects the projection dimension by the (sufficient)
schedule k = 5 log(n)/(ε²−ε³). Since ε²−ε³ ≤ 4/27 for ε < 1, that schedule is satisfiable
only when k ≥ (27/4)·5·ln n: thresholds 210.6 at n = 512, 233.9 at 1024, 257.3 at 2048,
280.7 at 4096. The paper's flagship k = 128 sits below the threshold at every deployed n,
and the underlying finite-n probability inequality is vacuous at k = 128 as well — **the
proof certifies nothing nontrivial at any headline configuration**. At k = 256 the schedule
certifies ε ≈ 0.49 at n = 512 and ε ≈ 0.55 at n = 1024 — and substituting the schedule
gives failure probability 2n^{-1/4} ≈ 0.42, i.e. ~50% relative error holding with only
~58% confidence. At n ≥ 2048 the schedule is empty (257.3 > 256); the raw finite-n
inequality remains technically nonvacuous there, but the best available certificate is
ε = 2/3 (67% relative error) at success probability 0.69 (n = 2048) and 0.38 (n = 4096).
Two scope caveats, both cutting the same way: the schedule is a sufficient choice, so this
is a statement about what the proof certifies, not about what smaller k can achieve; and
Theorem 1 covers the random-sketch construction P·RᵀR rather than the learned projections
actually trained — the architectural theorem is Theorem 2, whose proof constants exclude
k = 128 on both of its branches. Theorem 2 adds a statement/proof discrepancy: the
printed d-branch is 9d·log d where the proof chooses 9·log d, a factor-d gap; under the
proof reading k = 256 certifies ε ≈ 0.62, under the printed statement the minimum k is
16,166 and every deployed configuration is outside on both branches. This case was independently re-derived by a cross-model verification pass (a GPT-family
agent working only from the paper's PDF): all arithmetic confirmed, with the sufficiency
framing and the finite-n nonvacuity at k = 256, n ≥ 2048 refined as stated above. Our own round-1
reading (which dropped the ε³ term) had reported ε ≈ 0.40–0.49 at deployed k; the exact
formula supersedes it and is stricter. Separately, the certificate is existence-style —
it attaches to Johnson–Lindenstrauss random projections, not to the trained shared
projections deployment actually uses.

**Performer** (2009.14794) deploys an estimator its uniform-convergence theorem does not
cover. thm:uniform certifies the trigonometric estimator with orthogonal random features;
every quality-reported run uses positive features (FAVOR+) or ReLU generalized attention,
and the paper's one trigonometric deployment (PG-19) is reported as "highly unstable",
with "even NaN values in training". The four orthogonality theorems ("orthogonality
provably helps", including the abstract's claim) all require m ≤ d; every deployed model
runs m = 256 features at head dimension d = 64 — a factor-4 violation, in a regime where
m mutually orthogonal vectors do not exist. Even ignoring estimator identity, a constant-1
illustration of the m-formula at ε = 0.1 and an implausibly favourable norm bound R = 1
demands m ≈ 5.7 × 10⁴ (222× the deployed 256); at spiky-attention norms
R² = √d·ln n (n = 4096) it demands m ≈ 1.9 × 10¹². The exact MSE formulas are fully
pinned but never evaluated on deployed data: the positive estimator's relative MSE
provably exceeds 100% once ‖x+y‖ ≥ 2.36, and no run records where its inputs sit.

### 4.3 Certified-variant-never-runs, generalized

Round 1 found four papers whose guarantee and deployment are disjoint by construction —
SMYRF (exactness requires an infinite logit gap: the certified regime is empty for every
real input), EVA (exactness requires singleton partitions and circularly-defined
coefficients), LSSL (the certified O~(N+L) algorithm "was not implemented" and was later
found "not numerically stable and thus not usable on hardware"; the deployed path is
O(NL), a ~127× unrealized certificate at N = 128, L = 16000), and Mamba, whose only
theorem (thm:gating) requires N = 1, A = −1, B = 1 while deployment sets N = 16, learned
A initialized as diag(−1..−16), and input-dependent B — and whose own ablation shows the
certified corner more than 1.0 perplexity worse. Round 2 shows the pattern is general:

- **PolySketchFormer** (2310.01655): the guarantee is a probability over a Gaussian-sketch
  draw; deployment trains the sketches, which is not a draw from any sketch distribution
  (the paper itself calls learning "a heuristic"). Its appendix shows the certified random
  variant measurably worse: PG-19 32k perplexity 13.66 (random, r = 64) vs 12.19 (learned)
  vs 11.55 (softmax). Deployment deliberately trades the certificate for quality.
- **HyperAttention** (2310.05869): the certified algorithm samples columns by squared row
  norms of V; the deployed pipeline, by the paper's own description, uses uniform sampling
  — a different estimator carrying no certificate. The main theorem's precondition
  quantity α is "verified" empirically only after excluding the first 32 columns because
  they "often contain heavy entries" — i.e. the precondition as defined is dominated at
  deployment by exactly the attention-sink columns the measurement discards; κ (which
  enters a supporting lemma to the seventh power) is never measured.
- **Scissorhands** (2305.17118): the error theorem requires the kept set to be the exact
  top-B by *current-step* attention scores over all tokens including evicted ones — a
  policy no budget-B algorithm can evaluate, since evicted keys are gone. The paper
  concedes the gap in prose; its own persistence measurement (~95%, dipping in later
  layers) quantifies a mismatch the theorem does not model. The power-law constants the
  bound needs are never fitted for any deployed model.
- **MagicPIG** (2410.16179): the unbiasedness theorem holds for oracle sampling from the
  exact attention distribution, which the paper twice states is unavailable to the
  efficient method; the deployed self-normalized importance sampler is biased at every
  finite budget, with no bias or variance bound. Observed accuracy drops (GSM8K
  77.6 → 71.0–72.7) are unconstrained by the theory.
- **BalanceKV** (2502.07861): the streaming guarantee couples the recursion depth to the
  batch size as T = log₂(n/t); at deployed t = 256 the certified T is 4, 5, and 7 for the
  4k, 8k, and 32k input buckets, but deployment fixes T = 2 for all inputs (the coupling
  holds only at n = 1024, which no bucket is). The certified configuration — retaining
  ~256 tokens with n-independent memory — runs on no LongBench-E input; deployment
  retains 0.25n.
- **2110.14416**: the generalization theorem's construction is available only to the dense
  softmax variant; the deployed kernelized and sparse variants implement a decoupled
  approximation the proof cannot instantiate.

### 4.4 Exact-arithmetic misses

Two round-2 items show how fine the certified/deployed boundary can be. The relative
positional encoding separation of 2106.12566 (Proposition 1) requires n > d + 1; at the
language-modelling configuration n = 512 and d = 512, the condition needs n ≥ 514 —
**missed by two**. Every main-paper configuration fails the condition (the sole inside
configuration, ImageNet32 at n = 3072, is an appendix task), so the proposition certifies
no separation at any headline experiment. Conversely PowerAttention (2503.03588) is
genuinely inside its reachability theorem at every deployed context, but the theorem's
printed strict bound "out-degree < log n" is falsified by exact equality at the paper's
own flagship 32k configuration (128 blocks; vertex with out-degree exactly
7 = log₂ 128); the proof supports ≤. Cosmetic — and exactly the kind of defect a
formula-evaluation audit catches and an eyeball never will.

### 4.5 Inside but vacuous; retroactive certification

A fourth de-facto category emerged in round 2: bounds genuinely satisfied at deployment
that certify nothing. 2505.12252's concentration bound is fully pinned and its
preconditions hold at every configuration — but inverting it shows the certificate is
non-trivial only for errors 4.3× to 155× larger than the largest value the approximated
quantity can take; certifying a 10% error at 95% confidence would need ≈ 2.9 × 10⁶
features against the deployed 128. MambaJSCC (2409.16592) certifies a coupling term of
about 6 × 10⁻¹¹ at its stated operating point — true, and trivially so. FAVOR#
(2302.00787) is inside on all three theorems, but the certified object is a
data-dependent variance value that is never recorded for any deployed model. RFA
(2103.02143) is the limiting case: an unbiasedness certificate with no tolerance
parameter at all, under which D = 1 feature receives the identical guarantee as the
deployed 128–256.

FlashAttention (2205.14135) provides the corpus's one case of **retroactive
certification**. Its own IO theorem's sub-regime (d ≤ M ≤ Nd, boundary N* = M/d = 1536 on
A100) places the BERT and GPT-2 headline configurations outside — their measured speedups
there are kernel fusion, not the certified IO reduction. But 2402.07443's later tight
characterization certifies Θ(N²d²/M) exactly in the large-cache regime M ≥ d², and every
standard deployment sits there (M/d² = 24 at d = 64, 15.4 at d = 80, 6.0 at d = 128): a
2024 paper certifies a 2022 deployment the original theorem's own sub-regime excluded.
The audit framework has no difficulty with this — certificates are edges in a graph, not
properties of papers — but it is worth noticing that the field's most successful kernel
was certified-at-deployment only two years after the fact, by other authors.

### 4.6 Model citizens

Scope hygiene is attainable, and the audit should say so as loudly as it says the rest.
2404.00560 pins its coverage-based length-generalization preconditions per task: five
deployed problems provably satisfy the positive theorems (and reach 100% at every test
length), two provably sit inside the impossibility regime (and degrade as predicted), and
the one configuration falling in the theory's gap — addition in one-line format — is
exactly where generalization fails; the paper's theory–deployment map is essentially
complete, honest gap included. 2502.09287 states fully pinned lower bounds with no hidden
constants: at the deployed S = 128, K = 1300, ρ = 0 configuration the white-noise bound
evaluates to a 90.2% loss floor, and the autocorrelated bound is active at five of seven
deployed (K, ρ) pairs and vacuous precisely at the two most-correlated ones, where the
theory says copying gets easy. 2410.10101 measures its certificate quantity
(λ_min = 0.06 vs 0) on the deployed datasets and deliberately deploys on both sides of
its own regime boundary. 2411.12537 is the cleanest scope match in the corpus: all four
audited results inside, with the deployed baseline variants provably satisfying every
hypothesis of the impossibility theorems and the deployed fix a one-parameter exit from
the certified-failure regime — the observed 0.0-vs-1.0 accuracy split lands exactly on
the regime boundary.

### 4.7 What the 55% means

The modal audit outcome is not "outside" but **not evaluable**: 87 of 157 claims (55%),
and 29 of 43 papers in round 1. The dominant causes, in order: big-O/Θ constants never
pinned (fatal when the constant sits in an exponent); guarantees that are limit statements
with no rate; and — most tellingly — premise parameters that are physically measurable but
never recorded: no Performer run records the query/key norm bound R its theorem needs; no
HyperAttention deployment records κ; Radar's margin condition depends on a norm ζ measured
in no experiment (evaluated at the natural scale ζ = √d, its certificate demands a margin
of 223.9 where margins cannot exceed 1, and a feature budget seven orders of magnitude
above the deployed one). Universal-approximation-style theorems are structurally
incapable of scoping efficiency–quality tradeoffs — BigBird's and Sumformer's certify
identical tolerances at any sparsity, and BigBird's explicit value-network construction
needs ~10^946,962 layers at illustration scale. One mirror-image case deserves note:
Repeat-After-Me (2402.01032) has fully explicit constants, and evaluating them shows its
certified-failure regime begins at ~10.7M tokens — roughly four orders of magnitude
beyond every experiment, so the copying failures it observes at L ≤ 1000 are a learning
phenomenon its own information-theoretic theorem does not certify (the paper concedes
this qualitatively; the graph makes it quantitative).

---

## 5. Finding 3: contradictions and integrity

### 5.1 The anomaly that started it

The ABLATES layer's same-table win rates against Transformer-class baselines put the two
most-theoremed linear-attention methods near the bottom: at the round-1 adjudication,
Linformer 15W–62L–4T (19.5%) and Performer 51W–69L–12T (42.5%); over the widened corpus
(4,798 comparisons) the rates are essentially unchanged at 19% and 42%, against e.g. S4
at 95% and hybrids at 77%. Are the losses *inside* the quality-preservation theorems'
preconditions (a genuine theory–evidence contradiction) or outside them? Adjudicating
claim-by-claim against the deployed configurations (§4.2's arithmetic) gave the same
verdict for both: **scope-mismatch**. No losing row operates where the theorems are
strong; Performer's catastrophic losses concentrate exactly where its own
exp(2R²/√d) sample cost explodes (ListOps at 18.01 ≈ chance, replicated in nine
independent papers), and Linformer's LRA losses sit where its theorems certify a
relative error of ~0.5–0.6 — or, at the flagship k = 128, nothing at all.
The theories are narrower than their reputations; the evidence contradicts the
reputation, not the theorems.

### 5.2 Cross-paper baseline drift

Entity-resolved joins make baseline provenance queryable, and the results are not
flattering.

- **Three generations of "the S4 baseline"** (E8): the S4 paper revised its LRA numbers
  between arXiv versions, and the corpus circulates v1, intermediate, and updated values
  for the same (model, dataset, metric) — Path-X 88.10 / 86.26 / 96.35 across 10+ papers,
  mostly without version annotation. The smoking gun is mechanical: 2408.05391 reports S4
  ListOps = 88.65, 29 points above all twelve other reports (59.60) — its S4 row is the
  v1 row except ListOps, which carries the updated *Image* value. No S4 configuration in
  any version scored 88.65 on ListOps; this is a column-transposed citation, verifiable
  from the two source tables, and 2404.11163's S4 row shows the same shift pattern.
- **BigBird LRA Retrieval spans 59.29–81.50** (E9) across ten papers: 59.29 (seven papers
  citing the official run), 75.05 (own run, config unannotated), 79.73 (an honestly
  flagged reimplementation), 81.50 (a citation of a citation matching no primary run in
  the DB). A 22.2-point spread on the one LRA task where retrieval-style matching
  dominates: every "X beats BigBird on Retrieval" comparison is decided by baseline
  choice, not architecture.
- **Transformer Pathfinder spans 40.57–80.38** (E10): one paper's own rerun at 40.57 —
  below the 50% chance line, a failed training run published as the baseline — against a
  canonical 71.40 and reimplementations at 73.6–75.1; another paper tabulates three
  different values from three citation sources for the identical model/dataset/metric.
  The WikiText-103 perplexity spread (18.5–34.1) is the well-behaved contrast: every gap
  there is config-annotated. Any efficient-attention win rate computed over the
  literature inherits ±5–9 points of pure baseline noise on LRA.

### 5.3 Within-paper defects

The widened extraction pass produced an integrity catalogue of roughly 15 papers with
provable internal defects: proven row-label swaps, averages contradicting their own
components, byte-identical duplicate tables, caption-vs-body metric contradictions, and
one admitted post-hoc data adjustment. We emphasise the modifier *provable*: each entry
is an arithmetic or textual inconsistency internal to the paper, checkable from its
source, not a judgement about undisclosed methodology.

### 5.4 A formal contradiction, and the reconciliations

Round 2's contradiction mining produced 11 findings: 4 contradictions, 6
reconciled-by-scope, 1 tension-needs-experiment.

The one formal contradiction (F1): **FlashAttention's optimality claim is refuted in the
small-cache regime.** 2205.14135 pairs its Θ(N²d²/M) IO upper bound with a lower bound
asserting no algorithm does better "for all M ∈ [d, Nd]"; 2402.07443 exhibits an
algorithm computing exact attention with O(N²d/√M) IO, which beats N²d²/M exactly when
M < d² — so throughout d ≤ M = o(d²), FlashAttention does a factor d/√M more IO than
optimal, and the per-M optimality reading under which the theorem pair certifies
FlashAttention is false. The literal lower-bound statement survives only through its ∀M
quantifier, whose proof anchors at M = Θ(Nd) where the bound is the trivial input-size
bound. No experiment is needed; a constructive algorithm settles it. Deployed
configurations are unaffected (M ≈ 98,304 ≫ d² = 4,096 — the large-cache regime, where
§4.5's retroactive certificate applies).

The reconciliations are, if anything, the more useful output, because each yields a
discriminator the papers do not state. The clearest (F2): the corpus's four
impossibility and five expressivity results on linear-RNN state tracking all reconcile on
a single axis — **the structure of the input-dependent transition matrix**. Diagonal with
nonnegative real spectrum (the Mamba/S4 parameterization): TC⁰, commutative-only,
parity-incapable. Diagonal with negative or complex eigenvalues: parity and mod-counting
unlock. Non-diagonal products of generalized Householder reflections: all regular
languages. No expressivity claim's precondition intersects any impossibility claim's,
and the discriminator is corroborated inside the DB (Mamba restricted to eigenvalues
[0,1]: formal-language score 0.073; the [−1,1] variant: 0.452; DeltaProduct₄: 0.739).
This reconciliation is promoted to a theorem in §7 (F2, no-free-lunch). The remaining
reconciliations follow the same pattern — a hidden window-size hypothesis (the "polylog
SSM copies" theorem's convolution reads the whole input, so it satisfies rather than
violates the copying memory bound), chain-of-thought step budgets, spiky-instance
exclusions in SETH-hardness vs HyperAttention, and input autocorrelation vacating the
shift-K lower bound exactly in the LRA regime where S4 shines. One tension is left
explicitly to experiment (T11): whether Mamba's full-string copying failures are the
information-theoretic phenomenon or an optimization one — the certified threshold sits at
~10.7M tokens, far beyond every observed failure.

---

## 6. Interlude: what the graph proposes

The generative mechanisms (SPEC §7) ran twice. Round 1 (assumption transfer over 455
claims) produced 7 composite conjectures, 3 graded provable-by-composition, with novelty
enforced by corpus-wide co-occurrence greps and citation-lineage checks (one candidate
was rejected after source inspection found the adjacency already present). Round 2, over
the widened claim set, produced 17 conjectures — 9 in a KV-cache/streaming cluster and 8
in a length-generalization/expressivity cluster — of which 7 were proof-sketch-complete
at mining time. Gap ranking separately produced 15 testable never-tested claims, headed
by a designed duel: a polylog-size-SSM copying theorem against a fixed-state
impossibility bound on shared benchmark infrastructure, where either outcome refutes a
published claim (this duel drives the copy experiments of §7.2; its theorem-level
resolution turned out to be a scope reconciliation, F3, leaving the learnability question
— which the experiments address — open).

---

## 7. Finding 4: composed theorems, machine-checked, and cheaply falsified

### 7.1 The nine compositions

The composition stage takes source theorems as proven by their papers and proves the
*composition*, with every bridging assumption named and classed: (a) immediate from
definitions, (b) true but needing its own argument, given in the dossier, or (c) a
genuine gap. Source claims and class-(b) bridges enter Lean as named axioms anchored to
file:line in the papers; 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. In plain terms:

1. **AT-2** (round 1). Under the Orthogonal Vectors Conjecture, any network using
   PowerAttention's power-of-2 attention graph (which has Õ(n) edges by its own theorem)
   needs Ω̃(n^{1−o(1)}) layers for BigBird's minimum-inner-product task — although one
   full-attention layer solves it, and although every pair of positions in the graph is
   connected in ≤ log n hops. Attention-graph reachability is provably insufficient for
   inner-product search.
2. **AT2-KV-1.** Any prefix-decided KV eviction or merging policy with budget B is a
   streaming algorithm with B·d·p bits of state; BalanceKV's INDEX lower bound then
   forces B·d·p = Ω(min{ε⁻², n}) once query/key inner products may reach
   Θ(√d·ln(n/d)) — in the high-accuracy retrieval regime ε ≤ n^{−1/2}, a linear-in-n
   budget floor for every eviction heuristic in the cluster.
3. **AT2-KV-4.** Under the (L, δ)-matching-window assumption of 2410.03810, a purely
   content-oblivious sliding-window cache of any budget B ≥ L is deterministically
   ε′-lossless for COPY (with the margin constant raised by log(2·V_max/ε′)); the window
   length L separates eviction-safe inputs from the eviction-hard INDEX family, where
   L = n and theorem 2 applies.
4. **AT2-KV-6.** Under Scissorhands' empirical power-law attention-weight model with
   exponent k > 3 (plus bounded values and non-cancellation), vAttention's verified
   sampling budget is bounded by a constant independent of context length — a statement
   in neither paper. The dossier's secondary 2 < k ≤ 3 clause was deliberately *not*
   formalized: its analytic core (stable-law behaviour) is supported by no corpus claim,
   and axiomatizing it would have manufactured a theorem.
5. **AT2-LG-3.** No diagonal-real finite-precision linear RNN — any depth, any width —
   can count modulo 3 (the transition products are diagonal real by induction, hence have
   real spectra; 2411.12537's mod-counting theorem requires a non-real eigenvalue; 3 is
   not a power of two). Conjoined with 2410.11687's constructions, one fixed model class
   provably implements in-context gradient descent *and* provably cannot count mod 3:
   ICL expressivity gives zero leverage against the eigenvalue obstruction. Parity is
   deliberately not claimed — diagonal entries at −1 suffice for it.
6. **AT2-LG-4.** Spectral-filtering (STU) networks are in L-uniform TC⁰; hence, unless
   TC⁰ = NC¹, no STU network solves the S5 word problem — while the same architecture
   carries the literature's strongest provable length-generalization guarantee. Provable
   length generalization and state-tracking power are orthogonal axes.
7. **AT2-LG-6.** Any looped transformer whose per-pass computation is a Periodic+Local
   LimitTransformer needs T(n) = Ω(n/log n) passes to copy n tokens (per-pass
   communication O(log n) against an Ω(n) information requirement). The matching upper
   end — n-RASP-L's T(n) = n program — is conditional on an explicitly open compilation
   bridge (class (c)), and is stated as such; the lower bound does not touch it.
8. **AT2-LG-7.** Full-coverage length generalization (2404.00560) is class-relative:
   from identical full-coverage data on the S5 word problem, Householder-product linear
   RNNs provably generalize at every length, while the diagonal/gated SSM class
   (conditional on TC⁰ ≠ NC¹) contains no solution for any training procedure to find.
   The naive transfer "full transition coverage + enough training ⇒ length
   generalization" is false as a composition of corpus theorems.
9. **F2 (no-free-lunch).** No linear-RNN/SSM class is both regular-language complete and
   L-uniform TC⁰ unless TC⁰ = NC¹ — regular-language completeness necessarily forfeits
   the O(log)-depth parallel-scan computability that motivated linear RNNs. A second,
   hypothesis-free route: classes with only nonnegative real transition spectra are
   unconditionally incomplete (they cannot solve parity, which is regular).

A tenth composition — AT-3, that SMYRF's exactness-assumption triple must fail on
worst-case inputs under OVC — is machine-checked but rests on two explicitly accepted
readings (a randomized form of OVC, and a reformulation of an assumption that is
literally unsatisfiable over the reals); we count it separately as
proof-complete-modulo-bridges.

The Lean stage was not stenography. Formalization corrected two defects in our own
dossiers: AT2-KV-1's English gloss ("B = Ω(n/(d·p)) for constant ε") was internally
inconsistent — the honest bound carries the min and the Ω(n/(d·p)) form holds only in
the retrieval regime ε ≤ n^{−1/2}; and AT2-KV-4's schematic dropped-mass axiom was
unsound as sketched (quantified over arbitrary retained sets) and was repaired to
last-L-containing sets, which is both sound and exactly what the proof needs. Composed
theorems that survive a proof assistant are, in our experience, different objects from
composed theorems that survive a careful reader.

### 7.2 The validation loop

The epistemic chain we are testing is: graph-mined conjecture → Lean-checked composition
→ cheap falsification attempt. The falsification harness is deliberately minimal —
d = 128, 2 layers, 60k steps with a length curriculum, training length 32, identical
recipes across architectures, run locally in minutes per configuration. It can only
probe computational-class predictions at toy scale (§8); what it buys is speed from
conjecture to contact with data.

**S5 word problem (round-1 conjecture AT-1: RetNet and GLA are in L-uniform TC⁰, hence
no NC¹-hard state tracking unless TC⁰ = NC¹; the same ceiling round 2 extended to STU).**
Prediction: a genuinely recurrent control learns running S5 products; linear-state models
and fixed-depth Transformers do not. Across three seeds, at training length 32 the LSTM
reaches 77.1–99.8% accuracy while RetNet reaches 6.2–6.7%, GLA 7.3–10.0%, and the
Transformer 11.6–15.5%, all decaying toward chance (0.83%) with length; at length 256
the LSTM still scores 29.0–93.2% (35–112× chance). Every recurrent seed beats every
linear-state and attention seed by roughly an order of magnitude. Consistent with the
composition; and failure-to-learn at this scale is evidence, not an impossibility proof.

**Copy-capacity duel (gap rank 1), three rounds — including one retraction.** Round 1
(3k steps, flat training) showed a collapse at content length K ≥ 32 (94.1% at K = 8,
66.7% at K = 16, 6.2% at K = 32) that looked like the fixed-state impossibility bound —
and the dose-response control refuted our reading: at 3k steps, K = 32 sat at chance for
*every* state size in {32, 64, 128, 256}, including one with ample capacity. An
optimization artifact; interpretation retracted. Round 2 (30k steps) lifted K = 32 to
~35% with still no state-size gradient. Round 3 (30k steps with a K-ramp curriculum —
the same medicine that made S5 learnable — 3 seeds) finally isolated capacity: mean
token accuracy 36.9% (range 28.3–41.4) at state size 16, 42.8% (38.7–46.8) at 64, and
68.7% (65.5–73.6) at 256, with every large-state seed beating every small-state seed by
more than 18 points. The 16-vs-64 gap (~6 points) is within seed noise and is not
claimed. State capacity causally limits copying at K = 32 once the optimization barrier
is lifted — a coarse small-vs-large separation, not a fine monotone curve — and no
configuration here touches the certified regime of the Repeat-After-Me bound (threshold
~10.7M tokens): consistent with, not certified by, the theorem. We record the arc —
retraction, then dose-response under curriculum — as the honest cost of cheap
experiments.

**Z3 mod-counting probe of AT2-LG-3.** The composed theorem predicts that diagonal-real
linear RNNs admit no length-uniform mod-3 counter, while imposing no such obstruction on
a nonlinear recurrent control. At the time of writing the harness records: LSTM at 100%
accuracy at every evaluation length (32/64/128/256) in both completed seeds; RetNet at
94.1% in-distribution decaying 75.1 → 53.8 → 43.6% toward chance (33.3%) under length
extrapolation; GLA at 99.5% decaying 96.4 → 82.0 → 60.1%; a Transformer reference at
66.4% decaying to 37.5% (RetNet/GLA are seed-0 runs; further seed replications were
still running and are not reported here). This is the theorem-consistent signature:
where no length-uniform solution exists, in-distribution fit is achievable but decays
toward chance under extrapolation, and the control is flat at ceiling. Two features make this probe unusually
clean: the source impossibility (2411.12537) is itself 4/4 *inside* at deployment in the
scope audit — the harness probes a theorem whose deployment-validity is verified — and
the prediction was fixed by a machine-checked composition before the experiment ran.

Both S5 and copy results are new graph nodes: experiments that exist because the graph
composed or contrasted claims across papers with no citation path.

---

## 8. Limitations

**The Lean tier verifies statements, not proofs.** The 660 corpus statements compile
with sorry proofs; only the nine compositions' composition layers are sorry-free, and
those are proved over named axioms standing for source theorems we take on the papers'
authority. A wrong source theorem propagates. (The audit found statement/proof
discrepancies in the corpus — Linformer's factor d, PowerAttention's strict inequality —
so this is not hypothetical.)

**Validation is toy-scale and partly single-seed.** The harness tests
computational-class predictions (can this class represent/learn this structure at all),
not scale phenomena; d = 128, 2-layer models trained for minutes say nothing about what
emerges at 7B parameters. S5 and the copy round 3 have three seeds; at the time of
writing the Z3 probe had one seed for each linear-state architecture (two for the LSTM
control), with replications running. Failure to
learn is evidence, not proof; expressibility and learnability are different properties,
and our curriculum lifts but does not remove optimization barriers (the large-state copy
model plateaus near 69%, not 100%).

**Precision over recall, so recall is unknown.** The extraction gate is tuned to refute
rather than guess (5.5% rejection corpus-wide), and the gold-set audit measures parser
precision, but we do not know how many results and claims the pipeline misses. Known
debt: one paper's experiments were missed entirely (2509.09001, present in source);
theorem statements placed inside proof sections and \captionof-style captions defeat the
parser. Finding 1's denominators inherit this: the untested fraction is computed over
what we extracted.

**The 90% is an upper estimate pending edge enrichment.** The probed-claim count (34) is
inherited from the 220-paper edge layer; cross-paper edges over the widened corpus await
the entity-resolution increment (§2). At the previous enrichment ratio the untested rate
would remain in the 80–90% band, but the exact figure will move.

**The audit's modal verdict is a limitation of the literature and of the audit at once.**
55% of auditable claims are not evaluable: where constants are unpinned or premise
parameters unrecorded, we cannot say deployment is outside the certified regime — nobody
can, which is the point. We chose to report not_evaluable as a first-class outcome
rather than force verdicts; readers should resist summarizing this work as "29 claims
are violated" when its central number is that 87 cannot be checked at all.

**Scope.** One subfield, chosen because theory and experiments visibly interact there.
We do not know how the audit distributes over subfields with different publishing
cultures.

---

## 9. Related work

Formal dependency graphs exist for pure mathematics (mathlib and its visualizations),
and autoformalization is an active research area (the LeanDojo and AlphaProof lineage);
these supply the formal layer only. Papers with Code and leaderboard aggregators supply
a coarse empirical shadow — model/dataset/metric triples without provenance anchors,
preconditions, or claim linkage. Citation-graph infrastructure (S2ORC, Semantic Scholar)
supplies scaffolding but treats papers as atoms. The reproducibility literature has
documented baseline sensitivity and reporting inconsistency at the benchmark level; our
contribution there is mechanism, not sentiment — entity-resolved, provenance-anchored
joins that turn "baselines drift" into named, checkable defects (a transposed citation;
a 22-point baseline fork), and typed preconditions that turn "theory doesn't match
practice" into per-claim arithmetic. The individual scope findings have precedents
inside the audited papers themselves — several state their strongest caveats in
appendices (SMYRF: "far too tight to hold in practice"; Scissorhands' oracle concession)
— which is precisely why a graph that surfaces preconditions next to deployments, rather
than new mathematics, is the missing artifact.

## 10. Conclusion

At the resolution of individual claims and numbers, the efficient-sequence-model
literature is queryable, and querying it is informative: 90% of its formal claims are
empirically untested; where guarantees are checkable, deployment sits outside the
certified regime about as often as inside it, and most guarantees are not checkable at
all; its baselines fork silently; and its theorems, once typed and formalized, compose
across papers into machine-checked results none of the papers state — two of which
survived immediate contact with a falsification harness. None of this required new
mathematics or large-scale computation. It required representing what the papers already
say precisely enough that arithmetic could be done to it. The graph's next obligations
are the ones its own findings assign: edge enrichment over the widened corpus, the
decisive experiments the contradiction analyses specify, and the standing target of a
validated optimization that exists because of graph structure. We would regard the
audit's replication by others, on other subfields, as the more useful outcome.

---

*All corpus statistics, audit records (scope-sweep-A/B, C1–C12), contradiction analyses,
proof dossiers (PROOFS.md, PROOFS-r2.md), Lean sources (`composed-theorems*.lean`, 660
per-claim statements), and validation logs (s5.jsonl, copy.jsonl, z3.jsonl) are in the
project repository under `data/`.*