One bounded sparse-entry scan iteration

This module exposes the compositional hit-or-next-iteration contract for one encoded sparse register-store entry.

theorem Complexity.RAM.RegisterStore.Machine.entryScanStepTM_hoareTime_frame {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (rest queryBits : List Bool) (initialWork iterationWork : Fin n → Tape) (inp₀ out₀ : Tape) (hready : EntryScanReady tapes (entry.encode ++ rest) queryBits initialWork iterationWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (entryScanStepTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = iterationWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ (entry.1.bits = queryBits ∧ EntryScanHit tapes entry rest queryBits initialWork work ∨ entry.1.bits ≠ queryBits ∧ EntryScanReady tapes rest queryBits initialWork work) ∧ out = out₀) (entryScanStepTime tapes entry queryBits iterationWork)

Decode and compare one entry, then either expose its decoded value on a hit or restore the exact invariant for the remaining encoded stream.

theorem Complexity.RAM.RegisterStore.Machine.entryScanStepTM_isTransducer {n : ℕ} (tapes : EntryMatchTapes n) : (entryScanStepTM tapes).IsTransducer

One scan iteration preserves one-way output safety.

theorem Complexity.RAM.RegisterStore.Machine.entryScanStepTM_prefix_withinAuxSpace {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (queryBits : List Bool) (initialWork : Fin n → Tape) (inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (entryScanStepTM tapes).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (entryScanStepTM tapes).reachesIn time start current) (htime : time ≤ entryScanStepTime tapes entry queryBits initialWork) : current.WithinAuxSpace inputLength (initialSpace + entryScanStepTime tapes entry queryBits initialWork)

Coarse all-prefix auxiliary-space envelope for one scan iteration.