Provedattentionrelative-tailfinite-stochastic-computationinformation-complexity

Maintained finite attention with sharp relative-tail accuracy and work

For all $\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=1}{m \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=1}{q, R, F, \mathit{epsilon} \in \htmlData{mx=0}{\mathbb{R}}}$ and $\htmlData{mx=6}{k, v : \htmlData{mx=3}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=2}{\htmlData{mx=1}{n} + 1}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{m}$ , $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{q}$ , $\htmlData{mx=0}{q} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{R}$ , $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{F}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\mathit{epsilon}}$ , $\htmlData{mx=9}{\forall j,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{k}(\htmlData{mx=1}{j})} \mathbin{\htmlData{mx=8}{\land}} \htmlData{mx=6}{\htmlData{mx=4}{k}(\htmlData{mx=5}{j})} \mathrel{\htmlData{mx=7}{\leq}} 1}$ and $\htmlData{mx=6}{\forall j,\ \htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{v}(\htmlData{mx=1}{j})} \right\rvert} \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{F}}$ , then

\htmlData{mx=3}{(\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{let}}(\htmlData{mx=1}{D})})(\mathtt{:=\ polynomialDeadline\ n\ R\ let\ H\ :=\ relativeCopies\ m\ R\ F\ epsilon\ let\ r\ :=\ uniformRow\ n\ let\ a\ :=\ polynomialAccept\ q\ R\ k\ let\ c\ :=\ storedPolynomialControl\ m\ q\ (momentSums\ m\ (List.ofFn\ (fun\ j\ :\ Fin\ (n+1)\ =>\ (k\ j,v\ j))))\ let\ o\ :=\ softmaxOutput\ q\ k\ v\ let\ y\ :=\ finiteAccepted\ (sharpAccepted\ m\ q\ k\ v\ c)\ o\ D\ let\ law\ :=\ rejectionWeight\ r\ a\ D\ (\forall \ z,\ 0\ \leq \ copiesWeight\ law\ H\ z)\ \text{∧}\ Finset.sum\ Finset.univ\ (copiesWeight\ law\ H)\ =\ 1\ \text{∧}\ mean\ (copiesWeight\ law\ H)\ (average\ y\ H)\ =\ o\ \text{∧}\ mse\ (copiesWeight\ law\ H)\ (average\ y\ H)\ o\ \leq \ epsilon\^2\ \text{∧}\ mean\ (copiesWeight\ law\ H)\ (relativeQueryWork\ m\ H\ D\ R)\ \leq \ 15*(m\ :\ \text{ℝ})+8+(H\ :\ \text{ℝ})*(6*Real.exp\ R+10*(m\ :\ \text{ℝ})+22))})}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
<Less than: 0 is strictly smaller than m. (0 < m)
RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: q, R, F, epsilon range over real numbers: the statement must hold for every choice. ((q R F epsilon : ℝ))
≤At most: 0 is less than or equal to q. (0 ≤ q)
Fin: Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fin)
f(x)Function application: Fin applied to n + 1. Lean writes f x; papers write f(x). (Fin (n+1))
⟹Implies: If Fin(n + 1), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin (n+1) → ℝ)
x : TVariables: k, v range over Fin (n+1) → ℝ: the statement must hold for every choice. ((k v : Fin (n+1) → ℝ))
∀For all: The statement after the comma holds for every j. (∀ j, 0 ≤ k j ∧ k j ≤ 1)
let: let: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (let)
+Addition: n plus 1. (n+1)
∧And: Both hold: 0 ≤ k(j), and k(j) ≤ 1. (0 ≤ k j ∧ k j ≤ 1)
|x|Absolute value: The size of v(j) without its sign. (|v j|)

theorem attention-relative-tail-constructed-state-accuracy-work {n : ℕ} (m : ℕ) (hm : 0 < m) (q R F epsilon : ℝ) (hq : 0 ≤ q) (hqR : q ≤ R) (hF : 0 ≤ F) (he : 0 < epsilon) (k v : Fin (n+1) → ℝ) (hk : ∀ j, 0 ≤ k j ∧ k j ≤ 1) (hv : ∀ j, |v j| ≤ F) :
    (let D := polynomialDeadline n R
let H := relativeCopies m R F epsilon
let r := uniformRow n
let a := polynomialAccept q R k
let c := storedPolynomialControl m q (momentSums m (List.ofFn (fun j : Fin (n+1) => (k j,v j))))
let o := softmaxOutput q k v
let y := finiteAccepted (sharpAccepted m q k v c) o D
let law := rejectionWeight r a D
(∀ z, 0 ≤ copiesWeight law H z) ∧ Finset.sum Finset.univ (copiesWeight law H) = 1 ∧
mean (copiesWeight law H) (average y H) = o ∧
mse (copiesWeight law H) (average y H) o ≤ epsilon^2 ∧
mean (copiesWeight law H) (relativeQueryWork m H D R) ≤
15*(m : ℝ)+8+(H : ℝ)*(6*Real.exp R+10*(m : ℝ)+22))

Complete finite maintained original-softmax estimator with an exact relative Taylor certificate. The actual moment sums are constructed from keys and values, certificate arithmetic is charged once per query, and capped sampling, averaging and dense completion are included. Exact-real billing model; no executable RAM or floating-point claim.

How it was proved

Proved: 8 October 2026
By: Ajax
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: 21 lines of Lean

Maintained finite attention with sharp relative-tail accuracy and work

How it was proved

More proved statements