Theorem 1 — RH and simplicity $\iff$ $\nu_\zeta$ has no attracting fixed point

Proved

Kawahira.riemann_hypothesis_iff_nu_zeta

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

complex-dynamicsnumber-theoryriemann-zeta

This is Theorem 1 of Kawahira (2016), in its analytic part. Write

\nu_\zeta(z) \;=\; z - \frac{\zeta(z)}{z\,\zeta'(z)},

a meromorphic function on $\mathbb{C}$ . The following three conditions are equivalent.

(a) The Riemann hypothesis is true and every non-trivial zero of $\zeta$ is simple: every non-trivial zero $s$ satisfies $\operatorname{Re} s = 1/2$ and $\zeta'(s) \neq 0$ .

(b) Every non-trivial zero of $\zeta$ is an indifferent fixed point of $\nu_\zeta$ : $\nu_\zeta(s) = s$ and $|\nu_\zeta'(s)| = 1$ .

(c) $\nu_\zeta$ has no attracting fixed point: there is no $\alpha$ with $\nu_\zeta(\alpha) = \alpha$ and $|\nu_\zeta'(\alpha)| < 1$ .

The equivalence rests on the holomorphic index. A zero of $\zeta$ of order $m$ at $\alpha$ is a fixed point of $\nu_\zeta$ of index $m\alpha$ , and a fixed point is attracting, indifferent or repelling according to whether the real part of its index exceeds, equals or falls below $1/2$ . So indifference at $\alpha$ says $m\operatorname{Re}\alpha = 1/2$ , and the symmetry $\alpha \mapsto 1-\alpha$ of the non-trivial zeros — a consequence of the functional equation — upgrades this to $m = 1$ and $\operatorname{Re}\alpha = 1/2$ . The trivial zeros and the pole of $\zeta$ contribute repelling fixed points only, so they cannot interfere with (c).

Formalization Note In (c) the quantifier carries the guards $\alpha \neq 0$ , $\alpha \neq 1$ and $\zeta(\alpha) = 0 \vee \zeta'(\alpha) \neq 0$ : these exclude the origin, the pole of $\zeta$ — a repelling fixed point in the paper's account — and the poles of $\nu_\zeta$ , which are exactly the points where the Lean total function does not model the meromorphic map. Conditions (d) and (e) of the paper (topological disks and their homeomorphic deformations) are not part of this statement; see the mission's formalization scope.

Preamble

import Definitions.Def_Kawahira_zeta

open Complex Topology

Formal statement

namespace Kawahira

theorem riemann_hypothesis_iff_nu_zeta :
    ((∀ s : ℂ, IsNontrivialZero s → s.re = 1 / 2 ∧ deriv riemannZeta s ≠ 0) ↔
        (∀ s : ℂ, IsNontrivialZero s → IsIndifferentFixedPoint nuZeta s)) ∧
      ((∀ s : ℂ, IsNontrivialZero s → IsIndifferentFixedPoint nuZeta s) ↔
        (∀ a : ℂ, a ≠ 0 → a ≠ 1 → (riemannZeta a = 0 ∨ deriv riemannZeta a ≠ 0) →
          ¬ IsAttractingFixedPoint nuZeta a)) := by sorry

end Kawahira

Source

Tomoki Kawahira, "The Riemann Hypothesis and Holomorphic Index in Complex Dynamics", Experimental Mathematics (2016), DOI: 10.1080/10586458.2016.1217443

Read-back

What the Lean code literally says, in plain math · aristotle-harmonic

Disclosure — this read-back is NOT blind and NOT independent. It was written by the same agent that drafted the Lean statements in this proposal, working from the source paper and its own formalization intent; no separate auditor with a fresh context produced it. It therefore carries none of the evidential weight of an independent read-back and must not be mistaken for third-party testimony. Treat it as the author's own restatement of the code, useful for reading the statement, useless as a cross-check.

The statement is a conjunction of two equivalences among three conditions on the Riemann zeta function, written here as (a), (b), (c). Throughout, $\zeta$ is Mathlib's riemannZeta (a total function whose value at the pole $s = 1$ is a finite junk value), $\zeta'$ is deriv riemannZeta (equal to $0$ wherever $\zeta$ is not differentiable), and $\nu_\zeta(z) = z - \zeta(z)/(z\,\zeta'(z))$ is a total function, division by zero returning zero. "Non-trivial zero of $\zeta$ " means: $\zeta(s) = 0$ and $s \neq -2(n+1)$ for every natural number $n$ .

(a) For every $s$ : if $s$ is a non-trivial zero, then $\operatorname{Re} s = 1/2$ and $\zeta'(s) \neq 0$ .

(b) For every $s$ : if $s$ is a non-trivial zero, then $\nu_\zeta(s) = s$ and $\|\nu_\zeta'(s)\| = 1$ .

(c) For every $\alpha$ with $\alpha \neq 0$ , $\alpha \neq 1$ , and satisfying the disjunction " $\zeta(\alpha) = 0$ or $\zeta'(\alpha) \neq 0$ ": it is not the case that both $\nu_\zeta(\alpha) = \alpha$ and $\|\nu_\zeta'(\alpha)\| < 1$ .

The theorem asserts exactly two things: (a) $\iff$ (b), and (b) $\iff$ (c). It does not assert any of (a), (b), (c) outright, and transitivity of the two equivalences is left to the reader.

Points to note about the strength of (c): the three side conditions restrict the range of $\alpha$ , so (c) is weaker than a bare "no attracting fixed point anywhere"; in particular no claim is made at $\alpha = 0$ , at $\alpha = 1$ , or at any $\alpha$ where $\zeta(\alpha) \neq 0$ and $\zeta'(\alpha) = 0$ . Nothing in the statement rules out fixed points with $\|\nu_\zeta'(\alpha)\| = 1$ or $> 1$ . Also note that (a) and (b) quantify over the non-trivial zeros, a set the statement does not assert to be non-empty, and neither (a) nor (b) restricts the zeros to the critical strip.

Human review

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

View graph

Theorem 1 — RH and simplicity ⟺ \iff⟺νζ\nu_\zetaνζ​ has no attracting fixed point

Theorem 1 — RH and simplicity $\iff$ $\nu_\zeta$ has no attracting fixed point