RAM snapshot word-width decoder — definitions

RAM.RegisterStore.Machine.wordWidthTM is the first concrete Turing-machine phase of the reverse RAM simulation. It scans the unary-width prefix of one self-delimiting snapshot word and increments a canonical binary counter once per 1. The source head stops on the zero separator, ready for the payload copy phase.

def Complexity.RAM.RegisterStore.Machine.wordWidthTM {n : ℕ} (sourceIdx widthIdx : Fin n) : TM n

Scan the unary prefix on work tape sourceIdx and store its length in canonical little-endian binary on work tape widthIdx. The two indices must be distinct for the semantic theorem.

Equations

• Complexity.RAM.RegisterStore.Machine.wordWidthTM sourceIdx widthIdx = Complexity.TM.forWorkOnesTM sourceIdx (Complexity.TM.binarySuccTM widthIdx)

def Complexity.RAM.RegisterStore.Machine.wordWidthTime (width : ℕ) : ℕ

Exact transition count for decoding a unary prefix of length width.

Equations

• Complexity.RAM.RegisterStore.Machine.wordWidthTime width = Complexity.TM.forWorkOnesLoopTime Complexity.TM.binarySuccTime 0 width

inductive Complexity.RAM.RegisterStore.Machine.PayloadBitPhase : Type

Control states for copying one fixed-width payload bit.

• copy : PayloadBitPhase
• done : PayloadBitPhase

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instDecidableEqPayloadBitPhase : DecidableEq PayloadBitPhase

Equations

• Complexity.RAM.RegisterStore.Machine.instDecidableEqPayloadBitPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instFintypePayloadBitPhase : Fintype PayloadBitPhase

PayloadBitPhase has exactly two states.

Equations

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

def Complexity.RAM.RegisterStore.Machine.payloadBitTM {n : ℕ} (sourceIdx targetIdx : Fin n) : TM n

Copy the bit under sourceIdx to the append position on targetIdx, advancing both heads once. The semantic theorem assumes distinct indices and that the source reads a bit.

Equations

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

structure Complexity.RAM.RegisterStore.Machine.PayloadLoopDistinct {n : ℕ} (sourceIdx targetIdx counterIdx widthIdx : Fin n) : Prop

Pairwise distinct work tapes used by the bounded payload decoder.

• source_target : sourceIdx ≠ targetIdx

  Source and target tapes are distinct.

• source_counter : sourceIdx ≠ counterIdx

  Source and loop-counter tapes are distinct.

• source_width : sourceIdx ≠ widthIdx

  Source and width-limit tapes are distinct.

• target_counter : targetIdx ≠ counterIdx

  Target and loop-counter tapes are distinct.

• target_width : targetIdx ≠ widthIdx

  Target and width-limit tapes are distinct.

• counter_width : counterIdx ≠ widthIdx

  Counter and width-limit tapes are distinct.

def Complexity.RAM.RegisterStore.Machine.wordPayloadTM {n : ℕ} (sourceIdx targetIdx counterIdx widthIdx : Fin n) : TM n

Copy exactly the number of payload bits recorded on widthIdx. counterIdx is the canonical binary loop counter and targetIdx is an appendable binary prefix.

Equations

• Complexity.RAM.RegisterStore.Machine.wordPayloadTM sourceIdx targetIdx counterIdx widthIdx = (Complexity.RAM.RegisterStore.Machine.payloadBitTM sourceIdx targetIdx).binaryForTM counterIdx widthIdx

def Complexity.RAM.RegisterStore.Machine.wordPayloadTime (width : ℕ) : ℕ

Exact transition count for a complete fixed-width payload copy.

Equations

• Complexity.RAM.RegisterStore.Machine.wordPayloadTime width = Complexity.TM.binaryForLoopTime (fun (x : ℕ) => 1) width 0 width

inductive Complexity.RAM.RegisterStore.Machine.WordSeparatorPhase : Type

Control states for consuming the zero separator between a word's unary width and fixed-width payload.

• skip : WordSeparatorPhase
• done : WordSeparatorPhase

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instDecidableEqWordSeparatorPhase : DecidableEq WordSeparatorPhase

Equations

• Complexity.RAM.RegisterStore.Machine.instDecidableEqWordSeparatorPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instFintypeWordSeparatorPhase : Fintype WordSeparatorPhase

WordSeparatorPhase has exactly two states.

Equations

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

def Complexity.RAM.RegisterStore.Machine.wordSeparatorTM {n : ℕ} (sourceIdx : Fin n) : TM n

Consume exactly one zero separator on the selected source work tape.

Equations

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

def Complexity.RAM.RegisterStore.Machine.wordDecodeTM {n : ℕ} (sourceIdx targetIdx counterIdx widthIdx : Fin n) : TM n

Decode one complete self-delimiting word by scanning its unary width, consuming the separator, and copying exactly that many payload bits.

Equations

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

def Complexity.RAM.RegisterStore.Machine.wordDecodeTime (width : ℕ) : ℕ

Exact transition count for complete word decoding, including both sequential-composition seams.

Equations

• Complexity.RAM.RegisterStore.Machine.wordDecodeTime width = Complexity.RAM.RegisterStore.Machine.wordWidthTime width + 1 + (1 + 1 + Complexity.RAM.RegisterStore.Machine.wordPayloadTime width)

Linear unary-marker decoder

structure Complexity.RAM.RegisterStore.Machine.LinearWordDistinct {n : ℕ} (sourceIdx targetIdx markerIdx : Fin n) : Prop

Pairwise-distinct source, target, and unary-marker tapes for the optimized word decoder.

• source_target : sourceIdx ≠ targetIdx

  Source and target tapes are distinct.

• source_marker : sourceIdx ≠ markerIdx

  Source and marker tapes are distinct.

• target_marker : targetIdx ≠ markerIdx

  Target and marker tapes are distinct.

inductive Complexity.RAM.RegisterStore.Machine.LinearWordPhase : Type

Control phases of the optimized self-delimiting word decoder.

• mark : LinearWordPhase

  Copy the unary width prefix to the marker tape.

• rewind : LinearWordPhase

  Rewind the copied unary marker while parking the payload cursor.

• copy : LinearWordPhase

  Consume one marker and copy one payload bit per transition.

• done : LinearWordPhase

  Halt after the marker is exhausted.

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instDecidableEqLinearWordPhase : DecidableEq LinearWordPhase

Equations

• Complexity.RAM.RegisterStore.Machine.instDecidableEqLinearWordPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instFintypeLinearWordPhase : Fintype LinearWordPhase

LinearWordPhase has exactly four states.

Equations

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

def Complexity.RAM.RegisterStore.Machine.wordDecodeLinearTM {n : ℕ} (sourceIdx targetIdx markerIdx : Fin n) : TM n

Decode one unary-width/fixed-payload word in a single linear pass.

The prefix pass copies one unary marker per width bit. After rewinding that marker tape, the payload pass advances source, target, and marker together. This removes the old payload loop's repeated full binary-counter comparison. The marker tape starts as an empty appendable prefix and finishes containing width ones with its head on the following blank.

Equations

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

def Complexity.RAM.RegisterStore.Machine.wordDecodeLinearTime (width : ℕ) : ℕ

Exact transition count of the optimized decoder on a well-formed width width word.

Equations

• Complexity.RAM.RegisterStore.Machine.wordDecodeLinearTime width = 3 * width + 3