Reusable sparse-register lookup -- phase assembly

theorem Complexity.RAM.RegisterStore.Machine.entryLookupRestoreTail_hoareTime_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hinitial : EntryLookupRestoreReady tapes store address initialWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (entryLookupRestoreTailTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupCopied tapes store address initialWork work ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupRestoreResult tapes store address initialWork work ∧ out = out₀) (entryLookupRestoreTailTime tapes store address)

Scanner reset, source rewind, and count restoration form one reusable tail whose endpoint is the original blank-query scanner ABI.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupCopyRestore_hoareTime_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hinitial : EntryLookupRestoreReady tapes store address initialWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (entryLookupCopyRestoreTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupPrepared tapes store address initialWork work ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupRestoreResult tapes store address initialWork work ∧ out = out₀) (entryLookupCopyRestoreTime tapes store address)

Once the external query has been prepared, scanning, value extraction, and complete restoration form one reusable lookup.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupLoaded_hoareTime_internal {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)

Complete semantic and time contract for one reusable loaded sparse-register lookup.