Provedattentionfinite-probabilityreview-v7

Finite geometric accepted control with exact softmax mean and vector bounds

For all $\htmlData{mx=2}{E : \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Type}} \cdot }}$ , $\htmlData{mx=1}{n, d \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=3}{A, q \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Key}}\,\htmlData{mx=1}{d}}}$ , $\htmlData{mx=1}{w, F \in \htmlData{mx=0}{\mathbb{R}}}$ , $\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}}$ 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}{w}$ , $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{F}$ 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}{r})})(\mathtt{:=reference\ A\ q\ w\ k\ v\ \ \ \ \ let\ a:=relative\ A\ q\ w\ k\ \ \ \ \ let\ b:=surrogate\ A\ q\ w\ k\ \ \ \ \ let\ c:=controlC\ A\ q\ w\ k\ v\ \ \ \ \ let\ y:=finiteAccepted\ (accepted\ a\ b\ v\ c)\ (output\ q\ k\ v)\ m\ \ \ \ \ let\ law:=rejectionWeight\ r\ a\ m\ \ \ \ \ mean\ law\ y=output\ q\ k\ v\ \text{∧}\ \ \ \ \ mse\ law\ y\ (output\ q\ k\ v)\leq F\^2*(Real.exp\ (delta\ q\ w)*(delta\ q\ w)\^2/8)\^2\ \text{∧}\ \ \ \ \ (\forall \ f,\| y\ f-c\| \leq 2*F*(Real.exp\ (delta\ q\ w)*(delta\ q\ w)\^2/8))\ \text{∧}\ \ \ \ \ mean\ law\ (keyReads\ m)=(1-(1-scalarMean\ r\ a)\^m)/scalarMean\ r\ a\ \text{∧}\ \ \ \ \ mean\ law\ (valueReads\ m)=1-(1-scalarMean\ r\ a)\^m\ \text{∧}\ \ \ \ \ mean\ law\ (denseEvent\ m)=(1-scalarMean\ r\ a)\^m)})}

What the notation means · or point at any symbol

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)
·Multiplication: Type times . (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)
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 : ℕ))
Key: Key: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (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 → Key d)
<Less than: 0 is strictly smaller than n. (0<n)
≤At most: 0 is less than or equal to F. (0≤F)
∀For all: The statement after the comma holds for every j. (∀ j,‖v j‖≤F)
‖v‖Norm: The length (size) of v(j). (‖v j‖)
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)
RReal numbers: The real numbers: every point on the number line. (ℝ)

theorem attention-v8-geometric-accepted-control {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n d : ℕ} (A q : Key d) (w F : ℝ)
    (k : Fin n → Key d) (v : Fin n → E) (hn : 0<n) (hw : 0<w)
    (hF : 0≤F) (hv : ∀ j,‖v j‖≤F) (m : ℕ) :
    (    let r:=reference A q w k v
    let a:=relative A q w k
    let b:=surrogate A q w k
    let c:=controlC A q w k v
    let y:=finiteAccepted (accepted a b v c) (output q k v) m
    let law:=rejectionWeight r a m
    mean law y=output q k v ∧
    mse law y (output q k v)≤F^2*(Real.exp (delta q w)*(delta q w)^2/8)^2 ∧
    (∀ f,‖y f-c‖≤2*F*(Real.exp (delta q w)*(delta q w)^2/8)) ∧
    mean law (keyReads m)=(1-(1-scalarMean r a)^m)/scalarMean r a ∧
    mean law (valueReads m)=1-(1-scalarMean r a)^m ∧
    mean law (denseEvent m)=(1-scalarMean r a)^m)

Exact finite formal target reconstructed from the supplied version-7 review. Proof resides in the pinned additive library. Standard Lean axioms only. Does not certify floating-point implementation, full RAM runtime, weighted adaptive frontier, or unrestricted attention hardness.

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

Finite geometric accepted control with exact softmax mean and vector bounds

How it was proved

More proved statements