For a fixed machine and input, valid accepting computation histories form a decidable language

Because $M$ is fixed, the disjoint tagged alphabet $(\{\mathtt{s}\}\times Q)\cup (\{\mathtt{t}\}\times \mathrm{\Gamma })$ is finite. Choose pairwise distinct binary blocks of one common length for these tagged symbols. Encode each configuration word by replacing its unique state symbol $q$ with the block for $(\mathtt{s},q)$ and each tape symbol $a$ with the block for $(\mathtt{t},a)$. The common block length makes this code uniquely decodable back to the tagged configuration word.

Use the explicit pair encoding $E_2$ from [L3], and encode finite lists of configuration codes recursively by $\mathrm{Hist}():=0,\mathrm{Hist}(x_0,\dots ,x_n):=1E_2(x_0,\mathrm{Hist}(x_1,\dots ,x_n))\mathrm{.}$ A decoder returns the empty list only when its entire current candidate is exactly 0; a candidate beginning with 0 and containing any further bit is malformed. When the candidate begins with 1, the decoder applies the total decoder for $E_2$ to the remaining suffix. If that suffix is malformed it rejects; otherwise it recovers the first configuration code and a tail-code and continues on the tail. By [L3], every successfully decoded tail-code is strictly shorter than the current candidate, so this recursion halts on every binary input and returns either one finite list or the malformed-code output.

Given a decoded tagged word, check mechanically that it contains exactly one state-tagged block, all other blocks are tape-tagged, at least one tape-tagged block follows the state-tagged block, and whenever more than one tape-tagged block follows the state-tagged block the last of them is not the blank-tagged block $(\mathtt{t},\bigsqcup )$. By [L4], these are exactly the configuration words of $M$: the number of tape-tagged blocks before the unique state-tagged block is the head position, the tagged tape blocks recover the finite word $a_0\cdots a_r$, and the last-block test enforces the canonical choice $r=\max (\{h\}\cup \mathrm{supp}(t))$. Thus valid configuration codes can be parsed effectively back into configurations of $M$.

On input a candidate binary word $z$, first decode it by the recursive history decoder from step 1.2. If the decoder reports malformed input or the empty list, reject immediately. Otherwise step 2.1 parses each configuration code in the decoded list into a configuration, yielding $C_0,\dots ,C_n$. Check whether $C_0=I_M(w)$, whether each adjacent pair satisfies $C_i{⊢}_M{C}_{i+1}$, and whether $C_n$ is accepting. Each check is finite and local: the first compares one explicit configuration with the fixed start configuration, the middle checks one transition of the fixed machine $M$, and the last reads the final state. Accept exactly when all checks pass.

By [L2], a decoded list passes the step-3.1 test exactly when it is an accepting computation history of $M$ on input $w$. The machine just described halts on every candidate history code, because the recursive decoder from step 1.2 terminates and the subsequent checks are finite.

Therefore there is a deterministic Turing machine that decides $H_{M,w}$. By [L1], $H_{M,w}$ is a decidable language.