Linear-time canonical binary addition -- definitions

This module defines a finite-state ripple-carry scan over two preserved little-endian binary work tapes. Each scan step appends one sum bit to a fresh result tape. A composed wrapper then rewinds all three owned tapes.

def Complexity.BinaryRippleAdd.sumBit (carry lhs rhs : Bool) : Bool

The output bit of a one-column binary addition with incoming carry.

Equations

• Complexity.BinaryRippleAdd.sumBit carry lhs rhs = (lhs ^^ rhs ^^ carry)

def Complexity.BinaryRippleAdd.carryBit (carry lhs rhs : Bool) : Bool

The outgoing carry of a one-column binary addition.

Equations

• Complexity.BinaryRippleAdd.carryBit carry lhs rhs = (lhs && rhs || carry && lhs || carry && rhs)

@[irreducible]

def Complexity.BinaryRippleAdd.ripple : Bool → List Bool → List Bool → List Bool

Ripple-carry addition on little-endian bit strings, padding a missing side with zero and emitting a final high bit exactly when the carry remains set.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.BinaryRippleAdd.ripple false [] [] = []
• Complexity.BinaryRippleAdd.ripple true [] [] = [true]

inductive Complexity.TM.BinaryRippleAddPhase : Type

Carry-bearing scan states followed by the unique halt state.

• scan (carry : Bool) : BinaryRippleAddPhase
• done : BinaryRippleAddPhase

def Complexity.TM.instDecidableEqBinaryRippleAddPhase.decEq (x✝ x✝¹ : BinaryRippleAddPhase) : Decidable (x✝ = x✝¹)

Equations

• Complexity.TM.instDecidableEqBinaryRippleAddPhase.decEq (Complexity.TM.BinaryRippleAddPhase.scan a) (Complexity.TM.BinaryRippleAddPhase.scan b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleAddPhase.decEq (Complexity.TM.BinaryRippleAddPhase.scan carry) Complexity.TM.BinaryRippleAddPhase.done = isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleAddPhase.decEq Complexity.TM.BinaryRippleAddPhase.done (Complexity.TM.BinaryRippleAddPhase.scan carry) = isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleAddPhase.decEq Complexity.TM.BinaryRippleAddPhase.done Complexity.TM.BinaryRippleAddPhase.done = isTrue ⋯

@[implicit_reducible]

instance Complexity.TM.instDecidableEqBinaryRippleAddPhase : DecidableEq BinaryRippleAddPhase

Equations

• Complexity.TM.instDecidableEqBinaryRippleAddPhase = Complexity.TM.instDecidableEqBinaryRippleAddPhase.decEq

@[implicit_reducible]

instance Complexity.TM.instFintypeBinaryRippleAddPhase : Fintype BinaryRippleAddPhase

BinaryRippleAddPhase is finite, as required by the concrete machine model.

Equations

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

structure Complexity.TM.BinaryRippleAddDistinct {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) : Prop

Pairwise distinct work tapes used by the ripple-carry adder.

• lhs_rhs : lhsIdx ≠ rhsIdx
• lhs_result : lhsIdx ≠ resultIdx
• rhs_result : rhsIdx ≠ resultIdx

def Complexity.TM.binaryRippleAddScanTM {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) : TM n

Scan two canonical little-endian operands and append their sum to a fresh result tape. Operand cells are written back unchanged. An exhausted operand stays on its first blank while the longer operand continues to advance.

Equations

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

def Complexity.TM.binaryRippleAddScanTime (lhs rhs : List Bool) : ℕ

Exact number of scan transitions, including the final simultaneous-blank transition.

Equations

• Complexity.TM.binaryRippleAddScanTime lhs rhs = max lhs.length rhs.length + 1

def Complexity.TM.binaryRippleAddTM {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) : TM n

Scan the operands into a fresh result and then rewind both operands and the result to cell one.

Equations

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

def Complexity.TM.binaryRippleAddTime (lhs rhs : ℕ) : ℕ

Linear width bound for the scan, three rewinds, and three composition seams.

Equations

• Complexity.TM.binaryRippleAddTime lhs rhs = max lhs.size rhs.size + lhs.size + rhs.size + (lhs + rhs).size + 13