Provedsampleability-lawadaptive-exactnessunbiasedpitfall
Selection bias when the decision reuses the estimate's own samples: for X uniform on {0,1} (E[X] = 1/2), the output 'θ if X > θ else X' has mean 1/4
What the notation means · or point at any symbol
- ∧And
- Both hold: (∑ b, 1/2 · 1 if b, else 0) = 1/2, and (∑ b, 1/2 · 1/2 if 1 if b, else 0 > 1/2, else 1 if b, else…. (
(∑ b : Bool, (1 / 2 : ℝ) * (if b then (…) - ∑Summation
- Add up 1/2 · 1 if b, else 0 for every b in Bool. (
∑ b : Bool, (1 / 2 : ℝ) * (if b then (1…) - =Equality
- ∑ b, 1/2 · 1 if b, else 0 and 1/2 are the same. (
∑ b : Bool, (1 / 2 : ℝ) * (if b then (1…) - 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) - (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 if b, else 0. (
(1 / 2 : ℝ) * (if b then (1 : ℝ) else 0)) - a/bDivision
- 1 divided by 2. In Lean, dividing by 0 gives 0. (
1 / 2) - { a if c; b otherwiseCases (if … then … else)
- 1 when b, and 0 otherwise. (
if b then (1 : ℝ) else 0) - >Greater than
- 1 if b, else 0 is strictly larger than 1/2. (
(if b then (1 : ℝ) else 0) > 1 / 2)
theorem am-same-sample-selection-bias :
(∑ b : Bool, (1 / 2 : ℝ) * (if b then (1 : ℝ) else 0) = 1 / 2) ∧ (∑ b : Bool, (1 / 2 : ℝ) * (if (if b then (1 : ℝ) else 0) > 1 / 2 then 1 / 2 else (if b then (1 : ℝ) else 0)) = 1 / 4)Counterexample to reusing the same draws for the exact-or-sampled decision and for the estimate: the switched output is biased even though both branches are unbiased on their own. Adaptive exactness must use an independent pilot (or sample splitting). Part of 'The Sampleability Law' (adaptive exactness: deciding per (head, step) between exact and sampled attention without bias).
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
- 13 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.