Does $\mathsf{ZFC}$ prove that the field of real numbers has one of these compactness properties? Suppose $\mathcal{A}$ is a $\Sigma$-structure and $\kappa<\lambda$ are infinite cardinals. Say that $\mathcal{A}$-satisfiability is $(\kappa,\lambda)$-compact iff for every theory $T$ in an expansion $\Sigma'$ of $\Sigma$ by constant symbols with $\vert T\vert<\lambda$, if every subtheory of $T$ of size $<\kappa$ has a model whose $\Sigma$-reduct is $\mathcal{A}$ then $T$ has a model whose $\Sigma$-reduct is $\mathcal{A}$.
I'm specifically interested in $\mathcal{R}=(\mathbb{R};+,\times)$. Combining my own observations with those of Joel David Hamkins, Farmer S, and Harry West, what I know so far roughly amounts to the following:

*

*$\mathsf{ZFC}$ proves that $\mathcal{R}$-satisfiability is not $(\omega_1,\omega_2)$-compact, $(\omega_2,\omega_3)$-compact, $(2^\omega,(2^{\omega})^+)$-compact, or $((2^\omega)^+,(2^\omega)^{++})$-compact.


*If $\kappa$ is measurable then $\mathcal{R}$-satisfiability is $(\kappa,\kappa^+)$-compact, and if $\kappa$ is strongly compact then $\mathcal{R}$-satisfiability is $(\kappa,\lambda$)-compact for every $\lambda>\kappa$.
At this point I'd like to know what positive results are guaranteed. Here's one which seems particularly interesting to me at the moment:

Does $\mathsf{ZFC}$ prove that there is a $\kappa>(2^{\omega})^+$ such that $\mathcal{R}$-satisfiability is $(\kappa,\kappa^{++})$-compact?

This sort of "gap-$2$" compactness seems rather hard to get, as far as I can tell, but at the same time I can't immediately extract any strength from it as a hypothesis. I suspect I'm missing something rather easy here.
 A: No: working in a model of ZFC+GCH+no inaccessibles, $\mathcal R$-satisfiability is not $(\kappa,\kappa^+)$-compact for any uncountable $\kappa.$ $\DeclareMathOperator{\bool}{bool}
\DeclareMathOperator{\true}{true}
\DeclareMathOperator{\false}{false}
\newcommand{\Mp}{M_{\mathrm{prop}}}$
I will just argue a simpler illustrative statement, which should make the above claim seem plausible.
The logic I’ll use is many-sorted first order with equality. Let $\Sigma$ be the signature with two sorts $\bool,0,$ with bool constants for $\false,\true,$ and sort $0$ constants $c^0_i$ for each element $i\in \omega,$ and no other functions or relations. Let $\mathcal O$ be the $\Sigma$-structure where the bool sort is interpreted as $\{\false,\true\},$ and sort $0$ is interpreted as $\omega,$ with constants $c^0_i$ interpreted as $i.$ I claim that $\mathcal O$-satisfiability is not $(\beth_2,\beth_2^+)$-compact.
Start by defining an extension $\mathcal V$ of $\mathcal O$ over a signature $\Sigma_{\mathcal V}\supset\Sigma$ with new sorts $1,2$ interpreted as sets $\mathcal P(\omega),\mathcal P(\mathcal P(\omega)).$ The signature $\Sigma_{\mathcal V}$ also has constants $c^i_j$ of sort $i$ for each (external) element $j\in\mathcal P^i(\omega),$ the two membership relations $\in^1$ of type $0\times 1$ and $\in^2$ of type $1\times 2,$ and two Skolem functions witnessing disequality: $u^0_1$ of type $1\times 1\to 0$ and $u^1_2$ of type $2\times 2\to 1.$ We need to pick such functions to define the model $\mathcal V,$ though all I really need is the two axioms:

*

*U1:  $(\forall a^1,b^1)((u^0_1(a^1,b^1)\in^1 a^1 \iff u^0_1(a^1,b^1)\in^1 b^1)\implies a^1=b^1)$

