Helfgott–Platt block ladders, group 1 subgroup 2 of 10

Open

WeakGoldbach.helfgott_platt_block_ladders_grp01_sg02

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-certificatesgoldbachnumber-theoryprimes

Put $H = 2\cdot 10^{18}$ and $W = 2^{54}\cdot 10^9 = 18014398509481984000000000$ . For every integer $b$ in the range

$4927 \le b < 9854$,

there is a finite increasing sequence of primes $p_0,\ldots,p_k$ satisfying

bW < p_0 \le bW + H,\qquad p_i < p_{i+1} < p_i + 2H \quad (0 \le i < k),

p_k \le (b+1)W < p_k + H.

Role: this is subgroup $2$ of $10$ consecutive subgroups of WeakGoldbach.helfgott_platt_block_ladders_grp01, which covers block indices $0 \le b < 49270$ (group 1 of 10 of the parent WeakGoldbach.helfgott_platt_block_ladders). Each subgroup has width $4927$ in the block index $b$ . The subgroups meet end to end within group 1.

This isolates the local computational certificate for $4927$ of the $492700$ intervals of width $W$ reported in Section 4 of the source. The endpoint conditions allow consecutive blocks to be joined without a gap of size $2H$ .

The hypotheses are $4927 \le b < 9854$ . No certificate data are supplied here; the statement is an open certificate obligation for this index range.

Formalization Note The conclusion matches WeakGoldbach.helfgott_platt_block_ladders_grp01 exactly; only the range of $b$ is restricted.

Preamble

import Mathlib.Data.Nat.Prime.Basic

Formal statement

theorem WeakGoldbach.helfgott_platt_block_ladders_grp01_sg02 (b : ℕ) (hb_lo : 4927 ≤ b) (hb_hi : b < 9854) :
    ∃ (k : ℕ) (p : ℕ → ℕ),
      (∀ i, i ≤ k → Nat.Prime (p i)) ∧
      (b*18014398509481984000000000 < p 0 ∧
        p 0 ≤ b*18014398509481984000000000 + 2*10^18) ∧
      (∀ i, i < k → p i < p (i+1) ∧ p (i+1) < p i + 4*10^18) ∧
      (p k ≤ (b+1)*18014398509481984000000000 ∧
        (b+1)*18014398509481984000000000 < p k + 2*10^18) := by sorry

Source

H. A. Helfgott and D. J. Platt, Numerical Verification of the Ternary Goldbach Conjecture up to 8.875e30, arXiv:1305.3062v2, Section 3 (prime ladder algorithm) and Section 4 (width 2^54*10^9, endpoint distances 2*10^18, and 492700 intervals). https://arxiv.org/pdf/1305.3062. Subgroup 2 of 10 of WeakGoldbach.helfgott_platt_block_ladders_grp01 covering block indices [4927, 9854).

View graph