Sparse-entry replacement — definitions

The replacement branch emits the matched address paired with a distinct canonical new-value tape, rewinds that external value source, and restores the ordinary next-entry scan invariant.

structure Complexity.RAM.RegisterStore.Machine.EntryReplaceTapes (n : ℕ) : Type

Entry-match tapes plus a distinct source containing the replacement value.

• entry : EntryMatchTapes n

  The nine tapes used to decode and match the old entry.

• replacement : Fin n

  Canonical new-value source.

• replacement_ne (i : Fin 9) : self.replacement ≠ self.entry.idx i

  The replacement source is outside the complete entry-match assignment.

def Complexity.RAM.RegisterStore.Machine.EntryReplaceTapes.encodeTapes {n : ℕ} (tapes : EntryReplaceTapes n) : EntryEncodeTapes n

Emit the matched decoded address paired with the replacement source.

Equations

• tapes.encodeTapes = { address := tapes.entry.address, value := tapes.replacement, ne := ⋯ }

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryReplaceTapes.encodeTapes_address {n : ℕ} (tapes : EntryReplaceTapes n) : tapes.encodeTapes.address = tapes.entry.address

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryReplaceTapes.encodeTapes_value {n : ℕ} (tapes : EntryReplaceTapes n) : tapes.encodeTapes.value = tapes.replacement

def Complexity.RAM.RegisterStore.Machine.entryReplaceReadyWork {n : ℕ} (tapes : EntryReplaceTapes n) (entry : Entry) (work : Fin n → Tape) (i : Fin n) : Tape

Exact work family after replacement emission and restoration of the external replacement cursor. Only the decoded address head remains changed.

Equations

• Complexity.RAM.RegisterStore.Machine.entryReplaceReadyWork tapes entry work i = if i = tapes.entry.address then { head := entry.1.bits.length + 1, cells := (work i).cells } else work i

def Complexity.RAM.RegisterStore.Machine.entryReplaceCleanupTM {n : ℕ} (tapes : EntryReplaceTapes n) : TM n

Emit the replacement entry, restore the replacement cursor, and clear all entry decoder/result scratch.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryReplaceCleanupTime {n : ℕ} (tapes : EntryReplaceTapes n) (entry : Entry) (newValue : ℕ) (queryBits : List Bool) (initialWork matchedWork : Fin n → Tape) : ℕ

Compositional runtime bound for replacement emission and cleanup.

Equations

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