Provedretrieval-speed-dualityhead-triageattentionduality
Depth trade-off arithmetic: L·n^{1+α} ≤ n^{2−δ} when L ≤ n^{1−α−δ}
For all , if , and , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- n, α, δ, L range over real numbers: the statement must hold for every choice. (
(n α δ L : ℝ)) - <Less than
- 0 is strictly smaller than n. (
0 < n) - ≤At most
- L is less than or equal to n^(1 − α − δ). (
L ≤ n ^ (1 - α - δ)) - ·Multiplication
- L times n^(1 + α). (
L * n ^ (1 + α)) - aᵇPower
- n raised to the power 1 − α − δ. (
n ^ (1 - α - δ)) - -Subtraction
- 1 minus α. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - α) - +Addition
- 1 plus α. (
1 + α)
theorem rsd-depth-tradeoff (n α δ L : ℝ) (hn : 0 < n) (hL : L ≤ n ^ (1 - α - δ)) (hL0 : 0 ≤ L) :
L * n ^ (1 + α) ≤ n ^ (2 - δ)A model built only from range-limited layers (cost n^{1+α} each) stays truly subquadratic up to polynomial depth n^{1−α−δ}; emulating a SETH-hard retrieval task robustly would need more depth than that. Part of 'Retrieval–Speed Duality: the score range that lets a head retrieve is the range that makes it hard to accelerate'.
How it was proved
- Proved
- 4 October 2026
- By
- Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 12 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.