Provedunbiased-attentiongradient-hardnesssampler-lower-bound
Plant tuning: m e^R = n − m gives plant mass exactly 1/2, so the gradient gap is 1/4 at range R = ln((n−m)/m) = α ln n (1+o(1)) for m = n^{1−α}
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 m. (
0 < m) - ·Multiplication
- m times exp(R). (
m * Real.exp R) - =Equality
- m · exp(R) and n − m are the same. (
m * Real.exp R = n - m) - a/bDivision
- m · exp(R) divided by m · exp(R) + (n − m). In Lean, dividing by 0 gives 0. (
(m * Real.exp R) / (m * Real.exp R + (n…) - eˣExponential function
- e raised to the power R, where e ≈ 2.718. (
Real.exp R) - -Subtraction
- n minus m. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
n - m) - +Addition
- m · exp(R) plus n − m. (
m * Real.exp R + (n - m))
theorem ug-plant-half (m n R : ℝ) (hm : 0 < m) (h : m * Real.exp R = n - m) :
(m * Real.exp R) / (m * Real.exp R + (n - m)) = 1 / 2The gradient lower bound lives at the same score range as the forward threshold. Part of 'Unbiased randomized attention: cost x variance thresholds', gradient-hardness round: the unconditional sampler lower bound transferred to the query gradient.
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.