Sparse-entry miss copy

This module exposes the update-scan branch that appends one unmatched entry to the new store and restores the exact invariant needed to inspect the next one.

theorem Complexity.RAM.RegisterStore.Machine.entryMissCopyTM_hoareTime_frame {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (rest queryBits emitted : List Bool) (initialWork matchedWork : Fin n → Tape) (inp₀ out₀ : Tape) (hmatch : ReadableEntryMatch tapes entry rest queryBits initialWork matchedWork) (hinput : TM.Parked inp₀) (houtput : out₀.HasBinaryPrefix emitted) : (entryMissCopyTM 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.HasBinaryPrefix (emitted ++ entry.encode)) (entryMissCopyTime tapes entry queryBits initialWork matchedWork)

Copy one decoded unmatched entry to the output stream and restore the ordinary next-entry scan invariant, with an explicit intermediate work frame.

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

Miss-copy is append-only on the output tape.

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

Coarse all-prefix auxiliary-space envelope for one miss-copy branch.