{"id":"palomar/PALOMAR-2026-11-03-000029","url":"https://github.com/sthubbar/goldbach-lean/tree/d0d978d2cf565be71d6949ce529ed5503affa72e/entries/helfgott62","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-03-000029-v1.json","repo":"https://github.com/sthubbar/goldbach-lean","tags":["math.NT","msc:11P32","msc:11P55"],"score":0,"title":"Helfgott's Proposition 6.2 on the ternary Goldbach minor arcs","trust":"high","domain":"math.NT","source":"palomar","authors":["Steve Hubbard"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 proof of Lemma 6.1 and Proposition 6.2 of H. A. Helfgott, The ternary Goldbach conjecture is true, arXiv 1312.7748v2, Section 6.1, pages 46 to 48. Lemma 6.1 is a summation by parts bound. Proposition 6.2 turns l2 bounds on S1 over the major arcs and l-infinity bounds on S2 off them into a bound for the integral of |S1|^2 |S2| over the minor arcs, without the factor log x that a plain product of norms would lose. Lemma 6.1 is stated as in the paper. Proposition 6.2 is given in three forms: an abstract measure form with a natural upper endpoint; the arcs of display 3.5 for a finite…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-03","reactions":{},"formalized":true,"formalizes":[{"title":"The ternary Goldbach conjecture is true","identifier":"arXiv:1312.7748","relationship":"formalizes"}]}