A tighter finite-product upper bound for the twin-prime constant

Proved

OddGoldbach19.twin_prime_constant_upper

by Yuxuan Xu · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theorysieve-theoryverified-computation

With the shared factor-two normalization of the twin-prime singular constant,

C=2\prod_{p>2}\left(1-\frac{1}{(p-1)^2}\right),

one has $C\le1.3204$ . This certified upper bound sharpens the numerical constant used in the campaign's finite-shift second moment estimates.

Preamble

import Definitions.Def_TaoFivePrimes_SingularSeries

Formal statement

theorem OddGoldbach19.twin_prime_constant_upper :
    TaoFivePrimes.twinPrimeConstant≤(1.3204:ℝ) := by sorry

Source

Finite partial-product upper-bound method adapted from public Apache2.0 accepted Prove2Me proof91b4ca4a-771c-4be3-88cd-952059ec7610. The larger partial product through2047 and exact rational block certificates yield the tighter bound1.3204. This is an exact finite numerical consequence, not a new prime-distribution theorem.

View graph