Binary reduction of the GKP conjecture

Kummer's theorem at p = 2 identifies the two-adic valuation of a central binomial coefficient with binary popcount. Hence every positive non-power of two already satisfies the divisibility-by-four branch of GKP.

theorem GKPCarry.padicValNat_two_centralBinom (n : ℕ) : padicValNat 2 n.centralBinom = (Nat.digits 2 n).sum

The two-adic valuation of Nat.centralBinom n is the binary popcount of n.

theorem GKPCarry.four_dvd_centralBinom_of_binary_popcount_ge_two {n : ℕ} (hpop : 2 ≤ (Nat.digits 2 n).sum) : 4 ∣ n.centralBinom

Binary popcount at least two forces divisibility by four.

theorem GKPCarry.popcount_le_one_zero_or_pow_two (n : ℕ) (hpop : (Nat.digits 2 n).sum ≤ 1) : n = 0 ∨ ∃ (k : ℕ), n = 2 ^ k

A natural number with binary popcount at most one is zero or a power of two.

theorem GKPCarry.popcount_pow_two (k : ℕ) : (Nat.digits 2 (2 ^ k)).sum = 1

Every power of two has binary popcount one.

theorem GKPCarry.four_dvd_centralBinom_of_not_power_of_two {n : ℕ} (hn : 0 < n) (hnp : ¬∃ (k : ℕ), n = 2 ^ k) : 4 ∣ n.centralBinom

Every positive non-power of two satisfies the divisibility-by-four branch of GKP.

theorem GKPCarry.gkpConjecture_of_powerOfTwo (h : gkpPowerOfTwoConjecture) : gkpConjecture

The full GKP conjecture follows from its power-of-two restriction.

theorem GKPCarry.gkpPowerOfTwoConjecture_of_gkp (h : gkpConjecture) : gkpPowerOfTwoConjecture

The power-of-two restriction follows from the full GKP conjecture.

theorem GKPCarry.gkpConjecture_iff_powerOfTwo : gkpConjecture ↔ gkpPowerOfTwoConjecture

GKP is equivalent to its restriction to powers of two.