*U2:  $(\forall a^2,b^2)((u^1_2(a^2,b^2)\in^2 a^2 \iff u^1_2(a^2,b^2)\in^2 b^2)\implies a^2=b^2)$
Add to the true theorems of this structure a constant $t^2$ of sort $2$ with axioms $t^2\neq c^2_i$ for each $i\in \mathcal P(\mathcal P(\omega)).$ This produces a theory $T$ of signature $\Sigma_T.$
Add bool constants $I^{\bool}[\phi]$ for each formula $\phi$ in the signature of $T,$ and sort $0$ constants $I^0[s^0]$ for each term $s^0$ of sort $0,$ and add the following "interpretation axiom scheme":

*

*"$I^{\bool}[\phi]=\true\iff \phi$" for each $\phi$

*"$I^0[s^0]=s^0$" for each $s^0$
Add all logical consequences. Take the subtheory $T_0$ that restricts the signature to constants of sort $0$ and $\bool,$ and keep the theorems that can be expressed in this signature. $T_0$ is the theory we will use to disprove $(\beth_2,\beth_2^+)$-compactness. Note that its signature is an extension of $\Sigma$ by constants, as required.
Any subtheory $T’$ of $T_0$ of cardinality less than $\mathcal P(\mathcal P(\omega))$ has a model whose $\Sigma$-retract is $\mathcal O.$ Just pick a value $i$ of $t^2$ such that no theorem in $T’$ uses $c^2_i.$ Then $\mathcal V$ can be turned into a model of $T’$ by swapping the symbols $t^2$ and $c^2_i$ and interpreting the $I^{\bool}[\phi]$ and $I^0[s^0]$ constants in the unique manner consistent with the "interpretation axiom scheme".
Suppose for contradiction that $T_0$ itself has a model $M$ with $\Sigma$-reduct $\mathcal O.$ Let $\Mp$ be the set of statements $\phi$ in the language of $\Sigma_T$ such that $M\models I^{\bool}[\phi]=\true.$ This is a complete propositional theory extending the underlying propositional theory of $T.$ Define:
\begin{align*}
z&=\{y\in\mathcal P(\omega) : \Mp \vdash c^1_y \in^2 t^2 \} \in\mathcal P(\mathcal P(\omega))\\
t^1&=u^1_2(t^2,c^2_z)\text{ (just abbreviating the term)}\\
y&=\{x\in\omega : \Mp \vdash c^0_x \in^1 t^1 \} \in\mathcal P(\omega)\\
t^0&=u^0_1(t^1,c^1_y)\\
x&=(\text{$M$’s interpretation of $I^0[t^0]$})\in\omega
\end{align*}
$M \Vdash I^0[t^0]=c^0_x,$ and $T_0\vdash I^0[t^0]=c^0_x\implies I^{\bool}[t^0=c^0_x]=\true.$ So $\Mp \vdash t^0=c^0_x.$
And $\Mp\vdash t^1=c^1_y$:

*

*by substitution into axiom (U1), $T\vdash (t^0\in^1 t^1 \iff t^0\in^1 c^1_y)\implies t^1=c^1_y$

*hence $\Mp\vdash (t^0\in^1 t^1 \iff t^0\in^1 c^1_y) \implies t^1=c^1_y$

*we know $\Mp \vdash t^0=c^0_x$ (see previous paragraph)

*also, $\Mp \vdash c^0_x\in^1 t^1 \iff c^0_x\in^1 c^1_y$ by construction of $y$

*substitution rules using terms in $T$ are theorems of $\Mp$

*hence $\Mp\vdash t^0\in^1 t^1 \iff t^0\in^1 c^1_y$

*hence $\Mp\vdash t^1=c^1_y$
And $\Mp\vdash t^2=c^2_z$:

*

*by substitution into axiom (U2), $T\vdash (t^1\in^2 t^2 \iff t^1\in^2 c^2_z)\implies t^2=c^2_z$

*hence $\Mp\vdash (t^1\in^2 t^2 \iff t^1\in^2 c^2_z) \implies t^2=c^2_z$

*we know $\Mp \vdash t^1=c^1_y$ (see previous paragraph)

*also, $\Mp \vdash c^1_y\in^2 t^2 \iff c^1_y\in^2 c^2_z$ by construction of $z$

*substitution rules using terms in $T$ are theorems of $\Mp$

*hence $\Mp\vdash t^1\in^2 t^2 \iff t^1\in^2 c^2_z$

