This is perhaps more of an extended comment than a real answer, but I do think it goes a long way towards answering these kinds of questions.
The set-theoretic result referred to as Shoenfield absoluteness is actually extremely broad and in fact cover a huge swath of 'ordinary mathematics' once one understands the relevant techniques for coding statements in terms of real numbers. This is to the extent that I actually suspect that the 'dezornification' mentioned in this answer to the referenced question could actually have been done using an absoluteness argument (which isn't to say that there isn't both practical and theoretical value in actually working out the details as is done in that paper).
Okay so what does Shoenfield absoluteness say? Given any model $V$ of $\mathsf{ZF}$ and an inner model $M \subseteq V$ containing the same ordinals, $\mathbf{\Sigma}^1_2$ sentences are absolute between $M$ and $V$ (i.e., $V$ satisfies a given $\mathbf{\Sigma}^1_2$ sentence if and only if $M$ satisfies the same sentence). A $\mathbf{\Sigma}^1_2$ sentence is roughly speaking a sentence of the form "There exists a real number $x$ such that for all real numbers $y$, $(x,y) \in B$." where $B$ is some Borel set. (Technically we need that the 'instructions for building $B$' live inside $M$, but that's not going to be an issue for how we're going to apply this result.) This implies that $\mathbf{\Pi}^1_2$ sentences (for all reals $x$, there is a real $y$ such that...) are similarly absolute and that $\mathbf{\Sigma}^1_3$ sentences (there exists an $x$ such that for all $y$ there exists a $z$...) are upwards absolute (i.e., if they hold in $M$, then they hold in $V$).
While this may seem relatively specific (since we're talking about just pairs or maybe triples of real numbers), it's important to recognize that since we're working with Borel conditions (rather than, say, merely continuous operations), a huge amount of information can be encoded in a single real number. The intuitive paradigm is this: Any object that can be specified by a countable amount of data can be encoded as a real number. This includes continuous functions, separable metric spaces, separable manifolds, countable algebraic rings, etc., and it also includes any sequences of such objects, since a countable bundle of countable bundles of data is still countable. (We think of the data as coming with an explicit enumeration, so the whole 'countable union of countable sets' issue is irrelevant here.)
The other thing that makes this powerful is the fact that given any such 'countably specified object' $x$, there is an inner model $L[x]$ of $V$ (containing the same ordinals) which satisfies a very strong form of the axiom of choice (specifically, global choice) as well as the (generalized) continuum hypothesis and a lot of other strong set-theoretic principles. In particular, this requires no choice at all in $V$.
Let's think about this in the case of a particular toy model (in possibly excruciating detail). Suppose we're thinking about some explicitly defined ordinarly differential equation $x' = f(x)$ (where $f$ is some fixed continuous function) and we want to show that for any given initial conditions $x(t_0) = x_0$, there is a solution to this differential equation that exists in some interval around $t_0$ and is maximal (in the sense that it cannot be extended to a larger interval). Suppose moreover that for the life of us we just can't see how to prove this without appealing to Zorn's lemma or (equivalently) transfinite induction and choice. Regardless we are able to show the following: $\mathsf{ZFC}$ proves that for any $(x_0,t_0)$, there is an interval $I$ and functions $X_0,X_1: I \to \mathbb{R}$ such that
- $t_0 \in I$,
- $X_0'(t) = X_1(t)$ for all $t \in I$,
- $X_0(t_0) = x_0$,
- $X_1(t) = f(X_0(t))$ for all $t \in I$, and
- for any larger interval $J \supset I$, no extension $(Y_0,Y_1)$ of $(X_0,X_1)$ to $J$ satisfies the above conditions.
At its face, this is a mess of quantifiers and seems like it might be too complicated to fit into the absoluteness framework I was talking about before, but it actually can. To make the statement a little more sane, we need some preliminary definitions.
A tame function is a function from $\mathbb{R}$ to $\mathbb{R}$ that is continuous and piecewise linear with rational coefficients and with finitely many conditions defined by rational endpoints. Note that a tame function can be coded by a single natural number. Given an open interval $I$ and a sequence of tame functions $(f^i)$, we say that $(f^i)$ represents a continuous function on $I$ if for each closed interval $K \subset I$ with rational endpoints, the sequence $(f^i)$ is a Cauchy sequence in the sup norm computed on rational points in $K$.
For a fixed $x_0$ and $t_0$, the claim can be written like this: There exists $\alpha \in \mathbb{R}$ such that for all $\beta \in \mathbb{R}$ there exists $\gamma \in \mathbb{R}$ such that
- $\alpha$ encodes an infinite tuple $(I,X_0^0,X_0^1,X_0^2,\dots,X_1^0, X_1^1, X_1^2,\dots)$ where $I$ is an open interval and $(X_0^i)$ and $(X_1^i)$ are sequences of tame functions representing continuous functions on $I$,
- $t_0 \in I$,
- if $\beta \in I$, then the derivative of $\lim_i X^i_0(t)$ at $\beta$ is equal to $\lim_i X^i_1(\beta)$,
- $\lim_i X^i_0(t_0) = x_0$,
- if $\beta \in I$, then $\lim_i X^i_1(\beta) = f(\lim_i X^i_0(\beta))$, and
IF $\beta$ codes an infinite tuple $(J_L,Y_0^0, Y_0^1,Y_0^2,\dots,Y_1^0, Y_1^1,Y_1^2,\dots)$ such that $J \supset I$ and $(Y^i_0)$ and $(Y^i_1)$ are sequences of tame functions representing continuous functions on $J$, $\lim_i X^i_j(r) = \lim_i Y^i_j(r)$ for both $j < 2$ and each rational $r \in I$, THEN $\gamma \in J$ and either
- the derivative of $\lim_i Y^i_0(t)$ at $\gamma$ is not equal to $\lim_i Y^i_1(\gamma)$ or
- $\lim_i Y^i_1(\gamma) \neq f(\lim_i Y^i_0(\gamma))$.
I claim that everything after the initial $\alpha\beta\gamma$ quantifiers is a Borel condition. The key is that at each point we're only quantifying over countable sets (such as the naturals or the rationals). This means that for a fixed choice of $t_0$ and $x_0$, this is a $\mathbf{\Sigma}^1_3$ sentence (and I actually think we can get away with only quantifying over rational $\gamma$, so it's probably actually only $\mathbf{\Sigma}^1_2$). Since we proved this in $\mathsf{ZFC}$, we know that it holds in the inner model $L[f,t_0,x_0]$ and then by Shoenfield absoluteness it actually holds in $V$. Therefore our choice-y proof can actually be systematically transformed into a proof in $\mathsf{ZF}$ with no choice at all.
This argument generalizes and shows that if you have any 'explicitly written' $\Pi^1_4$ sentence and you can prove it in $\mathsf{ZFC}$, then you can actually prove it in $\mathsf{ZF}$. Any $\Pi^1_4$ theorem that's actually written down in a paper is going to be explicit in this sense.
Now regarding GR in particular, there's ostensibly a jump in complexity, since not only does GR deal with PDEs instead of ODEs, but it deals with PDEs on differential manifolds that are themselves influenced by the dynamics of the PDE. Nevertheless, I actually claim that the story is not going to be so different from the toy model above (except for a proportionately greater amount of pain in actually coding things). For just 'ordinary' PDEs, assuming we're talking about bona fide pointwise solutions that are continuous functions (rather than, say, weak solutions), there's no different in terms of the quantifier complexity between specifying an initial condition that is a single real number and specifying an initial condition that is a continuous function defined on $\mathbb{R}^n$ (or indeed a Borel function of bounded Borel rank or a manifold with some specified Riemannian metric). These things are all countable bundles of data and the questions you ask about them are 'simple' enough that they can be expressed in a Borel way. The same is actually true of a (separable) manifold with a given metric. You can think of the manifold as being coded by a specific countable atlas which can ultimately be coded by a countable bundle of data.
In particular, this is why I think that the aforementioned 'dezornification' could have been done in a completely systematic way using Shoenfield absolutness. There's another additional wrinkle, which is that the result says that the solution is not just maximal but is in fact the unique maximal solution. This is a little bit more technical to state with GR because of the fact that solutions are manifolds with metrics on them rather than functions on a fixed background, but I believe it can still be formalized as an 'explicit' $\Pi^1_4$ sentence: For all initial data $x$, there is a solution $y$ such that [all proper extensions $z$ fail to be solutions] and [for all solutions $w$, there is a manifold embedding $f$ of $w$ into $y$ witnessing that $y$ is an extension of $w$]. With some massaging, this can be brought into the same form as what we did in the toy model (although this will use the fact that for continuous things we can get away with quantifying over rationals instead of arbitrary reals).
The reason I'm not comfortable calling this a proper answer is that I don't have enough background in mathematical GR to actually get a sense for whether all of the major results in it can be expressed as 'explicit' $\Pi^1_4$ sentences (or simpler), but I would actually be really, really surprised if this weren't the case. And in some sense, this is why I think these kinds of set theoretic issues are a bit of a red herring. $\mathsf{ZF}$ is not really any more 'constructive' than $\mathsf{ZFC}$ when it comes to 'tangibly small' objects. To me the more pernicious issue is whether the resulting object is in fact computable. Non-computable objects usually sneak in through compactness arguments (which are used in the kind of analysis that is relevant to applications such as physics), and (again for tangibly small objects) these are already valid in $\mathsf{ZF}$ alone with no choice at all.
