A three-halves prime-counting bound for the Schnirelmann additive set

Proved

OddGoldbach19.small_count_A

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

goldbachnumber-theory

Let A be the shared set B+B, where B consists of (p-3)/2 for odd primes p. For every natural number N at least 5, write A(N) for the number of positive integers at most N belonging to A, and pi(x) for the number of primes at most x. Then 3pi(2N+1) <= 2A(N)+12. The finite correction 12 accounts for excluding primes below 11. This is an explicit small-range counting input; it does not assert a complete 19-prime representation theorem.

Preamble

import Mathlib
import Definitions.Def_Schnir_defs
open Classical

Formal statement

theorem OddGoldbach19.small_count_A (N : ℕ) (hN : 5 ≤ N) :
    3 * Nat.primeCounting (2 * N + 1) ≤
      2 * ((Finset.Ioc 0 N).filter (fun a => a ∈ Schnir.A)).card + 12 := by sorry

Source

H. Riesel and R. C. Vaughan, On sums of primes, Arkiv for Matematik21(1983), pp45–74, Lemma7 proof on p58: union of p+3 and p+5, excluding three consecutive odd primes. https://doi.org/10.1007/BF02384300 . The affine A-count statement and finite correction are derived here.

View graph