Reusable sparse-register lookup -- scanner restoration

theorem Complexity.RAM.RegisterStore.Machine.entryLookupReset_hoareTime_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork copiedWork : Fin n → Tape) (inp₀ out₀ : Tape) (hcopied : EntryLookupCopied tapes store address initialWork copiedWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (TM.resetBinaryWorkManyTM (entryLookupResetTargets tapes)).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = copiedWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupResetDone tapes store address initialWork copiedWork work ∧ out = out₀) (entryLookupResetTime tapes store address)

Reset all nine scanner-owned binary tapes under one uniform width and cursor envelope.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupSourceRewind_hoareTime_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork copiedWork resetWork : Fin n → Tape) (inp₀ out₀ : Tape) (hinitial : EntryLookupRestoreReady tapes store address initialWork) (hdone : EntryLookupResetDone tapes store address initialWork copiedWork resetWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (TM.rewindWorkTM tapes.scan.entry.source).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = resetWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupSourceReady tapes store address initialWork work ∧ out = out₀) (entryLookupRestoreHeadBound tapes store address + 2)

Rewind the read-only encoded store after resetting scanner scratch.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupCountRestore_hoareTime_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork work₀ : Fin n → Tape) (inp₀ out₀ : Tape) (hready : EntryLookupSourceReady tapes store address initialWork work₀) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (TM.binaryCopyIntoTM tapes.countSource tapes.scan.count 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₀ ∧ EntryLookupRestoreResult tapes store address initialWork work ∧ out = out₀) (TM.binaryCopyTime (List.length store) 0)

Restore the runtime entry count from its preserved canonical copy. This is the final phase returning the scanner to its reusable blank-query boundary.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupReset_ready_hoareTime_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (TM.resetBinaryWorkManyTM (entryLookupResetTargets 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₀ ∧ EntryLookupScratchReset tapes store address initialWork work ∧ out = out₀) (entryLookupResetTime tapes store address)

Semantic reset boundary used by sequential lookup composition.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupSourceRewind_ready_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₀) : (TM.rewindWorkTM tapes.scan.entry.source).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupScratchReset tapes store address initialWork work ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupSourceReady tapes store address initialWork work ∧ out = out₀) (entryLookupRestoreHeadBound tapes store address + 2)

Semantic encoded-source rewind boundary used by sequential composition.

theorem Complexity.RAM.RegisterStore.Machine.entryLookupCountRestore_ready_hoareTime_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (TM.binaryCopyIntoTM tapes.countSource tapes.scan.count tapes.copyScratch).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryLookupSourceReady 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₀) (TM.binaryCopyTime (List.length store) 0)

Semantic count-copy boundary used by sequential composition.