Bounded encoded sparse-store update — controller definitions

The fixed controller owns thirteen pairwise-distinct work tapes. It scans a runtime-counted entry stream, copying misses, replacing or deleting a hit, and appending a fresh nonzero entry only when the old count is exhausted without a match. A second count tape tracks the output-store cardinality.

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

Thirteen pairwise-distinct tapes used by encoded sparse-store update.

• idx : Fin 13 → Fin n

  Assignment order: nine entry-match tapes, remaining count, replacement value, found flag, and output count.

• injective : Function.Injective self.idx

  The complete assignment is injective.

def Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.entry {n : ℕ} (tapes : EntryUpdateTapes n) : EntryMatchTapes n

The nine-tape decode-and-match assignment.

Equations

• tapes.entry = { idx := fun (i : Fin 9) => tapes.idx ⟨↑i, ⋯⟩, injective := ⋯ }

def Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.remaining {n : ℕ} (tapes : EntryUpdateTapes n) : Fin n

Runtime number of old entries still unread.

Equations

• tapes.remaining = tapes.idx 9

def Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.replacement {n : ℕ} (tapes : EntryUpdateTapes n) : Fin n

Canonical source containing the requested new value.

Equations

• tapes.replacement = tapes.idx 10

def Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.found {n : ℕ} (tapes : EntryUpdateTapes n) : Fin n

One-bit flag recording whether a matching old address has been seen.

Equations

• tapes.found = tapes.idx 11

def Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.resultCount {n : ℕ} (tapes : EntryUpdateTapes n) : Fin n

Canonical count of entries emitted by the completed update.

Equations

• tapes.resultCount = tapes.idx 12

theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.ne {n : ℕ} (tapes : EntryUpdateTapes n) {i j : Fin 13} (h : i ≠ j) : tapes.idx i ≠ tapes.idx j

Distinct indices in the thirteen-tape assignment remain distinct.

def Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.replace {n : ℕ} (tapes : EntryUpdateTapes n) : EntryReplaceTapes n

Replacement-emission view of the update assignment.

Equations

• tapes.replace = { entry := tapes.entry, replacement := tapes.replacement, replacement_ne := ⋯ }

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.replace_entry {n : ℕ} (tapes : EntryUpdateTapes n) : tapes.replace.entry = tapes.entry

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateTapes.replace_replacement {n : ℕ} (tapes : EntryUpdateTapes n) : tapes.replace.replacement = tapes.replacement

def Complexity.RAM.RegisterStore.Machine.EntryUpdateFrame {n : ℕ} (tapes : EntryUpdateTapes n) (initialWork finalWork : Fin n → Tape) : Prop

Exact preservation predicate outside the thirteen tapes owned by update.

Equations

• Complexity.RAM.RegisterStore.Machine.EntryUpdateFrame tapes initialWork finalWork = ∀ (i : Fin n), (∀ (slot : Fin 13), i ≠ tapes.idx slot) → finalWork i = initialWork i

