The Kung-Traub conjecture asserts that a deterministic stationary root-finding algorithm without memory using at most 
scalar function or derivative
evaluations in each iteration has universal local order at most 
at simple roots (Kung
and Traub 1974). Each evaluation returns one scalar value of the function or of a
derivative of any chosen nonnegative
integer order. The evaluation points and derivative
orders may depend on the answers already received in the current iteration.
Colbrook (2026) proves the bound for the class of real analytic functions. For every proposed order 
, a single entire
function that is real on the real axis has a simple root and arbitrarily close starting points at
which the local order-
estimate fails. The sharp order 
is attained for 
by the methods of Kung and Traub (1974). Colbrook (2026)
also proves a complex-observation version and reports a Lean formalization developed
with ChatGPT assistance. The formal definitions and main theorem statements were
inspected, but the development was not independently rebuilt here.
