Finite deterministic criterion for Gilbreath arrays

Proved

Gilbreath.chase_hunter_tao_finite_criterion

by EvanLLL · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsgilbreathnumber-theory

Let an array be generated by N nonnegative integers. Choose M,L≥1, a cutoff N', and scales R₀,…,R_M satisfying the inequalities in Theorem 1.6. If every initial entry is at most 2^M, no row contains L consecutive zeros, and the indicated shallow right-hand region contains no sufficiently long block taking only the values 0 and d for the specified d-ranges, then the bottom entry is 0 or 1. The Lean statement uses zero-based input indices; its block inequalities translate the displayed bounds of the source.

Preamble

import Definitions.Def_gilbreath_triangle

Formal statement

namespace Gilbreath

-- Chase--Hunter--Tao, arXiv:2607.08712v1, Theorem 1.6, pp. 7--8.
-- Zero-based inputs: a 0 represents the paper's a₁.
theorem chase_hunter_tao_finite_criterion
    (a : ℕ → ℕ) (N N' M L : ℕ) (R : ℕ → ℕ)
    (hbounds :
      1 ≤ N' ∧ N' ≤ N ∧ 1 ≤ M ∧ 1 ≤ L ∧
      1 < R 0 ∧
      (∀ m, m < M → R m < R (m + 1)) ∧
      2 * R M + N' < N ∧
      (∀ m, 1 ≤ m → m ≤ M → 4 * R (m - 1) ≤ R m) ∧
      100 * L * 8 ^ M ≤ R 0)
    (hinput : ∀ j < N, a j ≤ 2 ^ M)
    (hzero : ¬ ∃ i j : ℕ,
      i + L ≤ N ∧ j + i + L ≤ N ∧
      ∀ t < L, iterAbsDiff a i (j + t) = 0)
    (htwo : ¬ ∃ m d i k j : ℕ,
      1 ≤ m ∧ m ≤ M ∧
      2 ^ (M - m) < d ∧ d ≤ 2 ^ (M - m + 1) ∧
      i ≤ 2 * R (m - 1) ∧
      R m ≤ k + 3 * R (m - 1) ∧
      N' ≤ j + 1 ∧ j + i + k + 1 ≤ N ∧
      ∀ t < k, iterAbsDiff a i (j + t) = 0 ∨
        iterAbsDiff a i (j + t) = d) :
    iterAbsDiff a (N - 1) 0 = 0 ∨
      iterAbsDiff a (N - 1) 0 = 1 := by sorry

end Gilbreath

Source

Z. Chase, Z. Hunter, T. Tao, Gilbreath's conjecture: a Cramér random model and a deterministic analysis, arXiv:2607.08712v1, pp. 7–8, Theorem 1.6 and equations (1.6)–(1.8), https://arxiv.org/pdf/2607.08712v1. The displayed input range n=0,…,N is read as the N entries a_1,…,a_N; the displayed constant is 100 as in (1.8).

View graph