Bounded encoded sparse-store update — static runtime bounds

The entry subroutines expose exact compositional times parameterized by the current work family. This file discharges that dependency at the update-loop boundary: a ready loop invariant fixes every owned starting head, while a readable match bounds the one cursor whose endpoint is intentionally in-place.

theorem Complexity.RAM.RegisterStore.Machine.EntryScanReady.query_head_eq_one_internal {n : ℕ} {tapes : EntryMatchTapes n} {remaining queryBits : List Bool} {initialWork work : Fin n → Tape} (h : EntryScanReady tapes remaining queryBits initialWork work) : (work tapes.query).head = 1

The preserved query is rewound at every update-loop boundary.

theorem Complexity.RAM.RegisterStore.Machine.EntryScanReady.cleanup_target_head_eq_one_internal {n : ℕ} {tapes : EntryMatchTapes n} {remaining queryBits : List Bool} {initialWork work : Fin n → Tape} (h : EntryScanReady tapes remaining queryBits initialWork work) (i : Fin n) : i ∈ entryMissTargets tapes → (work i).head = 1

Every scratch target cleared by an update branch starts at cell one at a ready loop boundary.

theorem Complexity.RAM.RegisterStore.Machine.entryMissCleanupTime_eq_entryUpdateReadyCleanupTime_internal {n : ℕ} (tapes : EntryUpdateTapes n) (entry : Entry) (address : ℕ) {remaining : List Bool} {initialWork work : Fin n → Tape} (hready : EntryScanReady tapes.entry remaining address.bits initialWork work) : entryMissCleanupTime tapes.entry entry address.bits work = entryUpdateReadyCleanupTime tapes entry address

On a ready loop boundary, the exact deletion-cleanup time is the static controller bound.

theorem Complexity.RAM.RegisterStore.Machine.entryMissCopyTime_le_entryUpdateMissTime_internal {n : ℕ} (tapes : EntryUpdateTapes n) (entry : Entry) (address : ℕ) (rest : List Bool) (initialWork readyWork matchedWork : Fin n → Tape) (hready : EntryScanReady tapes.entry (entry.encode ++ rest) address.bits initialWork readyWork) (hmatch : ReadableEntryMatch tapes.entry entry rest address.bits readyWork matchedWork) : entryMissCopyTime tapes.entry entry address.bits readyWork matchedWork ≤ entryUpdateMissTime tapes entry address

A ready comparison followed by miss emission has a work-independent runtime bounded by the controller's static miss budget.

theorem Complexity.RAM.RegisterStore.Machine.entryReplaceCleanupTime_le_entryUpdateReplaceTime_internal {n : ℕ} (tapes : EntryUpdateTapes n) (entry : Entry) (address newValue : ℕ) (rest : List Bool) (initialWork readyWork matchedWork : Fin n → Tape) (hready : EntryScanReady tapes.entry (entry.encode ++ rest) address.bits initialWork readyWork) (hmatch : ReadableEntryMatch tapes.entry entry rest address.bits readyWork matchedWork) : entryReplaceCleanupTime tapes.replace entry newValue address.bits readyWork matchedWork ≤ entryUpdateReplaceTime tapes entry address newValue

A ready comparison followed by replacement emission has a work-independent runtime bounded by the controller's static replacement budget.

theorem Complexity.RAM.RegisterStore.Machine.binaryPredTime_le_entryUpdateCountTime_internal {value total : ℕ} (hvalue : value + 1 ≤ total) : TM.binaryPredTime value ≤ entryUpdateCountTime total

A positive counter no larger than the initial store size can be decremented within the update controller's uniform counter budget.

theorem Complexity.RAM.RegisterStore.Machine.binarySuccTime_le_entryUpdateCountTime_internal {value total : ℕ} (hvalue : value ≤ total) : TM.binarySuccTime value ≤ entryUpdateCountTime total

A counter no larger than the initial store size can be incremented within the update controller's uniform counter budget.