Provedphase-diagrampolynomial-methodattentiondiagram
Sampling wins the phase diagram whenever 2c ≥ (e−1)α: then e_poly(α, c) = 2c ln(1+α/2c) + α ln(1+2c/α) ≥ α
For all , if , and , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- α, c range over real numbers: the statement must hold for every choice. (
(α c : ℝ)) - <Less than
- 0 is strictly smaller than α. (
0 < α) - ≤At most
- 0 is less than or equal to c. (
0 ≤ c) - ·Multiplication
- exp(1) − 1 times α. (
(Real.exp 1 - 1) * α) - eˣExponential function
- e raised to the power 1, where e ≈ 2.718. (
Real.exp 1) - -Subtraction
- exp(1) minus 1. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
Real.exp 1 - 1) - logNatural logarithm
- The logarithm of 1 + α/(2 · c) to base e: the power e must be raised to to give 1 + α/(2 · c). (
Real.log (1 + α / (2 * c))) - +Addition
- 1 plus α/(2 · c). (
1 + α / (2 * c)) - a/bDivision
- α divided by 2 · c. In Lean, dividing by 0 gives 0. (
α / (2 * c))
theorem pd-sampling-wins (α c : ℝ) (hα : 0 < α) (hc : 0 ≤ c) (h : (Real.exp 1 - 1) * α ≤ 2 * c) :
α ≤ 2 * c * Real.log (1 + α / (2 * c)) + α * Real.log (1 + 2 * c / α)The polynomial-method exponent 1 + e_poly is at least the sampling exponent 1 + α as soon as the head dimension satisfies d = c ln n ≥ (e−1)α ln n / 2 ≈ 0.86·R. For Baguette (d_h = 64, n = 4096, c ≈ 7.7) this holds for every score range up to α ≈ 9, so uniform-proposal sampling dominates the polynomial method on all realistic heads. Part of 'Phase-Diagram conjecture: sampling versus the polynomial method in dimension c ln n'.
How it was proved
- Proved
- 4 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
- 24 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.