Provedphase-diagrampolynomial-methodattentiondiagram
e_poly(x, c) = 2c·log(1 + x/2c) + x·log(1 + 2c/x) is increasing in x > 0
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, x, y range over real numbers: the statement must hold for every choice. (
(c x y : ℝ)) - <Less than
- 0 is strictly smaller than c. (
0 < c) - ≤At most
- x is less than or equal to y. (
x ≤ y) - ·Multiplication
- 2 times c. (
2 * c) - logNatural logarithm
- The logarithm of 1 + x/(2 · c) to base e: the power e must be raised to to give 1 + x/(2 · c). (
Real.log (1 + x / (2 * c))) - +Addition
- 1 plus x/(2 · c). (
1 + x / (2 * c)) - a/bDivision
- x divided by 2 · c. In Lean, dividing by 0 gives 0. (
x / (2 * c))
theorem pd-epoly-mono (c x y : ℝ) (hc : 0 < c) (hx : 0 < x) (hxy : x ≤ y) :
2 * c * Real.log (1 + x / (2 * c)) + x * Real.log (1 + 2 * c / x) ≤ 2 * c * Real.log (1 + y / (2 * c)) + y * Real.log (1 + 2 * c / y)Makes the Phase-Diagram formula a proven lower bound on the polynomial-method exponent: the true Taylor degree is κ(α)·α·ln n with κ ≥ e (the self-correction of the conjecture), and since e_poly is monotone, evaluating it at κα only raises the exponent. Proof via log u ≤ u − 1 applied twice (chord bounds), no calculus. 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
- 57 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.