Reusable sparse-register operand lookup

This module exposes one complete sparse-register read as a reusable TM subroutine. It loads a canonical query, scans the encoded store, copies the semantic value out, resets every scanner-owned tape, rewinds the read-only source, restores the runtime entry count, and returns to the same scanner ABI.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupLoadedTM_hoareTime_frame {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hready : EntryLookupRestoreReady tapes store address initialWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (entryLookupLoadedTM 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₀ ∧ EntryLookupRestoreResult tapes store address initialWork work ∧ out = out₀) (entryLookupLoadedTime tapes store address)

One loaded lookup returns the scanner to its blank-query boundary, places exactly RegisterStore.read store address on the destination tape, and preserves the complete external frame.

theorem Complexity.RAM.RegisterStore.Machine.denseOverlayLookupTM_hoareTime_frame {n : ℕ} (tapes : EntryLookupRestoreTapes n) (input : List Bool) (overlay : Store) (address : ℕ) (initialWork : Fin n → Tape) (out₀ : Tape) (hvalid : DenseOverlay.Valid overlay) (hready : EntryLookupRestoreReady tapes overlay address initialWork) (houtput : TM.Parked out₀) : (denseOverlayLookupTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseOverlayLookupResult tapes input overlay address initialWork work ∧ out = out₀) (denseOverlayLookupTime tapes input.length overlay address)

A reusable lookup through a positive-tag mutable overlay returns either the decoded tag or the corresponding immutable public-input register.

theorem Complexity.RAM.RegisterStore.Machine.denseOverlayLookupStaticTM_hoareTime_frame {n : ℕ} (tapes : EntryLookupRestoreTapes n) (input : List Bool) (overlay : Store) (address : ℕ) (initialWork : Fin n → Tape) (out₀ : Tape) (hvalid : DenseOverlay.Valid overlay) (hready : EntryLookupStaticReady tapes overlay initialWork) (houtput : TM.Parked out₀) : (denseOverlayLookupStaticTM tapes address).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseOverlayLookupStaticResult tapes input overlay address initialWork work ∧ out = out₀) (denseOverlayLookupStaticTime tapes input.length overlay address)

A fixed-address dense-overlay lookup synthesizes and clears its query, while returning the decoded register value at the reusable scanner boundary.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupLoadedTM_isTransducer {n : ℕ} (tapes : EntryLookupRestoreTapes n) : (entryLookupLoadedTM tapes).IsTransducer

Reusable sparse-register lookup never moves the output head left.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupLoadedTM_prefix_withinAuxSpace {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (entryLookupLoadedTM tapes).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (entryLookupLoadedTM tapes).reachesIn time start current) (htime : time ≤ entryLookupLoadedTime tapes store address) : current.WithinAuxSpace inputLength (initialSpace + entryLookupLoadedTime tapes store address)

Every prefix of a loaded lookup stays within its initial auxiliary space plus the advertised total running-time bound.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupStaticTM_hoareTime_frame {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hready : EntryLookupStaticReady tapes store initialWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (entryLookupStaticTM tapes address).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₀ ∧ EntryLookupStaticResult tapes store address initialWork work ∧ out = out₀) (entryLookupStaticTime tapes store address)

A fixed-address lookup synthesizes its query from zero, returns the scanner to its reusable boundary, places the semantic register value in the destination, and clears the temporary query source.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupStaticTM_isTransducer {n : ℕ} (tapes : EntryLookupRestoreTapes n) (address : ℕ) : (entryLookupStaticTM tapes address).IsTransducer

Fixed-address lookup never moves the output head left.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupStaticTM_prefix_withinAuxSpace {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (entryLookupStaticTM tapes address).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (entryLookupStaticTM tapes address).reachesIn time start current) (htime : time ≤ entryLookupStaticTime tapes store address) : current.WithinAuxSpace inputLength (initialSpace + entryLookupStaticTime tapes store address)

Every fixed-address lookup prefix stays within its initial auxiliary space plus the advertised total running-time bound.