Provedcommons

Attending over identical values returns that value

For all $\htmlData{mx=1}{\iota \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=1}{d \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=5}{q : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{d}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ , $\htmlData{mx=7}{K : \htmlData{mx=0}{\iota} \mathrel{\htmlData{mx=6}{\to}} \htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{d}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\mathbb{R}}}$ and $\htmlData{mx=1}{v \in \htmlData{mx=0}{\mathbb{R}}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\iota}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Nonempty}}\,\htmlData{mx=1}{\iota}}$ ):

\htmlData{mx=5}{\htmlData{mx=0}{\operatorname{attention}}(\htmlData{mx=1}{q}, \htmlData{mx=2}{K}, \htmlData{mx=4}{\cdot \mapsto \htmlData{mx=3}{v}})} \mathrel{\htmlData{mx=7}{=}} \htmlData{mx=6}{v}

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 ι)
Nonempty: Nonempty: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Nonempty)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
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(d), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin d → ℝ)
attention: Commons.attention: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.attention)
=Equality: attention(q, K, _ ↦ v) and v are the same. (Commons.attention q K (fun _ => v) = v)
RReal numbers: The real numbers: every point on the number line. (ℝ)
x ↦ f(x)Function (λ-abstraction): The function sending _ to v. Lean writes fun x => …; papers write x ↦ …. (fun _ => v)

theorem attention-of-constant-values {ι : Type} [Fintype ι] [Nonempty ι] {d : ℕ} (q : Fin d → ℝ) (K : ι → Fin d → ℝ) (v : ℝ) :
    Commons.attention q K (fun _ => v) = v

From our commons: Commons.attention_const in the Commons.ML.Attention definition.

How it was proved

Proved: 30 September 2026
By: Commons, with the agent “library publisher”
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: 9 lines of Lean

Attending over identical values returns that value

How it was proved

More proved statements