Propagation lemma: a leading $1$ followed by $0$ s and $2$ s persists

Proved

Gilbreath.propagation

by Lucas · Sep 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsconjecturenumber-theoryprime-numbers

Odlyzko's propagation lemma, stated for an arbitrary sequence of natural numbers. Suppose $a(0) = 1$ and $a(n) \in \{0, 2\}$ for all $1 \le n \le m$ . Then for every $j \le m$ the $j$ -th iterated absolute-difference row of $a$ again begins with $1$ : $(\Delta^j a)(0) = 1$ .

The point is that the hypothesis is self-reproducing with one entry less of margin: if $a$ begins $1$ and continues in $\{0,2\}$ for $m$ entries, then $\Delta a$ begins $1$ and continues in $\{0,2\}$ for $m-1$ entries. A block of $m$ good entries therefore certifies the leading $1$ for the next $m$ rows, and nothing more. This is the mechanism behind every computational verification of Gilbreath's conjecture.

Preamble

import Definitions.Def_gilbreath_triangle

Formal statement

namespace Gilbreath
theorem propagation (a : ℕ → ℕ) (m : ℕ) (h0 : a 0 = 1)
    (h : ∀ n, 1 ≤ n → n ≤ m → a n = 0 ∨ a n = 2) (j : ℕ) (hj : j ≤ m) :
    iterAbsDiff a j 0 = 1 := by sorry
end Gilbreath

Source

Gilbreath's conjecture. N. L. Gilbreath (1958), as reported in R. B. Killgrove and K. E. Ralston, On a conjecture concerning the primes, MTAC 13 (1959), 121-122, https://doi.org/10.1090/S0025-5718-1959-0105398-3; A. M. Odlyzko, Iterated absolute values of differences of consecutive primes, Math. Comp. 61 (1993), 373-380, https://doi.org/10.1090/S0025-5718-1993-1192979-9; https://en.wikipedia.org/wiki/Gilbreath%27s_conjecture

Read-back

What the Lean code literally says, in plain math · self-authored by the drafting agent (non-blind, not an independent auditor)

Disclosure — this read-back is not independent. It was written by the same agent that drafted the Lean statements in this proposal, at the mission owner's explicit instruction, rather than blind by a separate auditor. It is therefore self-testimony, not independent testimony, and the usual protection against an unfaithful formalization — a reader who does not know what the code is supposed to say — is absent here. An independent read-back is recommended before this item is confirmed.

Let $a : \mathbb{N} \to \mathbb{N}$ be an arbitrary sequence of natural numbers and let $m$ be a natural number. Assume:

$a(0) = 1$ ; and
for every natural number $n$ with $1 \le n \le m$ , either $a(n) = 0$ or $a(n) = 2$ .

Then for every natural number $j$ with $j \le m$ ,

(\Delta^j a)(0) = 1,

where $\Delta^0 a = a$ and $\Delta^{k+1} a = \Delta(\Delta^k a)$ with $(\Delta b)(n) = |b(n+1) - b(n)|$ , the absolute difference formed in the integers.

The conclusion is only about index $0$ of the iterated row; nothing is claimed about later indices, and nothing about iterates beyond $j = m$ . The case $j = 0$ is included and there restates $a(0) = 1$ . The case $m = 0$ is included: then the second hypothesis is empty and the only admissible $j$ is $0$ . The hypotheses constrain $a$ only at indices $0$ through $m$ ; the values $a(n)$ for $n > m$ are arbitrary. The hypotheses are satisfiable (for instance by the constant-after-1 sequence $1, 0, 0, \dots$ ), so the statement is not vacuous. This statement mentions no primes.

Human review

Endorsed by Shuze Chen · Sep 16, 2026
Endorsed by Lucas · Sep 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Propagation lemma: a leading 111 followed by 000s and 222s persists

Propagation lemma: a leading $1$ followed by $0$ s and $2$ s persists