Reusable sparse-register lookup -- value rewind and copy

theorem Complexity.RAM.RegisterStore.Machine.entryLookupValueRewind_hoareTime_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork preparedWork scannedWork : Fin n → Tape) (inp₀ out₀ : Tape) (hprepared : EntryLookupPrepared tapes store address initialWork preparedWork) (hscanned : EntryLookupScanned tapes store address initialWork preparedWork scannedWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (TM.rewindWorkTM tapes.scan.entry.value).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = scannedWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupValueReady tapes store address initialWork work ∧ out = out₀) (entryLookupRestoreHeadBound tapes store address + 2)

Rewinding the decoded value converts its append-position prefix into a canonical binary natural without losing any cleanup or frame information.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupValueCopy_hoareTime_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork work₀ : Fin n → Tape) (inp₀ out₀ : Tape) (hready : EntryLookupValueReady tapes store address initialWork work₀) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (TM.binaryCopyIntoTM tapes.scan.entry.value tapes.destination 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₀ ∧ EntryLookupCopied tapes store address initialWork work ∧ out = out₀) (TM.binaryCopyTime (read store address) 0)

Copy the rewound decoded value into the instruction operand tape. The source value and zero scratch stay canonical, and all restoration data is preserved.