The floor of the zeta states

The zeta state of weight s > 1 has populations (n + 1)^{−s} / ζ(s) on the equally spaced levels n + 1; its autocorrelation is Li_s(z) / ζ(s) with z = e^{−iθ}. From η(s) ≤ |Li_s z| on the unit circle (Polylog.polylog_circle_floor) and the classical identity η(s) = (1 − 2^{1−s}) ζ(s), proved here by splitting the alternating series into even and odd terms, the autocorrelation never drops below 1 − 2^{1−s}, its value at θ = π. For s = 2 the floor is 1/2.

Main results

• Polylog.tendsto_partialEta_of_one_lt: η(s) = (1 − 2^{1−s}) ζ(s) for s > 1
• Polylog.zeta_floor: (1 − 2^{1−s}) ζ(s) ≤ |Li_s z| on the whole unit circle, s > 1
• Polylog.zetaState_floor: the normalized zeta state has |S(θ)| ≥ 1 − 2^{1−s} for every θ

References

• C. Marín, The Clock That Never Ticks: a machine-checked path from the dilogarithm to quantum speed limits in Lean 4, Zenodo (2026), doi:10.5281/zenodo.20675271, thm:clock.

theorem Polylog.summable_zeta_aux {s : ℝ} (hs : 1 < s) : Summable fun (n : ℕ) => 1 / (↑n + 1) ^ s

Summability of 1 / (n+1)^s for s > 1.

theorem Polylog.tendsto_partialEta_of_one_lt {s : ℝ} (hs : 1 < s) : Filter.Tendsto (partialEta s) Filter.atTop (nhds ((1 - 2 ^ (1 - s)) * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))

η(s) = (1 - 2^{1-s}) ζ(s) for s > 1, with ζ(s) = ∑ (n+1)^{-s}.

theorem Polylog.summable_circle_aux {s : ℝ} (hs : 1 < s) {z : ℂ} (hz : ‖z‖ = 1) : Summable fun (n : ℕ) => z ^ (n + 1) / ↑((↑n + 1) ^ s)

Partial sums of the circle series are partialLi, and the series is summable for s > 1.

theorem Polylog.zeta_floor {s : ℝ} (hs : 1 < s) {z : ℂ} (hz : ‖z‖ = 1) : (1 - 2 ^ (1 - s)) * ∑' (n : ℕ), 1 / (↑n + 1) ^ s ≤ ‖∑' (n : ℕ), z ^ (n + 1) / ↑((↑n + 1) ^ s)‖

The floor of Li_s for s > 1, on the whole unit circle (including z = 1): (1 - 2^{1-s}) ζ(s) ≤ ‖∑ z^{n+1} / (n+1)^s‖.

theorem Polylog.zetaState_floor {s : ℝ} (hs : 1 < s) (θ : ℝ) : 1 - 2 ^ (1 - s) ≤ ‖∑' (n : ℕ), ↑(1 / (↑n + 1) ^ s / ∑' (m : ℕ), 1 / (↑m + 1) ^ s) * Complex.exp (-↑((↑n + 1) * θ) * Complex.I)‖

The zeta state never gets closer to orthogonality than 1 - 2^{1-s}. With populations p n = (n+1)^{-s} / ζ(s) on the levels n + 1, the autocorrelation at every time θ has modulus at least 1 - 2^{1-s}.