Reusable sparse-register lookup -- reset certificates

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupResult.resetReady_internal {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork finalWork : Fin n → Tape) (hresult : EntryLookupResult tapes.scan store address initialWork finalWork) : EntryLookupResetReady tapes store address finalWork

Every semantic scanner result determines exact bounded contents for all nine reset targets.