Bounded encoded sparse-store update -- terminal loop case

This file closes the update loop once the old-entry counter is exhausted. A previous hit and an absent zero write halt immediately; an absent nonzero write runs the checked append and result-count successor subroutines.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTerminal_internal {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue : ℕ) (processed emitted : Store) (found : Bool) (resultCount : ℕ) (initialWork work : Fin n → Tape) (outPrefix : List Bool) (inp out : Tape) (hinv : EntryUpdateLoopInv tapes store address newValue processed [] emitted found resultCount initialWork work) (hinput : TM.Parked inp) (houtput : out.HasBinaryPrefix (outPrefix ++ List.flatMap Entry.encode emitted)) : ∃ (final : Complexity.Cfg n (entryUpdateTM tapes).Q), ∃ time ≤ entryUpdateLoopTime tapes address newValue (List.length store) [], (entryUpdateTM tapes).reachesIn time (entryUpdateTestCfg tapes inp work out) final ∧ (entryUpdateTM tapes).halted final ∧ final.input = inp ∧ EntryUpdateOutcome tapes store address newValue initialWork final.work ∧ final.output.HasBinaryPrefix (outPrefix ++ List.flatMap Entry.encode (write store address newValue))

Once no old entries remain, the controller realizes the pure sparse-store write and establishes the complete final tape contract.