Bounded encoded sparse-store update -- semantic composition

This file composes the checked one-entry and terminal contracts into the complete update loop. The induction is over the runtime-counted remaining store, while the loop invariant carries the processed prefix and emitted output needed to connect the concrete controller to RegisterStore.write.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateLoop_internal {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue : ℕ) (processed remaining emitted : Store) (found : Bool) (resultCount : ℕ) (initialWork work : Fin n → Tape) (outPrefix : List Bool) (inp out : Tape) (hinv : EntryUpdateLoopInv tapes store address newValue processed remaining emitted found resultCount initialWork work) (hnodup : AddressesNodup store) (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) remaining, (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))

Starting from any valid loop boundary, the update controller finishes the remaining suffix within its recursive static budget.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_hoareTime_frame_internal {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue : ℕ) (emittedBits : List Bool) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hcanonical : Canonical store) (hready : EntryScanReady tapes.entry (List.flatMap Entry.encode store) address.bits initialWork initialWork) (hreplacement : (initialWork tapes.replacement).HasBinaryNat newValue) (hremaining : (initialWork tapes.remaining).HasBinaryNat (List.length store)) (hfound : (initialWork tapes.found).HasBinaryNat 0) (hresultCount : (initialWork tapes.resultCount).HasBinaryNat (List.length store)) (hinput : TM.Parked inp₀) (houtput : out₀.HasBinaryPrefix emittedBits) : (entryUpdateTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryUpdateOutcome tapes store address newValue initialWork work ∧ out.HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (write store address newValue))) (entryUpdateTime tapes store address newValue)

A complete encoded sparse-store update realizes RegisterStore.write, preserves input and the external work frame exactly, and appends precisely the new store encoding to the caller's existing output prefix.