Counting deficient-carry ternary units

Powers of two modulo a power of three range over unit residues, whose least significant ternary digit is nonzero. This file refines the full-word automaton count to that unit slice. Among unit words of length n + 3, exactly (n + 9) * 2 ^ n create fewer than two doubling carries.

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

Natural value of a fixed-length ternary word.

Equations

• GKPCarry.ternaryWordValue word = Nat.ofDigits 3 (GKPCarry.ternaryWordDigits word)

theorem GKPCarry.ternaryWordValue_lt {length : ℕ} (word : List.Vector (Fin 3) length) : ternaryWordValue word < 3 ^ length

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

The value of a ternary word, packaged in its complete residue block.

Equations

• GKPCarry.ternaryWordValueFin word = ⟨GKPCarry.ternaryWordValue word, ⋯⟩

theorem GKPCarry.ternaryWordValueFin_injective (length : ℕ) : Function.Injective ternaryWordValueFin

@[reducible, inline]

abbrev GKPCarry.TernaryUnitWords (length : ℕ) : Type

Fixed-length ternary words with a nonzero least significant digit. The parameter is the tail length, so the full word has length length + 1.

Equations

• GKPCarry.TernaryUnitWords length = { word : List.Vector (Fin 3) (length + 1) // ↑word.head ≠ 0 }

theorem GKPCarry.ternaryWordValue_mod_three {length : ℕ} (word : List.Vector (Fin 3) (length + 1)) : ternaryWordValue word % 3 = ↑word.head

theorem GKPCarry.ternaryWordValue_coprime_three_pow_iff {length : ℕ} (word : List.Vector (Fin 3) (length + 1)) : (ternaryWordValue word).Coprime (3 ^ (length + 1)) ↔ ↑word.head ≠ 0

def GKPCarry.ternaryUnitWordsHeadTailEquiv (length : ℕ) : TernaryUnitWords length ≃ { digit : Fin 3 // ↑digit ≠ 0 } × List.Vector (Fin 3) length

Split a unit word into its nonzero head digit and its remaining digits.

Equations

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

theorem GKPCarry.card_ternaryUnitWords (length : ℕ) : Fintype.card (TernaryUnitWords length) = 2 * 3 ^ length

There are 2 * 3 ^ length unit words with length + 1 ternary digits.

def GKPCarry.ternaryUnitWordToUnit (length : ℕ) : TernaryUnitWords length → (ZMod (3 ^ (length + 1)))ˣ

Convert a ternary unit word to the corresponding unit modulo a power of three.

Equations

• GKPCarry.ternaryUnitWordToUnit length word = ZMod.unitOfCoprime (GKPCarry.ternaryWordValue ↑word) ⋯

theorem GKPCarry.ternaryUnitWordToUnit_injective (length : ℕ) : Function.Injective (ternaryUnitWordToUnit length)

noncomputable def GKPCarry.ternaryUnitWordEquiv (length : ℕ) : TernaryUnitWords length ≃ (ZMod (3 ^ (length + 1)))ˣ

Unit words are equivalent to the full unit group modulo the corresponding power of three.

Equations

• GKPCarry.ternaryUnitWordEquiv length = Equiv.ofBijective (GKPCarry.ternaryUnitWordToUnit length) ⋯

@[simp]

theorem GKPCarry.ternaryUnitWordEquiv_apply (length : ℕ) (word : TernaryUnitWords length) : (ternaryUnitWordEquiv length) word = ternaryUnitWordToUnit length word

theorem GKPCarry.val_ternaryUnitWordEquiv_apply (length : ℕ) (word : TernaryUnitWords length) : (↑((ternaryUnitWordEquiv length) word)).val = ternaryWordValue ↑word

theorem GKPCarry.ternaryDoubleCarryCountAux_replicate_zero (count carry : ℕ) (hcarry : carry ≤ 1) : ternaryDoubleCarryCountAux (List.replicate count 0) carry = 0

theorem GKPCarry.ternaryDoubleCarryCountAux_append_replicate_zero (digits : List ℕ) (count carry : ℕ) (hcarry : carry ≤ 1) : ternaryDoubleCarryCountAux (digits ++ List.replicate count 0) carry = ternaryDoubleCarryCountAux digits carry

theorem GKPCarry.ternaryDoubleCarryCount_append_replicate_zero (digits : List ℕ) (count : ℕ) : ternaryDoubleCarryCount (digits ++ List.replicate count 0) = ternaryDoubleCarryCount digits

theorem GKPCarry.ternaryDoubleCarryCount_word_eq_value {length : ℕ} (word : List.Vector (Fin 3) length) : ternaryDoubleCarryCount (ternaryWordDigits word) = ternaryDoubleCarryCount (Nat.digits 3 (ternaryWordValue word))

Fixed-length leading zeroes do not change the carry count, so a word and the canonical ternary expansion of its value have the same count.

Deficient-carry unit words

@[reducible, inline]

abbrev GKPCarry.UnitBadCarryWords (length : ℕ) : Type

Unit words whose doubling produces fewer than two carries.

Equations

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

def GKPCarry.unitBadCarryWordsToSum (length : ℕ) : UnitBadCarryWords length → BadCarryWordsFrom BadCarryState.zeroCarry length ⊕ BadCarryWordsFrom BadCarryState.oneCarryOut length

Remove the nonzero leading digit and record the automaton state it enters.

Equations

• GKPCarry.unitBadCarryWordsToSum length word = if hone : ↑(↑↑word).head = 1 then Sum.inl ⟨(↑↑word).tail, ⋯⟩ else Sum.inr ⟨(↑↑word).tail, ⋯⟩

def GKPCarry.unitBadCarryWordsEquiv (length : ℕ) : UnitBadCarryWords length ≃ BadCarryWordsFrom BadCarryState.zeroCarry length ⊕ BadCarryWordsFrom BadCarryState.oneCarryOut length

Peeling the nonzero least significant digit splits deficient unit words into the states reached by digit 1 and digit 2.

Equations

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

theorem GKPCarry.card_unitBadCarryWords (n : ℕ) : Fintype.card (UnitBadCarryWords (n + 2)) = (n + 9) * 2 ^ n

Exact deficient-carry count on ternary unit words of length n + 3.