About proofs in descriptive complexity

Question

In descriptive complexity, we have theorems that look like $\mathrm{ESO} = \mathrm{NP}$ or "on linearly ordered structures, $FO(LFP) = P$", but I don't really understand the proofs of those.

For the latter, the intuitive equality really means that the statement "$\mathcal A\models \varphi$" can be verified to be true on a linearly ordered structure $\mathcal A$ in time $n^k$ iff $\varphi$ is expressible in some fixpoint logic. The right-to-left inclusion then reads $\forall M\; \mathrm{polytime \;TM}, \exists \varphi\in\mathrm{FO(LFP)} \quad \left[\mathcal A \models \varphi \Leftrightarrow M(\mathcal A) = 1\right]$.

The proof I have been taught in class for the right-to-left inclusion goes as follows: from a Turing machine M (with set of states $S$), we build a formula on the language $\{T_0,T_1\} \cup \{H_i : i\in S\}$, where all relations are of arity $2k$. This formula says that the structure it's being evaluated on is a correct computation of $M$ which ends in an accepting state. How does this prove the theorem? Of course, there is a bijection between accepting computations of $M$ and structures $\mathcal A$ s.t $M(\mathcal A) = 1$, but the statement of the theorem doesn't mention this bijection. In my opinion, the formula $\varphi$ that we create should really check properties of $\mathcal A$, and not properties of the computation of $M$ on $\mathcal A$... Where is my mistake? Am I overthinking this?