Sparse-entry miss cleanup

This module exposes the exact invariant-restoring miss branch used by the bounded sparse register-store scan.

theorem Complexity.RAM.RegisterStore.Machine.entryMissCleanupTM_hoareTime_frame {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (rest queryBits : List Bool) (initialWork matchedWork : Fin n → Tape) (inp₀ out₀ : Tape) (hmatch : ReadableEntryMatch tapes entry rest queryBits initialWork matchedWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (entryMissCleanupTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = matchedWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryScanReady tapes rest queryBits initialWork work ∧ out = out₀) (entryMissCleanupTime tapes entry queryBits initialWork)

After a failed readable entry match, rewind the preserved query and reset all seven decoder/result scratch tapes, restoring the next-iteration frame.

theorem Complexity.RAM.RegisterStore.Machine.entryMissCleanupTM_isTransducer {n : ℕ} (tapes : EntryMatchTapes n) : (entryMissCleanupTM tapes).IsTransducer

Miss cleanup preserves one-way output safety.

theorem Complexity.RAM.RegisterStore.Machine.entryMissCleanupTM_prefix_withinAuxSpace {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (queryBits : List Bool) (initialWork : Fin n → Tape) (inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (entryMissCleanupTM tapes).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (entryMissCleanupTM tapes).reachesIn time start current) (htime : time ≤ entryMissCleanupTime tapes entry queryBits initialWork) : current.WithinAuxSpace inputLength (initialSpace + entryMissCleanupTime tapes entry queryBits initialWork)

Coarse all-prefix auxiliary-space envelope for miss cleanup.