Provedunbiased-attentionrandomized-algorithmssoftmaxgradient-hardness
Isolated YES row: e^β ≤ S ≤ (9/8)e^β ⇒ o(1 − o) ≥ 72/289
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 range over real numbers: the statement must hold for every choice. (
(S E : ℝ)) - <Less than
- 0 is strictly smaller than E. (
0 < E) - ≤At most
- E is less than or equal to S. (
E ≤ S) - a/bDivision
- 9 divided by 8. In Lean, dividing by 0 gives 0. (
9 / 8) - ·Multiplication
- 9/8 times E. (
9 / 8 * E) - +Addition
- E plus S. (
E + S) - -Subtraction
- 1 minus S/(E + S). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - S / (E + S))
theorem ua-gradient-gadget-yes (S E : ℝ) (hE : 0 < E) (h1 : E ≤ S) (h2 : S ≤ 9 / 8 * E) :
72 / 289 ≤ (S / (E + S)) * (1 - S / (E + S))A row with exactly one partner (score β) plus far keys of total mass ≤ e^β/8 has o ∈ [1/2, 9/17], so its gradient coordinate is ≥ 72/289 ≈ 0.249. Part of 'Unbiased randomized attention: cost x variance thresholds', round 7 (gradient hardness via isolation).
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.