The regular language of deficient ternary carries

A four-state deterministic automaton recognizes the ternary words whose doubling creates fewer than two carries. Its language is classified as three explicit digit patterns. This turns the remaining GKP power-of-two condition into an exact regular-language avoidance statement.

inductive GKPCarry.BadCarryState : Type

State of the deficient-carry automaton while scanning little-endian ternary digits.

• zeroCarry : BadCarryState
• oneCarryOut : BadCarryState
• oneCarryNoCarry : BadCarryState
• good : BadCarryState

@[implicit_reducible]

instance GKPCarry.instDecidableEqBadCarryState : DecidableEq BadCarryState

Equations

• GKPCarry.instDecidableEqBadCarryState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance GKPCarry.instReprBadCarryState : Repr BadCarryState

Equations

• GKPCarry.instReprBadCarryState = { reprPrec := GKPCarry.instReprBadCarryState.repr }

def GKPCarry.instReprBadCarryState.repr : BadCarryState → ℕ → Std.Format

Equations

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

def GKPCarry.badCarryStateStep : BadCarryState → ℕ → BadCarryState

One transition of the deficient-carry automaton.

Equations

• One or more equations did not get rendered due to their size.
• GKPCarry.badCarryStateStep GKPCarry.BadCarryState.good x✝ = GKPCarry.BadCarryState.good
• GKPCarry.badCarryStateStep GKPCarry.BadCarryState.oneCarryOut x✝ = if x✝ = 0 then GKPCarry.BadCarryState.oneCarryNoCarry else GKPCarry.BadCarryState.good
• GKPCarry.badCarryStateStep GKPCarry.BadCarryState.oneCarryNoCarry x✝ = if x✝ < 2 then GKPCarry.BadCarryState.oneCarryNoCarry else GKPCarry.BadCarryState.good

def GKPCarry.badCarryStateAux : List ℕ → BadCarryState → BadCarryState

Run the automaton from an arbitrary state.

Equations

• GKPCarry.badCarryStateAux [] x✝ = x✝
• GKPCarry.badCarryStateAux (digit :: digits) x✝ = GKPCarry.badCarryStateAux digits (GKPCarry.badCarryStateStep x✝ digit)

def GKPCarry.badCarryState (digits : List ℕ) : BadCarryState

Run the automaton from its initial state.

Equations

• GKPCarry.badCarryState digits = GKPCarry.badCarryStateAux digits GKPCarry.BadCarryState.zeroCarry

def GKPCarry.badCarryLanguage (digits : List ℕ) : Bool

Boolean membership in the deficient-carry language.

Equations

• GKPCarry.badCarryLanguage digits = decide (GKPCarry.badCarryState digits ≠ GKPCarry.BadCarryState.good)

def GKPCarry.BadCarryState.incomingCarry : BadCarryState → ℕ

Incoming arithmetic carry represented by an automaton state.

Equations

• GKPCarry.BadCarryState.zeroCarry.incomingCarry = 0
• GKPCarry.BadCarryState.oneCarryOut.incomingCarry = 1
• GKPCarry.BadCarryState.oneCarryNoCarry.incomingCarry = 0
• GKPCarry.BadCarryState.good.incomingCarry = 0

def GKPCarry.BadCarryState.neededCarries : BadCarryState → ℕ

Additional carries required to reach the accepting state.

Equations

• GKPCarry.BadCarryState.zeroCarry.neededCarries = 2
• GKPCarry.BadCarryState.oneCarryOut.neededCarries = 1
• GKPCarry.BadCarryState.oneCarryNoCarry.neededCarries = 1
• GKPCarry.BadCarryState.good.neededCarries = 0

theorem GKPCarry.badCarryStateAux_good (digits : List ℕ) : badCarryStateAux digits BadCarryState.good = BadCarryState.good

theorem GKPCarry.badCarryStateAux_ne_good_iff_carryCount_lt_needed (digits : List ℕ) : (∀ digit ∈ digits, digit < 3) → ∀ (state : BadCarryState), badCarryStateAux digits state ≠ BadCarryState.good ↔ ternaryDoubleCarryCountAux digits state.incomingCarry < state.neededCarries

theorem GKPCarry.badCarryLanguage_true_iff_carryCount_lt_two {digits : List ℕ} (hdigits : ∀ digit ∈ digits, digit < 3) : badCarryLanguage digits = true ↔ ternaryDoubleCarryCount digits < 2

