The $n$ -dependent singular-series factor is at least $1$

Proved

WeakGoldbach.singular_series_factor_ge_one

by jjosh · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

circle-methodgoldbachnumber-theoryprimes

For every natural number $n$ , the $n$ -dependent part of the binary Goldbach singular series satisfies

\mathfrak{S}(n) = \prod_{\substack{p \mid n \\ p > 2}} \frac{p-1}{p-2} \;\ge\; 1,

since every local factor $(p-1)/(p-2) > 1$ for $p \ge 3$ . This is the elementary component of the Hardy–Littlewood estimate: the singular series never degenerates for even $n$ , so a lower bound on the representation count reduces to controlling the analytic error term.

Preamble

import Mathlib

Formal statement

namespace WeakGoldbach

theorem singular_series_factor_ge_one (n : ℕ) :
    1 ≤ ∏ p ∈ n.primeFactors.filter (2 < ·), ((p : ℝ) - 1) / ((p : ℝ) - 2) := by
  sorry

end WeakGoldbach

Source

Standard; elementary property of the Goldbach singular series

View graph

The nnn-dependent singular-series factor is at least 111

The $n$ -dependent singular-series factor is at least $1$