LaTeX tip: \limsup and \liminf exist.

I don't think it's entirely fair to call this a "theorem" if you don't have a proof of the statement.

I believe all results on strong BSD proceed by working $p$-adically, so all partial progress will proceed via (4). I believe this paper describes the state of the art of this result. It can probably be used to give examples for (2-a) and (3-b). FYI, the quotient $c(E)/c_1(E)$ is sometimes called the analytic order of Sha.

Strictly speaking, the first sentence doesn't make sense - the two formal groups won't be literally equal, I suppose you mean that they are isomorphic. This implies that for some choice of coordinates the corresponding formal group laws will be equal. However, over a field of characteristic zero, any two commutative formal group laws are isomorphic. As Daniel Litt suggests, you probably want to work integrally instead.

Positive (lower) density is not enough - for instance the set $R=\{n\in\mathbb N\mid \{n\sqrt{2}\}\in[0,1/2]\}$ has density $1/2$ (by Weyl) but by construction the set $R\sqrt{2}$ is not dense mod $1$. On the other hand, if $R$ has (upper?) density $1$, it should hold, as again by Weyl you can argue it will visit every interval infinitely often.

See this related question. The references in the question prove this result conditionally on some standard conjectures.

It is very unclear to me what your goal even is. You also seem to be neglecting any issues arising from nonuniqueness of binary expansions.

For the same reason it's true if the nilradical is itself a nilpotent ideal. I doubt it's necessary, but one necessary condition is $\bigcap_n I^n=\{0\}$, so for instance taking something like the Puiseaux ring modulo $x$ will give a nonexample. I'm not sure exactly what kind of answer you expect.

Do you specifically want the least such $r$ or just some such $r$?

Closely related OEIS sequence. This is sufficiently irregular that I highly doubt anything resembling a closed form exists.

@Anixx You are looking at the wrong subsection. You want to look at the one under "Line integral of a scalar field" like Carlo mentioned.

The key idea is to take a map $\mathbb Q(\alpha)\to F$ other than the standard embedding and extend it to all of $F$ using normality of $F$. That this is always possible is nontrivial but only uses pretty general field theory. For any more details I strongly urge you to pick up some textbook.

I agree with Alec. The statement that you are trying to prove is one of the foundational ones in Galois theory, and I'd say if you want to understand these things, there is no better way than picking up a text on Galois theory. If you were to prove this statement independently, then you would really be halfway to showing Galois correspondence anyway.

This is immediate from Galois correspondence - being a splitting field of $P_n$, $F/\mathbb Q$ is Galois, so $F^{Gal(F/\mathbb Q)}=\mathbb Q$, that is the only elements of this extension which are fixed by all automorphisms are rational. Your generalization is false for non-Galois extensions, e.g. $\mathbb Q(\sqrt[3]{2})$ has no nontrivial automorphisms.

Equal sets always have the same elements. That's a property of equality in classical logic way more fundamental than any axiom.

Well, the thing is that negating a universal axiom only demands there to be one counterexample. So for instance when negating the axiom of extensionality the universe might look largely the same, except for some extremely high rank counterexamples. In particular, you probably shouldn't expect these negations to have many interesting consequences. This makes the question not that different from asking what can and can't be proven without extensionality whatsoever.