Torsion subgroup of the group of points of an elliptic curve over local field Let $K$ be a local field with residue field $k$ and $E/K$ an elliptic curve. I'm interested for which $K$ and $E$ the group of torsion points on the curve is finite. I can prove that this group is finite for an $n$-dimensional local field $K$ such that its $(n-1)$'th residue field has zero characteristics i.e. a finite extension of $\mathbb Q_p$. The proof goes by induction on $n$.
Basis.
Let $K$ be a one-dimensional local field i.e. $k = \mathbb F_q$,$q=p^r$. We use the standard notation $E_0(K) = \{P\in E(K)|\tilde{P}\in \tilde{E_{ns}}(k)\}$ and $E_1(K) = \{P\in E(K)|\tilde{P} = \tilde{O}\}$. Then we have an exact sequence of abelian groups:
$$
0\to E_1(K) \to E_0(K) \to \tilde{E_{ns}}(k) \to 0.
$$
We know that $E_1(K) \cong \hat{E}(\mathcal M)$ where $\hat{E}$ is the formal group associated with $E$, hence $E_1(K)$ has no non-trivial elements of order $m$. From the exact sequence we see that $E_0(K)[m]$ injects to $\tilde{E_{ns}}(k)$ so all non-trivial torsion elements of $E_0(K)$ go to non trivial torsion elements of $\tilde{E_{ns}}(k)$. But $\#\tilde{E_{ns}}(k)$ is finite so the number of such torsion elements is finite. By Kodaira-Néron theorem the index of $E_0(K)$ in $E(K)$ is finite so we have proved that the torsion of $E(K)$ is finite.
Step.
Suppose we have proved the theorem for all $(n-1)$-dimensional local fields. Let $K$ be an $n$-dimensional local field i.e. $k$ is an $(n-1)$-dimensional local field. Then if the curve has good reduction the same argument reduces the case to $k$. If not $\tilde{E_{ns}}(k)$ is isomorphic either to $k^*$ or $k^+$ which have finite torsion.
Q.E.D.
I have two hypotheses. The first is that this is true for all local field of finite dimension. The second is that the only fields that have this property are subfields of higher local fields. In particular, having the property that the torsion of $E(K)$ is finite depends only on the field but not on the curve. Can you prove these statements or provide a counterexample?
EDIT There are some mistakes in my proof. First of all, there might exist $p$-torsion in $E_1(K)$ where $p$ is the characteristics but it is finite because $E_1(K)$ is a pro-$p$-finite group such that $p^r$-torsion is finite for every $r$. But I don't know how to generalize this to the case of higher-dimensional fields because now $E_1(K)$ is not at all pro-$p$-group.
 A: This is more of an answer to the stream of comments than to the question directly.  The comments concern the statement that for an elliptic curve $E$ defined over $\mathbb{F}_q((t))$, the torsion subgroup of $E(\mathbb{F}_q((t)))$ is finite.  Vesselin Dimitrov claimed that this appears in

Clark, Pete L.; Xarles, Xavier Local bounds for torsion points on abelian varieties. Canad. J. Math. 60 (2008), no. 3, 532–555. (doi: 10.4153/CJM-2008-026-x, Internet Archive))

The OP pointed out that it doesn't.  I just looked back myself: the OP is right, but Vesselin is also morally right.  The statement of that result does not appear in the paper, but Section 3 studies a standard three term filtration on $A(K)$ for $K$ a complete DVF with finite residue field and $A_{/K}$ an abelian variety.  To show that $A(K)[\operatorname{tors}]$ is finite, it suffices to show that the torsion subgroups of the successive quotients of the filtration are finite.  The point of this section is to do better than that: i.e., give explicit upper bounds on the the torsion subgroups
of the successive quotients of the filtration in terms of invariants of $A$ like its dimension and reduction type.  In case $K = \mathbb{F}_q((t))$ this is not achieved -- rather, a counterexample is given to the form of the bounds obtained in the characteristic $0$ case -- but nevertheless the successive quotients are shown to have finite torsion subgroups, so $A(K)[\operatorname{tors}]$ is finite.  The part that needs separate attention in positive characteristic is the torsion in the formal group: for this, see Proposition 3.2.
I also wanted to mention that a more recent (or recently published; the paper was accepted several years ago!) paper gives a treatment of the structure theory of (compact, commutative, second countable) $\mathbb{F}_q((t))$-analytic Lie groups, which in particular gives another proof of the finiteness of the torsion subgroup in the case of an abelian variety.  See Theorem 5.2 of

Clark, Pete L.; Lacy, Allan; There are genus one curves of every index over every infinite, finitely generated field. J. Reine Angew. Math. 749 (2019), 65–86. (doi: 10.1515/crelle-2016-0037 ;arXiv: 1405.2108)

