Bounded sparse-entry scan — definitions

entryScanTM is a fixed machine, independent of the runtime store size. A canonical binary remaining-count tape bounds the scan. Each iteration runs the checked entry step; a hit leaves its readable result at 1 and halts, while a miss restores scratch, decrements the count, and loops. Count zero halts with the blank miss result.

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

Entry-match tapes plus a distinct canonical binary remaining-count tape.

• entry : EntryMatchTapes n

  The nine tapes used by one decode/compare iteration.

• count : Fin n

  Runtime remaining-entry count.

• count_ne (i : Fin 9) : self.count ≠ self.entry.idx i

  The count tape is distinct from every entry-step tape.

theorem Complexity.RAM.RegisterStore.Machine.EntryScanTapes.count_ne_source {n : ℕ} (tapes : EntryScanTapes n) : tapes.count ≠ tapes.entry.source

The count tape is distinct from the encoded entry source.

theorem Complexity.RAM.RegisterStore.Machine.EntryScanTapes.count_ne_result {n : ℕ} (tapes : EntryScanTapes n) : tapes.count ≠ tapes.entry.result

The count tape is distinct from the readable match-result tape.

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

Finite controller phases outside the nested entry-step and predecessor machines.

• test : EntryScanPhase
• done : EntryScanPhase

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instDecidableEqEntryScanPhase : DecidableEq EntryScanPhase

Equations

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

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instFintypeEntryScanPhase : Fintype EntryScanPhase

EntryScanPhase has exactly two states.

Equations

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

@[reducible, inline]

abbrev Complexity.RAM.RegisterStore.Machine.EntryScanQ {n : ℕ} (tapes : EntryScanTapes n) : Type

State type of the bounded sparse-entry controller.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryScanTM {n : ℕ} (tapes : EntryScanTapes n) : TM n

Fixed bounded scan controlled by a runtime canonical binary count.

The test phase halts on the empty encoding of zero. At positive count it runs one entry step. A readable 1 result exits immediately with the decoded value; the blank miss result enters binary predecessor and then loops.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryScanCanonicalWork {n : ℕ} : Fin n → Tape

Canonical all-blank work family used only to state the iteration bound; every tape head is at cell one.

Equations

• Complexity.RAM.RegisterStore.Machine.entryScanCanonicalWork = Function.const (Fin n) Complexity.TM.resetBinaryBlank

def Complexity.RAM.RegisterStore.Machine.entryScanOneTime {n : ℕ} (tapes : EntryScanTapes n) (entry : Entry) (queryBits : List Bool) : ℕ

Work-value-independent bound for one invariant-preserving entry step.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryScanTime {n : ℕ} (tapes : EntryScanTapes n) (queryBits : List Bool) : Store → ℕ

Recursive bound for scanning a whole finite store. It reserves the miss path at every entry, so it also bounds an earlier successful exit.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.RegisterStore.Machine.entryScanTime tapes queryBits [] = 1

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

Exact preservation predicate outside the ten tapes owned by the bounded entry scanner.

Equations

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

structure Complexity.RAM.RegisterStore.Machine.EntryScanFound {n : ℕ} (tapes : EntryScanTapes n) (store scanned : Store) (matched : Entry) (rest : Store) (queryBits : List Bool) (initialWork hitBase finalWork : Fin n → Tape) : Prop

Successful bounded scan result. The decomposition records the first matching entry, the decoded value remains readable, and the runtime count is the number of entries beginning at that hit.

• store_eq : store = scanned ++ matched :: rest
• prefixMiss (prior : Entry) : prior ∈ scanned → prior.1.bits ≠ queryBits
• hit : EntryScanHit tapes.entry matched (List.flatMap Entry.encode rest) queryBits hitBase finalWork
• count : (finalWork tapes.count).HasBinaryNat (List.length rest + 1)
• frame : EntryScanFrame tapes initialWork finalWork

structure Complexity.RAM.RegisterStore.Machine.EntryScanMiss {n : ℕ} (tapes : EntryScanTapes n) (store : Store) (queryBits : List Bool) (initialWork readyBase finalWork : Fin n → Tape) : Prop

Unsuccessful bounded scan result. Every address is certified different, the source and scratch invariant is exhausted, and the runtime count is zero.

• notFound (entry : Entry) : entry ∈ store → entry.1.bits ≠ queryBits
• ready : EntryScanReady tapes.entry [] queryBits readyBase finalWork
• count : (finalWork tapes.count).HasBinaryNat 0
• frame : EntryScanFrame tapes initialWork finalWork

def Complexity.RAM.RegisterStore.Machine.EntryScanOutcome {n : ℕ} (tapes : EntryScanTapes n) (store : Store) (queryBits : List Bool) (initialWork finalWork : Fin n → Tape) : Prop

Complete semantic outcome of a bounded sparse-entry scan.

Equations

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