Reusable sparse-register lookup -- query preparation

theorem Complexity.RAM.RegisterStore.Machine.entryLookupPrepare_hoareTime_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (work₀ : Fin n → Tape) (inp₀ out₀ : Tape) (hready : EntryLookupRestoreReady tapes store address work₀) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (TM.binaryCopyIntoTM tapes.querySource tapes.scan.entry.query tapes.copyScratch).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupPrepared tapes store address work₀ work ∧ out = out₀) (TM.binaryCopyTime address 0)

Copying the external query source into the blank scanner query tape establishes the exact lookup-ready boundary and changes no other tape.