A Tight Linear Deterministic Competitive Ratio for Fully Online KV-Cache Scheduling

Jaillet et al. introduced a fully online model for batching nonpreemptive LLM requests under a growing KV-cache memory constraint. For total end-to-end latency they proved that every deterministic algorithm has competitive ratio Omega(sqrt(n)), while the elementary sequential upper bound is n. We close this gap. Let R_det(n,M) be the optimal deterministic ratio for exactly n requests at memory M, and let R_det(n)=sup_M R_det(n,M). For every n >= 2 we prove (n-1)/12 <= R_det(n) <= n, so R_det(n)=Theta(n). The hard instance uses the explicit fixed memory M=2(n-1)n, chosen before the lower-bound scheduler is quantified. The exact model, causality argument, both comparator branches, and quantifier order are machine-checked in Lean 4. This deposit includes the six-page preprint and a one-command reproducibility archive. The archive verifies all packaged files against a canonical manifest, downloads and hash-checks pinned sources, builds the Lean module, runs all 30 tests, checks theorem identity and axioms, regenerates the exact control artifact byte for byte, and recompiles the paper. Extract the ZIP and run python3 verify_all.py. Research-system disclosure: Beyond, the research system operated by Nth Research Collective, materially assisted with literature retrieval, hypothesis generation, exact computation, formalization, proof critique, adversarial review, and drafting. Ian D'Ambrosio selected the target, directed the investigation, reconciled the evidence, verified the final claims, and accepts full responsibility for the manuscript. Beyond is not an author.