Bounded sparse-entry scan — semantic internals

theorem Complexity.RAM.RegisterStore.Machine.entryScanTM_hoareTime_frame_internal {n : ℕ} (tapes : EntryScanTapes n) (store : Store) (queryBits : List Bool) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hready : EntryScanReady tapes.entry (List.flatMap Entry.encode store) queryBits initialWork initialWork) (hcount : (initialWork tapes.count).HasBinaryNat (List.length store)) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (entryScanTM 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₀ ∧ EntryScanOutcome tapes store queryBits initialWork work ∧ out = out₀) (entryScanTime tapes queryBits store)