A regular-language characterization of the GKP conjecture

For every n, the deficient-carry automaton on the canonical ternary digits of n accepts exactly when 9 does not divide Nat.centralBinom n. Combining this exact local characterization with the binary reduction yields an equivalence between the Graham--Knuth--Patashnik conjecture and avoidance of an explicit regular language by nonexceptional powers of two.

This equivalence is a reduction of the open conjecture, not a proof of it.

theorem GKPCarry.nine_dvd_centralBinom_iff_two_le_ternaryDoubleCarryCount (n : ℕ) : 9 ∣ n.centralBinom ↔ 2 ≤ ternaryDoubleCarryCount (Nat.digits 3 n)

Divisibility by nine is exactly the condition that ternary doubling creates at least two carries.

theorem GKPCarry.badCarryLanguage_digits_true_iff_not_nine_dvd (n : ℕ) : badCarryLanguage (Nat.digits 3 n) = true ↔ ¬9 ∣ n.centralBinom

The automaton accepts the canonical ternary expansion of n exactly when 9 does not divide its central binomial coefficient.

def GKPCarry.gkpBadCarryLanguageExclusion : Prop

The remaining language-avoidance statement for nonexceptional powers of two. This proposition is open.

Equations

• GKPCarry.gkpBadCarryLanguageExclusion = ∀ (k : ℕ), 2 < k → k ≠ 6 → k ≠ 8 → GKPCarry.badCarryLanguage (Nat.digits 3 (2 ^ k)) = false

theorem GKPCarry.gkpBadCarryLanguageExclusion_iff_shape_exclusions : gkpBadCarryLanguageExclusion ↔ (∀ (k : ℕ), 2 < k → k ≠ 6 → k ≠ 8 → ¬badCarryAllZeroOrOne (Nat.digits 3 (2 ^ k))) ∧ (∀ (k : ℕ), 2 < k → k ≠ 6 → k ≠ 8 → ¬badCarryExactlyOneTopTwo (Nat.digits 3 (2 ^ k))) ∧ ∀ (k : ℕ), 2 < k → k ≠ 6 → k ≠ 8 → ¬badCarryExactlyOneTwoFollowedByZero (Nat.digits 3 (2 ^ k))

The language-avoidance statement is equivalent to excluding each of the three concrete deficient-carry shapes.

theorem GKPCarry.gkpBadCarryLanguageExclusion_of_gkp (h : gkpConjecture) : gkpBadCarryLanguageExclusion

GKP implies avoidance of the deficient-carry language.

theorem GKPCarry.gkpConjecture_of_badCarryLanguageExclusion (h : gkpBadCarryLanguageExclusion) : gkpConjecture

Avoidance of the deficient-carry language implies GKP.

theorem GKPCarry.gkpConjecture_iff_badCarryLanguageExclusion : gkpConjecture ↔ gkpBadCarryLanguageExclusion

Headline theorem: the GKP conjecture is equivalent to avoidance of the explicit deficient-carry regular language by nonexceptional powers of two.

theorem GKPCarry.erdos406_tail_of_gkpBadCarryLanguageExclusion (h : gkpBadCarryLanguageExclusion) (k : ℕ) : 8 < k → ¬badCarryAllZeroOrOne (Nat.digits 3 (2 ^ k))

The GKP exclusion would imply the tail of Erdős Problem 406: powers of two above 2 ^ 8 cannot have ternary expansions using only 0 and 1.