Finite deterministic criterion for Gilbreath arrays
ProvedGilbreath.chase_hunter_tao_finite_criterioncombinatoricsgilbreathnumber-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 GilbreathSource
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).