A doubt in Ladner's Proof
Every string in $SAT_H$ has length $m+1+m^{H(m)}$ for some $m$. In particular, there will be strings of length at most $\log n$ whenever $m+1+m^{H(m)} \leq \log n$. For some reason you insist that $m$ equal $n$. Perhaps you should consider the following equivalent definition of $SAT_H$:
$$SAT_H = \{\psi01^{|\psi|^{H(|\psi|)}} : \psi \in SAT\}. $$
There is, however, a subtle point: the definition of $H(n)$ relies on the set $SAT_H$, whose definition in turn relies on the definition of $H(n)$ in what seems to be a circular fashion! However, if you work out the details you see that $H(n)$ relies on those parts of $SAT_H$ which depend on $H(m)$ for much smaller $m$. Indeed, we need to know the members of $SAT_H$ of size at most $\log n$. Each such member comes from a $\psi$ of size $m+1+m^{H(m)} \leq \log n$, and in particular $m \leq \log n$. So we only need to know the value of $H$ on the much smaller values up to $\log n$.