Provedattentionversion-9finite-lawconstructible-state

Direct stored channel and member positions preserve the complete finite history

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}}$ , $\htmlData{mx=6}{\mathit{accept} : \htmlData{mx=3}{\htmlData{mx=0}{\operatorname{Row}}\,\htmlData{mx=1}{d}\,\htmlData{mx=2}{E}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\mathbb{R}}}$ , $\htmlData{mx=1}{m \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=12}{f : (\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{m}} \mathrel{\htmlData{mx=9}{\to}} \htmlData{mx=8}{\htmlData{mx=6}{\htmlData{mx=3}{\operatorname{Row}}\,\htmlData{mx=4}{d}\,\htmlData{mx=5}{E}} \times \htmlData{mx=7}{\operatorname{Bool}}}) \mathrel{\htmlData{mx=11}{\to}} \htmlData{mx=10}{\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

\begin{aligned} & \left(\right. (\htmlData{mx=62}{\htmlData{mx=1}{\operatorname{sum}}(\htmlData{mx=2}{\operatorname{univ}}, \htmlData{mx=61}{z \mapsto \htmlData{mx=51}{\htmlData{mx=23}{\htmlData{mx=3}{\operatorname{rejectionWeight}}(\htmlData{mx=10}{\htmlData{mx=4}{\operatorname{indexedChannelWeight}}(\htmlData{mx=5}{A}, \htmlData{mx=6}{q}, \htmlData{mx=7}{w}, \htmlData{mx=8}{k}, \htmlData{mx=9}{v})}, \htmlData{mx=20}{j \mapsto \htmlData{mx=19}{\htmlData{mx=11}{\mathit{accept}}(\htmlData{mx=18}{\htmlData{mx=12}{\operatorname{indexedRow}}(\htmlData{mx=13}{A}, \htmlData{mx=14}{w}, \htmlData{mx=15}{k}, \htmlData{mx=16}{v}, \htmlData{mx=17}{j_{2}})})}}, \htmlData{mx=21}{m}, \htmlData{mx=22}{z})} \cdot \htmlData{mx=50}{\htmlData{mx=24}{f}(\htmlData{mx=49}{i \mapsto \htmlData{mx=48}{\left( \htmlData{mx=43}{\operatorname{1.2}\left(\htmlData{mx=42}{\htmlData{mx=34}{\operatorname{indexedRow}}(\htmlData{mx=35}{A}, \htmlData{mx=36}{w}, \htmlData{mx=37}{k}, \htmlData{mx=38}{v}, \htmlData{mx=41}{\htmlData{mx=39}{z}(\htmlData{mx=40}{i})})}\right)}, \htmlData{mx=47}{\htmlData{mx=46}{\htmlData{mx=44}{z}(\htmlData{mx=45}{i})}_{2}} \right)}})}}})}) \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=124}{\htmlData{mx=63}{\operatorname{sum}}(\htmlData{mx=64}{\operatorname{univ}}, \htmlData{mx=123}{z \mapsto \htmlData{mx=116}{\htmlData{mx=94}{\htmlData{mx=65}{\operatorname{rejectionWeight}}(\htmlData{mx=80}{\htmlData{mx=66}{\operatorname{surrogateProposal}}(\htmlData{mx=73}{\htmlData{mx=67}{\operatorname{reference}}(\htmlData{mx=68}{A}, \htmlData{mx=69}{q}, \htmlData{mx=70}{w}, \htmlData{mx=71}{k}, \htmlData{mx=72}{v})}, \htmlData{mx=79}{\htmlData{mx=74}{\operatorname{surrogate}}(\htmlData{mx=75}{A}, \htmlData{mx=76}{q}, \htmlData{mx=77}{w}, \htmlData{mx=78}{k})})}, \htmlData{mx=91}{j \mapsto \htmlData{mx=90}{\htmlData{mx=81}{\mathit{accept}}(\htmlData{mx=89}{\htmlData{mx=88}{\left\langle \htmlData{mx=84}{\htmlData{mx=82}{k}(\htmlData{mx=83}{j})}, \htmlData{mx=87}{\htmlData{mx=85}{v}(\htmlData{mx=86}{j})} \right\rangle}})}}, \htmlData{mx=92}{m}, \htmlData{mx=93}{z})} \cdot \htmlData{mx=115}{\htmlData{mx=95}{f}(\htmlData{mx=114}{i \mapsto \htmlData{mx=113}{\left( \htmlData{mx=108}{\left\langle \htmlData{mx=101}{\htmlData{mx=100}{\htmlData{mx=96}{k}(\htmlData{mx=99}{\htmlData{mx=97}{z}(\htmlData{mx=98}{i})})}_{1}}, \htmlData{mx=107}{\htmlData{mx=106}{\htmlData{mx=102}{v}(\htmlData{mx=105}{\htmlData{mx=103}{z}(\htmlData{mx=104}{i})})}_{1}} \right\rangle}, \htmlData{mx=112}{\htmlData{mx=111}{\htmlData{mx=109}{z}(\htmlData{mx=110}{i})}_{2}} \right)}})}}})} \left.\right) \end{aligned}

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)
Row: Row: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Row)
=Equality: sum(univ, z ↦ rejectionWeight(indexedChannelWeight(A, q, w… and sum(univ, z ↦ rejectionWeight(surrogateProposal(reference(… are the same. ((Finset.sum Finset.univ (fun z : Path (…)
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)
×Product: Pairs of an element of Row(d, E) and an element of Bool. (Row d E × Bool)
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. (ℝ)
Bool: Bool: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Bool)
Path: Path: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Path)
ChannelDraw: ChannelDraw: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (ChannelDraw)
rejectionWeight: rejectionWeight: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (rejectionWeight)
indexedChannelWeight: indexedChannelWeight: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (indexedChannelWeight)
x ↦ f(x)Function (λ-abstraction): The function sending j to accept(indexedRow(A, w, k, v, j.2)). Lean writes fun x => …; papers write x ↦ …. (fun j => accept (indexedRow A w k v j.2))
indexedRow: indexedRow: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (indexedRow)
p₁Component: The second component of the pair j. (j.2)
(a, b)Tuple: The ordered pair (or tuple) of 1.2(indexedRow(A, w, k, v, z(i))), z(i).2. ((indexedRow A w k v (z i).1.2,(z i).2))
e.f1.2: 1.2 of indexedRow(A, w, k, v, z(i)): Lean's dot notation e.1.2 means 1.2 applied to e. (indexedRow A w k v (z i).1.2)
surrogateProposal: surrogateProposal: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (surrogateProposal)
reference: reference: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (reference)
surrogate: surrogate: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (surrogate)
(x : T)Type ascription: ⟨k(j), v(j)⟩ read as a Row(d, E). Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((⟨k j,v j⟩ : Row d E))
⟨a, b⟩Anonymous constructor: Builds a structure (a pair, a subtype element, …) from k(j), v(j). (⟨k j,v j⟩)

theorem attention-v9-indexed-channel-history {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) (accept : Row d E → ℝ)
    (m : ℕ) (f : (Fin m → Row d E × Bool) → ℝ) :
    (    (Finset.sum Finset.univ (fun z : Path (ChannelDraw A w k v) m =>
      rejectionWeight (indexedChannelWeight A q w k v)
        (fun j => accept (indexedRow A w k v j.2)) m z *
      f (fun i => (indexedRow A w k v (z i).1.2,(z i).2)))) =
    Finset.sum Finset.univ (fun z : Path (Fin n) m =>
      rejectionWeight (surrogateProposal (reference A q w k v) (surrogate A q w k))
        (fun j => accept (⟨k j,v j⟩ : Row d E)) m z *
      f (fun i => (⟨k (z i).1,v (z i).1⟩,(z i).2))))

Version 9 exact frozen target. Proof references the validated additive definition library. This mathematical finite-law/invariant target does not certify compiled Rust RAM runtime or the general linear-summary LP bridge.

How it was proved

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

Direct stored channel and member positions preserve the complete finite history

How it was proved

More proved statements