Provedunbiased-attentionrandomized-algorithmssoftmaxhardness
Padding keeps NO: if real plus padding mass is ≤ e^β/4 the output stays ≤ 1/4
For all , if , , , and , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- S, E, P, w range over real numbers: the statement must hold for every choice. (
(S E P w : ℝ)) - <Less than
- 0 is strictly smaller than E. (
0 < E) - ≤At most
- 0 is less than or equal to S. (
0 ≤ S) - +Addition
- S plus P · w. (
S + P * w) - ·Multiplication
- P times w. (
P * w) - a/bDivision
- E divided by 4. In Lean, dividing by 0 gives 0. (
E / 4)
theorem ua-padding-preserves-no (S E P w : ℝ) (hE : 0 < E) (hS : 0 ≤ S) (hP : 0 ≤ P) (hw : 0 ≤ w) (h : S + P * w ≤ E / 4) :
(S + P * w) / (E + (S + P * w)) ≤ 1 / 4With n counting all keys including padding, the far-mass bound covers padding at score 0 ≤ βs. Part of 'Unbiased randomized attention: cost x variance thresholds', round 9 (true derivative, whole-instance reduction, compositions).
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
- 13 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.