Encoded-length bounds for sparse-entry scans -- proof internals

The optimized word decoder leaves unary width markers. This makes decoding, matching, and cleanup linear in the two words actually traversed. The final scan theorem retains only the separate binary remaining-count charge.

theorem Complexity.RAM.RegisterStore.Machine.entryScanOneTime_le_linear_internal {n : ℕ} (tapes : EntryScanTapes n) (entry : Entry) (queryBits : List Bool) : entryScanOneTime tapes entry queryBits ≤ 400 * (entry.1.bits.length + entry.2.bits.length + queryBits.length + 1)

theorem Complexity.RAM.RegisterStore.Machine.entryScanTime_le_encoded_internal {n : ℕ} (tapes : EntryScanTapes n) (queryBits : List Bool) (store : Store) : entryScanTime tapes queryBits store ≤ 1000 * (encodedStoreLength store + List.length store * (queryBits.length + bitlen (List.length store) + 2) + 1)