*hence $\Mp\vdash t^2=c^2_z$
But $\Mp\vdash t^2\neq c^2_z,$ a contradiction.
A: (Edit: This replaces an earlier attempt I had in the opposite direction, which was bogus, as pointed out by @HarryWest, and to which some comments below refer.)
(Edit 2: It now gets weak compactness as a consistency strength lower bound.)
(Edit 3: A part initially missing at the end of the Subcase 2.2 argument has been filled in.)
(Edit 4: 2 observations specifically on $(\kappa,\kappa^{++})$-compactness added at the end.)
Remark: It looks like @HarryWest has already answered the original question.
Below I work more directly with $\mathcal{R}$-satisfiability and extract some more strength. I don't know to what extent Harry's method would also lead to the following.
Remark 2: The reader unfamiliar with the Dodd-Jensen core model $K^{\mathrm{DJ}}$, but familiar with $0^\sharp$,
should replace "there is an inner model with a measurable cardinal"
in the claim below with "$0^\sharp$ exists", and replace $K^{\mathrm{DJ}}$ with $L$ throughout; this results in a weaker result, but the proof is essentially identical, and it suffices for Corollaries 1 and 3.
Claim. Assume ZFC. Let $\kappa$ be an uncountable cardinal
such that $\mathcal{R}$-satisfiability is $(\kappa,\kappa^+)$-compact.
Then there is a weakly inaccessible cardinal $\mu\leq\kappa$, and either:

*

*there is an inner model with a measurable cardinal, or


