Sparse-store update source preservation

The update controller advances its encoded source cursor but never changes the source cells. This file packages that local transition fact as a reusable read-only certificate.

theorem Complexity.RAM.RegisterStore.Machine.entryScanTM_source_readOnly_internal {n : ℕ} (tapes : EntryScanTapes n) : (entryScanTM tapes).WorkReadOnly tapes.entry.source

The bounded lookup scanner advances but never changes its encoded source cells.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_source_readOnly_internal {n : ℕ} (tapes : EntryUpdateTapes n) : (entryUpdateTM tapes).WorkReadOnly tapes.entry.source