Ternary prefixes and doubling carries

This file gives the definitions used by the carry-language theory and its bounded C3 corollary. Ternary digit lists are little-endian, following Nat.digits.

def GKPCarry.ternaryLength (n : ℕ) : ℕ

Length of the canonical base-three expansion of n.

Equations

• GKPCarry.ternaryLength n = (Nat.digits 3 n).length

def GKPCarry.hasTwoTernaryTwosBelow (depth n : ℕ) : Prop

The first depth ternary digits of n contain at least two 2s.

Equations

• GKPCarry.hasTwoTernaryTwosBelow depth n = (2 ≤ List.count 2 (List.take depth (Nat.digits 3 n)))

def GKPCarry.ternaryDoubleCarryStep (carry digit : ℕ) : ℕ

One outgoing-carry step when a ternary digit is doubled.

Equations

• GKPCarry.ternaryDoubleCarryStep carry digit = if 3 ≤ 2 * digit + carry then 1 else 0

def GKPCarry.ternaryDoubleCarryCountAux : List ℕ → ℕ → ℕ

Count outgoing carries while doubling a little-endian ternary digit list.

Equations

• GKPCarry.ternaryDoubleCarryCountAux [] x✝ = 0
• GKPCarry.ternaryDoubleCarryCountAux (digit :: digits) x✝ = GKPCarry.ternaryDoubleCarryStep x✝ digit + GKPCarry.ternaryDoubleCarryCountAux digits (GKPCarry.ternaryDoubleCarryStep x✝ digit)

def GKPCarry.ternaryDoubleCarryCount (digits : List ℕ) : ℕ

Count carries while doubling a little-endian ternary digit list.

Equations

• GKPCarry.ternaryDoubleCarryCount digits = GKPCarry.ternaryDoubleCarryCountAux digits 0

def GKPCarry.prefixTernaryDoubleCarryCount (depth n : ℕ) : ℕ

Number of doubling carries visible in the first depth ternary digits.

Equations

• GKPCarry.prefixTernaryDoubleCarryCount depth n = GKPCarry.ternaryDoubleCarryCount (List.take depth (Nat.digits 3 n))

theorem GKPCarry.count_two_le_ternaryDoubleCarryCountAux (digits : List ℕ) (carry : ℕ) : List.count 2 digits ≤ ternaryDoubleCarryCountAux digits carry

theorem GKPCarry.two_le_prefixTernaryDoubleCarryCount_of_hasTwoTernaryTwosBelow {depth n : ℕ} (h : hasTwoTernaryTwosBelow depth n) : 2 ≤ prefixTernaryDoubleCarryCount depth n

Two digit-2s in a prefix force at least two ternary doubling carries.

theorem GKPCarry.ternaryDoubleCarryCountAux_take_le (depth : ℕ) (digits : List ℕ) (carry : ℕ) : ternaryDoubleCarryCountAux (List.take depth digits) carry ≤ ternaryDoubleCarryCountAux digits carry

theorem GKPCarry.prefixTernaryDoubleCarryCount_le (depth n : ℕ) : prefixTernaryDoubleCarryCount depth n ≤ ternaryDoubleCarryCount (Nat.digits 3 n)

A prefix cannot contain more doubling carries than the complete word.