Provedattentionfinite-probabilityvector

Constructed attention: finite vector correctness

For all $\htmlData{mx=1}{n, d \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=1}{E \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=3}{A, q \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Key}}\,\htmlData{mx=1}{d}}}$ , $\htmlData{mx=7}{k : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{n}} \mathrel{\htmlData{mx=6}{\to}} \htmlData{mx=5}{\htmlData{mx=3}{\operatorname{Key}}\,\htmlData{mx=4}{d}}}$ , $\htmlData{mx=5}{v : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{n}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{E}}$ , $\htmlData{mx=1}{F, Q, \delta, \varepsilon \in \htmlData{mx=0}{\mathbb{R}}}$ and $\htmlData{mx=1}{m \in \htmlData{mx=0}{\mathbb{N}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{n}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{d}$ , $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{F}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{Q}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\delta}$ , $\htmlData{mx=0}{\delta} \mathrel{\htmlData{mx=1}{\leq}} 1$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\varepsilon}$ , $\htmlData{mx=7}{\htmlData{mx=0}{\operatorname{sum}}(\htmlData{mx=1}{\operatorname{univ}}, \htmlData{mx=6}{i \mapsto \htmlData{mx=5}{(\htmlData{mx=4}{\htmlData{mx=2}{q}(\htmlData{mx=3}{i})})^{2}}})} \mathrel{\htmlData{mx=10}{\leq}} \htmlData{mx=9}{\htmlData{mx=8}{Q}^{2}}$ 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}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{NormedAddCommGroup}}\,\htmlData{mx=1}{E}}$ and $\htmlData{mx=3}{\htmlData{mx=0}{\operatorname{InnerProductSpace}}\,\htmlData{mx=1}{\mathbb{R}}\,\htmlData{mx=2}{E}}$ ), then

\htmlData{mx=3}{(\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{let}}(\htmlData{mx=1}{w})})(\mathtt{:=\ AttentionE2E.queryWidth\ d\ Q\ {\delta};\ (\forall \ z,0\leq AttentionE2E.queryWeight\ A\ q\ w\ k\ v\ F\ {\varepsilon}\ m\ z)\ \text{∧}\ Finset.sum\ Finset.univ\ (AttentionE2E.queryWeight\ A\ q\ w\ k\ v\ F\ {\varepsilon}\ m)=1\ \text{∧}\ AttentionE2E.mean\ (AttentionE2E.queryWeight\ A\ q\ w\ k\ v\ F\ {\varepsilon}\ m)\ (AttentionE2E.queryOutput\ A\ q\ w\ k\ v\ F\ {\varepsilon}\ m)=AttentionE2E.output\ q\ k\ v\ \text{∧}\ AttentionE2E.mse\ (AttentionE2E.queryWeight\ A\ q\ w\ k\ v\ F\ {\varepsilon}\ m)\ (AttentionE2E.queryOutput\ A\ q\ w\ k\ v\ F\ {\varepsilon}\ m)\ (AttentionE2E.output\ q\ k\ v)\leq {\varepsilon}\^2\ \text{∧}\ AttentionE2E.accuracyGate\ (AttentionE2E.queryKappa\ A\ q\ w\ k\ v\ F\ {\varepsilon})*(AttentionE2E.accuracyCopies\ (AttentionE2E.queryKappa\ A\ q\ w\ k\ v\ F\ {\varepsilon})\ :\ \text{ℝ})\leq 2*AttentionE2E.queryKappa\ A\ q\ w\ k\ v\ F\ {\varepsilon})})}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x ∈ TVariables: n, d range over natural numbers: the statement must hold for every choice. ((n d : ℕ))
Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
NormedAddCommGroup: NormedAddCommGroup: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (NormedAddCommGroup)
f(x)Function application: NormedAddCommGroup applied to E. Lean writes f x; papers write f(x). (NormedAddCommGroup E)
InnerProductSpace: InnerProductSpace: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (InnerProductSpace)
Key: AttentionE2E.Key: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (AttentionE2E.Key)
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)
⟹Implies: If Fin(n), then Key(d). (Between types, A → B is the type of functions from A to B.) (Fin n → AttentionE2E.Key d)
<Less than: 0 is strictly smaller than n. (0<n)
≤At most: 0 is less than or equal to F. (0≤F)
sum: Finset.sum: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset.sum)
∀For all: The statement after the comma holds for every j. (∀ j,‖v j‖≤F)
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)
‖v‖Norm: The length (size) of v(j). (‖v j‖)
univ: Finset.univ: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset.univ)
RReal numbers: The real numbers: every point on the number line. (ℝ)
x ↦ f(x)Function (λ-abstraction): The function sending i to q(i)^2. Lean writes fun x => …; papers write x ↦ …. (fun i => (q i)^2)
aᵇPower: q(i) raised to the power 2. ((q i)^2)

theorem attention-e2e-raw-input-vector-correctness {n d : ℕ} {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A q : AttentionE2E.Key d) (k : Fin n → AttentionE2E.Key d) (v : Fin n → E) (F Q δ ε : ℝ) (hn : 0<n) (hd : 0<d) (hF : 0≤F) (hQ : 0<Q) (hδ : 0<δ) (hδ1 : δ≤1) (hε : 0<ε) (hq : Finset.sum Finset.univ (fun i => (q i)^2)≤Q^2) (hv : ∀ j,‖v j‖≤F) (m : ℕ) :
    (let w := AttentionE2E.queryWidth d Q δ; (∀ z,0≤AttentionE2E.queryWeight A q w k v F ε m z) ∧ Finset.sum Finset.univ (AttentionE2E.queryWeight A q w k v F ε m)=1 ∧ AttentionE2E.mean (AttentionE2E.queryWeight A q w k v F ε m) (AttentionE2E.queryOutput A q w k v F ε m)=AttentionE2E.output q k v ∧ AttentionE2E.mse (AttentionE2E.queryWeight A q w k v F ε m) (AttentionE2E.queryOutput A q w k v F ε m) (AttentionE2E.output q k v)≤ε^2 ∧ AttentionE2E.accuracyGate (AttentionE2E.queryKappa A q w k v F ε)*(AttentionE2E.accuracyCopies (AttentionE2E.queryKappa A q w k v F ε) : ℝ)≤2*AttentionE2E.queryKappa A q w k v F ε)

From raw keys and bounded vector values, proves normalized finite path law, original exponential-softmax expectation and MSE using constructed grid and maintained affine moments. Exact real arithmetic. Data-structure lifecycle complexity and lower-bound transcript coupling remain separate obligations.

How it was proved

Proved: 6 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: 12 lines of Lean

Constructed attention: finite vector correctness

How it was proved

More proved statements