Bounded encoded sparse-store update -- one positive iteration

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateIteration_internal {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue : ℕ) (processed emitted : Store) (entry : Entry) (rest : Store) (found : Bool) (resultCount : ℕ) (initialWork work : Fin n → Tape) (outPrefix : List Bool) (inp out : Tape) (hinv : EntryUpdateLoopInv tapes store address newValue processed (entry :: rest) emitted found resultCount initialWork work) (hnodup : AddressesNodup store) (hinput : TM.Parked inp) (houtput : out.HasBinaryPrefix (outPrefix ++ List.flatMap Entry.encode emitted)) : ∃ (processed' : Store) (emitted' : Store) (found' : Bool) (resultCount' : ℕ) (nextWork : Fin n → Tape) (nextOut : Tape), ∃ time ≤ entryUpdateIterationTime tapes entry rest address newValue (List.length store), (entryUpdateTM tapes).reachesIn time (entryUpdateTestCfg tapes inp work out) (entryUpdateTestCfg tapes inp nextWork nextOut) ∧ EntryUpdateLoopInv tapes store address newValue processed' rest emitted' found' resultCount' initialWork nextWork ∧ nextOut.HasBinaryPrefix (outPrefix ++ List.flatMap Entry.encode emitted')

One positive old-entry iteration advances the semantic and tape loop invariant, returning to the controller's test state.