Provedunbiased-attentionchi-squarerejectionreview-response
Second-moment cost and rejection envelope separate: π = (1/M, 1−1/M), r = (1/M², 1−1/M²) has C = Σπ²/r = 2M/(M+1) < 2 but max π/r = M
For all , if , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - <Less than
- 1 is strictly smaller than M. (
1 < M) - a/bDivision
- 1 divided by M^2. In Lean, dividing by 0 gives 0. (
1 / M ^ 2) - +Addition
- 1/M^2 plus 1 − 1/M^2. (
1 / M ^ 2 + (1 - 1 / M ^ 2)) - =Equality
- 1/M^2 + (1 − 1/M^2) and 1 are the same. (
1 / M ^ 2 + (1 - 1 / M ^ 2) = 1) - aᵇPower
- M raised to the power 2. (
M ^ 2) - -Subtraction
- 1 minus 1/M^2. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - 1 / M ^ 2) - ·Multiplication
- 2 times M. (
2 * M) - ∧And
- Both hold: 1/M/(1/M^2) = M, and (1 − 1/M)/(1 − 1/M^2) ≤ M. (
(1 / M) / (1 / M ^ 2) = M ∧ (1 - 1 / M)…) - ≤At most
- (1 − 1/M)/(1 − 1/M^2) is less than or equal to M. (
(1 - 1 / M) / (1 - 1 / M ^ 2) ≤ M)
theorem cv-second-moment-vs-envelope-separation (M : ℝ) (hM : 1 < M) :
(1 / M ^ 2 + (1 - 1 / M ^ 2) = 1) ∧ (1 / M + (1 - 1 / M) = 1) ∧ (1 / M) ^ 2 / (1 / M ^ 2) + (1 - 1 / M) ^ 2 / (1 - 1 / M ^ 2) = 2 * M / (M + 1) ∧ 2 * M / (M + 1) < 2 ∧ (1 / M) / (1 / M ^ 2) = M ∧ (1 - 1 / M) / (1 - 1 / M ^ 2) ≤ MThe importance-sampling cost factor C and the rejection envelope K = max π/r measure different things and can differ arbitrarily: here C < 2 for every M > 1 while rejection from r with its optimal fixed envelope needs M proposals per accepted sample. Raised in an external review (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
- 31 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.