Counting deficient-carry ternary words

The automaton gives an exact enumeration theorem. Among all ternary words of length m ≥ 2, precisely (m + 5) * 2 ^ (m - 2) create fewer than two carries when doubled. The theorem below uses the subtraction-free parameterization m = n + 2.

def GKPCarry.ternaryWordDigits {length : ℕ} (word : List.Vector (Fin 3) length) : List ℕ

Convert a fixed-length word over Fin 3 to a list of natural digits.

Equations

• GKPCarry.ternaryWordDigits word = List.map Fin.val word.toList

@[reducible, inline]

abbrev GKPCarry.BadCarryWordsFrom (state : BadCarryState) (length : ℕ) : Type

Fixed-length ternary words that remain outside .good when read from a given automaton state.

Equations

• GKPCarry.BadCarryWordsFrom state length = { word : List.Vector (Fin 3) length // GKPCarry.badCarryStateAux (GKPCarry.ternaryWordDigits word) state ≠ GKPCarry.BadCarryState.good }

@[reducible, inline]

abbrev GKPCarry.BadCarryWords (length : ℕ) : Type

Fixed-length ternary words whose doubling creates fewer than two carries.

Equations

• GKPCarry.BadCarryWords length = GKPCarry.BadCarryWordsFrom GKPCarry.BadCarryState.zeroCarry length

def GKPCarry.badCarryWordsFromSuccEquiv (state : BadCarryState) (length : ℕ) : BadCarryWordsFrom state (length + 1) ≃ (digit : Fin 3) × BadCarryWordsFrom (badCarryStateStep state ↑digit) length

Peeling the least significant digit gives the recursive decomposition of deficient-carry words.

Equations

• One or more equations did not get rendered due to their size.

def GKPCarry.badCarryWordCountFrom : BadCarryState → ℕ → ℕ

Recursive dynamic-programming count for words read from a given state.

Equations

• GKPCarry.badCarryWordCountFrom x✝ 0 = if x✝ = GKPCarry.BadCarryState.good then 0 else 1
• GKPCarry.badCarryWordCountFrom x✝ length.succ = ∑ digit : Fin 3, GKPCarry.badCarryWordCountFrom (GKPCarry.badCarryStateStep x✝ ↑digit) length

theorem GKPCarry.card_badCarryWordsFrom_eq_count (state : BadCarryState) (length : ℕ) : Fintype.card (BadCarryWordsFrom state length) = badCarryWordCountFrom state length

The recursive count is the actual cardinality of the corresponding finite word type.

theorem GKPCarry.badCarryWordCountFrom_good (length : ℕ) : badCarryWordCountFrom BadCarryState.good length = 0

theorem GKPCarry.badCarryWordCountFrom_oneCarryNoCarry (length : ℕ) : badCarryWordCountFrom BadCarryState.oneCarryNoCarry length = 2 ^ length

theorem GKPCarry.badCarryWordCountFrom_oneCarryOut_succ (length : ℕ) : badCarryWordCountFrom BadCarryState.oneCarryOut (length + 1) = 2 ^ length

theorem GKPCarry.badCarryWordCountFrom_zeroCarry_succ (length : ℕ) : badCarryWordCountFrom BadCarryState.zeroCarry (length + 1) = 2 * badCarryWordCountFrom BadCarryState.zeroCarry length + badCarryWordCountFrom BadCarryState.oneCarryOut length

theorem GKPCarry.badCarryWordCountFrom_zeroCarry_closed (n : ℕ) : badCarryWordCountFrom BadCarryState.zeroCarry (n + 2) = (n + 7) * 2 ^ n

Exact dynamic-programming count of deficient-carry ternary words.

theorem GKPCarry.card_badCarryWords (n : ℕ) : Fintype.card (BadCarryWords (n + 2)) = (n + 7) * 2 ^ n

Headline enumeration theorem: among all ternary words of length n + 2, exactly (n + 7) * 2 ^ n have fewer than two doubling carries.

theorem GKPCarry.card_allTernaryWords (n : ℕ) : Fintype.card (List.Vector (Fin 3) (n + 2)) = 3 ^ (n + 2)

The ambient set contains all 3 ^ (n + 2) ternary words.