Provedunbiased-attentionrandomized-algorithmssoftmaxhardness

Tensor powers: ⟨u^⊗k, v^⊗k⟩ = ⟨u, v⟩^k

For all $\htmlData{mx=1}{\iota \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=1}{k \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=3}{u, v : \htmlData{mx=0}{\iota} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\iota}}$ ):

\htmlData{mx=17}{\sum_{f : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{k}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\iota}} \htmlData{mx=16}{\prod_{i} \htmlData{mx=15}{\htmlData{mx=9}{\htmlData{mx=5}{u}(\htmlData{mx=8}{\htmlData{mx=6}{f}(\htmlData{mx=7}{i})})} \cdot \htmlData{mx=14}{\htmlData{mx=10}{v}(\htmlData{mx=13}{\htmlData{mx=11}{f}(\htmlData{mx=12}{i})})}}}} \mathrel{\htmlData{mx=28}{=}} \htmlData{mx=27}{\left(\htmlData{mx=25}{\sum_{j} \htmlData{mx=24}{\htmlData{mx=20}{\htmlData{mx=18}{u}(\htmlData{mx=19}{j})} \cdot \htmlData{mx=23}{\htmlData{mx=21}{v}(\htmlData{mx=22}{j})}}}\right)^{\htmlData{mx=26}{k}}}

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)
Fintype: Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype)
f(x)Function application: Fintype applied to ι. Lean writes f x; papers write f(x). (Fintype ι)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
⟹Implies: If ι, then ℝ. (Between types, A → B is the type of functions from A to B.) (ι → ℝ)
x : TVariables: u, v range over ι → ℝ: the statement must hold for every choice. ((u v : ι → ℝ))
∑Summation: Add up ∏ i, u(f(i)) · v(f(i)) for every f in Fin(k) → ι. (∑ f : Fin k → ι, ∏ i, u (f i) * v (f i))
=Equality: ∑ f, ∏ i, u(f(i)) · v(f(i)) and (∑ j, u(j) · v(j))^k are the same. (∑ f : Fin k → ι, ∏ i, u (f i) * v (f i)…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
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)
∏Product: Multiply together u(f(i)) · v(f(i)) for every i. (∏ i, u (f i) * v (f i))
·Multiplication: u(f(i)) times v(f(i)). (u (f i) * v (f i))
aᵇPower: ∑ j, u(j) · v(j) raised to the power k. ((∑ j, u j * v j) ^ k)

theorem ua-tensor-power-inner-product {ι : Type} [Fintype ι] (k : ℕ) (u v : ι → ℝ) :
    ∑ f : Fin k → ι, ∏ i, u (f i) * v (f i) = (∑ j, u j * v j) ^ k

Σ over f : Fin k → ι of ∏ u(f i)v(f i) equals (Σ u v)^k. Applied to Rubinstein's perfect-completeness / soundness-1/2 vectors, k-fold tensoring keeps YES at normalized inner product 1 and drives NO below 2^{-k}, at dimension O(log N)^k. Part of 'Unbiased randomized attention: cost x variance thresholds', round 3 (sharp threshold at score range ln n).

How it was proved

Proved: 4 October 2026
By: Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
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

Tensor powers: ⟨u^⊗k, v^⊗k⟩ = ⟨u, v⟩^k

How it was proved

More proved statements