Bounded encoded sparse-store update — output safety internals

The update controller delegates every nested phase to an independently checked one-way-output machine. Its own dispatch transitions either read back or leave the output head idle, so the complete controller remains a transducer.

theorem Complexity.RAM.RegisterStore.Machine.parked_of_binaryPrefix_internal {t : Tape} {bits : List Bool} (h : t.HasBinaryPrefix bits) : TM.Parked t

A canonical binary prefix parks its tape head away from the left endmarker and contains no spurious left endmarkers.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_isTransducer_internal {n : ℕ} (tapes : EntryUpdateTapes n) : (entryUpdateTM tapes).IsTransducer

The fixed sparse-store update controller never moves its output head left.