Provedattentionfinite-probabilityreview-v7

Mass-tree leaves return direct entry indices with the paid regional mass law

For all $\htmlData{mx=1}{n, d \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=2}{E : \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Type}} \cdot }}$ , $\htmlData{mx=3}{A, q \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Key}}\,\htmlData{mx=1}{d}}}$ , $\htmlData{mx=1}{w \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=8}{f : \htmlData{mx=5}{\htmlData{mx=0}{\operatorname{EntryIndex}}\,\htmlData{mx=1}{A}\,\htmlData{mx=2}{w}\,\htmlData{mx=3}{k}\,\htmlData{mx=4}{v}} \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{n}$ (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}{\operatorname{xs}})})(\mathtt{:=indexArray\ A\ w\ k\ v\ \ \ \ \ let\ h:=Nat.clog\ 2\ xs.size\ \ \ \ \ let\ hh:=Nat.le\_pow\_clog\ (by\ decide\ :\ 1<2)\ xs.size\ \ \ \ \ let\ t:=MassTree.build\ h\ (MassTree.arrayLeaf\ xs\ (entryMass\ A\ q\ w\ k\ v)\ h\ hh)\ \ \ \ \ (Finset.sum\ Finset.univ\ (fun\ z\ =>\ MassTree.probability\ t\ z\ *\ \ \ \ \ \ \ (match\ MassTree.returned\ t\ z\ with\ |\ none\ =>\ 0\ |\ some\ i\ =>\ f\ i)))\ =\ \ \ \ \ Finset.sum\ Finset.univ\ (fun\ i\ :\ EntryIndex\ A\ w\ k\ v\ =>\ \ \ \ \ \ \ entryMass\ A\ q\ w\ k\ v\ i\ /\ normalizer\ A\ q\ w\ k\ v\ *\ f\ i))})}

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)
·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)
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)
EntryIndex: EntryIndex: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (EntryIndex)
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)
xs: xs: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (xs)
RReal numbers: The real numbers: every point on the number line. (ℝ)

theorem attention-v8-indexed-tree-law {n d : ℕ} {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A q : Key d) (w : ℝ) (k : Fin n → Key d) (v : Fin n → E)
    (hn : 0<n) (f : EntryIndex A w k v → ℝ) :
    (let xs:=indexArray A w k v
    let h:=Nat.clog 2 xs.size
    let hh:=Nat.le_pow_clog (by decide : 1<2) xs.size
    let t:=MassTree.build h (MassTree.arrayLeaf xs (entryMass A q w k v) h hh)
    (Finset.sum Finset.univ (fun z => MassTree.probability t z *
      (match MassTree.returned t z with | none => 0 | some i => f i))) =
    Finset.sum Finset.univ (fun i : EntryIndex A w k v =>
      entryMass A q w k v i / normalizer A q w k v * f i))

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

Mass-tree leaves return direct entry indices with the paid regional mass law

How it was proved

More proved statements