No constant $K < 1$ works in all degrees

Proved

SmaleMeanValue.no_uniform_constant_below_one

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysispolynomials

For every real number $K < 1$ there exist a complex polynomial $P$ of degree at least $2$ and a point $z \in \mathbb C$ with $P'(z) \neq 0$ such that every critical point $c$ of $P$ satisfies

\left| \frac{P(z) - P(c)}{z - c} \right| > K\,|P'(z)|.

Thus no constant bound better than $K = 1$ can hold for polynomials of all degrees, which makes $K = 1$ the natural degree-independent form of the conjecture.

Preamble

import Mathlib
open Polynomial

Formal statement

namespace SmaleMeanValue

theorem no_uniform_constant_below_one (K : ℝ) (hK : K < 1) :
    ∃ P : ℂ[X], 2 ≤ P.natDegree ∧ ∃ z : ℂ, P.derivative.eval z ≠ 0 ∧
      ∀ c : ℂ, P.derivative.eval c = 0 →
        K * ‖P.derivative.eval z‖ < ‖(P.eval z - P.eval c) / (z - c)‖ := by sorry

end SmaleMeanValue

Source

Wikipedia, "Mean value problem", revision oldid=1374678764, https://en.wikipedia.org/w/index.php?title=Mean_value_problem&oldid=1374678764, lead section ("so no constant bound better than K = 1 can exist")

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; NON-BLIND

Disclosure — NOT an independent read-back. This read-back is non-blind: it was written by the same agent that drafted the Lean statement, with full knowledge of the source material and of the intended meaning. It must not be treated as independent testimony. Reviewers should compare the Lean code against the source themselves.

Let $K$ be any real number with $K < 1$ (this includes negative $K$ , for which the claim is easy). The statement asserts that there exist a complex polynomial $P$ whose (natural-number) degree is at least $2$ and a complex number $z$ with $P'(z) \neq 0$ ( $P'$ the formal derivative) such that for every complex number $c$ with $P'(c) = 0$ ,

K\,|P'(z)| < \left| \frac{P(z) - P(c)}{z - c} \right| .

The inequality is strict. Since $P'(z) \neq 0$ , every such $c$ differs from $z$ , so the quotient is a genuine difference quotient. The degree of $P$ is not fixed in advance; it may depend on $K$ .

Human review

Endorsed by Shuze Chen · Sep 30, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

No constant K<1K < 1K<1 works in all degrees

No constant $K < 1$ works in all degrees