Provedcertified-residual-attentioncounterexamplegradient-unbiasedness

Unbiased forward and local derivative estimates need not give an unbiased dense-loss gradient

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

\htmlData{mx=4}{\htmlData{mx=3}{\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{let}}(\htmlData{mx=1}{w})}}(\mathtt{:=\ fun\ x\ =>\ if\ x\ then\ p\ else\ 1\ -\ p\ let\ v\ :\ Bool\ \to \ \text{ℝ}\ :=\ fun\ x\ =>\ if\ x\ then\ 1\ else\ 0\ let\ f\ :\ Bool\ \to \ Bool\ \to \ \text{ℝ}\ :=\ fun\ x\ y\ =>\ (v\ x\ +\ v\ y)\ /\ 2\ let\ d\ :\ Bool\ \to \ Bool\ \to \ \text{ℝ}\ :=\ fun\ x\ y\ =>\ (v\ x\ -\ v\ y)\ \^\ 2\ /\ 2\ (\forall \ x,\ 0\ \leq \ w\ x)\ \text{∧}\ (\Sigma \ x,\ w\ x\ =\ 1)\ \text{∧}\ (\Sigma \ x,\ \Sigma \ y,\ w\ x\ *\ w\ y\ *\ f\ x\ y\ =\ p)\ \text{∧}\ (\Sigma \ x,\ \Sigma \ y,\ w\ x\ *\ w\ y\ *\ d\ x\ y\ =\ p\ *\ (1\ -\ p))\ \text{∧}\ (\Sigma \ x,\ \Sigma \ y,\ w\ x\ *\ w\ y\ *\ (f\ x\ y\ *\ d\ x\ y)\ =\ p\ *\ (1\ -\ p)\ /\ 2)\ \text{∧}\ (\Sigma \ x,\ \Sigma \ y,\ \Sigma \ z,\ w\ x\ *\ w\ y\ *\ w\ z\ *\ (v\ x\ \^\ 2\ *\ d\ y\ z)\ =\ p\ \^\ 2\ *\ (1\ -\ p))\ \text{∧}\ (p\ =\ 1\ /\ 4\ \to \ (\Sigma \ x,\ \Sigma \ y,\ w\ x\ *\ w\ y\ *\ (f\ x\ y\ *\ d\ x\ y)\ =\ 3\ /\ 32)\ \text{∧}\ p\ \^\ 2\ *\ (1\ -\ p)\ =\ 3\ /\ 64\ \text{∧}\ (\Sigma \ x,\ \Sigma \ y,\ w\ x\ *\ w\ y\ *\ (f\ x\ y\ *\ d\ x\ y))\ \neq \ p\ \^\ 2\ *\ (1\ -\ p)\ \text{∧}\ (\Sigma \ x,\ \Sigma \ y,\ \Sigma \ z,\ w\ x\ *\ w\ y\ *\ w\ z\ *\ (v\ x\ \^\ 2\ *\ d\ y\ z))\ \neq \ p\ \^\ 3\ *\ (1\ -\ p)))})}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to p. (0 ≤ p)
(x : T)Type ascription: let(w) read as a Bool → ℝ. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((let w : Bool → ℝ)
let: let: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (let)
f(x)Function application: let applied to w. Lean writes f x; papers write f(x). (let w)

theorem cra-gradient-composition-counterexamples (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) :
    (let w : Bool → ℝ := fun x => if x then p else 1 - p
let v : Bool → ℝ := fun x => if x then 1 else 0
let f : Bool → Bool → ℝ := fun x y => (v x + v y) / 2
let d : Bool → Bool → ℝ := fun x y => (v x - v y) ^ 2 / 2
(∀ x, 0 ≤ w x) ∧ (∑ x, w x = 1) ∧
(∑ x, ∑ y, w x * w y * f x y = p) ∧
(∑ x, ∑ y, w x * w y * d x y = p * (1 - p)) ∧
(∑ x, ∑ y, w x * w y * (f x y * d x y) = p * (1 - p) / 2) ∧
(∑ x, ∑ y, ∑ z, w x * w y * w z * (v x ^ 2 * d y z) = p ^ 2 * (1 - p)) ∧
(p = 1 / 4 → (∑ x, ∑ y, w x * w y * (f x y * d x y) = 3 / 32) ∧ p ^ 2 * (1 - p) = 3 / 64 ∧ (∑ x, ∑ y, w x * w y * (f x y * d x y)) ≠ p ^ 2 * (1 - p) ∧ (∑ x, ∑ y, ∑ z, w x * w y * w z * (v x ^ 2 * d y z)) ≠ p ^ 3 * (1 - p)))

Exact Bernoulli finite-product expectations: same-sample product has mean p(1-p)/2 rather than p²(1-p); for an independent forward Bernoulli and derivative pair, the cubic-loss product has mean p²(1-p) rather than p³(1-p). Both inequalities hold at p=1/4. The target establishes the probability weights and all sums explicitly. Logistic loss derivatives are a separate analytic obligation.

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: 36 lines of Lean

Unbiased forward and local derivative estimates need not give an unbiased dense-loss gradient

How it was proved

More proved statements