structure Complexity.RAM.RegisterStore.Machine.EntryUpdateOutcome {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Auditable final work-tape contract for one encoded sparse-store update.

• ready : EntryScanReady tapes.entry [] address.bits finalWork finalWork

  The encoded old store has been consumed and all entry scratch is reset.

• replacement : finalWork tapes.replacement = initialWork tapes.replacement

  The external replacement source is restored literally.

• remaining : (finalWork tapes.remaining).HasBinaryNat 0

  The runtime old-entry counter is exhausted.

• found : (finalWork tapes.found).HasBinaryNat (if address ∈ List.map Prod.fst store then 1 else 0)

  The flag records whether the old store contained the updated address.

• resultCount : (finalWork tapes.resultCount).HasBinaryNat (List.length (write store address newValue))

  The result counter is the exact cardinality of the pure sparse write.

• frame : EntryUpdateFrame tapes initialWork finalWork

  Every work tape outside the fixed assignment is unchanged.

def Complexity.RAM.RegisterStore.Machine.entryUpdatePostEmitHead {n : ℕ} (tapes : EntryUpdateTapes n) (entry : Entry) (i : Fin n) : ℕ

Canonical head profile after an old decoded entry has been emitted.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateReadyCleanupTime {n : ℕ} (tapes : EntryUpdateTapes n) (entry : Entry) (address : ℕ) : ℕ

Work-independent cleanup bound when deletion emits no entry.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdatePostEmitCleanupTime {n : ℕ} (tapes : EntryUpdateTapes n) (entry : Entry) (address : ℕ) : ℕ

Work-independent cleanup bound after miss-copy or replacement emission.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateMissTime {n : ℕ} (tapes : EntryUpdateTapes n) (entry : Entry) (address : ℕ) : ℕ

Fixed bound for copying one unmatched entry and restoring scratch.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateReplaceTime {n : ℕ} (tapes : EntryUpdateTapes n) (entry : Entry) (address newValue : ℕ) : ℕ

Fixed bound for emitting a replacement and restoring scratch.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateCountTime (total : ℕ) : ℕ

Uniform binary counter-update budget below the initial store size.

Equations

• Complexity.RAM.RegisterStore.Machine.entryUpdateCountTime total = 2 * total.size + 2

def Complexity.RAM.RegisterStore.Machine.entryUpdateBranchTime {n : ℕ} (tapes : EntryUpdateTapes n) (entry : Entry) (address newValue total : ℕ) : ℕ

Maximum controller branch cost after one readable comparison.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateIterationTime {n : ℕ} (tapes : EntryUpdateTapes n) (entry : Entry) (rest : Store) (address newValue total : ℕ) : ℕ

Fixed cost of one positive-count iteration, excluding the recursive tail.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateLoopTime {n : ℕ} (tapes : EntryUpdateTapes n) (address newValue total : ℕ) : Store → ℕ

Recursive fixed bound for updating a remaining sparse-store suffix.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateTime {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue : ℕ) : ℕ

Public runtime bound for one complete encoded sparse-store update.

Equations

• Complexity.RAM.RegisterStore.Machine.entryUpdateTime tapes store address newValue = Complexity.RAM.RegisterStore.Machine.entryUpdateLoopTime tapes address newValue (List.length store) store

inductive Complexity.RAM.RegisterStore.Machine.EntryUpdateQ {n : ℕ} (tapes : EntryUpdateTapes n) : Type

Controller states, including each checked nested machine.

• test {n : ℕ} {tapes : EntryUpdateTapes n} : EntryUpdateQ tapes
• matching {n : ℕ} {tapes : EntryUpdateTapes n} : (entryMatchReadTM tapes.entry).Q → EntryUpdateQ tapes
• miss {n : ℕ} {tapes : EntryUpdateTapes n} : (entryMissCopyTM tapes.entry).Q → EntryUpdateQ tapes
• delete {n : ℕ} {tapes : EntryUpdateTapes n} : (entryMissCleanupTM tapes.entry).Q → EntryUpdateQ tapes
• replace {n : ℕ} {tapes : EntryUpdateTapes n} : (entryReplaceCleanupTM tapes.replace).Q → EntryUpdateQ tapes
• append {n : ℕ} {tapes : EntryUpdateTapes n} : (entryAppendRestoreTM tapes.replace).Q → EntryUpdateQ tapes
• remaining {n : ℕ} {tapes : EntryUpdateTapes n} : (TM.binaryPredTM tapes.remaining).Q → EntryUpdateQ tapes
• deleteCount {n : ℕ} {tapes : EntryUpdateTapes n} : (TM.binaryPredTM tapes.resultCount).Q → EntryUpdateQ tapes
• appendCount {n : ℕ} {tapes : EntryUpdateTapes n} : (TM.binarySuccTM tapes.resultCount).Q → EntryUpdateQ tapes
• done {n : ℕ} {tapes : EntryUpdateTapes n} : EntryUpdateQ tapes

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instDecidableEqEntryUpdateQ {n✝ : ℕ} {tapes✝ : EntryUpdateTapes n✝} : DecidableEq (EntryUpdateQ tapes✝)

Equations

• Complexity.RAM.RegisterStore.Machine.instDecidableEqEntryUpdateQ = Complexity.RAM.RegisterStore.Machine.instDecidableEqEntryUpdateQ.decEq

def Complexity.RAM.RegisterStore.Machine.instDecidableEqEntryUpdateQ.decEq {n✝ : ℕ} {tapes✝ : EntryUpdateTapes n✝} (x✝ x✝¹ : EntryUpdateQ tapes✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instFintypeEntryUpdateQ {n : ℕ} (tapes : EntryUpdateTapes n) : Fintype (EntryUpdateQ tapes)

The update controller has finitely many states because every nested machine state type is finite.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateTM {n : ℕ} (tapes : EntryUpdateTapes n) : TM n

Fixed runtime-counted update controller. The old remaining count reaches zero on every complete scan; the result count is decremented only for deletion and incremented only for absent-address append.

Equations

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