Provedunbiased-attentionrandomized-algorithmssoftmaxaggregate
Aggregate range: log(4n² / n^{2−a}) = log 4 + a log n
For all , if , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- n, a range over real numbers: the statement must hold for every choice. (
(n a : ℝ)) - <Less than
- 0 is strictly smaller than n. (
0 < n) - logNatural logarithm
- The logarithm of 4 · n^2/n^(2 − a) to base e: the power e must be raised to to give 4 · n^2/n^(2 − a). (
Real.log (4 * n ^ (2 : ℝ) / n ^ (2 - a))) - =Equality
- log(4 · n^2/n^(2 − a)) and log(4) + a · log(n) are the same. (
Real.log (4 * n ^ (2 : ℝ) / n ^ (2 - a)…) - ·Multiplication
- 4 times n^2. (
4 * n ^ (2 : ℝ)) - a/bDivision
- 4 · n^2 divided by n^(2 − a). In Lean, dividing by 0 gives 0. (
4 * n ^ (2 : ℝ) / n ^ (2 - a)) - aᵇPower
- n raised to the power 2. (
n ^ (2 : ℝ)) - -Subtraction
- 2 minus a. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
2 - a) - +Addition
- log(4) plus a · log(n). (
Real.log 4 + a * Real.log n)
theorem ua-aggregate-range (n a : ℝ) (hn : 0 < n) :
Real.log (4 * n ^ (2 : ℝ) / n ^ (2 - a)) = Real.log 4 + a * Real.log nSo the aggregate gadget lives at score range (a ln n + ln 4)/(1−s), i.e. just above a ln n after tensoring. Part of 'Unbiased randomized attention: cost x variance thresholds', round 13 (aggregate / batch partition function).
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
- 14 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.