Linear-time canonical binary subtraction -- definitions

This module defines a full-borrow scan over two preserved little-endian binary work tapes. The scan writes a fixed-width difference to a fresh result tape. A single backward pass then erases the complete result on underflow or removes only its redundant high zeros, while returning the result head to cell one.

def Complexity.BinaryRippleSub.diffBit (borrow lhs rhs : Bool) : Bool

The low output bit of one binary-subtraction column.

Equations

• Complexity.BinaryRippleSub.diffBit borrow lhs rhs = (lhs ^^ rhs ^^ borrow)

def Complexity.BinaryRippleSub.borrowBit (borrow lhs rhs : Bool) : Bool

The outgoing borrow of one binary-subtraction column.

Equations

• Complexity.BinaryRippleSub.borrowBit borrow lhs rhs = (!lhs && rhs || !lhs && borrow || rhs && borrow)

structure Complexity.BinaryRippleSub.ScanResult : Type

Raw fixed-width output of a borrow scan.

• bits : List Bool

  Little-endian difference bits produced so far.

• borrow : Bool

  Borrow propagated beyond the most-significant scanned column.

def Complexity.BinaryRippleSub.instDecidableEqScanResult.decEq (x✝ x✝¹ : ScanResult) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Complexity.BinaryRippleSub.instDecidableEqScanResult : DecidableEq ScanResult

Equations

• Complexity.BinaryRippleSub.instDecidableEqScanResult = Complexity.BinaryRippleSub.instDecidableEqScanResult.decEq

@[irreducible]

def Complexity.BinaryRippleSub.scan : Bool → List Bool → List Bool → ScanResult

Scan two little-endian bit strings with an incoming borrow. A missing side is padded by zero; the final borrow is retained separately from the raw bits.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.BinaryRippleSub.scan x✝ [] [] = { bits := [], borrow := x✝ }

def Complexity.BinaryRippleSub.trimHighZeros : List Bool → List Bool

Remove redundant most-significant zeros from a little-endian bit string.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.BinaryRippleSub.trimHighZeros [] = []

def Complexity.BinaryRippleSub.subtract (lhs rhs : List Bool) : List Bool

Canonical truncated subtraction semantics on arbitrary little-endian bit strings. Underflow is represented by canonical zero.

Equations

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

inductive Complexity.TM.BinaryRippleSubPhase : Type

Forward-borrow states, backward cleanup states, and the unique halt state.

• scan (borrow : Bool) : BinaryRippleSubPhase
• erase : BinaryRippleSubPhase
• trim (seenOne : Bool) : BinaryRippleSubPhase
• done : BinaryRippleSubPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqBinaryRippleSubPhase : DecidableEq BinaryRippleSubPhase

Equations

• Complexity.TM.instDecidableEqBinaryRippleSubPhase = Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq

def Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq (x✝ x✝¹ : BinaryRippleSubPhase) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq (Complexity.TM.BinaryRippleSubPhase.scan a) (Complexity.TM.BinaryRippleSubPhase.scan b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq (Complexity.TM.BinaryRippleSubPhase.scan borrow) Complexity.TM.BinaryRippleSubPhase.erase = isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq (Complexity.TM.BinaryRippleSubPhase.scan borrow) (Complexity.TM.BinaryRippleSubPhase.trim seenOne) = isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq (Complexity.TM.BinaryRippleSubPhase.scan borrow) Complexity.TM.BinaryRippleSubPhase.done = isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq Complexity.TM.BinaryRippleSubPhase.erase (Complexity.TM.BinaryRippleSubPhase.scan borrow) = isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq Complexity.TM.BinaryRippleSubPhase.erase Complexity.TM.BinaryRippleSubPhase.erase = isTrue ⋯
• Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq Complexity.TM.BinaryRippleSubPhase.erase (Complexity.TM.BinaryRippleSubPhase.trim seenOne) = isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq (Complexity.TM.BinaryRippleSubPhase.trim seenOne) (Complexity.TM.BinaryRippleSubPhase.scan borrow) = isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq (Complexity.TM.BinaryRippleSubPhase.trim seenOne) Complexity.TM.BinaryRippleSubPhase.erase = isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq (Complexity.TM.BinaryRippleSubPhase.trim a) (Complexity.TM.BinaryRippleSubPhase.trim b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq (Complexity.TM.BinaryRippleSubPhase.trim seenOne) Complexity.TM.BinaryRippleSubPhase.done = isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq Complexity.TM.BinaryRippleSubPhase.done (Complexity.TM.BinaryRippleSubPhase.scan borrow) = isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq Complexity.TM.BinaryRippleSubPhase.done (Complexity.TM.BinaryRippleSubPhase.trim seenOne) = isFalse ⋯
• Complexity.TM.instDecidableEqBinaryRippleSubPhase.decEq Complexity.TM.BinaryRippleSubPhase.done Complexity.TM.BinaryRippleSubPhase.done = isTrue ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeBinaryRippleSubPhase : Fintype BinaryRippleSubPhase

BinaryRippleSubPhase is finite, as required by the concrete TM model.

Equations

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

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

Pairwise distinct work tapes owned by the ripple-borrow subtractor.

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

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

Scan two canonical operands, write their fixed-width raw difference, and canonicalize the result while moving backward. A final borrow erases the whole result; otherwise high zeros are erased until the first high one is seen.

Equations

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

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

Forward scan time, including the simultaneous-blank turn.

Equations

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

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

Backward cleanup time, including the final marker bounce.

Equations

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

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

Exact time of the forward scan followed by backward canonicalization.

Equations

• Complexity.TM.binaryRippleSubCoreTime lhs rhs = 2 * max lhs.length rhs.length + 2

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

Canonical subtraction followed by rewinds of the two preserved operands.

Equations

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

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

Width-linear time bound for the core, two rewinds, and two seams.

Equations

• Complexity.TM.binaryRippleSubTime lhs rhs = 2 * max lhs.size rhs.size + lhs.size + rhs.size + 10