Provedunbiased-attentionrandomized-algorithmssoftmaxlower-bound
Planted instance: m special keys of weight e^R (value 1) among n with m e^R ≥ n give output ≥ 1/2
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
- m, n, R range over real numbers: the statement must hold for every choice. (
(m n R : ℝ)) - <Less than
- 0 is strictly smaller than n. (
0 < n) - ≤At most
- 0 is less than or equal to m. (
0 ≤ m) - a/bDivision
- 1 divided by 2. In Lean, dividing by 0 gives 0. (
1 / 2) - ·Multiplication
- m times exp(R). (
m * Real.exp R) - eˣExponential function
- e raised to the power R, where e ≈ 2.718. (
Real.exp R) - +Addition
- m · exp(R) plus n − m. (
m * Real.exp R + (n - m)) - -Subtraction
- n minus m. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
n - m)
theorem ua-planted-output (m n R : ℝ) (hn : 0 < n) (hm : 0 ≤ m) (hmn : m ≤ n) (h : n ≤ m * Real.exp R) :
1 / 2 ≤ (m * Real.exp R) / (m * Real.exp R + (n - m))The planted world of the sampling lower bound (m = n^{1−α}, R = α ln n); the unplanted world has output 0. 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.