Making the coprimality convention explicit in a mean value theorem of Halupczok for the ternary Goldbach problem

Abstract

Theorem 1.2 of Halupczok (2013) is a Bombieri-Vinogradov type mean value theorem for the ternary Goldbach problem with one prime in an arithmetic progression and two primes in short intervals. Her proof works with residue classes a mod q coprime to the modulus, as stated on p. 344 of her paper, and a formal verification requires that this convention be written explicitly into the statement. We give two closely related explicit formulations, Formulation A and Formulation B, where Lean proves that Formulation A implies Formulation B, and verify both in Lean 4 assuming the two cited inputs PPS1984Remark and PP1993Goldbach, or alternatively Theorems 2.1 and 2.3 of her paper, which Lean deduces from these two inputs. The later results of Halupczok's paper use only coprime residue classes and are unaffected. Lean source: github.com/sthubbar/goldbach-lean, entries/halupczok2012, commit 12f09bf; Palomar registry PALOMAR-2026-10-28-000026.

Keywords