*letting $K=K^{\mathrm{DJ}}$ be the Dodd-Jensen core model below a measurable, $K\models$"$\kappa$ is weakly compact", and if $2^\gamma\leq\kappa$ for all $\gamma<\kappa$ then $\kappa$ is weakly compact.
Corollary 1. ZFC + "There is an uncountable cardinal $\kappa$ such that $\mathcal{R}$-satisfiability is $(\kappa,\kappa^+)$-compact"
is equiconsistent with ZFC + "There is a weakly compact cardinal".
Corollary 2. Assume ZFC + GCH + "there is no inner model with a measurable cardinal". Let $\kappa$ be an uncountable cardinal. Then $\mathcal{R}$-satisfiability
is $(\kappa,\kappa^+)$-compact iff $\kappa$ is weakly compact.
Corollary 3. Assume ZFC + GCH + "$0^\sharp$ does not exist".
Let $\kappa$ be an uncountable cardinal. Then $\mathcal{R}$-satisfiability
is $(\kappa,\kappa^+)$-compact iff $\kappa$ is weakly compact.
(Note that the converse direction of Corollaries 2 and 3, i.e. if $\kappa$ is weakly compact
then $\mathcal{R}$-satisfiability is $(\kappa,\kappa^+)$-compact,
holds in general.)
Proof of Claim: Fix $\kappa$. Except for the proof that there is a weakly inaccessible cardinal $\leq\kappa$, we may assume there is no inner model with a measurable cardinal, so write $K=K^{\mathrm{DJ}}$. (As mentioned in Remark 2, the reader unfamiliar with $K$ but familiar with
$0^\#$ should just assume $0^\#$ does not exist, in which case $K=L$.)
I will formally assume this, but it is easy to drop this assumption and still get the weakly inaccessible $\mu\leq\kappa$.
The plan is to find a reasonable elementary substructure $\bar{\mathcal{H}}$
of some fragment of $V$ and an elementary embedding $j:\bar{\mathcal{H}}\to M$ with a critical point $\mu$,  and use this to get the desired conclusions.
If there is $\gamma<\kappa$ such that $2^\gamma\geq\kappa$ then letting $\gamma$ be least such, fix a sequence $\left<A_\alpha\right>_{\alpha<\kappa}$
of pairwise distinct subsets of $\gamma$. Otherwise let $A_\alpha=\emptyset$
for all $\alpha<\kappa$. Let $\mathcal{H}=(\mathcal{H}_{\kappa^+},\vec{A},<^*)$,
where $<^*$ is a wellorder of $\mathcal{H}_{\kappa^+}$ (the set of all sets hereditarily of cardinality $\leq\kappa$).
We will build a theory $T$, of size $\kappa$, such that every sub-theory of size ${<\kappa}$ is $\mathcal{R}$-realizable. Basically, we want $T$  to describe
a model which contains a version of $\mathcal{H}$ as an element, together with the statement "$\kappa$ is not a cardinal".
The theory $T$ will use primary constants $\dot{\vec{\alpha}}$ for certain
sequences $\vec{\alpha}$ of ordinals ${<\kappa^+}$. The sequences $\vec{\alpha}$ used we call the relevant sequences,
and which are considered relevant depends on the following cases.
If (i) $\gamma^{\omega}\leq\kappa$ for all $\gamma<\kappa$
then there are only $\kappa$-many $\omega$-sequences $\vec{\alpha}\in{^\omega}\kappa$ such that $\vec{\alpha}$ is bounded in $\kappa$
(and of course if $\mathrm{cof}(\kappa)>\omega$, "bounded in $\kappa$" can be struck out), and in this case these sequences $\vec{\alpha}$ are the relevant ones.
Suppose instead (ii) there is $\gamma<\kappa$ such that $\gamma^{\omega}>\kappa$. If (ii.1) $\kappa^{+K}<\kappa^+$ then  the relevant
sequences are just the finite tuples $\vec{\alpha}\in\kappa^{<\omega}$. Suppose instead (ii.2) $\kappa^{+K}=\kappa^+$. In this case we need to be a little more careful. Fix from now on an ordinal $\eta\in(\kappa,\kappa^+)$  of cofinality
$\kappa$ and such that letting $\bar{\mathcal{H}}=\mathrm{Hull}^{\mathcal{H}}(\eta)$,
we have $\eta=\bar{\mathcal{H}}\cap\eta$. Then  the relevant
sequences are the finite tuples $\vec{\alpha}\in\eta^{<\omega}$. (Also
for the proof that there is a weakly inaccessible cardinal $\mu\leq\kappa$, i.e. without assuming $K$ exists,
in case (ii), proceed as in (ii.1).)
Using the process in the answer here: https://mathoverflow.net/questions/394526/is-this-compactness-property-for-satisfiability-on-mathbbr-consistent, we then also augment the theory
with some secondary constants, so as to allow us to talk about subsets of $\omega$ coded by reals, and to make arithmetic statements about those coded sets using (infinitely many) statements in $T$. We will skip the details of those extra constants, and just directly make arithmetic statements about the coded subsets of $\omega$.
For each relevant $\vec{\alpha}$, let $t_{\vec{\alpha}}$ be the full theory of the single parameter $\vec{\alpha}$ in the structure $\mathcal{H}$ (note this includes predicates for $\vec{A}$ and $<^*$).
Add the following statements to $T$ (they mostly refer to theories coded by reals):

*

*$\dot{\vec{\alpha}}$ codes a consistent complete theory $u_{\dot{\vec{\alpha}}}$ in the language of set theory augmented with symbols $\hat{\vec{\beta}},\hat{\mathcal{H}},\hat{f},\hat{\kappa},\hat{\xi}$,


*$u_{\dot{\vec{\alpha}}}$ contains the formula
"$\hat{\mathcal{H}}=(\mathcal{J},<',\vec{A}')$
is a structure with transitive universe $\hat{\mathcal{J}}$,
$<'$ is a wellorder of $\mathcal{J}$, and
$\hat{\kappa}$ is the largest cardinal of $\mathcal{J}$",


*$u_{\dot{\vec{\alpha}}}$ contains the formula "$V=L(\hat{\mathcal{H}},\hat{f})$ and
$\hat{\xi}<\hat{\kappa}$ and $\hat{f}:\hat{\xi}\to\hat{\kappa}$ is a surjection",


*the model determined by $u_{\dot{\vec{\alpha}}}$ has standard $\omega$,
and for each formula
$\varphi[\vec{\alpha}]\in t_{\vec{\alpha}}$, add the statement

*

*$u_{\dot{\vec{\alpha}}}$ contains the formula "$\hat{\mathcal{H}}\models\varphi[\dot{\vec{\beta}}]$"

to $T$.
Moreover, if $\vec{\gamma}$ is also relevant
and $\mathrm{rg}(\vec{\alpha})\subseteq\mathrm{rg}(\vec{\gamma})$
and in the $\omega$-sequence case, $\vec{\alpha}$ itself is easily computed from $\vec{\gamma}$
(say there is a recursive function $i:\omega\to\omega$ such that
$\vec{\alpha}_n=\vec{\gamma}_{i(n)}$),
then we add the formula

*

*$u_{\dot{\vec{\alpha}}}$ is the theory induced by $u_{\dot{\vec{\gamma}}}$
(according to how $\vec{\alpha}$ is computed from $\vec{\gamma}$)

to $T$.
Now let $S\subseteq T$ be a sub-theory of size ${<\kappa}$. We find an $\mathcal{R}$-realization of $S$.
Let $C$ be the set of relevant sequences $\vec{\alpha}$ used in $S$;
so $C$ has size ${<\kappa}$, and $C\subseteq\mathcal{H}$.
Let $H=\mathrm{Hull}^{\mathcal{H}}(C)$; that is, the structure whose universe is the set of all elements of $\mathcal{H}_{\kappa^+}$ definable over $\mathcal{H}$ from parameters in $C$ (using the predicates of $\mathcal{H}$),
and with predicates being the restrictions of those of $\mathcal{H}$. So $H\preccurlyeq\mathcal{H}$. Let $\bar{H}$ be the transitive collapse of $H$.
Let $\pi:\bar{H}\to H$ be the uncollapse map. Let $\bar{\kappa}=\pi^{-1}(\kappa)$ etc.
By enlarging $S,C$ if necessary, we may assume that $\bar{\kappa}$ has cardinality ${\xi<\bar{\kappa}}$. So let $f:\xi\to\bar{\kappa}$ be a surjection.
Let $N=L_\beta(\bar{H},f)$ for some ordinal $\beta>0$.
Now  for each
$\vec{\alpha}\in C$, let $u_{\vec{\alpha}}$ be the theory in $N$ of the parameters $\bar{\vec{\alpha}},\bar{H},f,\xi,\bar{\kappa}$, where bars denote preimage under $\pi$.
Then note that by interpreting
$\dot{\vec{\alpha}}$ as the real naturally coding $u_{\vec{\alpha}}$,
we get an $\mathcal{R}$-realization of $S$.
By $(\kappa,\kappa^+)$-compactness, we can fix
an $\mathcal{R}$-realization $\mathcal{R}^+$ of $T$.
Let $u_{\vec{\alpha}}$ be the theory coded by $\dot{\vec{\alpha}}^{\mathcal{R}^+}$.
Note that we can define a term model $M$, pointwise definable from constants
$\widetilde{\vec{\alpha}}$ (for relevant sequences $\vec{\alpha}$ as before)
and constants $\widetilde{\mathcal{H}},\widetilde{f},\widetilde{\xi},\widetilde{\kappa}$, and
such that $u_{\vec{\alpha}}$ is just the theory
in $M$ of $\widetilde{\vec{\alpha}}^M,\widetilde{\mathcal{H}}^M,\widetilde{f}^M,\widetilde{\xi}^M,\widetilde{\kappa}^M$ (the super-$M$ denotes the interpretation of a constant in $M$).
Let $\bar{\mathcal{H}}=\mathrm{Hull}^{\mathcal{H}}(C)$
where $C$ is the set of all relevant sequences (the hull is uncollapsed);
note that $\bar{\mathcal{H}}$ is in fact transitive (so actually it's the same as the collapsed hull) so $\bar{\mathcal{H}}\preccurlyeq\mathcal{H}$
(here $\bar{\mathcal{H}}$ is a structure with predicates induced by those of $\mathcal{H}$) (and note that in case (ii.2), what we defined as $\bar{\mathcal{H}}$ earlier is the same as the model we have just now defined, and so in this case $\mathrm{OR}\cap\bar{\mathcal{H}}=\eta$). We have $\kappa+1\subseteq\bar{\mathcal{H}}$.
(But $\kappa^+\not\subseteq\bar{\mathcal{H}}$,
since $\bar{\mathcal{H}}$ has cardinality $\kappa$.)
Note that there is an elementary embedding $j:\bar{\mathcal{H}}\to\widetilde{\mathcal{H}}^M$ given by setting $j(\vec{\alpha})=\widetilde{\vec{\alpha}}^M$ for each relevant $\vec{\alpha}$.
We have $j(\kappa)=\kappa^M$.
Since $\kappa$ is a cardinal in $V$, but $\kappa^M$ is not a cardinal in $M$
(though it is of course a cardinal in $\widetilde{\mathcal{H}}^M$), $j$ has a critical point $\mu\leq\kappa$ (here $M$ might be illfounded).
So $\mu$ is a regular cardinal in $\bar{\mathcal{H}}$,
and hence also regular in $V$. Note that $\mu>\omega$, as $M$ has standard $\omega$, as this held for each sub-model coded by $u_{\vec{\alpha}}$.
Note that $\mu$ is not a successor cardinal
(if $\mu=\gamma^+$ then $$\gamma^+=\mu<j(\mu)=j(\gamma^+)=j(\gamma)^{+M}=\gamma^{+M},$$
so $\mu$ is collapsed in $M$, a contradiction).
So $\mu$ is weakly inaccessible, in particular giving
the existence of a weakly inaccessible $\leq\kappa$
(we didn't yet use $K$). So from now on we do assume we have $K$,
i.e. there is no inner model with a measurable.
Case 1: $\gamma^{\omega}\leq\kappa$ for all $\gamma<\kappa$.
So the relvant sequences are the bounded-in-$\kappa$ $\omega$-sequences $\vec{\alpha}$. We consider two subcases.
Subcase 1.1: $\mu<\kappa$.
In this case there is an inner model with a measurable cardinal.
For if not, then the Dodd-Jensen core model $K$ (below an inner model with a measurable cardinal) exists. So there is no transitive proper class $K'$
and non-trivial elementary $k:K\to K'$.
And $K\models GCH$, and $\mathcal{P}(\mu)\cap K\subseteq\bar{\mathcal{H}}$.
Let $\delta$ be some "ordinal" of $M$ such that $\beta<\delta<j(\mu)$
for all $\beta<\mu$ (it doesn't matter whether $M$ is wellfounded;
but we will use that $M$ has wellfounded $\omega$).
Let $U$ be the $K$-ultrafilter
derived from $j$ with seed $\delta$. Then $\mathrm{Ult}(K,U)$ is wellfounded.
For suppose not, and let $\left<f_n,X_n\right>_{n<\omega}\subseteq K$ be such that $f_n:\mu\to\mathrm{OR}$ and $X_n\subseteq\mu$ and $X_n\in U$
and $f_{n+1}(\alpha)<f_n(\alpha)$ for all $\alpha\in X_n$,
for all $n<\omega$. Let $\vec{X}=\left<X_n\right>_{n<\omega}$.
Because $K|\mu^{+K}$ is definable over $\mathcal{H}_\kappa$
and satisfies "$V=\mathrm{HOD}$",  each $X_n$ is specified
by some ordinal $\alpha<\mu^+$, so there is a relevant $\vec{\alpha}$
such that $\left<X_n\right>_{n<\omega}$ is defined from $\vec{\alpha}$.
Let $X=\bigcap_{n<\omega}X_n$.
So $X\in\bar{\mathcal{H}}$, and (as $M$ has wellfounded $\omega$) $X\in U$,
and in particular $X\neq\emptyset$. But then letting $\beta\in X$,
we have $f_{n+1}(\beta)<f_n(\beta)$ for all $n<\omega$, a contradiction.
So $K'=\mathrm{Ult}(K,U)$ is wellfounded, but then the ultrapower
map $k:K\to K'$ is non-trivial, a contradiction.
Subcase 1.2: $\mu=\kappa$.
So all $\omega$-sequences $\subseteq\kappa$ are relevant, and it easily follows
that $M$ is closed under $\omega$-sequences, and hence wellfounded. We claim that $K\models$"$\kappa$ is weakly compact". For since $\kappa$ is weakly inaccessible,
it is inaccessible in $K$. Suppose $\kappa$ is not weakly compact in $K$.
We have $K_\kappa=V_\kappa^K\subseteq\bar{\mathcal{H}}$ and $V_{\kappa+1}^K\subseteq\mathcal{H}$, and so $\bar{\mathcal{H}}\models$"$\kappa$ is not weakly compact in $K$". Let $A\in V_{\kappa+1}^K$
with $A\in\bar{\mathcal{H}}$ and $\varphi$ be a $\Pi_1$ formula
such that $(V_{\kappa+1}^K,A)\models\varphi$
but there is no $\kappa'<\kappa$
such that $(V_{\kappa'+1}^K,A\cap V_{\kappa'}^K)\models\varphi$.
So the same holds for $j(\kappa)$ in $M$.
Since $M$ is wellfounded, we have $\kappa\in M$,
and can apply the statement at $\kappa'=\kappa$ in $M$,
which implies $(V_{\kappa+1}^{K^M},j(A)\cap V_{\kappa}^{K^M})\models\neg\varphi$, and so in fact $(V_{\kappa+1}^{K^M},A)\models\neg\varphi$.
But $M$ is closed under $\omega$-sequences, which implies that $K^M$
is iterable, and so $K^M|\kappa^{+K^M}$ is a segment of $K$
so $V_{\kappa+1}^{K^M}\subseteq K^M$, and since $\neg\varphi$ is $\Sigma_1$,
therefore $(V_{\kappa+1}^K,A)\models\neg\varphi$, a contradiction.
Now suppose $2^\gamma\leq\kappa$ for all $\gamma<\kappa$.
We first claim that $\kappa$ is actually inaccessible.
For suppose not, and let $\gamma<\kappa$ be least such that
$2^\gamma\geq\kappa$; by our assumption then, $2^\gamma=\kappa$.
Thus, we chose $\vec{A}$ to enumerate all subsets of $\gamma$,
in a one-to-one fashion.
But then $j(\vec{A})$ properly extends $\vec{A}$ with new subsets
of $\gamma$, a contradiction. Now one can show that $\kappa$ is weakly compact via an argument just like that used for $K$ above, but now in $V$
(and it is easier).
Case 2: Otherwise (there is $\gamma<\kappa$ such that $\gamma^{\omega}>\kappa$).
This case will be dealt with similarly to the previous one, but it is a little subtler. The relevant sequences are the finite tuples $\vec{\alpha}\in\eta^{<\omega}$, where $\eta=\kappa$ in case (ii.1).
Subcase 2.1: $\mu<\kappa$.
Define $\delta,U$ as in Subcase 1.1. We claim again that $\mathrm{Ult}(K,U)$ is wellfounded, which is again enough. Suppose not and let $\left<f_n,X_n\right>_{n<\omega}\subseteq K$ be as before. We have $X_n\subseteq\mu$.
Let $\alpha_n$ be the rank
of $X_n$ in the $K$-constructibility order. Then $\alpha_n<\mu^{+K}\leq\mu^+\leq\kappa$. By covering for $K$, there is a set $\mathcal{X}\in K$,
of cardinality $\leq\aleph_1^V$, such that $X_n\in\mathcal{X}$ for each $n$,
and $Y\subseteq\mu$ for each $Y\in\mathcal{X}$. Since $\aleph_2^V<\mu$,
the usual argument shows that $Z=\{Y\in\mathcal{X}\bigm|Y\in U\}$ is in $K$.
(That is, consider $\{Y\in j(\mathcal{X})\bigm|\delta\in Y\}\in M$,
and use the agreement between $M$ and $\bar{\mathcal{H}}$ below $\mu$.)
But then also since $\aleph_2^V<\mu$, it follows that $\bigcap Z\neq\emptyset$. Therefore $\bigcap_{n<\omega}X_n\neq\emptyset$,
so now we can argue for contradiction like in Subcase 2.1.
Subcase 2.2: $\mu=\kappa$.
In this case we show that $\kappa$ is weakly compact in $K$.
Suppose (ii.2) holds, so $\kappa^{+K}=\kappa^+$ and $\bar{\mathcal{H}}=\mathrm{Hull}^{\mathcal{H}}(\eta)$, and $\mathrm{cof}(\eta)=\kappa$.
Suppose $\kappa$ is not weakly compact in $K$. Then $K|\eta=K^{\bar{\mathcal{H}}}\models$"$\kappa$ is not weakly compact". So fix a counterexample $A,\varphi\in K|\eta$.
Define $U,\delta$ as before. We claim that $\mathrm{Ult}(K|\eta,U)$ is wellfounded. So suppose otherwise and let $\left<f_n,X_n\right>_{n<\omega}$ be a counterexample $\subseteq K|\eta$. Let $\alpha_n$ be the rank of $X_n$ in the order of constructibility of $K$. Let $\mathcal{X}=\{\alpha_n\bigm|n<\omega\}$. So by covering, there is $\mathcal{Y}\subset\mathrm{OR}$
such that $\mathcal{Y}\in K$ and $\mathcal{X}\subseteq\mathcal{Y}$ and $\mathcal{Y}$ has cardinality $\leq\aleph_1^V$. It suffices to see there is such a $\mathcal{Y}\in K|\eta$, as then we can argue as before.
Since $\kappa$ is the largest cardinal of $K|\eta$, there are cofinally many $\beta<\eta$ such that $K|\beta$ projects to $\kappa$, which means here that
there is a surjection $f:\kappa\to K|\beta$ which is definable without parameters over $K|\beta$. Fix such a $\beta,f$ with $X_n\in K|\beta$ for all $n$; this exists because $\mathrm{cof}(\eta)=\kappa$ and $\kappa$ is weakly inaccessible. So $f\in K|(\beta+1)\subseteq K|\eta$. Let $\mathcal{X}'$
be the set of all $\alpha<\kappa$ such that $f(\alpha)\in\mathcal{X}'$ and for no $\alpha'<\alpha$ is $f(\alpha')=f(\alpha)$. So $\mathcal{X}'\subset\kappa$ and $\mathcal{X}'$ is countable. So by covering, there is $\mathcal{Y}'\in K$ with $|\mathcal{Y}'|\leq\aleph_1^V$ and $\mathcal{X}'\subseteq\mathcal{Y}'$. Since $\kappa$ is weakly inaccessible,  $\mathcal{Y}'\in K|\kappa$. But then $\mathcal{Y}=f``\mathcal{Y}'$ covers $\mathcal{X}$ and $\mathcal{Y}\in K|(\beta+1)\subseteq K|\eta$, as desired.
Also, $N=\mathrm{Ult}(K|\eta,U)$ is iterable.
For it suffices to see that all countable elementary substructures
of $N$ are iterable. For this, given $\left<f_n\right>_{n<\omega}\subseteq K$, it suffices to see that $\bar{N}=\mathrm{Hull}^N(\{[f_n]\bigm|n<\omega\})$
is iterable (where $f_n$ represents $[f_n]\in N$). But we can find
sets $X_n\in K|\eta$ such that the $\Sigma_n$-elementary theory of $(f_0(\alpha),\ldots,f_n(\alpha))$ in $K|\eta$ is independent of $\alpha\in X_n$, and then arguing as before, $\bigcap_{n<\omega}X_n\neq\emptyset$,
so letting $\alpha\in\bigcap_{n<\omega}X_n$,   $\bar{N}$
is isomorphic to $\mathrm{Hull}^{K|\eta}(\{f_n(\alpha)\bigm|n<\omega\})$,
and is therefore iterable.
By the iterability, $N|\kappa^{+N}=K|\kappa^{+N}$, and so the failure of weak compactness now leads to a contradiction like before (applying the ultrapower map $i^{K_\eta}_U:K|\eta\to N$).
Finally if (ii.1) holds, it is almost the same as for (ii.2), but easier: note that $\kappa^{+K}<\eta=\mathrm{OR}\cap\bar{\mathcal{H}}$ in this case, so taking any (small) covering set $\mathcal{Y}\in K$  for a countable set $\mathcal{X}$, we get $\mathcal{Y}\in\bar{\mathcal{H}}$, which is again enough.

Regarding specifically $(\kappa,\kappa^{++})$-compactness of $\mathcal{R}$-satisfiability:
Observation 1: Assuming ZFC + $\kappa$ is uncountable + $\mathcal{R}$-satisfiability is $(\kappa,\kappa^{++})$-compact, we get an inner model with a measurable, by arguing much as above, but  allowing relevant sequences to take values anywhere ${<\kappa^+}$; this leads to a model $\bar{\mathcal{H}}\preccurlyeq\mathcal{H}$ with $\kappa^+\subseteq\bar{\mathcal{H}}$ and an embedding $j:\bar{\mathcal{H}}\to\widetilde{\mathcal{H}}^M$ at the end, and $j(\kappa)>\kappa$. This then gives an inner model with a measurable like when $\mu<\kappa$ in the preceding proof.
Observation 2: In the converse direction: Assume ZFC + GCH + $\kappa$ is $\kappa^+$-supercompact. Let $G$ be generic over $V$ for adding a $\kappa^{++}$-seqence of Cohen reals with the finite support product. Then $V[G]\models$"$2^{\aleph_0}=\kappa^{++}$ and $\mathcal{R}$-satisfiability is $(\kappa,\kappa^{++})$-compact".
This can be shown using a small variant of the argument in Update 2 of my answer to https://mathoverflow.net/questions/394526/is-this-compactness-property-for-satisfiability-on-mathbbr-consistent, which does the analogous thing for $(\kappa,\kappa^+)$-compactness from weak compactness.
