Parentage trichotomy for a {0,d}-valued Gilbreath block

Proved

Gilbreath.chase_hunter_tao_parentage

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

combinatoricsgilbreathnumber-theory

Let d be positive. Suppose a nonempty block of adjacent absolute differences of a nonnegative integer sequence takes values only in {0,d} and attains d. Then its parent block satisfies one of three alternatives: some entry is at least 2d; or every entry is 0 or d and both values occur; or there is 0<r<d such that every entry is r or r+d and both values occur. The Lean statement uses a zero-based block of k child entries and k+1 parent entries.

Preamble

import Definitions.Def_gilbreath_triangle

Formal statement

namespace Gilbreath
theorem chase_hunter_tao_parentage (a : ℕ → ℕ) (n k D : ℕ)
    (hD : 0 < D)
    (hchild : ∀ t, t < k →
      absDiff a (n + t) = 0 ∨ absDiff a (n + t) = D)
    (hatt : ∃ t, t < k ∧ absDiff a (n + t) = D) :
    (∃ u, u ≤ k ∧ 2 * D ≤ a (n + u)) ∨
    ((∀ t, t ≤ k → a (n + t) = 0 ∨ a (n + t) = D) ∧
      (∃ u, u ≤ k ∧ a (n + u) = 0) ∧
      (∃ v, v ≤ k ∧ a (n + v) = D)) ∨
    (∃ r, 0 < r ∧ r < D ∧
      (∀ t, t ≤ k → a (n + t) = r ∨ a (n + t) = r + D) ∧
      (∃ u, u ≤ k ∧ a (n + u) = r) ∧
      (∃ v, v ≤ k ∧ a (n + v) = r + D)) := 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, p. 14, Lemma 3.8 (Parentage), https://arxiv.org/pdf/2607.08712v1. This is the zero-based local-sequence form of the three alternatives.

View graph