Infinite periodic slices of the GKP carry condition

The first three ternary digits of 2 ^ k are periodic in k modulo 18. Exactly nine of those eighteen exponent classes already create at least two doubling carries in that three-digit prefix. Consequently, every exponent in those classes satisfies the divisibility-by-nine branch of the GKP conjecture.

This is an infinite scoped result. The other nine residue classes are not settled here, and the universal GKP conjecture remains open.

Modular carry certificates

theorem GKPCarry.ternaryDoubleCarryCountAux_append_le (prefixDigits suffix : List ℕ) (carry : ℕ) : ternaryDoubleCarryCountAux prefixDigits carry ≤ ternaryDoubleCarryCountAux (prefixDigits ++ suffix) carry

theorem GKPCarry.ternaryDoubleCarryCount_mod_pow_le (depth n : ℕ) : ternaryDoubleCarryCount (Nat.digits 3 (n % 3 ^ depth)) ≤ ternaryDoubleCarryCount (Nat.digits 3 n)

The carry count of a canonical ternary residue modulo 3 ^ depth is a lower bound for the carry count of the whole number.

theorem GKPCarry.nine_dvd_centralBinom_of_modular_carry_certificate {depth n : ℕ} (hcarry : 2 ≤ ternaryDoubleCarryCount (Nat.digits 3 (n % 3 ^ depth))) : 9 ∣ n.centralBinom

Any finite modular prefix with two carries certifies divisibility by nine for the full central binomial coefficient.

The period modulo 27

theorem GKPCarry.two_pow_eighteen_mod_twentySeven : 2 ^ 18 % 27 = 1

The exponent period used for the three-digit ternary prefix.

theorem GKPCarry.two_pow_mod_twentySeven_eq_reduced_exponent (k : ℕ) : 2 ^ k % 27 = 2 ^ (k % 18) % 27

The residue of 2 ^ k modulo 27 depends only on k % 18.

Exact three-digit sieve

def GKPCarry.gkpSafeExponentResiduesMod18 : Finset ℕ

Exponent classes whose first three ternary digits already create at least two doubling carries.

Equations

• GKPCarry.gkpSafeExponentResiduesMod18 = {3, 4, 5, 7, 9, 10, 11, 15, 17}

theorem GKPCarry.card_gkpSafeExponentResiduesMod18 : gkpSafeExponentResiduesMod18.card = 9

Exactly half of the exponent classes modulo 18 pass the three-digit carry sieve.

theorem GKPCarry.lowThreeCarryCertificate_iff (k : ℕ) : 2 ≤ ternaryDoubleCarryCount (Nat.digits 3 (2 ^ k % 27)) ↔ k % 18 ∈ gkpSafeExponentResiduesMod18

Exact classification of the exponent classes whose residue modulo 27 already displays two ternary doubling carries.

theorem GKPCarry.nine_dvd_centralBinom_two_pow_of_safe_mod_eighteen {k : ℕ} (hk : k % 18 ∈ gkpSafeExponentResiduesMod18) : 9 ∣ (2 ^ k).centralBinom

Infinite periodic GKP slice. If k lies in one of nine explicit classes modulo 18, then the central binomial coefficient indexed by 2 ^ k is divisible by 9.

theorem GKPCarry.badCarryLanguage_two_pow_eq_false_of_safe_mod_eighteen {k : ℕ} (hk : k % 18 ∈ gkpSafeExponentResiduesMod18) : badCarryLanguage (Nat.digits 3 (2 ^ k)) = false

On the same nine infinite classes, powers of two avoid the deficient-carry language used in the exact GKP characterization.