Provedbi-cover-lawtraining-attentionclustered-attentionlaw

Two-level proposal: cluster c w.p. ∝ m_c e^{u_c}, then uniform inside, gives key j probability softmax(u_{c(j)})

For all $\htmlData{mx=1}{n, M \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=7}{\mathit{cl} : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{n}} \mathrel{\htmlData{mx=6}{\to}} \htmlData{mx=5}{\htmlData{mx=3}{\operatorname{Fin}}\,\htmlData{mx=4}{M}}}$ , $\htmlData{mx=5}{u : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{M}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ and $\htmlData{mx=3}{j \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{n}}}$ , if $0 \mathrel{\htmlData{mx=22}{<}} \htmlData{mx=21}{\htmlData{mx=20}{\lvert \htmlData{mx=19}{\htmlData{mx=10}{\operatorname{filter}}(\htmlData{mx=18}{i \mapsto \htmlData{mx=13}{\htmlData{mx=11}{\mathit{cl}}(\htmlData{mx=12}{i})} \mathrel{\htmlData{mx=17}{=}} \htmlData{mx=16}{\htmlData{mx=14}{\mathit{cl}}(\htmlData{mx=15}{j})}})} \rvert}}$ , then

\begin{aligned} & \htmlData{mx=77}{\htmlData{mx=53}{\frac{\htmlData{mx=28}{\htmlData{mx=21}{\lvert \htmlData{mx=20}{\htmlData{mx=11}{\operatorname{filter}}(\htmlData{mx=19}{i \mapsto \htmlData{mx=14}{\htmlData{mx=12}{\mathit{cl}}(\htmlData{mx=13}{i})} \mathrel{\htmlData{mx=18}{=}} \htmlData{mx=17}{\htmlData{mx=15}{\mathit{cl}}(\htmlData{mx=16}{j})}})} \rvert} \cdot \htmlData{mx=27}{e^{\htmlData{mx=26}{\htmlData{mx=22}{u}(\htmlData{mx=25}{\htmlData{mx=23}{\mathit{cl}}(\htmlData{mx=24}{j})})}}}}}{\htmlData{mx=52}{\sum_{c} \htmlData{mx=51}{\htmlData{mx=46}{\htmlData{mx=45}{\lvert \htmlData{mx=44}{\htmlData{mx=37}{\operatorname{filter}}(\htmlData{mx=43}{i \mapsto \htmlData{mx=40}{\htmlData{mx=38}{\mathit{cl}}(\htmlData{mx=39}{i})} \mathrel{\htmlData{mx=42}{=}} \htmlData{mx=41}{c}})} \rvert}} \cdot \htmlData{mx=50}{e^{\htmlData{mx=49}{\htmlData{mx=47}{u}(\htmlData{mx=48}{c})}}}}}}} \cdot \left(\htmlData{mx=76}{\frac{1}{\htmlData{mx=75}{\htmlData{mx=74}{\lvert \htmlData{mx=73}{\htmlData{mx=64}{\operatorname{filter}}(\htmlData{mx=72}{i \mapsto \htmlData{mx=67}{\htmlData{mx=65}{\mathit{cl}}(\htmlData{mx=66}{i})} \mathrel{\htmlData{mx=71}{=}} \htmlData{mx=70}{\htmlData{mx=68}{\mathit{cl}}(\htmlData{mx=69}{j})}})} \rvert}}}}\right)} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=91}{\frac{\htmlData{mx=83}{e^{\htmlData{mx=82}{\htmlData{mx=78}{u}(\htmlData{mx=81}{\htmlData{mx=79}{\mathit{cl}}(\htmlData{mx=80}{j})})}}}}{\htmlData{mx=90}{\sum_{i} \htmlData{mx=89}{e^{\htmlData{mx=88}{\htmlData{mx=84}{u}(\htmlData{mx=87}{\htmlData{mx=85}{\mathit{cl}}(\htmlData{mx=86}{i})})}}}}}} \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, M range over natural numbers: the statement must hold for every choice. ((n M : ℕ))
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)
f(x)Function application: Fin applied to n. Lean writes f x; papers write f(x). (Fin n)
⟹Implies: If Fin(n), then Fin(M). (Between types, A → B is the type of functions from A to B.) (Fin n → Fin M)
<Less than: 0 is strictly smaller than card(filter(i ↦ cl(i) = cl(j))). (0 < ((Finset.univ.filter (fun i => cl i…)
·Multiplication: card(filter(i ↦ cl(i) = cl(j))) times exp(u(cl(j))). ((Finset.univ.filter (fun i => cl i = cl…)
a/bDivision: card(filter(i ↦ cl(i) = cl(j))) · exp(u(cl(j))) divided by ∑ c, card(filter(i ↦ cl(i) = c)) · exp(u(c)). In Lean, dividing by 0 gives 0. ((Finset.univ.filter (fun i => cl i = cl…)
(x : T)As real numbers: card(filter(i ↦ cl(i) = cl(j))) read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (((Finset.univ.filter (fun i => cl i = c…)
|s|Cardinality: The number of elements of filter(i ↦ cl(i) = cl(j)). ((Finset.univ.filter (fun i => cl i = cl…)
filter: Finset.univ.filter: 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.filter)
RReal numbers: The real numbers: every point on the number line. (ℝ)
x ↦ f(x)Function (λ-abstraction): The function sending i to cl(i) = cl(j). Lean writes fun x => …; papers write x ↦ …. (fun i => cl i = cl j)
=Equality: cl(i) and cl(j) are the same. (cl i = cl j)
eˣExponential function: e raised to the power u(cl(j)), where e ≈ 2.718. (Real.exp (u (cl j)))
∑Summation: Add up card(filter(i ↦ cl(i) = c)) · exp(u(c)) for every c. (∑ c, ((Finset.univ.filter (fun i => cl …)

theorem bc-two-level-proposal {n M : ℕ} (cl : Fin n → Fin M) (u : Fin M → ℝ) (j : Fin n) (hm : 0 < ((Finset.univ.filter (fun i => cl i = cl j)).card : ℝ)) :
    ((Finset.univ.filter (fun i => cl i = cl j)).card * Real.exp (u (cl j)) / ∑ c, ((Finset.univ.filter (fun i => cl i = c)).card : ℝ) * Real.exp (u c)) * (1 / ((Finset.univ.filter (fun i => cl i = cl j)).card : ℝ)) = Real.exp (u (cl j)) / ∑ i, Real.exp (u (cl i))

The N_q × M_k centre-to-centre table plus cluster sizes defines, for every query, a proposal that is a softmax over centre scores, i.e. exactly the snapshot form required by the exact rejection lemma. Cost per draw O(1) after an alias table over M_k clusters. Part of 'Bi-Cover Law: exact, unbiased clustered attention for training'.

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

Two-level proposal: cluster c w.p. ∝ m_c e^{u_c}, then uniform inside, gives key j probability softmax(u_{c(j)})

How it was proved

More proved statements