Proved

Finite certified attention from constructed polynomial moments

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:=polynomialCopies\ m\ R\ F\ epsilon\ \ \ \ \ let\ r:=uniformRow\ n\ \ \ \ \ let\ a:=polynomialAccept\ q\ R\ k\ \ \ \ \ let\ b:=polynomialSurrogate\ m\ q\ R\ k\ \ \ \ \ let\ U:=1+polynomialResidual\ m\ R\ \ \ \ \ let\ o:=softmaxOutput\ q\ k\ v\ \ \ \ \ let\ y:=finiteAccepted\ (scaledAccepted\ a\ b\ v\ (storedPolynomialControl\ m\ q\ \ \ \ \ \ \ (momentSums\ m\ (List.ofFn\ (fun\ j\ :\ Fin\ (n+1)\ =>\ (k\ j,v\ j)))))\ (1/U))\ o\ D\ \ \ \ \ let\ law:=rejectionWeight\ r\ a\ D\ \ \ \ \ (\forall \ z,0\leq copiesWeight\ law\ H\ z)\ \text{∧}\ (\Sigma \ z,copiesWeight\ law\ H\ z)=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)\ (polynomialQueryWork\ m\ H\ D)\leq \ \ \ \ \ \ \ 12*(m\ :\ \text{ℝ})+4+(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)
∧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|)
+Addition: n plus 1. (n+1)

theorem attention-precision-constructed-moment-state {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:=polynomialCopies m R F epsilon
    let r:=uniformRow n
    let a:=polynomialAccept q R k
    let b:=polynomialSurrogate m q R k
    let U:=1+polynomialResidual m R
    let o:=softmaxOutput q k v
    let y:=finiteAccepted (scaledAccepted a b v (storedPolynomialControl m q
      (momentSums m (List.ofFn (fun j : Fin (n+1) => (k j,v j))))) (1/U)) o D
    let law:=rejectionWeight r a D
    (∀ z,0≤copiesWeight law H z) ∧ (∑ z,copiesWeight law H z)=1 ∧
    mean (copiesWeight law H) (average y H)=o ∧
    mse (copiesWeight law H) (average y H) o≤epsilon^2 ∧
    mean (copiesWeight law H) (polynomialQueryWork m H D)≤
      12*(m : ℝ)+4+(H : ℝ)*(6*Real.exp R+10*(m : ℝ)+22))

Starts from actual key/value arrays and constructed moment state. Derives certificate, finite law, original-softmax mean, MSE, copy count, deadline and explicit charged work; exact real arithmetic.

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: 26 lines of Lean

Finite certified attention from constructed polynomial moments

How it was proved

More proved statements