Automaton correctness: on valid ternary words, membership is equivalent to creating fewer than two carries under doubling.

Concrete classification of the language

def GKPCarry.badCarryAllZeroOrOne (digits : List ℕ) : Prop

Every digit in the word is 0 or 1.

Equations

• GKPCarry.badCarryAllZeroOrOne digits = ∀ digit ∈ digits, digit < 2

def GKPCarry.badCarryExactlyOneTopTwo (digits : List ℕ) : Prop

The unique digit 2 is the most significant digit.

Equations

• GKPCarry.badCarryExactlyOneTopTwo digits = ∃ (lows : List ℕ), GKPCarry.badCarryAllZeroOrOne lows ∧ digits = lows ++ [2]

def GKPCarry.badCarryExactlyOneTwoFollowedByZero (digits : List ℕ) : Prop

The unique digit 2 is followed by a higher 0, with all other digits equal to 0 or 1.

Equations

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

def GKPCarry.badCarryLanguageShape (digits : List ℕ) : Prop

The union of the three concrete deficient-carry shapes.

Equations

• GKPCarry.badCarryLanguageShape digits = (GKPCarry.badCarryAllZeroOrOne digits ∨ GKPCarry.badCarryExactlyOneTopTwo digits ∨ GKPCarry.badCarryExactlyOneTwoFollowedByZero digits)

theorem GKPCarry.badCarryAllZeroOrOne_cons {digit : ℕ} {digits : List ℕ} : badCarryAllZeroOrOne (digit :: digits) ↔ digit < 2 ∧ badCarryAllZeroOrOne digits

theorem GKPCarry.badCarryAllZeroOrOne_cons_of_lt {digit : ℕ} {digits : List ℕ} (hdigit : digit < 2) : badCarryAllZeroOrOne (digit :: digits) ↔ badCarryAllZeroOrOne digits

theorem GKPCarry.badCarryExactlyOneTopTwo_cons_of_lt {digit : ℕ} {digits : List ℕ} (hdigit : digit < 2) : badCarryExactlyOneTopTwo (digit :: digits) ↔ badCarryExactlyOneTopTwo digits

theorem GKPCarry.badCarryExactlyOneTwoFollowedByZero_cons_of_lt {digit : ℕ} {digits : List ℕ} (hdigit : digit < 2) : badCarryExactlyOneTwoFollowedByZero (digit :: digits) ↔ badCarryExactlyOneTwoFollowedByZero digits

theorem GKPCarry.badCarryLanguageShape_cons_of_lt {digit : ℕ} {digits : List ℕ} (hdigit : digit < 2) : badCarryLanguageShape (digit :: digits) ↔ badCarryLanguageShape digits

theorem GKPCarry.badCarryStateAux_oneCarryNoCarry_ne_good_iff_allZeroOrOne (digits : List ℕ) : badCarryStateAux digits BadCarryState.oneCarryNoCarry ≠ BadCarryState.good ↔ badCarryAllZeroOrOne digits

theorem GKPCarry.badCarryStateAux_oneCarryOut_ne_good_iff (digits : List ℕ) : badCarryStateAux digits BadCarryState.oneCarryOut ≠ BadCarryState.good ↔ digits = [] ∨ ∃ (highs : List ℕ), badCarryAllZeroOrOne highs ∧ digits = 0 :: highs

theorem GKPCarry.badCarryLanguageShape_two_cons_iff {digits : List ℕ} : badCarryLanguageShape (2 :: digits) ↔ digits = [] ∨ ∃ (highs : List ℕ), badCarryAllZeroOrOne highs ∧ digits = 0 :: highs

theorem GKPCarry.badCarryLanguageShape_cons_of_invalid {digit : ℕ} {digits : List ℕ} (hsmall : ¬digit < 2) (htwo : digit ≠ 2) : ¬badCarryLanguageShape (digit :: digits)

theorem GKPCarry.badCarryStateAux_zeroCarry_ne_good_iff_shape (digits : List ℕ) : badCarryStateAux digits BadCarryState.zeroCarry ≠ BadCarryState.good ↔ badCarryLanguageShape digits

theorem GKPCarry.badCarryLanguage_true_iff_shape (digits : List ℕ) : badCarryLanguage digits = true ↔ badCarryLanguageShape digits

Exact classification of the deficient-carry language into three explicit little-endian digit shapes.