For a specific natural $k$ we define the language of couples $(\langle M \rangle, x)$ such that $M$ stops on $x$ and the couple's encoding is bounded by $k$ i.e $L_k := \{(\langle M \rangle ,x)\in HP : |(\langle M \rangle ,x)| \le k \}$ This language is finite thus in $R$. I wish to understand how to build (Not formally) a TM, $\tilde{M}$ which decide this language. Since the only given information is that the encoding is bounded, I tried to think about "Pigeonhole" claim, i.e define $\tilde{M}$ which simulate $M$ computation on $x$ and remembering the configurations made by $M$ or by counting steps made by $M$ during the simulation in order to determine that $M$ is stuck in a loop. Since $M$ is deterministic, if $\tilde{M}$ "see" the same configuration twice, it guarantees that $M$ entered a loop, but I can't explain why the finite encoding of $(\langle M \rangle,x)$ promises that a configuration will repeat itself.
You cannot construct an explicit algorithm/TM which will decide the language $L_k$. Regarding your attempt at the proof: you are right that there is no guarantee that the configuration will repeat because these machines are not given to be space bounded.
The TM $M_k$ to decide $L_k$ will have all the tuples (which are finite in number) which are accepted hard coded in it. The TM will basically perform a search in a look up table: if that tuple is found then accept it, else reject. We don't care how these tuples are actually obtained.
We can perhaps even prove that a general method to construct such TM $M_k$ for each $L_k$ cannot exists: Suppse there exists, then for a given input $<M,x>$, find the length of input, let it be $k$ and construct the TM $M_k$. Simulate $M_k$ over $<M,x>$. This will act as a decider for Halting Problem: which we know is undecidable. Hence, the assumption that we can have such a method is false.
