Provedunbiased-attentiongradient-hardnesssampler-lower-bound

The planted gradient gap p(1 − p) is at least 3/16 for plant mass p ∈ [1/2, 3/4]

For all $\htmlData{mx=1}{p \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=0}{\frac{1}{2}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{p}$ and $\htmlData{mx=0}{p} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\frac{3}{4}}$ , then

\htmlData{mx=0}{\frac{3}{16}} \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{\htmlData{mx=1}{p} \cdot (\htmlData{mx=3}{1 - \htmlData{mx=2}{p}})}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
a/bDivision: 1 divided by 2. In Lean, dividing by 0 gives 0. (1 / 2)
≤At most: 1/2 is less than or equal to p. (1 / 2 ≤ p)
·Multiplication: p times 1 − p. (p * (1 - p))
-Subtraction: 1 minus p. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - p)

theorem ug-gradient-gap-bound (p : ℝ) (h1 : 1 / 2 ≤ p) (h2 : p ≤ 3 / 4) :
    3 / 16 ≤ p * (1 - p)

Quantifies the gap used in the unconditional gradient-sampler lower bound. 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: 10 lines of Lean

The planted gradient gap p(1 − p) is at least 3/16 for plant mass p ∈ [1/2, 3/4]

How it was proved

More proved statements