Here is a way to do this in ZFC. Similar ideas work in a bunch of other contexts.

First, given any set $A$ in the universe of sets $V$ we can form the set theoretic universe $V(A)$ by mimicking the cumulative hierarchy, where the elements of $A$ are considered to be atoms. Start with $V_0(A) = A$, at successors $V_alpha+1(A) = V_alpha(A) cup mathcalP(V_alpha(A))$, at limits $V_delta(A) = bigcup_alpha<delta V_alpha(A)$. (Some care must be taken to carefully distinguish atoms. Indeed, $A$ will appear at some point in the pure part of $V(A)$ and we don't want to confound this pure $A$ with the set of atoms $A$. Fortunately, it is well-understood how to do this formally. Since these details are irrelevant, I will not mention them further.)

If $A$ has additional structure, say it's a complete ordered field, then that structure will appear quickly in the hierarchy since we add all possible subsets at each step. Therefore $A$ has all the same ordered field structure it originally had in $V$. Even completeness carries through since the subsets of $A$ in $V(A)$ come from subsets of the original $A$ in $V$. The difference is that $A$ has no internal structure in $V(A)$ since we can't inspect the innards of atoms: all we can say about atoms is whether two atoms equal or not. The main kicker is that if $A'$ is any isomorphic structure to $A$, then the isomorphism of $A'$ and $A$ lifts uniquely to an isomorphism of $V(A')$ and $V(A)$!

A normal mathematical statement about $A$ in $V$, say BSD, makes perfect sense about the structure $A$ in $V(A)$. This is because BSD makes no mention at all of the innards of the elements of $A$. Furthermore, if BSD holds of the original $A$ in $V$ then it will hold of the $A$ in $V(A)$ since they have identical external structure. Because $V(A')$ is isomorphic to $V(A)$, the isomorphism ensures that BSD holds of $A'$ in $V(A')$. Then, for the reverse reason explained above, BSD holds of the original $A'$ in $V$.

For this transfer from $A$ to $A'$, we only needed that BSD was a normal mathematical statement in the sense that it relies only on the external structure of $A$ and $A'$ and not on the innards of these structures. Whether some proof of BSD for $A$ relies heavily on the innards of $A$ is irrelevant since the statement proven makes no mention of the internal structure of $A$ and will therefore transfer to any isomorphic structure as described above.

From a logical viewpoint, this has nothing to do with platonism, ZFC, or the cumulative hierarchy.
$
defnnmathbbN
defzzmathbbZ
defqqmathbbQ
defrrmathbbR
defccmathbbC
$

Almost all reasonable mathematical statements about the reals are actually about any structure that satisfies the axiomatization of the reals. It is clear that this axiomatization can be expressed in very weak foundational systems, whether or not compatible with ZFC. Of course, if you are only familiar with ZFC then you may have to look at how things go in ZFC (as François G. Dorais has explained). But ZFC is really a red herring here.

The Cauchy-sequence or Dedekind-cut constructions merely serve to prove the existence of such a structure that satisfies the axiomatization of the reals. From then on, we can literally forget the exact objects in the construction (which is precisely what $∃$-intro does), because we are only interested in theorems concerning the axiomatized properties (interface) of the reals. Similarly when you construct the complex numbers by a quadratic extension of $rr$ by some object $i$ such that $i^2 = -1$ in the field extension $rr(i)$, it is completely irrelevant what objects are 'used' as elements in the field extension. For instance, you could use linear polynomials in $X$ with addition and multiplication modulo $X^2+1$. All that matters is that you get an algebraically closed field containing an isomorphic copy of the reals. Relatedly, we can assume that $rr ⊆ cc$ because we only care about the axiomatized properties of $rr$, which are preserved under isomorphism. One could manually preserve the original $rr$ as an actual subset of its quadratic extension, but that is unnecessary for the reason I just stated.

Long before $rr$, to even get from $nn$ to $zz$ we could either encode an integer as a sign with a magnitude, or as an equivalence class of pairs from $nn$. Does it matter? No, because all we care about are certain properties.

If someone claims to have proved something about reals but their proof needs to look at the concrete implementation of reals, then that someone simply has taken a silly route. This is akin to expressing an algorithm in the SOAP assembly language for the IBM 650, instead of expressing it in at least a high-level language supporting loops and function calls. Good software is always written to separate interface from implementation, and so are good proofs (whether in a formal system or not).

Consider simple examples. The IVT (intermediate value theorem) concerns continuous functions on a closed bounded interval of the reals. To state it directly, we must be able to quantify over real functions. This only needs 3rd-order arithmetic (since a real can be naturally encoded as a function of naturals, which is 2nd-order, so a function from reals to reals would be 3rd-order). More generally, if you want to talk about objects in specific higher-order types where the 0th-order type is the naturals, then all you need is HOA (higher-order arithmetic). Practically any modern foundational system for mathematics can interpret HOA, namely that there is a computable translation of proofs from HOA into the system that interprets it. You can check that Z set theory for instance interprets HOA, and if you want some extra interesting sets you might want some form of AC (axiom of choice).

Anyway, IVT is provable in HOA using only the axiomatization of the reals. And so are EVT (extreme value theorem), MVT (mean value theorem), Dini's theorem for real functions, ... You only need to go beyond HOA if you want to handle arbitrary types, such as general metric spaces, topological spaces and so on. Even then, every mathematical structure of interest will be defined via axiomatization, and all proofs based on that axiomatization alone would of course carry over to all those structures.

There is one possible snag, namely what if the proof was found by a computer rather than a human? Well, if the proof is really just one huge mess, then the easiest solution has been provided by Gareth McCaughan: We can tack on a proof of the equivalence of the desired theorem about Cauchy-reals with the same theorem stated for any isomorphic copy of the reals, and hence we can treat the given computer-generated proof as a black-box. More generally, we can write a computer program $P$ such that, given any desired statement $Q$ about a model $M$ of some second-order axiomatization $A$ that only uses $M$ via its interface $A$, $P(Q)$ outputs a proof that $Q(M)$ implies $Q(N)$ for every model $N$ of $A$. Then we do not even have to manually construct such kind of tack-on proofs but can just run that single program $P$ on any theorem that that 'wag' throws at you, and not just for those about reals. The exact details would depend on the chosen foundational system, but Z set theory certainly suffices.

There is no need to even go as far as $mathbbR$ for an example of this type of phenomena. Even $mathbbZ$ could be defined as different sets in ZFC. Let $omega$ be the first infinite cardinal, as usual

Option 1: We could take $mathbbZ=(omegatimes 0)cup ((omega-0)times 1),$ where the second coordinate tells us whether the integer is positive or negative.

Option 2: Switch second coordinates.

Now, if our background theory is ZFC, we can certainly create statements about $mathbbZ$ that are true for one of our constructions, and false for the other. (For instance, consider the statement: The additive identity of $mathbbZ$ is an ordered pair whose second coordinate is the empty set.)

What makes BSD and other questions often avoid this kind of problem, is that they are stated in a language of rings, or topological rings, etc... where the derived objects (like analytic rank) will be invariant when extended to a language allowing multiple identical copies of the structure at hand. (When it isn't immediately clear whether or not a definition or property is well-defined/invariant for the given context, good mathematical writing requires one to point this out.) And, yes, it is obvious that BSD only requires $mathbbR$ to be a completion of $mathbbQ$ at the archimedean place. (Obvious, because we would otherwise have required more in the statement of BSD.) And, yes, you can show that analytic ranks and algebraic ranks are preserved by isomorphisms between completions.

I see a lot of confusion in the comments about what you are asking and why. The way I interpret your question is this:

Given the fact that mathematical statements about (or involving) the reals can be divided into two classes,

A. those that are “isomorphism invariant” (their truth does not depend on which model of the reals you’re using) and

B. those that aren’t,

what is a way to decide whether a given statement belongs to class A or to class B?

I’ll offer a sociological rather than mathematical criterion: if the statement is (as in your example) an open problem with a $1,000,000 prize, or is otherwise a famous/important question, you can be pretty darn sure that it’s in class A; or, conceivably (but with a much lower likelihood) that it’s in class B but that the statement of the question would make very clear which model of the reals it pertains to.

The remaining possibility, that the question contains some kind of hidden ambiguity that makes it belong in class B but in a way that isn’t formally stated, seems essentially inconceivable to me in the context of well-known open problems. The reason is that most working mathematicians are Platonists who, when they think of the real numbers, think of some ideal set satisfying the properties they know the real numbers satisfy, and never concern themselves with pesky foundational issues regarding the actual model of the reals underlying the discussion. For such people, the statements in class A are the only interesting statements (and in some Platonist sense, the only “real” statements) about the reals. A model-dependent question would likely never deserve to be labeled as important, unless it was in some explicit foundations of math context where that model dependence would be an explicit part of the statement of the problem.

As for a formal mechanism that you are asking about for distinguishing between class A and class B statements, as others have said, you need to check that the statement will survive being passed through an isomorphism. How this is done in practice for something like BSD would probably be extremely tedious (and in my opinion isn’t worth the trouble), but an intuitive level, if the statement is phrased in a “coordinate-free” manner that doesn’t appeal to Dedekind cuts or other objects used in a specific realization of the reals, that’s probably good enough to declare “it’s obvious” and go and do something more productive with your time. Well, at least it would be for a Platonist like me.

I think it is essentially the Frege–Hilbert controversy on the nature of mathematical axioms, cf. e.g. https://plato.stanford.edu/entries/frege-hilbert/ :

The central difference between Frege and Hilbert over the nature of axioms, i.e., over the question whether axioms are determinately true claims about a fixed subject-matter or reinterpretable sentences expressing multiply-instantiable conditions, lies at the heart of the difference between an older way of thinking of theories, exemplified by Frege, and a new way that gathered strength at the end of the nineteenth century.

Frege (i) understands the consistency and independence of thoughts to turn not just on the surface syntax of the sentences that express them but also on the contents of the simple terms used in their expression, and (ii) consistency and independence, so understood, are not demonstrable in Hilbert’s manner.

[On] Frege’s conception of logic … given a good formal system, a sentence σ is deducible from a set Σ only if the thought expressed by σ is in fact logically entailed by the thoughts expressed by the members of Σ. (This simply requires that one’s axioms and rules of inference are well-chosen.) But the converse is false: that σ is not deducible in such a system from Σ is no guarantee that the thought expressed by σ is independent of the set of thoughts expressed by the members of Σ. For it may well be, as in the cases treated explicitly by Frege’s own analyses, that further analysis of the thoughts and their components will yield a more-complex structure. When this happens, the analysis may return yet-more complex (sets of) sentences σ′ and Σ′ such that σ′ is, after all, deducible from Σ′. … This is the explanation of Frege’s rejection of Hilbert’s treatment of consistency and independence …

Taking a theory to be axiomatized by a set of multiply-interpretable sentences, Hilbert’s view is that the consistency of such a set suffices for the existence of the (or a) collection of mathematical entities mentioned in the theory. The consistency, for example, of a theory of complex numbers is all that’s needed to justify the mathematical practice of reasoning in terms of such numbers. For Frege on the other hand, consistency can never guarantee existence. His preferred example to make this point is that the consistency (in Hilbert’s sense) of the trio of sentences 1. A is an intelligent being, 2. A is omnipresent, 3. A is omnipotent is insufficient to guarantee their instantiation. (See, e.g., Frege’s letter to Hilbert of 6 January 1900.)

Hilbert is clearly the winner in this debate, in the sense that roughly his conception of consistency [and logic] is what one means today by consistency [and logic] in the context of formal theories.

There is no need to use explicit models of $mathbb R$ in formulations of Swinnerton-Dyer conjecture. You could extend $mathbfZFC$ with symbols $(mathbb R,+_mathbb R,times_mathbb R,<_mathbb R,0_mathbb R,1_mathbb R)$ (in addition to symbols $=,in$) and add obvious axioms of Reals. After that you obtain new system, say $mathbfZFC+mathbb R$ in which you able to formulate any theorem about Reals model-independently using those new symbols. To be sure that $mathbfZFC+mathbb R$ is conservative extension of $mathbfZFC$ you should to justify your axioms by construction of either Dedekind or Cauchy reals. So, you should to proof in $mathbfZFC$ statement $$exists mathbb R_Cauchy, +_mathbb R_Cauchy,times_mathbb R_Cauchy,<_mathbb R_Cauchy,0_mathbb R_Cauchy,1_mathbb R_Cauchy (axiom_1 wedge axiom_2 wedge ... wedge axiom_n)$$
where $axiom_1,...,axiom_n$ is axioms of real numbers rewritten in terms of Cauchy reals, for example $axiom_1$ is
$$0_mathbb R_Cauchy in mathbbR_Cauchy$$ $axiom_2$ is $$forall x forall y (x in mathbb R_Cauchy wedge y in mathbb R_Cauchy to x+_mathbb R_Cauchy y = y +_mathbb R_Cauchy x)$$ and so on (of course you additionaly need to state that $+_mathbb R_Cauchy$ is well-defined function on $mathbb R_Cauchy$ and write $((x,y),t) in +_mathbbR_Cauchy$ rather than $x +_mathbbR_Cauchy y = t$) . After that you could (externally, on metalevel) deduce that your system $mathbfZFC+mathbbR$ is conservative extension of $mathbfZFC$ so you could work now inside $mathbfZFC + mathbbR$ instead of $mathbfZFC$ and formulate statements about Reals model-independently.

Maybe it sounds a little bit artificial but this is exactly how proof-checkers work see Note on definitions on Metamath Proof Explorer. Also, for example, see axiom ax-resscn and construction-dependent theorem axresscn which is justification of axiom ax-resscn and "should not be referenced directly".

I have a proposal for a (Nearly trivial) instance of such a theorem. Let $Form_(+,cdot,lt)$ be the set of a logical formulas constructed from the atoms $x+y$, $xcdot y$, and $xlt y$, with $x=y$ defined as $forall z(zlt xleftrightarrow zlt y)$. Then it is a simple to see (Though I will write it here anyway) that if $(mathbb R,+,cdot,lt)$ and $(mathbb R',+,cdot,lt)$ are Dedkind complete ordered fields, then $(mathbb R,+,cdot,lt)prec(mathbb R',+,cdot,lt)$, where "$prec$" denotes elementarity in $Form_(+,cdot,lt)$.

Given an ismorphisim $pi: (mathbb R,+,cdot,lt)rightarrow(mathbb R',+,cdot,lt)$, it is immediate that the relation holds for atomic formula, and inductively for logical connectives. Let $exists x(phi(x,x_0...x_n))$ be a $Form_(+,cdot,lt)$ formula, such that $(mathbb R,+,cdot,lt)vDash exists x(phi(x,x_0...x_n))$, and let $z$ be a witness to this. $$(mathbb R,+,cdot,lt)vDashphi(z,x_0...x_n)leftrightarrow(mathbb R',+,cdot,lt)vDashphi(pi(z),pi(x_0)...pi(x_n))$$

Therefore $(mathbb R',+,cdot,lt)vDashexists x(phi(x,pi(x_0)...pi(x_n)))$, and so $(mathbb R,+,cdot,lt)prec(mathbb R',+,cdot,lt)$. Why is this important? Well every formula about the Reals in $Form_(+,cdot,lt)$ is therefore absolute between Dedkind complete ordered fields.

They also satisfy the same second order assertions. Extend the language $Form_(+,cdot,lt)$ with an atomic formula $xin X$, and call $x$ a real if $M(x)leftrightarrow exists X(xin X)$. For a non-real $X$, then extend the isomorphisim $pi$ to $pi'$ by $pi'(X)=xin X$, and say $X=Y$ if and only if $forall x(xin Xleftrightarrow xin Y)$. Note that then $xin Xleftrightarrow pi'(x)in pi'(X)$, and so by the same argument as before $(mathbb R,+,cdot,lt,in)prec(mathbb R',+,cdot,lt,in)$.

So in order to get a result you want what we really want to show is that nearly every sensible statement about the Reals can be coded in just $Form_(+,cdot,lt,in)$. This can be verified individually, but a will give you an example: $x=0$, $x=1$, $xin mathbb N$, $xin mathbb Z$, $xin mathbb Q$, $xin mathbb CR$ (Constructible numbers), as well as algebraic functions can be written in $Form_(+,cdot,lt,in)$. First off, $x=0leftrightarrow forall y(M(y)rightarrow x+y=y)$, and similarly with $x=1$.

$$xinmathbb Nleftrightarrow forall X(0in Xlandforall nin X(n+1in X))$$

$$xinmathbb Zleftrightarrow xinmathbb Nlorexists yinmathbb N(x+y=0)$$

$$xinmathbb Qleftrightarrow forall X((Xsupseteqmathbb Zlandforall y,zin X(yover zin X))rightarrow xin X)$$ (See below)

$$xinmathbb CRleftrightarrow forall X((Xsupseteqmathbb Qlandforall yin X(sqrtyin X))rightarrow xin X)$$ (See below)

For the rest, $x=yover zleftrightarrow xcdot y=z$ and $x=sqrt yleftrightarrow xcdot x=y$. This process is just a couple examples. In fact, you could even though this for the Riemann Hypothesis and other complex mathematical problems. Therefore, your conjecture would almost certainly be absolute between the Cauchy and Dedkind reals.