Reusable sparse-register lookup -- bounded scan phase

theorem Complexity.RAM.RegisterStore.Machine.entryLookupScan_hoareTime_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork preparedWork : Fin n → Tape) (inp₀ out₀ : Tape) (hprepared : EntryLookupPrepared tapes store address initialWork preparedWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (entryLookupTM tapes.scan).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = preparedWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupScanned tapes store address initialWork preparedWork work ∧ out = out₀) (entryLookupTime tapes.scan address store)

The scanner phase preserves the reusable external ABI and packages every fact needed to copy the value and restore the scanner-owned tapes.