Let $\{p_0,\dots,p_{n-1}\}$ be an enumeration of all variables occurring in $A$, and if $e$ is any Boolean assignment $e\colon\{p_i:i<n\}\to\{0,1\}$, put $$p^e:=\ET_{e(p_i)=1}p_i\land\ET_{r(p_i)=0}\neg p_i.$$ We can write an arbitrary Boolean formula $B$ in the full conjunctive normal form $$\vdash_{\mathrm{CPC}}B\leftrightarrow\ET_{e(B)=0}\neg p^e.$$ Since $v$ makes true all axioms of type (2), we have $$\tag{$*$}v(\Box B)=v\Bigl(\ET_{e(B)=0}\Box\neg p^e\Bigr).$$ Let $e_0$ be the restriction of $v$ to variables, and put $$E=\{e:v(\Box\neg p^e)=0\}.$$ Define a Kripke model $M=\langle W,R,\models\rangle$ by \begin{align*} W&=E\cup\{e_0\},\\ e\mathrel R e'&\EQ\begin{cases} e'\in E&\text{if $e=e_0$,}\\ e=e'&\text{otherwise,} \end{cases}\\ e\models p_i&\EQ e(p_i)=1. \end{align*} In other words, $M$ is a tree of height $\le2$ with root $e_0$, and reflexive leaves $e\in E\smallsetminus\{e_0\}$. The root is reflexive iff $e_0\in E$. It follows immediately from $(*)$ and the definition that $$\tag{$**$}v(B)=1\iff M,e_0\models B$$ for every formula $B$ of degree $\le1$, in particular $M,e_0\nvDash A$.

It remains to verify that $\langle W,R\rangle$ is an $S$-frame. Since every subset $X\subseteq W$ is definable by a Boolean formula in $M$ (namely, $\LOR_{e\in X}p^e$), it suffices to show that $M$ satisfies all Boolean substitution instances of $S$-axioms. Every such instance $B$ is an axiom of the type (3), hence $(**)$ gives immediately that $M,e_0\models B$. In order to verify $M,e\models B$ for $e\ne e_0$, let $\theta$ be the Boolean substitution $$\theta(p_i)=\begin{cases}\top&\text{if $e(p_i)=1$,}\\\bot&\text{otherwise.}\end{cases}$$ Then $$M,e'\models\theta(C)\iff M,e_0\models C$$ for every $e'\in W$ and every formula $C$ by induction on the complexity of $C$. (The induction step for $\Box$ needs that $e_0$ has a successor, i.e., $E$ is nonempty. This follows from the assumption $e\ne e_0$.) Since we already know that $M,e_0\models\theta(B)$, we obtain $M,e\models B$.

Let $\{p_0,\dots,p_{n-1}\}$ be an enumeration of all variables occurring in $A$, and if $e$ is any Boolean assignment $e\colon\{p_i:i<n\}\to\{0,1\}$, put $$p^e:=\ET_{e(p_i)=1}p_i\land\ET_{r(p_i)=0}\neg p_i.$$ We can write an arbitrary Boolean formula $B$ in the full conjunctive normal form $$\vdash_{\mathrm{CPC}}B\leftrightarrow\ET_{e(B)=0}\neg p^e.$$ Since $v$ makes true all axioms of type (2), we have $$\tag{$*$}v(\Box B)=v\Bigl(\ET_{e(B)=0}\Box\neg p^e\Bigr).$$ Let $e_0$ be the restriction of $v$ to variables, and put $$E=\{e:v(\Box\neg p^e)=0\}.$$ Define a Kripke model $M=\langle W,R,\models\rangle$ by \begin{align*} W&=E\cup\{e_0\},\\ e\mathrel R e'&\EQ\begin{cases} e'\in E&\text{if $e=e_0$,}\\ e=e'&\text{otherwise,} \end{cases}\\ e\models p_i&\EQ e(p_i)=1. \end{align*} In other words, $M$ is a tree of height $\le2$ with root $e_0$, and reflexive leaves $e\in E\smallsetminus\{e_0\}$. The root is reflexive iff $e_0\in E$. It follows immediately from $(*)$ and the definition that $$\tag{$*{*}$}v(B)=1\iff M,e_0\models B$$ for every formula $B$ of degree $\le1$, in particular $M,e_0\nvDash A$.

It remains to verify that $\langle W,R\rangle$ is an $S$-frame. Since every subset $X\subseteq W$ is definable by a Boolean formula in $M$ (namely, $\LOR_{e\in X}p^e$), it suffices to show that $M$ satisfies all Boolean substitution instances of $S$-axioms. Every such instance $B$ is an axiom of the type (3), hence $(**)$ gives immediately that $M,e_0\models B$. In order to verify $M,e\models B$ for $e\ne e_0$, let $\theta$ be the Boolean substitution $$\theta(p_i)=\begin{cases}\top&\text{if $e(p_i)=1$,}\\\bot&\text{otherwise.}\end{cases}$$ Then $$\tag{$*{*}{*}$}M,e'\models\theta(C)\iff M,e\models C$$ for every $e'\in W$ and every formula $C$ by induction on the complexity of $C$. (The induction step for $\Box$ needs that $e_0$ has a successor, i.e., $E$ is nonempty. This follows from the assumption $e\ne e_0$.) Since we already know that $M,e_0\models\theta(B)$, we obtain $M,e\models B$ by taking $C=B$ and $e'=e_0$ in $(*{*}*)$.

$\let\ET\bigwedge\let\LOR\bigvee\let\EQ\Leftrightarrow$The property is true for extensions of K (i.e., normal modal logics). You didn’t really describe the proof system you are interested in, but based on the discussion in the question, I will assume it is a Hilbert-style proof system with the rules of modus ponens and necessitation, and substitution instances of a fixed set of axioms, including a complete axiomatization of classical propositional logic, and the distributivity axiom of K.

First, note that the “stronger property” putting a bound on the number of variables is trivially equivalent to the original formulation: given a proof of a formula $A$, you can uniformly substitute a fixed formula (e.g., $\bot$ if it’s in the language, or a variable from $A$) for every variable in the proof which does not occur in $A$, obtaining a proof of $A$ which only involves variables from $A$.

$\let\ET\bigwedge\let\LOR\bigvee\let\EQ\Leftrightarrow$The property is true for extensions of K (i.e., normal modal logics). You didn’t really describe the proof system you are interested in, but based on the discussion in the question, I will assume it is a Hilbert-style proof system with the rules of modus ponens and necessitation, and substitution instances of a fixed set of axioms, including a complete axiomatization of classical propositional logic, and the distributivity axiom of K. (It seems that you also allow substitution to be used as a rule. I prefer the formulation I gave with no substitution rule, but axioms schemata closed under substitution, because it has nicer structural properties. Of course, one can simulate schemata in the other system by an explicit application of substitution on the base form of the axiom.)

First, note that the “stronger property” putting a bound on the number of variables is trivially equivalent to the original formulation: given a proof of a formula $A$, you can uniformly substitute a fixed formula (e.g., $\bot$ if it’s in the language, or a variable from $A$) in all formulas in the proof for each variable which does not occur in $A$, obtaining a proof of $A$ which only involves variables from $A$.