Reusable sparse-register lookup -- reset bounds

theorem Complexity.RAM.RegisterStore.Machine.entryLookupEntryWidth_le_storeWidth_internal (store : Store) (address : ℕ) (entry : Entry) (hentry : entry ∈ store) : entryLookupEntryWidth entry address ≤ entryLookupStoreWidth address store

theorem Complexity.RAM.RegisterStore.Machine.entryLookupEntryWidth_le_resetWidth_internal (store : Store) (address : ℕ) (entry : Entry) (hentry : entry ∈ store) : entryLookupEntryWidth entry address ≤ entryLookupResetWidth store address

theorem Complexity.RAM.RegisterStore.Machine.entryLookupAddressWidth_le_resetWidth_internal (store : Store) (address : ℕ) : address.bits.length ≤ entryLookupResetWidth store address

theorem Complexity.RAM.RegisterStore.Machine.entryLookupRemainingWidth_le_resetWidth_internal (store : Store) (address remaining : ℕ) (hle : remaining ≤ List.length store) : remaining.bits.length ≤ entryLookupResetWidth store address

theorem Complexity.RAM.RegisterStore.Machine.entryLookupEntryAddressWidth_le_internal (entry : Entry) (address : ℕ) : entry.1.bits.length ≤ entryLookupEntryWidth entry address

theorem Complexity.RAM.RegisterStore.Machine.entryLookupEntryValueWidth_le_internal (entry : Entry) (address : ℕ) : entry.2.bits.length ≤ entryLookupEntryWidth entry address

theorem Complexity.RAM.RegisterStore.Machine.entryLookupEntryAddressCounterWidth_le_internal (entry : Entry) (address : ℕ) : bitlen entry.1 ≤ entryLookupEntryWidth entry address

theorem Complexity.RAM.RegisterStore.Machine.entryLookupEntryValueCounterWidth_le_internal (entry : Entry) (address : ℕ) : bitlen entry.2 ≤ entryLookupEntryWidth entry address

theorem Complexity.RAM.RegisterStore.Machine.entryLookupResultWidth_le_internal (entry : Entry) (address : ℕ) : 1 ≤ entryLookupEntryWidth entry address