Documentation

LeanPool.GKPCarry.CarryArithmetic

Arithmetic correctness of the ternary doubling transducer #

The transducer in GKPCarry.Definitions counts outgoing carries while doubling a little-endian ternary word. This file proves that, on the canonical ternary digits of n, twice that count is exactly Kummer's ternary digit excess.

source
def GKPCarry.ternaryDigitExcess (n : ℕ) :
ℕ

Kummer's ternary digit excess for a central binomial coefficient.

Equations
Instances For
    source
    def GKPCarry.ternaryDoubleDigitsAux :
    List ℕ → ℕ → List ℕ

    Fixed-length output digits emitted while doubling a ternary word. The final carry is retained as the last digit.

    Equations
    Instances For
      source
      theorem GKPCarry.ternaryDoubleCarryStep_le_one (carry digit : ℕ) :
      ternaryDoubleCarryStep carry digit ≤ 1
      source
      theorem GKPCarry.ternaryDoubleCarryStep_lt_three (carry digit : ℕ) :
      ternaryDoubleCarryStep carry digit < 3
      source
      theorem GKPCarry.ternaryDoubleCarryStep_eq_div {carry digit : ℕ} (hcarry : carry ≤ 1) (hdigit : digit < 3) :
      ternaryDoubleCarryStep carry digit = (2 * digit + carry) / 3
      source
      theorem GKPCarry.ternaryDoubleCarryStep_local {carry digit : ℕ} (hcarry : carry ≤ 1) (hdigit : digit < 3) :
      (2 * digit + carry) % 3 + 3 * ternaryDoubleCarryStep carry digit = 2 * digit + carry
      source
      theorem GKPCarry.ternaryDoubleDigitsAux_length (digits : List ℕ) (carry : ℕ) :
      (ternaryDoubleDigitsAux digits carry).length = digits.length + 1
      source
      theorem GKPCarry.ternaryDoubleDigitsAux_lt_three {digits : List ℕ} {carry : ℕ} (hcarry : carry < 3) (hdigits : ∀ digit ∈ digits, digit < 3) (value : ℕ) :
      value ∈ ternaryDoubleDigitsAux digits carry → value < 3
      source
      theorem GKPCarry.ternaryDoubleDigitsAux_ofDigits {digits : List ℕ} {carry : ℕ} (hcarry : carry ≤ 1) (hdigits : ∀ digit ∈ digits, digit < 3) :
      Nat.ofDigits 3 (ternaryDoubleDigitsAux digits carry) = 2 * Nat.ofDigits 3 digits + carry
      source
      theorem GKPCarry.ternaryDoubleDigitsAux_sum_add_two_mul_carries {digits : List ℕ} {carry : ℕ} (hcarry : carry ≤ 1) (hdigits : ∀ digit ∈ digits, digit < 3) :
      (ternaryDoubleDigitsAux digits carry).sum + 2 * ternaryDoubleCarryCountAux digits carry = 2 * digits.sum + carry
      source
      theorem GKPCarry.ternaryDigitExcess_eq_two_mul_ternaryDoubleCarryCount (n : ℕ) :
      ternaryDigitExcess n = 2 * ternaryDoubleCarryCount (Nat.digits 3 n)

      Headline carry identity: Kummer's ternary digit excess is exactly twice the number of carries generated by ternary doubling.

      source
      theorem GKPCarry.nine_dvd_centralBinom_of_two_le_ternaryDoubleCarryCount {n : ℕ} (h : 2 ≤ ternaryDoubleCarryCount (Nat.digits 3 n)) :
      9 ∣ n.centralBinom

      Two ternary doubling carries imply divisibility of the central binomial coefficient by nine.

      source
      theorem GKPCarry.gkpConjecture_of_ternaryCarryCount (h : ∀ (k : ℕ), 2 < k → k ≠ 6 → k ≠ 8 → 2 ≤ ternaryDoubleCarryCount (Nat.digits 3 (2 ^ k))) :
      gkpConjecture

      A universal carry certificate on nonexceptional powers of two would imply the GKP conjecture.