Provedunbiased-gradientsimpossibilitytrainingfirst-principles

No estimator from two Bernoulli(p) samples is unbiased for p³: bounded-sample unbiased estimation of a nonlinear functional of an attention output is impossible

\htmlData{mx=37}{\lnot \htmlData{mx=36}{\exists h : \htmlData{mx=31}{\operatorname{Bool}} \mathrel{\htmlData{mx=35}{\to}} \htmlData{mx=32}{\operatorname{Bool}} \mathrel{\htmlData{mx=34}{\to}} \htmlData{mx=33}{\mathbb{R}},\ \htmlData{mx=30}{\forall p \in \htmlData{mx=29}{\mathbb{R}},\ 0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{p} \mathrel{\htmlData{mx=28}{\implies}} \htmlData{mx=2}{p} \mathrel{\htmlData{mx=3}{\leq}} 1 \mathrel{\htmlData{mx=27}{\implies}} \htmlData{mx=23}{\sum_{x \in \htmlData{mx=4}{\operatorname{Bool}}} \htmlData{mx=22}{\sum_{y \in \htmlData{mx=5}{\operatorname{Bool}}} \htmlData{mx=21}{\htmlData{mx=16}{\left(\htmlData{mx=10}{\begin{cases} \htmlData{mx=6}{p} & \text{if } \htmlData{mx=7}{x} \\ \htmlData{mx=9}{1 - \htmlData{mx=8}{p}} & \text{otherwise} \end{cases}}\right) \cdot \left(\htmlData{mx=15}{\begin{cases} \htmlData{mx=11}{p} & \text{if } \htmlData{mx=12}{y} \\ \htmlData{mx=14}{1 - \htmlData{mx=13}{p}} & \text{otherwise} \end{cases}}\right)} \cdot \htmlData{mx=20}{\htmlData{mx=17}{h}(\htmlData{mx=18}{x}, \htmlData{mx=19}{y})}}}} \mathrel{\htmlData{mx=26}{=}} \htmlData{mx=25}{\htmlData{mx=24}{p}^{3}}}}}

What the notation means · or point at any symbol

¬Not: It is not the case that ∃ h, ∀ p, 0 ≤ p → (p ≤ 1 → (∑ x, ∑ y, p if x, else 1 − p ·…. (¬ ∃ h : Bool → Bool → ℝ, ∀ p : ℝ, 0 ≤ p…)
∃There exists: At least one h makes the statement after the comma true. (∃ h : Bool → Bool → ℝ, ∀ p : ℝ, 0 ≤ p →…)
∀For all: The statement after the comma holds for every p. (∀ p : ℝ, 0 ≤ p → p ≤ 1 → ∑ x : Bool, ∑ …)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to p. (0 ≤ p)
⟹Implies: If p ≤ 1, then (∑ x, ∑ y, p if x, else 1 − p · p if y, else 1 − p · h(x, …. (Between types, A → B is the type of functions from A to B.) (p ≤ 1 → ∑ x : Bool, ∑ y : Bool, (if x t…)
=Equality: ∑ x, ∑ y, p if x, else 1 − p · p if y, else 1 − p · h(x, y) and p^3 are the same. (∑ x : Bool, ∑ y : Bool, (if x then p el…)
Bool: Bool: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Bool)
∑Summation: Add up p if x, else 1 − p · p if y, else 1 − p · h(x, y) for every y in Bool. (∑ y : Bool, (if x then p else 1 - p) * …)
·Multiplication: p if x, else 1 − p times p if y, else 1 − p. ((if x then p else 1 - p) * (if y then p…)
{ a if c; b otherwiseCases (if … then … else): p when x, and 1 − p otherwise. (if x then p else 1 - p)
-Subtraction: 1 minus p. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - p)
f(x)Function application: h applied to x, y. Lean writes f x; papers write f(x). (h x y)
aᵇPower: p raised to the power 3. (p ^ 3)

theorem ug-bounded-samples-cannot-debias-cubic :
    ¬ ∃ h : Bool → Bool → ℝ, ∀ p : ℝ, 0 ≤ p → p ≤ 1 → ∑ x : Bool, ∑ y : Bool, (if x then p else 1 - p) * (if y then p else 1 - p) * h x y = p ^ 3

For the two-key row with output o = p, any function of two exact samples has expectation that is a quadratic polynomial in p, so it cannot equal p³ for all p. Hence a nonlinear downstream loss cannot be estimated without bias from any fixed number of attention samples; a random number of samples (the randomised telescope with a dense terminal) is necessary, not merely convenient. Proof: evaluate at p = 0, 1, 1/2, 1/4 and derive a contradiction. First-principles reformulation, 2026-10-05.

How it was proved

Proved: 5 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: 17 lines of Lean

No estimator from two Bernoulli(p) samples is unbiased for p³: bounded-sample unbiased estimation of a nonlinear functional of an attention output is impossible

How it was proved

More proved statements