Provedalphabaguettealgorithm-ideaa2

A position-only causal softmax head is a causal convolution divided by a prefix normalizer

For all $\htmlData{mx=3}{a, v : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{i \in \htmlData{mx=0}{\mathbb{N}}}$ :

\begin{aligned} & \htmlData{mx=23}{\sum_{j=0}^{\htmlData{mx=2}{\htmlData{mx=1}{i} + 1} - 1} \htmlData{mx=22}{\htmlData{mx=18}{\frac{\htmlData{mx=8}{e^{\htmlData{mx=7}{\htmlData{mx=3}{a}(\htmlData{mx=6}{\htmlData{mx=4}{i} - \htmlData{mx=5}{j}})}}}}{\htmlData{mx=17}{\sum_{j'=0}^{\htmlData{mx=10}{\htmlData{mx=9}{i} + 1} - 1} \htmlData{mx=16}{e^{\htmlData{mx=15}{\htmlData{mx=11}{a}(\htmlData{mx=14}{\htmlData{mx=12}{i} - \htmlData{mx=13}{j'}})}}}}}} \cdot \htmlData{mx=21}{\htmlData{mx=19}{v}(\htmlData{mx=20}{j})}}} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=44}{\frac{\htmlData{mx=36}{\sum_{d=0}^{\htmlData{mx=25}{\htmlData{mx=24}{i} + 1} - 1} \htmlData{mx=35}{\htmlData{mx=29}{e^{\htmlData{mx=28}{\htmlData{mx=26}{a}(\htmlData{mx=27}{d})}}} \cdot \htmlData{mx=34}{\htmlData{mx=30}{v}(\htmlData{mx=33}{\htmlData{mx=31}{i} - \htmlData{mx=32}{d}})}}}}{\htmlData{mx=43}{\sum_{d=0}^{\htmlData{mx=38}{\htmlData{mx=37}{i} + 1} - 1} \htmlData{mx=42}{e^{\htmlData{mx=41}{\htmlData{mx=39}{a}(\htmlData{mx=40}{d})}}}}}} \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. (ℕ)
⟹Implies: If ℕ, then ℝ. (Between types, A → B is the type of functions from A to B.) (ℕ → ℝ)
x : TVariables: a, v range over ℕ → ℝ: the statement must hold for every choice. ((a v : ℕ → ℝ))
=Equality: ∑ j, exp(a(i − j))/(∑ j', exp(a(i − j'))) · v(j) and (∑ d, exp(a(d)) · v(i − d))/(∑ d, exp(a(d))) are the same. (∑ j ∈ Finset.range (i + 1), Real.exp (a…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
+Addition: i plus 1. (i + 1)
eˣExponential function: e raised to the power a(i − j), where e ≈ 2.718. (Real.exp (a (i - j)))
a/bDivision: exp(a(i − j)) divided by ∑ j', exp(a(i − j')). In Lean, dividing by 0 gives 0. (Real.exp (a (i - j)) / (∑ j' ∈ Finset.r…)
·Multiplication: exp(a(i − j))/(∑ j', exp(a(i − j'))) times v(j). (Real.exp (a (i - j)) / (∑ j' ∈ Finset.r…)
f(x)Function application: a applied to i − j. Lean writes f x; papers write f(x). (a (i - j))
-Subtraction: i minus j. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (i - j)
∑Summation: Add up exp(a(i − j')) for j' = 0, 1, …, i + 1 − 1. (∑ j' ∈ Finset.range (i + 1), Real.exp (…)

theorem pos-head-is-causal-convolution (a v : ℕ → ℝ) (i : ℕ) :
    ∑ j ∈ Finset.range (i + 1), Real.exp (a (i - j)) / (∑ j' ∈ Finset.range (i + 1), Real.exp (a (i - j'))) * v j = (∑ d ∈ Finset.range (i + 1), Real.exp (a d) * v (i - d)) / ∑ d ∈ Finset.range (i + 1), Real.exp (a d)

Idea A2 (positional heads become convolutions). If a head's score for query i and key j depends only on i − j (score a(i−j)), its causal softmax output at position i equals (Σ_{d≤i} e^{a(d)} v_{i−d}) / (Σ_{d≤i} e^{a(d)}): an exact causal convolution of the values with kernel e^{a}, divided by a prefix sum of the kernel. One value channel is shown; channels are independent.

How it was proved

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

A position-only causal softmax head is a causal convolution divided by a prefix normalizer

How it was proved

More proved statements