Sparse register lookup

theorem Complexity.RAM.RegisterStore.Machine.entryLookupTM_source_readOnly {n : ℕ} (tapes : EntryScanTapes n) : (entryLookupTM tapes).WorkReadOnly tapes.entry.source

A bounded lookup advances the encoded source cursor without modifying its cells.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupTM_hoareTime_frame {n : ℕ} (tapes : EntryScanTapes n) (store : Store) (address : ℕ) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hready : EntryScanReady tapes.entry (List.flatMap Entry.encode store) address.bits initialWork initialWork) (hcount : (initialWork tapes.count).HasBinaryNat (List.length store)) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (entryLookupTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupResult tapes store address initialWork work ∧ out = out₀) (entryLookupTime tapes address store)

Scan a runtime-sized encoded sparse store and leave exactly RegisterStore.read store address on the decoded-value tape.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupTM_hoareTime_frame_source {n : ℕ} (tapes : EntryScanTapes n) (store : Store) (address : ℕ) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hready : EntryScanReady tapes.entry (List.flatMap Entry.encode store) address.bits initialWork initialWork) (hcount : (initialWork tapes.count).HasBinaryNat (List.length store)) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (entryLookupTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupResult tapes store address initialWork work ∧ (work tapes.entry.source).cells = (initialWork tapes.entry.source).cells ∧ (∀ (i : Fin n), (work i).head ≤ (initialWork i).head + entryLookupTime tapes address store) ∧ out = out₀) (entryLookupTime tapes address store)

Framed lookup with explicit preservation of the complete encoded source cell function.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupTM_isTransducer {n : ℕ} (tapes : EntryScanTapes n) : (entryLookupTM tapes).IsTransducer

Sparse lookup preserves one-way output safety.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupTM_prefix_withinAuxSpace {n : ℕ} (tapes : EntryScanTapes n) (store : Store) (address inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (entryLookupTM tapes).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (entryLookupTM tapes).reachesIn time start current) (htime : time ≤ entryLookupTime tapes address store) : current.WithinAuxSpace inputLength (initialSpace + entryLookupTime tapes address store)

Sparse lookup inherits the scanner's all-prefix auxiliary-space envelope.