The singular series of an admissible tuple is positive
ProvedHardyLittlewood.singular_series_positiveFor a tuple of pairwise distinct offsets that is admissible — the doubled offsets miss a residue class modulo every prime — the singular series constant C_P is a strictly positive real number: the Euler product over the odd primes converges to a positive limit, since all but finitely many of its factors are 1 + O(1/q²) and every factor is positive. Positivity is what turns the conjecture's asymptotic into an infinitude.
import Mathlib import Definitions.Def_HardyLittlewood_constellation import Definitions.Def_HardyLittlewood_counting import Definitions.Def_HardyLittlewood_series
namespace HardyLittlewood
/-- The singular series of an admissible tuple of distinct offsets is a
well-defined positive constant: for injective m whose doubled offsets miss a
residue class modulo every prime, the Euler product over the odd primes
converges to a strictly positive value. -/
theorem singular_series_positive {k : ℕ} (m : Fin k.succ → ℕ)
(hinj : Function.Injective m) (hadm : IsAdmissibleTuple m) :
0 < singularSeriesConstant m := by
sorry
end HardyLittlewood
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for every natural number k and every function m from {0, 1, ..., k} to the natural numbers, if m is injective and the doubled offsets are admissible — for every prime q the residues of 2 · m i modulo q do not cover all residue classes — then the real number "singularSeriesConstant m" is strictly positive. That number is 2^k times the product over all primes q at least 3 of the quantity (1 − w/q) / (1 − 1/q)^(k+1), where w is the number of residues occupied by the offsets modulo q, with the infinite product understood in Mathlib's unconditional sense.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.