proofs
Provedattentiongradientcounterexample

At p = 1/4 the reused estimator expectation is twice the dense gradient

(12⋅(14)⋅(34)=332)∧(142⋅(34)=364)∧(332≠364)\begin{aligned} & \left(\htmlData{mx=6}{\htmlData{mx=4}{\htmlData{mx=2}{\htmlData{mx=1}{\frac{1}{2}}} \cdot \left(\htmlData{mx=3}{\frac{1}{4}}\right)} \cdot \left(\htmlData{mx=5}{\frac{3}{4}}\right)} \mathrel{\htmlData{mx=8}{=}} \htmlData{mx=7}{\frac{3}{32}}\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=13}{\htmlData{mx=11}{\htmlData{mx=10}{\htmlData{mx=9}{\frac{1}{4}}}^{2}} \cdot \left(\htmlData{mx=12}{\frac{3}{4}}\right)} \mathrel{\htmlData{mx=15}{=}} \htmlData{mx=14}{\frac{3}{64}}\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=17}{\htmlData{mx=16}{\frac{3}{32}}} \mathrel{\htmlData{mx=19}{\neq}} \htmlData{mx=18}{\frac{3}{64}}\right) \end{aligned}
What the notation means · or point at any symbol
(x : T)As real numbers
1/2 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((1 / 2 : ℝ))
·Multiplication
1/2 times 1/4. ((1 / 2 : ℝ) * (1 / 4))
=Equality
1/2 · (1/4) · (3/4) and 3/32 are the same. ((1 / 2 : ℝ) * (1 / 4) * (3 / 4) = 3 / 32)
a/bDivision
1 divided by 2. In Lean, dividing by 0 gives 0. (1 / 2)
∧And
Both hold: (1/4)^2 · (3/4) = 3/64, and 3/32 ≠ 3/64. ((((1 / 4 : ℝ) ^ 2) * (3 / 4) = 3 / 64) …)
aᵇPower
1/4 raised to the power 2. ((1 / 4 : ℝ) ^ 2)
≠Not equal
3/32 and 3/64 are different. ((3 / 32 : ℝ) ≠ 3 / 64)

Concrete arithmetic witness for the two-key squared-loss counterexample: reused expected term = 3/32 while dense gradient = 3/64.

How it was proved

Proved
5 October 2026
By
Ajax
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
9 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements