Preserve validity between the two Kripke frames

The background of our discussion is intuitionistic logic, i.e. the following definitions are intuitionistic Kripke frame.

For $$n \geq 1$$, let $$\mathcal{C}_n$$ denote the frame which is shown in Fig.1. It is formed by the set: $$\left\{(i, j)\in \omega \times \omega \mid (i=0, 0 \leq j \leq 1) \vee (1 \leq i \leq n-2, 0 \leq j \leq 3) \vee (i=n-1, j=0)\right\},$$ with the accessibility relation described in

.

For $$1\leq s\leq n-2$$, the frame $$\mathcal{C}_n(s)$$ denote the frame which is shown in Fig.2. It is formed by the set: $$\left\{(i, j)\in \omega \times \omega \mid (i=0, 0 \leq j \leq 1) \vee (1 \leq i \leq n-2, i \neq s, 0 \leq j \leq 3)\vee (i=s, j=0) \vee (i=n-1, j=0)\right\},$$ with the accessibility relation described in

Thus the frame $$\mathcal{C}_n(s)$$ is obtained by gluing $$(s,0)$$, $$(s,1)$$, $$(s,2)$$, $$(s,3)$$ together of the frame $$\mathcal{C}_n$$.

I want to prove the following result:

Assuming $$\psi$$ is a formula with $$m$$ variables, $$n$$ is a sufficiently large number. Then there exists $$s \leq n$$ such that, if $$\mathcal{C}_n \nvDash \psi$$ then $$\mathcal{C}_n(s)\nvDash \psi$$.

My attempt at analysis is: let $$\psi(p_1, ... ,p_m)$$ be a formula with $$m$$ varibles. Because $$V(p_j)$$, the valuation on $$\mathcal{C}_n$$ of a given variable $$p_t$$, is an upset, there will be $$(i,0)$$, $$(i,1)$$, $$(i,2)$$, $$(i,3)$$, $$(i-1,0)$$, $$(i-1,1)$$, $$(i-1,2)$$, $$(i-1,3)$$ (or similar result for more points) agree on any variable when the height $$n$$ of $$\mathcal{C}_n$$ is sufficiently large. Then we have a valuation $$V'(p_j):=V(p_j)\setminus \{(i,1), (i,2), (i,3)\}$$ on $$\mathcal{C}_n(i)$$. $$f$$ is a map from $$\langle\mathcal{C}_n, V\rangle$$ onto $$\langle\mathcal{C}_n(i), V'\rangle$$: $$f(x)=(i,0)$$ if $$x \in \{(i,0),(i,1), (i,2), (i,3)\}$$ and $$f(x)=x$$ otherwise. I am in trouble since $$f$$ is not a $$p$$-morphism.

The result is actually false, for $$m=6$$. (One can bring it down to $$m=2$$ with a bit of effort.)

Let $$n$$ be arbitrarily large, and $$\phi_n(\vec q)$$ be a Jankov–De Jongh frame formula of $$\def\p#1{\langle#1\rangle}\def\C{\mathcal C}\C_n$$, so that for any frame $$F$$, $$F\nvDash\phi_n\iff\text{\C_n is a p-morphic image of a generated subframe of F}.$$ Let $$V$$ be the valuation in $$\C_n$$ to the six variables $$p_{(i,j)}$$, $$(i,j)\in\C_n$$, $$i\le1$$, such that $$V(p_x)=\{y\in\C_n:y\nleq x\}.$$ We define a formula $$\alpha_x(\vec p)$$ for each $$x\in\C_n$$ by induction on $$i$$: $$\alpha_{(i,j)}=\begin{cases} p_{(i,j)}&i\le1,\\ \alpha_{(i-1,j)}\to\bigvee_{j'\ne j}\alpha_{(i-1,j')}&2\le i\le n-2,\\ \bigvee_{j'}\alpha_{(i-1,j')}&i=n-1. \end{cases}$$ Then we see by induction on $$i$$ that for all $$x,y\in\C_n$$, $$\p{\C_n,V},y\models\alpha_x\iff y\nleq x.$$ It follows that if $$U$$ is an arbitrary upper subset of $$\C_n$$, then $$y\in U\iff\p{\C_n,V},y\models\beta_U,$$ where $$\beta_U=\bigwedge_{x\notin U}\alpha_x.$$

Since $$\C_n$$ is a p-morphic image of itself, there is a valuation $$W$$ to the variables $$\vec q$$ such that $$\p{\C_n,W}\nvDash\phi_n$$. Let $$\sigma$$ be the substitution $$\sigma(q_i)=\beta_{W(q_i)}.$$ Then $$\p{\C_n,W},x\models\chi\iff\p{\C_n,V},x\models\sigma(\chi)$$ for all $$x\in\C_n$$ and all formulas $$\chi(\vec q)$$.

Thus, $$\psi_n=\sigma(\phi_n)$$ is a formula in the six variables $$\vec p$$, and by construction, $$\C_n\nvDash\psi_n$$ under $$V$$. However, for all $$s\le n-2$$, we have $$\C_n(s)\models\phi_n$$, and a fortiori $$\C_n(s)\models\psi_n$$, as $$\C_n$$ is not a p-morphic image of a generated subframe of $$\C_n(s)$$ (or of any other frame of size strictly smaller than $$|\C_n|$$, for that matter).

To reduce $$m$$ from $$6$$ to $$3$$, replace $$V$$ with a valuation of $$\{p_0,p_1,p_2\}$$ such that $$V(p_0)=\{(0,0),(0,1),(1,0),(1,1)\}$$, $$V(p_1)=\{(0,0),(0,1),(1,0),(1,2)\}$$, and $$V(p_2)=\{(0,0)\}$$. Show that you can still define suitable formulas $$\alpha_x$$.

To reduce it further to $$m=2$$, drop $$p_2$$, and show that you can define every upset $$U\subseteq\C_n$$ that does not differentiate the points $$(0,0)$$, $$(0,1)$$, and $$(1,0)$$. This allows you to carry out the argument above with $$\phi_n$$ replaced with the frame formula of the frame $$\C'_n$$ obtained from $$\C_n$$ by identifying $$(0,0)$$, $$(0,1)$$, and $$(1,0)$$. Note that $$\C'_n$$ still has strictly larger cardinality than $$\C(s)$$.

Finally, it is easy to show that the result holds for $$m=1$$, as there are only a constant number of formulas in one variable (up to equivalence) not valid in any $$\C_n$$.