Provedhashingcounterexamplereview-response
Counterexample: buckets {1} and {1,2} (each w.p. 1/2) have inclusion probabilities (1, 1/2) = √(1, 1/4), yet uniform-in-bucket sampling returns key 1 w.p. 3/4, not 2/3
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. (
(1 / 2 : ℝ) * 1) - +Addition
- 1/2 · 1 plus 1/2 · (1/2). (
(1 / 2 : ℝ) * 1 + (1 / 2) * (1 / 2)) - =Equality
- 1/2 · 1 + 1/2 · (1/2) and 3/4 are the same. (
(1 / 2 : ℝ) * 1 + (1 / 2) * (1 / 2) = 3…) - a/bDivision
- 1 divided by 2. In Lean, dividing by 0 gives 0. (
1 / 2) - ≠Not equal
- 3/4 and 2/3 are different. (
(3 / 4 : ℝ) ≠ 2 / 3) - √Square root
- The non-negative number whose square is 1. (
Real.sqrt 1) - ∧And
- Both hold: √(1) = 1, and √(1/4) = 1/2. (
Real.sqrt 1 = (1 : ℝ) ∧ Real.sqrt (1 / …)
theorem hbe-bucket-sampling-is-not-inclusion-proposal :
((1 / 2 : ℝ) * 1 + (1 / 2) * (1 / 2) = 3 / 4) ∧ ((1 : ℝ) / (1 + 1 / 2) = 2 / 3) ∧ ((3 / 4 : ℝ) ≠ 2 / 3) ∧ (Real.sqrt 1 = (1 : ℝ) ∧ Real.sqrt (1 / 4) = (1 / 2 : ℝ))Machine-checked instance of the external reviewer's point (2026-10-05): the sampled index of a hashing-based estimator (random bucket, then a uniform element of it) does not follow the proposal proportional to inclusion probabilities. So 'hashing samples from r ∝ √π' is false as stated; the hashing-to-attention transfer must analyse the actual bucket estimator and its correction weights.
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
- 12 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.