Provedphase-diagrampolynomial-methodattentiondiagram
Polynomial-method rank: the number of monomials of degree ≤ g in D variables, choose(D+g, D), is ≤ (1 + g/D)^D (1 + D/g)^g
For all , if and , then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - x ∈ TVariables
- D, g range over natural numbers: the statement must hold for every choice. (
(D g : ℕ)) - <Less than
- 0 is strictly smaller than D. (
0 < D) - (x : T)As real numbers
- choose(D + g, D) read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(Nat.choose (D + g) D : ℝ)) - ≤At most
- choose(D + g, D) is less than or equal to (1 + g/D)^D · (1 + D/g)^g. (
(Nat.choose (D + g) D : ℝ) ≤ (1 + (g : …) - (n k)Binomial coefficient
- “D + g choose D”: the number of ways to pick D things from D + g. (
Nat.choose (D + g) D) - +Addition
- D plus g. (
D + g) - aᵇPower
- 1 + g/D raised to the power D. (
(1 + (g : ℝ) / D) ^ D) - ·Multiplication
- (1 + g/D)^D times (1 + D/g)^g. (
(1 + (g : ℝ) / D) ^ D * (1 + (D : ℝ) / …) - a/bDivision
- g divided by D. In Lean, dividing by 0 gives 0. (
(g : ℝ) / D)
theorem pd-rank-bound (D g : ℕ) (hD : 0 < D) (hg : 0 < g) :
(Nat.choose (D + g) D : ℝ) ≤ (1 + (g : ℝ) / D) ^ D * (1 + (D : ℝ) / g) ^ gWith D = 2d = 2c ln n variables and degree g = α ln n this gives rank n^{e_poly(α,c)}, e_poly = 2c ln(1+α/2c) + α ln(1+2c/α): the polynomial-method branch of the Phase-Diagram conjecture min(1+α, 1+e_poly, 2). At Baguette's head dimension 64 (c ≈ 7.7 at n = 4096) e_poly exceeds α for every α, so sampling wins. 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
- 30 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.