Sparse-entry final append

theorem Complexity.RAM.RegisterStore.Machine.entryAppendRestoreTM_hoareTime_frame {n : ℕ} (tapes : EntryReplaceTapes n) (address newValue : ℕ) (emitted : List Bool) (initialWork readyWork : Fin n → Tape) (inp₀ out₀ : Tape) (hready : EntryScanReady tapes.entry [] address.bits initialWork readyWork) (hreplacement : (readyWork tapes.replacement).HasBinaryNat newValue) (hinput : TM.Parked inp₀) (houtput : out₀.HasBinaryPrefix emitted) : (entryAppendRestoreTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = readyWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = readyWork ∧ out.HasBinaryPrefix (emitted ++ Entry.encode (address, newValue))) (entryAppendRestoreTime address newValue)

Append one absent query/nonzero-value entry and restore both canonical source tapes exactly, retaining the caller's complete work family.

theorem Complexity.RAM.RegisterStore.Machine.entryAppendRestoreTM_isTransducer {n : ℕ} (tapes : EntryReplaceTapes n) : (entryAppendRestoreTM tapes).IsTransducer

Final append and restoration are append-only on the output tape.

theorem Complexity.RAM.RegisterStore.Machine.entryAppendRestoreTM_prefix_withinAuxSpace {n : ℕ} (tapes : EntryReplaceTapes n) (address newValue inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (entryAppendRestoreTM tapes).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (entryAppendRestoreTM tapes).reachesIn time start current) (htime : time ≤ entryAppendRestoreTime address newValue) : current.WithinAuxSpace inputLength (initialSpace + entryAppendRestoreTime address newValue)

Coarse all-prefix auxiliary-space envelope for final append/restoration.