One bounded sparse-entry scan iteration — definitions

One iteration decodes and compares the next entry, branches directly on the readable equality flag, preserves the decoded value on a hit, and restores the next-iteration scratch invariant on a miss.

def Complexity.RAM.RegisterStore.Machine.entryScanBranchTM {n : ℕ} (tapes : EntryMatchTapes n) : TM n

Direct hit/miss branch selected by the readable equality-result tape.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryScanStepTM {n : ℕ} (tapes : EntryMatchTapes n) : TM n

Decode, compare, and dispatch one encoded sparse entry.

Equations

• Complexity.RAM.RegisterStore.Machine.entryScanStepTM tapes = (Complexity.RAM.RegisterStore.Machine.entryMatchReadTM tapes).seqTM (Complexity.RAM.RegisterStore.Machine.entryScanBranchTM tapes)

def Complexity.RAM.RegisterStore.Machine.entryScanBranchTime {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (queryBits : List Bool) (initialWork : Fin n → Tape) : ℕ

Coarse branch bound covering both the one-step hit and miss cleanup.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryScanStepTime {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (queryBits : List Bool) (initialWork : Fin n → Tape) : ℕ

Compositional time bound for one complete scan iteration.

Equations

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

structure Complexity.RAM.RegisterStore.Machine.EntryScanHit {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (rest queryBits : List Bool) (initialWork finalWork : Fin n → Tape) : Prop

Successful scan endpoint exposing the decoded value and the global external frame.

• addressEq : entry.1.bits = queryBits
• source : (finalWork tapes.source).HasBinarySuffix rest
• value : (finalWork tapes.value).HasBinaryPrefix entry.2.bits
• valueStart : (finalWork tapes.value).cells 0 = Γ.start
• query : (finalWork tapes.query).HasBinaryContent queryBits
• queryStart : (finalWork tapes.query).cells 0 = Γ.start
• result : (finalWork tapes.result).HasBinaryString [true]
• resultStart : (finalWork tapes.result).cells 0 = Γ.start
• parked (i : Fin n) : TM.Parked (finalWork i)
• frame (i : Fin n) : i ≠ tapes.source → i ≠ tapes.address → i ≠ tapes.value → i ≠ tapes.addressCounter → i ≠ tapes.addressWidth → i ≠ tapes.valueCounter → i ≠ tapes.valueWidth → i ≠ tapes.query → i ≠ tapes.result → finalWork i = initialWork i
• readable : ∃ (iterationWork : Fin n → Tape), ReadableEntryMatch tapes entry rest queryBits iterationWork finalWork

  The complete readable-match endpoint is retained for downstream consumers that must reset every decoder scratch tape after a hit.