Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
Not really relevant, but: I don't know which book the quote of Manin comes from, claiming Deligne's proof of Ramanujan's conjecture as a record for "length of proof / length of statement", but it is clearly utterly out-of-date by now. For instance the proof of Fermat's last theorem, or the Nikolov-Segal theorem in group theory (which is relatively short to state but whose proof uses the classification of finite simple groups), or Hales on Kepler's conjecture ... all of these are vastly more involved and lengthy proofs than Ramanujan.
This is the correct statement for (2). For (1) your formulation is correct if $K$ itself is totally real; but if $K$ isn't totally real, "the maximal totally real subfield of $K^{\mathrm{ab}}$" will not contain $K$! You want to replace "totally real" with "unramified at the real places of $K$" (i.e. as close to totally real as $K$ itself is).
I heard you the first time – you don't need to "@" tag someone who is already part of the comment exchange, they'll already get the notification. (It's sometimes done anyway when there are lots of different people involved in the conversation but that's not the case here.)
Kimball's construction can certainly be used to force $a_{n} = 0$ for all $n$ divisible by $\ell$, where $\ell$ is some prime dividing the level. But if we restrict to vanishing of $a_n$'s for $n$ coprime to the level of the Hida family then I don't know, and I think the question is a very interesting one.
Have you tried working out the $m = 1$ case first? In this case you're just looking for everything that commutes with a given linear endomorphism; and there are three cases according to whether $\phi$ is (a) diagonalisable with distinct eigenvalues, (b) scalar, or (c) a single 2x2 Jordan block, all of which you can easily bash out by hand.
MO comments are not the place for discussions. Moreover, your argument seems to have gone some way off-piste – "assuming $w_{\mathrm{alg}} = 0$ implies the HT weights are non-negative" is almost the opposite of the truth ($w_{\mathrm{alg}}$ is the average of the HT weights, so if $w_{\mathrm{alg}} = 0$, then the HT weights cannot all be non-negative unless they are all 0).
Regarding other (rather different) kinds of links between formal groups and values of L-functions, you might enjoy e.g. this paper of Kobayashi from a few years back: S. Kobayashi, Iwasawa theory for elliptic curves at supersingular primes, Invent. math. 152 (2003) 1, 1-36.
It's a rather "fragile" statement which doesn't generalise well (e.g. for an elliptic curve over a number field $F \ne \mathbb{Q}$ there is no statement like this).
For what it's worth, the particular paper I was referring to was a different one, arxiv.org/abs/2307.07004. But the one from Carlo's link does indeed use the same methods.