Encoded-length sparse-update bounds -- proof internals

The update controller reserves the slower of copy, replacement, and deletion at each iteration. With unary-marker decoding, each such reservation is still linear in the current entry and the instruction's query/replacement widths.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTime_le_encoded_internal {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue : ℕ) : entryUpdateTime tapes store address newValue ≤ 1000 * (encodedStoreLength store + (List.length store + 1) * (bitlen address + bitlen newValue + bitlen (List.length store) + 1) + 1)