\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage[a4paper,margin=28mm]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{microtype,enumitem}
\usepackage{tikz}
\usetikzlibrary{arrows.meta}
\usepackage[round,authoryear]{natbib}
\usepackage{xurl}
\usepackage[hidelinks]{hyperref}
\usepackage[nameinlink,noabbrev,capitalise]{cleveref}
\setlist{itemsep=3pt,topsep=5pt}
\setlength{\emergencystretch}{2em}
\providecommand{\doi}[1]{\href{https://doi.org/#1}{\nolinkurl{doi:#1}}}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\Lsf}{\mathcal L_{\mathrm{sf}}}
\newcommand{\Li}{\mathcal L_{\mathrm i}}
\newcommand{\B}{\mathfrak B}
\newcommand{\Comp}{\mathcal C}
\newcommand{\IPC}{\mathsf{IPC}}
\newcommand{\forces}{\Vdash}
\newcommand{\gforces}{\Vdash^{g}}
\newcommand{\Max}{\operatorname{Max}}
\newcommand{\Th}{\operatorname{Th}}
\newcommand{\Ass}{\operatorname{Ass}}
\newcommand{\Up}{\operatorname{Up}}
\newcommand{\id}{\operatorname{id}}

\title{Intuitionistic Compression and Optimal Verification Trees}
\author{Zhenyu Sun \and Jilin Wang}
\date{}
\hypersetup{
 pdftitle={Intuitionistic Compression and Optimal Verification Trees},
 pdfauthor={Zhenyu Sun and Jilin Wang},
 pdfsubject={Generation semantics, exact compression and optimal finite representations},
 pdfkeywords={strict finitism, intuitionistic logic, Kripke semantics, bounded morphisms, finite trees}
}

\begin{document}
\maketitle

\begin{abstract}
In strict finitistic generation semantics, a formula is assertible at a generation if some stage in its verification tree forces it. We ask when assertibility agrees with intuitionistic truth on the poset of generations. The leaves of the verification trees, ordered by generation extension, form an intuitionistic Kripke model that preserves truth at every leaf, even without atomic prevalence. For a finite bundle, compression to the generations is exact if and only if each fiber of leaves has a greatest intuitionistic theory and the map selecting these theories has the back property. Compression remains exact under every restriction of the generation poset if and only if atomic prevalence holds. Conversely, consider coherent tree representations of a finite Kripke model whose atomic valuation reflects its order. Among representations with atomic prevalence, the minimum numbers of leaves and nodes over $u$ are $h(u)$ and $\delta_C+\sum_{x\preceq u}h(x)$, where $h(x)$ counts saturated paths from minimal worlds to $x$, and $\delta_C$ is $1$ if the comparability component of $u$ has no least element and $0$ otherwise. Saturated-path trees attain both minima simultaneously. Among representations attaining the node minimum at every world, the common root labels in components without a least element determine the representation up to isomorphism over the outer frame. Allowing rooted posets in place of trees can reduce the number of nodes exponentially.
\end{abstract}

\noindent\textbf{Keywords.} Strict finitism; intuitionistic Kripke semantics; prevalence; bounded morphisms; finite trees; representation size.

\section{Introduction}\label{sec:introduction}

Verifying a conditional need not mean that its consequent has already been verified when its antecedent holds. In Wright's account of strict finitism, the verification of the consequent may take further steps \citep{Wright1982}. \citet{Yamada2023} formalized this distinction using finite trees of verification stages and an order on the trees themselves. Each tree represents a generation. To test an implication, one considers extensions at which the antecedent holds, including extensions in later generations. At each such extension, a witness for the consequent must be reachable within the generation in which the antecedent holds.

Call a formula \emph{assertible} at a generation if it holds at some stage of that generation. Under \emph{atomic prevalence}, any atom verified somewhere in a generation can still be verified from every stage in that generation. For his propositional generation structures, Yamada proves that prevalence extends to formulas, that an implication holds throughout a generation if it holds anywhere in it, and that assertibility agrees with intuitionistic truth on the poset of generations \citep[Proposition~2.28, Corollary~2.29 and Proposition~2.30]{Yamada2023}. His converse construction gives a representation of intuitionistic models in the class he considers and identifies the valid formulas with the theorems of intuitionistic propositional logic ($\IPC$) \citep[Propositions~2.31--2.32]{Yamada2023}. The first-order account gives the corresponding forcing clauses and a compression result for the fragment without primitive negation \citep[Definition~4.52 and Proposition~4.56]{Yamada2025}.

We ask when compression is exact for an individual bundle, even if atomic prevalence fails, and how large its verification trees must be to represent a prescribed finite Kripke model. Our bundles allow an arbitrary outer poset of generations. A transition embeds one verification tree into another as a downward-closed subtree, preserving the root and the atomic labels of all old stages. The local implication clause is the forcing clause for the internal Kuroda-style translation with double negation \citep[Sections~4--5]{VanDenBerg2019}; the generation clause also tests the antecedent in later trees.

\paragraph{Compression.}
Every stage has a maximal extension in its own finite tree. At a maximal stage the consequent cannot be postponed any further within that tree. Keeping all such stages and ordering them by generation extension gives an intuitionistic model in which truth at each retained stage agrees with generation forcing (\cref{thm:maximal-reduction}). Projecting this model onto the generations gives a surjective bounded morphism of frames. It is a bounded morphism of models precisely under atomic prevalence (\cref{thm:prevalence-projection}).

For a finite bundle, take the quotient of the maximal-stage model by equality of intuitionistic theories. Exact compression requires two things. Each fiber must contain a theory that includes all the others, so that separate witnesses for two conjuncts can be replaced by a common witness. Moreover, every theory above the selected theory of $u$ in the quotient must itself be selected at some $v\succeq u$. This lifting condition accounts for implication. Together the conditions are necessary and sufficient (\cref{thm:compression-criterion,cor:bundle-criterion}). The proof uses finite theory quotients and the bounded-morphism characterization of implication \citep{DeGrootPattinson2022,BezhanishviliEtAl2021}. A bundle can satisfy both conditions without atomic prevalence (\cref{ex:no-prevalence}). Requiring compression to remain exact after every restriction of the generations recovers prevalence (\cref{thm:hereditary}).

\paragraph{Size of representations.}
Fix a finite Kripke model $M=(U,\preceq,V)$ and assume that inclusion of atomic labels reflects the order on $U$. Let $h(x)$ count saturated paths from a minimal world to $x$. For the comparability component $C$ containing $u$, set $\delta_C=0$ if $C$ has a least element and $\delta_C=1$ otherwise. Every coherent representation of $M$ with atomic prevalence satisfies
\[
 |\Max K_u|\ge h(u),\qquad
 |K_u|\ge \delta_C+\sum_{x\preceq u}h(x).
\]
The standard unfolding into saturated paths \citep[Section~6.6]{AdamDayEtAl2024}, applied coherently to the principal ideals of $U$, attains both bounds at every world (\cref{thm:optimal-representation}). A representation attaining the node minimum at every world is determined up to isomorphism by the common root label in each component without a least element (\cref{thm:rigidity}). If the fibers may be arbitrary finite rooted posets, the sharp node bound becomes $\delta_C+|\downarrow u|$ (\cref{thm:poset-representation}). On a chain of diamonds the optimal top tree has exponentially many nodes, whereas the optimal top poset has only as many nodes as the outer frame.

Without prevalence, pointwise validity and validity by assertibility over the class of all bundles still give exactly $\IPC$ (\cref{thm:unrestricted-validity}). This class-wide result is distinct from deciding whether a particular bundle compresses exactly. For a finite atom set, the latter can be tested in polynomial time given the projection and the order and atomic tables of the two models (\cref{thm:recognition}). Appendix~\ref{app:arithmetic} gives a single bounded arithmetic formula evaluating generation forcing from codes for the bundle and formula. The objects it encodes are verification trees and their transitions; for a potentialist account in which the worlds are models of arithmetic, see \citet{Hamkins2026}.

\section{Verification bundles and the two forcing relations}\label{sec:semantics}

\subsection{Local verification}

The strict finitistic language $\Lsf$ is generated by
\[
 A ::= p\mid\bot\mid A\wedge A\mid A\vee A\mid A\Rightarrow A.
\]
We write $\neg_s A$ for $A\Rightarrow\bot$ and $\top_s$ for $\bot\Rightarrow\bot$. The intuitionistic language $\Li$ has $\to$ in place of $\Rightarrow$. The bijection $c:\Lsf\to\Li$ preserves atoms, absurdity, conjunction and disjunction, and sends $A\Rightarrow B$ to $c(A)\to c(B)$.

\begin{definition}\label[definition]{def:fiber}
A \emph{verification fiber} is $W=(K,\le,r,V)$, where $(K,\le)$ is a nonempty finite rooted tree with least element $r$, and $V(p)\subseteq K$ is upward closed for each atom $p$. Here the predecessors of each node form a chain. A branch represents one possible verification history.
\end{definition}

At a stage $k$, an atom $p$ is forced exactly when $k\in V(p)$; no stage forces $\bot$. Conjunction and disjunction have their usual pointwise clauses. For implication, set
\begin{equation}\label{eq:local-implication}
 k\forces_W A\Rightarrow B
 \quad\Longleftrightarrow\quad
 \forall l\ge k\,\bigl(l\forces_W A\ \Longrightarrow\
                 \exists m\ge l\ m\forces_W B\bigr).
\end{equation}
The witness $m$ may be $l$ itself. Local forcing is persistent: if $k\le k^{\prime}$, every extension tested at $k^{\prime}$ is also tested at $k$. This proves persistence for implication; for the other connectives it follows by induction. In particular, $k\forces_W\neg_s A$ exactly when no $l\ge k$ forces $A$.

\begin{proposition}[Local translations]\label[proposition]{prop:local-translations}
Define $\sigma:\Lsf\to\Li$ by preserving atoms, $\bot$, $\wedge$ and $\vee$, and putting
\[
 \sigma(A\Rightarrow B)=\sigma(A)\to\neg\neg\sigma(B).
\]
On the ordinary intuitionistic Kripke model with frame and valuation $(K,\le,V)$,
\begin{equation}\label{eq:sigma}
 k\forces_W A\quad\Longleftrightarrow\quad k\forces_{\mathrm i}\sigma(A).
\end{equation}
For a second translation, equip an auxiliary language with an implication $\to$ governed by the usual Kripke clause and a unary operator given by
\[
 k\forces^{\Diamond}\Diamond_t\varphi
 \quad\Longleftrightarrow\quad
 \exists l\ge k\ l\forces^{\Diamond}\varphi.
\]
The translation $\tau$ preserving the other connectives and satisfying
\[
 \tau(A\Rightarrow B)=\tau(A)\to\Diamond_t\tau(B)
\]
then satisfies $k\forces_W A\iff k\forces^{\Diamond}\tau(A)$.
\end{proposition}

\begin{proof}
We prove \eqref{eq:sigma} by induction on the formula. Only implication requires an argument. Suppose $k\forces_W A\Rightarrow B$, and let $l\ge k$ force $A$. By persistence, every $n\ge l$ forces $A$, so \eqref{eq:local-implication} gives an $m\ge n$ forcing $B$. By induction, this is precisely the condition for $l\forces_{\mathrm i}\neg\neg\sigma(B)$. Conversely, given $l\ge k$ forcing $A$, double negation at $l$ supplies the required witness by taking $n=l$. The equivalence for $\tau$ follows by induction from the clauses for $\to$ and $\Diamond_t$.
\end{proof}

In the notation of \citet[Sections~4--5]{VanDenBerg2019}, $\sigma$ is the internal translation $J$ for the nucleus $j=\neg\neg$. The full translation applies $j$ once more to $J$. Reversing the order convention in his forcing clause gives \eqref{eq:local-implication}.

The operator $\Diamond_t$ records the existence of a future witness. It need not preserve persistence. On a fork $r<a,b$ with $p$ true only at $a$, the formula $\Diamond_t p$ holds at $r$ and fails at $b$. With $\varphi=\Diamond_t p$ and $\top=(\bot\to\bot)$, even $\varphi\to(\top\to\varphi)$ fails at $r$. The Kripke universal clause on this full language therefore does not validate all substitution instances of $\IPC$. Every formula in the image of $\tau$ is nevertheless persistent by \cref{prop:local-translations} and persistence of local forcing.

\subsection{Coherent extensions of verification trees}

\begin{definition}\label[definition]{def:bundle}
A \emph{verification bundle} is
\[
 \B=(U,\preceq,(W_u)_{u\in U},(\iota_{uv})_{u\preceq v}),
\]
where $(U,\preceq)$ is a nonempty poset of generations and $W_u=(K_u,\le_u,r_u,V_u)$ is the verification fiber at $u$. For each $u\preceq v$ the map $\iota_{uv}:K_u\to K_v$ is an order embedding, subject to the following conditions:
\begin{enumerate}[label=(\roman*)]
\item $\iota_{uv}(r_u)=r_v$ and $\iota_{uv}(K_u)$ is downward closed in $K_v$;
\item $k\in V_u(p)$ if and only if $\iota_{uv}(k)\in V_v(p)$;
\item $\iota_{uu}=\id$ and $\iota_{uw}=\iota_{vw}\circ\iota_{uv}$ for $u\preceq v\preceq w$.
\end{enumerate}
The bundle is \emph{finite} when $U$ is finite. Each fiber is finite even when $U$ is infinite.
\end{definition}

Write $P_{\B}=\{(u,k):u\in U,\ k\in K_u\}$. The generation order is
\begin{equation}\label{eq:gorder}
 (u,k)\preceq_g(v,l)
 \quad\Longleftrightarrow\quad
 u\preceq v\text{ and }\iota_{uv}(k)\le_v l.
\end{equation}
Coherence and monotonicity give transitivity. Reflexivity follows from $\iota_{uu}=\id$, and antisymmetry follows first in $U$ and then in a fiber. Thus $\preceq_g$ is a partial order.

\begin{definition}\label[definition]{def:gforcing}
Generation forcing $(u,k)\gforces_{\B} A$ has the standard clauses for atoms, $\bot$, $\wedge$ and $\vee$, and the implication clause
\begin{equation}\label{eq:gimplication}
\begin{split}
 (u,k)\gforces_{\B} A\Rightarrow B
 \quad\Longleftrightarrow\quad
 \forall (v,l)\succeq_g(u,k)\,
 \bigl((v,l)\gforces_{\B}A\ \Longrightarrow\
 \exists m\ge_v l\ (v,m)\gforces_{\B}B\bigr).
\end{split}
\end{equation}
Write $\Ass_{\B}(u,A)$ when $(u,k)\gforces_{\B}A$ for some $k\in K_u$.
\end{definition}

In \eqref{eq:gimplication}, the test of $A$ can pass from $u$ to $v$, but the search for a witness to $B$ must remain in $K_v$. This is the generation clause of \citet{Yamada2023} written for the maps $\iota_{uv}$. If $\to$ in the auxiliary language uses $\preceq_g$ and $\Diamond_t$ still quantifies only within the current fiber, structural induction gives
\[
 (u,k)\gforces_{\B}A
 \quad\Longleftrightarrow\quad
 (u,k)\forces^{g,\Diamond}_{\B}\tau(A).
\]

\begin{lemma}[Persistence]\label[lemma]{lem:persistence}
If $(u,k)\gforces_{\B}A$ and $(u,k)\preceq_g(v,l)$, then $(v,l)\gforces_{\B}A$.
\end{lemma}
\begin{proof}
Induct on $A$. For an atom use preservation by $\iota_{uv}$ and upward closure in $K_v$. For implication, transitivity of $\preceq_g$ makes every extension tested at $(v,l)$ an extension already tested at $(u,k)$, with the same fiber in which to find a witness. The other clauses are immediate.
\end{proof}

\begin{definition}\label[definition]{def:compression}
The compressed Kripke model is $\Comp(\B)=(U,\preceq,V^{\sharp})$, where
\[
 u\in V^{\sharp}(p)\quad\Longleftrightarrow\quad V_u(p)\ne\varnothing.
\]
The valuation is monotone by the embeddings. We say that $\B$ has \emph{exact existential compression} if, for every $u$ and $A$,
\begin{equation}\label{eq:compression}
 \Ass_{\B}(u,A)\quad\Longleftrightarrow\quad
 u\forces_{\Comp(\B)}c(A).
\end{equation}
It has \emph{atomic prevalence} if every nonempty $V_u(p)$ is cofinal in $K_u$: for each $k\in K_u$ there is an $l\ge_u k$ with $l\in V_u(p)$.
\end{definition}

\begin{example}[Two generations and negation]\label[example]{ex:negation}
Let $u<v$, $K_u=\{r\}$ and $K_v=\{r<a\}$, with the inclusion map. Let $p$ hold only at $a$ in $K_v$, and let all other atoms be false. Both fibers have atomic prevalence. Local and generation forcing nevertheless differ:
\[
\begin{array}{c|cc}
 &\neg_s p&\neg_s\neg_s p\\\hline
 r\forces_{W_u}&\text{true}&\text{false}\\
 (u,r)\gforces_{\B}&\text{false}&\text{true}.
\end{array}
\]
Locally, no extension in $K_u$ verifies $p$. In the generation order, $(v,a)$ does verify $p$, and every extension of $(u,r)$ has a further extension verifying $p$. In the compressed two-point model, $p$ is false at $u$ and true at $v$, so $p\vee\neg p$ fails at $u$.
\end{example}

\section{Maximal verification stages}\label{sec:maximal}

Define
\[
 T_{\B}=\{(u,m):m\in\Max(K_u)\}.
\]
Restricting $\preceq_g$ and the atomic valuation to $T_{\B}$ gives an intuitionistic Kripke model $M_{\B}^{\max}$. Its points are maximal in their own fibers; they can have successors in later generations.

\begin{theorem}[Maximal-stage reduction]\label{thm:maximal-reduction}
For every verification bundle, every $A\in\Lsf$ and every $x\in T_{\B}$,
\begin{equation}\label{eq:maximal-reduction}
 x\gforces_{\B}A\quad\Longleftrightarrow\quad
 x\forces_{M_{\B}^{\max}}c(A).
\end{equation}
Consequently,
\begin{equation}\label{eq:maximal-assertibility}
 \Ass_{\B}(u,A)\quad\Longleftrightarrow\quad
 \exists m\in\Max(K_u)\ (u,m)\forces_{M_{\B}^{\max}}c(A).
\end{equation}
\end{theorem}

\begin{proof}
Induct on $A$. Only implication needs proof. Suppose $x\gforces C\Rightarrow D$, and take $y=(v,n)\in T_{\B}$ above $x$ with $y\forces c(C)$. The induction hypothesis gives $y\gforces C$. The consequent witness in $K_v$ must equal $n$, since $n$ is maximal. Thus $y\forces c(D)$.

Conversely, suppose $x\forces c(C)\to c(D)$ in $M_{\B}^{\max}$. Let $(v,l)\succeq_g x$ force $C$ in the generation semantics. Choose a maximal $n\ge_v l$. By \cref{lem:persistence}, $(v,n)\gforces C$. By induction, $(v,n)$ forces $c(C)$ in $M_{\B}^{\max}$. Since $(v,n)\succeq_g x$, it also forces $c(D)$ there. Applying the induction hypothesis to $D$ gives $(v,n)\gforces D$, with $n$ the required witness above $l$ in $K_v$. Finally, every verifying point extends to a maximal point of the same finite fiber, proving \eqref{eq:maximal-assertibility}.
\end{proof}

\begin{definition}\label[definition]{def:bounded-morphism}
A \emph{bounded morphism of frames} $f:X\to Y$ is an order-preserving map with the back property
\[
 f(x)\le y\quad\Longrightarrow\quad
 \exists x'\ge x\ f(x')=y.
\]
It is a bounded morphism of Kripke models when additionally $x\forces p$ if and only if $f(x)\forces p$ for every atom. Surjectivity is specified separately. A bounded morphism of models preserves and reflects forcing for all intuitionistic formulas. In the induction step for implication, order preservation sends extensions of $x$ to extensions of $f(x)$, and the back property lifts extensions of $f(x)$ to extensions of $x$.
\end{definition}

\begin{proposition}\label[proposition]{prop:projection-frame}
The projection $\pi:T_{\B}\to U$, $\pi(u,m)=u$, is a surjective bounded morphism of frames.
\end{proposition}
\begin{proof}
Every finite nonempty fiber has a maximal node, so $\pi$ is onto. It is order preserving by \eqref{eq:gorder}. Given $u\preceq v$ and $m\in\Max K_u$, extend $\iota_{uv}(m)$ to a maximal $n\in K_v$. Then $(u,m)\preceq_g(v,n)$ and $\pi(v,n)=v$.
\end{proof}

\begin{theorem}[Prevalence and the maximal-stage projection]\label{thm:prevalence-projection}
For a verification bundle $\B$, the following are equivalent:
\begin{enumerate}[label=(\roman*)]
\item $\B$ has atomic prevalence;
\item $\pi:M_{\B}^{\max}\to\Comp(\B)$ is a bounded morphism of models;
\item for every $u$, every $m\in\Max K_u$ and every $A\in\Lsf$,
\[
 (u,m)\gforces_{\B}A\quad\Longleftrightarrow\quad
 u\forces_{\Comp(\B)}c(A).
\]
\end{enumerate}
Each condition implies exact existential compression.
\end{theorem}
\begin{proof}
In a finite poset an upward-closed nonempty set is cofinal exactly when it contains every maximal element. Hence (i) says precisely that
\[
 m\in V_u(p)\quad\Longleftrightarrow\quad V_u(p)\ne\varnothing
 \qquad(m\in\Max K_u).
\]
Together with \cref{prop:projection-frame}, this is (ii). The bounded-morphism truth lemma and \cref{thm:maximal-reduction} give (iii). Its atomic instances imply (i). Existential compression follows from \eqref{eq:maximal-assertibility}.
\end{proof}

Under atomic prevalence, Yamada's propositional compression equivalence \citep[Proposition~2.30]{Yamada2023} thus holds for these bundles. Agreement with the outer world at \emph{every} maximal stage characterizes prevalence. Exact existential compression requires only that a formula hold at the outer world exactly when some maximal stage over it forces the corresponding strict formula. As the next section shows, maximal stages of such a fiber may disagree even on atoms.

\section{An exact criterion for finite compression}\label{sec:criterion}

\subsection{Finite intuitionistic theories}

Write $\Th_M(x)=\{\alpha:M,x\forces\alpha\}$ for the intuitionistic theory of a point $x$ in a Kripke model $M$. The finite Hennessy--Milner argument below relates inclusion of theories to the order on points and supplies formulas that distinguish theories \citep{Patterson1997,DeGrootPattinson2022}. We take the empty conjunction to be $\top=(\bot\to\bot)$ and the empty disjunction to be $\bot$.

\begin{lemma}[Realization of theory inclusion]\label[lemma]{lem:theory-inclusion}
Let $(M,x)$ and $(N,y)$ be pointed Kripke models in the same propositional language. If $\uparrow x$ is finite, then
\[
 \Th_M(x)\subseteq\Th_N(y)
 \quad\Longleftrightarrow\quad
 \exists x'\ge x\ \Th_M(x')=\Th_N(y).
\]
\end{lemma}
\begin{proof}
The reverse implication follows from persistence. For the forward implication, suppose no $z\ge x$ has the theory of $y$. For each such $z$, choose a formula that distinguishes $y$ from $z$. Put the chosen formula in $\Gamma$ if it is true at $y$, and in $\Delta$ otherwise. Let $\alpha=\bigwedge\Gamma$ and $\beta=\bigvee\Delta$. Each $z\ge x$ either fails a conjunct of $\alpha$ or forces a disjunct of $\beta$, so $x\forces\alpha\to\beta$. At $y$ every formula in $\Gamma$ holds and every formula in $\Delta$ fails. Thus $y\not\forces\alpha\to\beta$, contrary to theory inclusion.
\end{proof}

An \emph{intuitionistic bisimulation} relates points with the same atomic valuation. For each related pair, every successor of either point has a related successor of the other. Induction on formulas shows that related points have the same theory. Conversely, equality of theories defines a bisimulation between finite models. Indeed, if $\Th(x)=\Th(y)$ and $x'\ge x$, persistence gives $\Th(y)\subseteq\Th(x')$. By \cref{lem:theory-inclusion}, some $y'\ge y$ has the theory of $x'$. Interchanging the two models gives the other direction.

For a finite model $M=(X,\le,V)$, let $Q_M$ be its quotient by equality of theories. Order the classes by inclusion of their theories and give each class the atomic valuation of its representatives. Write $q:X\to Q_M$ for the quotient map.

\begin{lemma}\label[lemma]{lem:theory-quotient}
The map $q$ is a surjective bounded morphism of models. Every upset of $Q_M$ is definable by a formula in the given propositional language.
\end{lemma}
\begin{proof}
Persistence makes $q$ order preserving. The quotient valuation preserves and reflects atoms, and \cref{lem:theory-inclusion} gives the back property. Thus $q$ preserves and reflects every formula. Fix a class $a$. For each $b\not\ge a$, choose a formula in the theory of $a$ but outside the theory of $b$. Their conjunction defines $\uparrow a$. Since $Q_M$ is finite, every upset is a finite union of principal upsets and is therefore definable by a disjunction.
\end{proof}

\begin{lemma}\label[lemma]{lem:union-of-theories}
Let $T_1,\ldots,T_n$ be point theories, with $n\ge1$. Their union is closed under conjunction if and only if some $T_i$ contains all the others.
\end{lemma}
\begin{proof}
If no $T_i$ equals the union, choose $\alpha_i$ in the union but outside $T_i$. Closure under conjunction would put $\bigwedge_i\alpha_i$ in the union, although each $T_i$ omits its $i$th conjunct. Conversely, if some $T_i$ contains the others, the union is itself a point theory and hence is closed under conjunction.
\end{proof}

\subsection{Greatest fiber theories and the lifting condition}

Let $M=(X,\le,V)$ be a finite model, and let $\pi:(X,\le)\to(U,\preceq)$ be a surjective bounded morphism of frames. Define the atomic valuation of $N=(U,\preceq,V^\sharp)$ by
\[
 u\in V^\sharp(p)\quad\Longleftrightarrow\quad
 \exists x\in\pi^{-1}(u)\ x\in V(p).
\]
The back property of $\pi$ makes $V^\sharp$ monotone. In the theory quotient $Q=Q_M$, the types realized over $u$ form the set
\[
 S_u=\{q(x):\pi(x)=u\}\subseteq Q.
\]

\begin{theorem}[Exact existential compression]\label{thm:compression-criterion}
The equivalence
\begin{equation}\label{eq:general-compression}
 N,u\forces\alpha
 \quad\Longleftrightarrow\quad
 \exists x\in\pi^{-1}(u)\ M,x\forces\alpha
\end{equation}
holds for every $u\in U$ and every intuitionistic formula $\alpha$ if and only if the following two conditions hold.
\begin{enumerate}[label=(\roman*)]
\item Each $S_u$ has a greatest element $g(u)$.
\item For each $u\in U$ and each $a\in Q$ with $g(u)\le a$, some $v\succeq u$ satisfies $g(v)=a$.
\end{enumerate}
Under (i), $g:U\to Q$ preserves order and both preserves and reflects atoms. Condition (ii) is the back property for $g$. Its image may be a proper subset of $Q$.
\end{theorem}

\begin{proof}
Suppose \eqref{eq:general-compression} holds. Then
\[
 \Th_N(u)=\bigcup_{\pi(x)=u}\Th_M(x).
\]
The left-hand theory is closed under conjunction. By \cref{lem:union-of-theories}, one of the theories on the right equals the union. Its class is the greatest element $g(u)$ of $S_u$, and \cref{lem:theory-quotient} gives
\begin{equation}\label{eq:selected-theory}
 \Th_N(u)=\Th_Q(g(u)).
\end{equation}
For $g(u)\le a$, persistence in $Q$ gives $\Th_N(u)\subseteq\Th_Q(a)$. By \cref{lem:theory-inclusion}, some $v\succeq u$ has $\Th_N(v)=\Th_Q(a)$. Equation~\eqref{eq:selected-theory} then yields $g(v)=a$, since distinct points of $Q$ have distinct theories.

Conversely, assume (i). Given $u\preceq v$, choose $x$ over $u$ with $q(x)=g(u)$. By the back property of $\pi$, some $y\ge x$ lies over $v$. Hence
\[
 g(u)=q(x)\le q(y)\le g(v).
\]
An atom holds at some member of $S_u$ exactly when it holds at $g(u)$. Thus $g$ preserves order and preserves and reflects atoms. With (ii), $g$ is a bounded morphism of models. Its truth lemma gives the first equivalence below. The second follows because $g(u)$ is the greatest type realized over $u$.
\[
 N,u\forces\alpha
 \iff Q,g(u)\forces\alpha
 \iff \exists x\in\pi^{-1}(u)\ M,x\forces\alpha.
\]
\end{proof}

\begin{corollary}[Criterion for verification bundles]\label[corollary]{cor:bundle-criterion}
For a finite verification bundle $\B$, let $Q$ be the theory quotient of $M_{\B}^{\max}$ and let $S_u$ consist of the types in $Q$ represented by the maximal nodes of $K_u$. Then $\B$ has exact existential compression if and only if conditions (i) and (ii) of \cref{thm:compression-criterion} hold.
\end{corollary}
\begin{proof}
By \cref{prop:projection-frame}, the projection of the maximal-stage model satisfies the frame hypothesis of \cref{thm:compression-criterion}. Its existential atomic valuation is that of $\Comp(\B)$, since every atomic witness extends to a maximal node in the same fiber. By \eqref{eq:maximal-assertibility} and the bijectivity of $c$, the two compression equivalences agree.
\end{proof}

For a poset $X$, write $\Up(X)$ for its Heyting algebra of upsets, with implication given by
\[
 A\to B=\{x:\uparrow x\cap A\subseteq B\}.
\]
The Heyting subalgebra $H_M\subseteq\Up(X)$ generated by the atomic truth sets consists precisely of the truth sets of formulas. The back property ensures that $\pi_!(A)=\pi[A]$ is an upset of $U$ for every $A\in H_M$. This direct image preserves the empty set and finite unions, and surjectivity gives $\pi_!(X)=U$.

\begin{proposition}[The two connective conditions]\label[proposition]{prop:connective-conditions}
The direct image $\pi_!$ preserves finite intersections if and only if every $S_u$ has a greatest element. Under this condition, it preserves Heyting implication if and only if $g$ has the back property. Consequently, \eqref{eq:general-compression} is equivalent to $\pi_!$ being a Heyting homomorphism on $H_M$.
\end{proposition}
\begin{proof}
The direct image preserves intersections exactly when, in each fiber, any two formulas that have witnesses there also have a common witness. This is closure of the union of the fiber theories under conjunction, so \cref{lem:union-of-theories} gives the first equivalence. By \cref{lem:theory-quotient}, the inverse-image map $q^{-1}$ identifies $\Up(Q)$ with $H_M$. When greatest elements exist, $\pi_!q^{-1}=g^{-1}$, since an upset meets $S_u$ exactly when it contains $g(u)$. If $g$ has the back property, its inverse image preserves implication by the Kripke clause.

Conversely, suppose $g(u)\le a$ and no $v\succeq u$ maps to $a$. Take the upsets $A=\uparrow a$ and $B=A\setminus\{a\}$. Since $a\in A\setminus B$, we have $g(u)\notin A\to B$. But for each $v\succeq u$, membership of $g(v)$ in $A$ implies its membership in $B$. Hence $u\in g^{-1}(A)\to g^{-1}(B)$, so inverse image fails to preserve implication. Both upsets are definable by \cref{lem:theory-quotient}. A homomorphism therefore gives \eqref{eq:general-compression} by induction on formulas. Conversely, the equivalence for all formulas gives preservation of each operation on their truth sets.
\end{proof}

The implication condition is the bounded-morphism correspondence of finite Esakia duality \citep[Section~2.1]{BezhanishviliEtAl2021}. The greatest-element condition identifies when the direct image along $\pi$ can be written as an inverse image along $g$ after passage to the theory quotient.

\subsection{Examples separating the conditions}

In the following examples the maps between fibers are inclusions, and unlisted atoms are false everywhere.

\begin{example}[Failure of conjunction]\label[example]{ex:conjunction}
Let $U=\{u\}$ and let $K_u$ be the fork $r<a,b$, with $V_u(p)=\{a\}$ and $V_u(q)=\{b\}$. The theories of $a$ and $b$ are incomparable, so $S_u$ has no greatest element. In the compressed model $u$ forces $p\wedge q$, although no node of $K_u$ forces both atoms.
\end{example}

\begin{example}[Greatest types without the back property]\label[example]{ex:implication}
Take the chain $u<v<w$. Let $K_u=\{r\}$ and let $K_v$ be the fork $r<a,b$. In $K_w$, add a node $c$ above $a$. Give the fibers the following valuations.
\[
\begin{array}{c|cc}
 &V(p)&V(q)\\\hline
 K_u&\varnothing&\varnothing\\
 K_v&\{a,b\}&\{b\}\\
 K_w&\{a,b,c\}&\{b,c\}.
\end{array}
\]
The theory quotient of the maximal-stage model is the three-point chain $s<t<z$. In order, the three types have atomic labels $\varnothing$, $\{p\}$ and $\{p,q\}$. The types realized in each fiber are
\[
 S_u=\{s\},\qquad S_v=\{t,z\},\qquad S_w=\{z\}.
\]
Each set has a greatest element. Yet $g(u)=s$ and $g(v)=g(w)=z$, so the successor $t$ of $s$ has no preimage. The compressed model forces $p\to q$ at $u$, since $p$ and $q$ first hold together at $v$. In the bundle, $(v,a)$ is a generation extension of $(u,r)$ that forces $p$, and no node of $K_v$ above $a$ forces $q$. Thus $(u,r)\not\gforces p\Rightarrow q$.
\end{example}

\begin{example}[Exact compression without prevalence]\label[example]{ex:no-prevalence}
Let $u<v$, let $K_u$ be the fork $r<a,b$, and obtain $K_v$ by adding $c$ above $b$. Put
\[
 V_u(p)=\{a\},\qquad V_v(p)=\{a,c\}.
\]
Prevalence fails in $K_u$ because $b$ has no extension there that forces $p$. The maximal-stage model has two types $t<z$. The point $(u,b)$ has type $t$, and $(u,a),(v,a),(v,c)$ all have type $z$. Thus both fibers have greatest type $z$. Since $z$ is maximal in the quotient, the constant map $g$ with value $z$ has the back property. Compression is therefore exact for every formula.
\end{example}

\subsection{Prevalence under restrictions of generations}

For nonempty $S\subseteq U$, let $\B|_S$ be the bundle with generations in $S$ and the inherited order, fibers and maps. In $\B|_S$, the implication clause ranges only over future generations in $S$.

\begin{theorem}[Compression in every outer restriction]\label{thm:hereditary}
For any verification bundle $\B$, the following conditions are equivalent.
\begin{enumerate}[label=(\roman*)]
\item $\B$ has atomic prevalence.
\item $\B|_S$ has exact existential compression for every nonempty $S\subseteq U$.
\item $\B|_{\{u\}}$ has exact existential compression for every $u\in U$.
\end{enumerate}
\end{theorem}
\begin{proof}
An outer restriction keeps the valuations and order within each retained fiber. Hence it preserves atomic prevalence, and \cref{thm:prevalence-projection} gives (i)$\Rightarrow$(ii). Taking $S=\{u\}$ gives (ii)$\Rightarrow$(iii). For the converse, suppose prevalence fails for $p$ at $u$. Then $V_u(p)\ne\varnothing$, but some $l\in K_u$ has no extension verifying $p$. In the restriction to $\{u\}$, $(u,l)$ therefore forces $\neg_s p$. Its compressed one-point model forces $p$ and hence fails $\neg p$, contradicting (iii).
\end{proof}

Call a formula \emph{cofinally robust} at $u$ if, whenever some point of $K_u$ forces it in the generation semantics, every node of $K_u$ has an extension in $K_u$ that forces it.

\begin{corollary}\label[corollary]{cor:robustness}
A bundle has atomic prevalence if and only if every formula is cofinally robust at every world. Under this condition, an implication true at one point of a fiber is true at every point of that fiber.
\end{corollary}
\begin{proof}
Suppose some node in $K_u$ forces $A$. By persistence, it extends to a maximal node of $K_u$ forcing $A$. Under atomic prevalence, \cref{thm:prevalence-projection} transfers $c(A)$ to the compressed world $u$ and $A$ back to every maximal node of $K_u$. Since every node has a maximal extension, $A$ is cofinally robust at $u$. Taking $A$ to be an atom gives the converse.

Now suppose $C\Rightarrow D$ holds somewhere in $K_u$. By compression, $u\forces c(C)\to c(D)$. Fix any $k\in K_u$ and any $(v,l)\succeq_g(u,k)$ forcing $C$. Compression gives $v\forces c(C)$ and, since $u\preceq v$, also $v\forces c(D)$. Another application of compression supplies a witness for $D$ in $K_v$. Cofinal robustness gives such a witness above $l$, as required for $(u,k)\gforces C\Rightarrow D$.
\end{proof}


\section{Optimal finite representations}
\label{sec:optimal-representations}

Let $M=(U,\preceq,V)$ be a finite intuitionistic Kripke model. Write
\[
 \Lambda(u)=\{p:u\in V(p)\}
\]
for the atomic label of $u$. These labels are monotone in $u$.
A representation of $M$ in this section is an atomic-prevalent bundle
$\B$ on $(U,\preceq)$ with $\Comp(\B)=M$. If the compressed model
is only specified up to isomorphism, that isomorphism identifies its
outer frame with $U$.

For $u\in U$, let
\[
 \operatorname{Pred}(u)=\operatorname{Max}(\downarrow u\setminus\{u\})
\]
be the set of lower covers of $u$. Let $h(u)$ be the number of saturated
chains from a minimal element of $U$ to $u$. Equivalently,
\[
 h(u)=
 \begin{cases}
  1,&u\text{ is minimal},\\
  \displaystyle\sum_{v\in\operatorname{Pred}(u)}h(v),&u\text{ is not minimal}.
 \end{cases}
\]
Let $C(u)$ be the connected component of $u$ in the undirected
comparability graph of $U$. Put
\[
 \delta_C=
 \begin{cases}
  0,&C\text{ has a least element},\\
  1,&C\text{ has no least element}.
 \end{cases}
\]
The parameter $\delta_{C(u)}$ depends on the whole component of $u$.
Indeed, the transition maps preserve roots and atomic labels, so the
roots of all fibers in a component have the same label.

We apply the saturated-chain unfolding of a finite rooted poset
\citep[Section~6.6]{AdamDayEtAl2024} to the principal ideals of $U$.
Ordering the chains by prefix makes the resulting trees compatible
under inclusion.

\begin{proposition}[Saturated-path representation]
\label[proposition]{prop:saturated-representation}
Every finite intuitionistic Kripke model $M$ has an atomic-prevalent
verification bundle $\B^{\mathrm{sat}}_M$ with
$\Comp(\B^{\mathrm{sat}}_M)=M$ and, for every $u\in U$,
\[
 \left|\operatorname{Max}K_u\right|=h(u),\qquad
 |K_u|=\delta_{C(u)}+\sum_{x\preceq u}h(x).
\]
\end{proposition}

\begin{proof}
Work separately in each comparability component $C$. If $C$ has a least
element $b$, let $K_u$ consist of all saturated chains
\[
 b=x_0\prec x_1\prec\cdots\prec x_j\preceq u,
\]
where each successive pair is a cover in $U$. The order is by prefix
and the root is $(b)$. If $C$ has no least element, take all saturated
chains from a minimal element of $C$ to a world $x\preceq u$, again
ordered by prefix, and adjoin the empty chain as root. A nonempty
chain $s$ has label $\Lambda(\ell(s))$, where $\ell(s)$ is its last
element. The empty chain has label $\varnothing$.

For $u\preceq v$, take $\iota_{uv}$ to be the inclusion
$K_u\hookrightarrow K_v$. Every prefix of a chain in $K_u$ belongs
to $K_u$, so the image is downward closed. These inclusions preserve
roots and labels, are order embeddings, and compose as required.
Monotonicity of $\Lambda$ makes each atomic valuation upward closed.

Every chain in $K_u$ extends to a saturated chain ending at $u$.
For the empty chain, choose a minimal world below $u$ as the starting
point. Thus every node has an extension labelled $\Lambda(u)$, and
all node labels in $K_u$ are subsets of $\Lambda(u)$. This proves
atomic prevalence and recovers the valuation $V$ under compression.

A nonempty chain is maximal in $K_u$ exactly when its last element is
$u$. Hence there are $h(u)$ maximal nodes. For each $x\preceq u$,
there are $h(x)$ nodes ending at $x$. There is one additional empty
root precisely when $\delta_C=1$, giving the asserted count.
\end{proof}

\begin{definition}[Order-reflecting atomic valuation]
\label[definition]{def:order-reflecting-valuation}
The atomic valuation of $M$ is \emph{order-reflecting} if
\[
 u\preceq v\quad\Longleftrightarrow\quad
 \Lambda(u)\subseteq\Lambda(v)
 \qquad (u,v\in U).
\]
Equivalently, whenever $u\npreceq v$, there is an atom verified at $u$
and not verified at $v$.
\end{definition}

Every finite poset admits such a valuation. For each $x\in U$, introduce
an atom $p_x$ and set
\[
 V(p_x)=\uparrow x.
\]
Let all other atoms be false. Then $\Lambda(u)=\{p_x:x\preceq u\}$.
If $u\npreceq v$, the atom $p_u$ belongs to $\Lambda(u)$ and is absent
from $\Lambda(v)$. We call this the \emph{canonical valuation}.

\begin{lemma}[Labels of maximal verification nodes]
\label[lemma]{lem:maximal-node-labels}
Let $\B$ be an atomic-prevalent verification bundle with
$\Comp(\B)=M$. Every maximal node of $K_u$ has atomic label
exactly $\Lambda(u)$.
\end{lemma}

\begin{proof}
If $p\in\Lambda(u)$, some node of $K_u$ verifies $p$. Atomic
prevalence applied at a maximal node $a$ gives a node above $a$
verifying $p$, necessarily $a$ itself. If $p\notin\Lambda(u)$,
no node of $K_u$ verifies $p$, by the definition of compression.
\end{proof}

\begin{theorem}[Sharp simultaneous bounds for tree representations]
\label{thm:optimal-representation}
Suppose the atomic valuation of $M$ is order-reflecting. For every
atomic-prevalent verification bundle $\B$ representing $M$, put
$L_\B(u)=|\operatorname{Max}K_u|$. Then, for every $u\in U$,
\[
 L_\B(u)\ge h(u),\qquad
 |K_u|\ge\delta_{C(u)}+\sum_{x\preceq u}h(x).
\]
The saturated-path representation attains both bounds at every outer
world simultaneously. In particular, the least possible total number
of generation points is
\[
 \sum_{u\in U}\left(\delta_{C(u)}+\sum_{x\preceq u}h(x)\right)
 =\sum_{x\in U}h(x)|\uparrow x|
   +\sum_C\delta_C|C|.
\]
\end{theorem}

\begin{proof}
Fix a nonminimal world $u$. For each lower cover
$v\in\operatorname{Pred}(u)$, the image of $\operatorname{Max}K_v$
under $\iota_{vu}$ is an antichain because $\iota_{vu}$ is an order
embedding. By Lemma~\ref{lem:maximal-node-labels}, every node of
this image has label $\Lambda(v)$. Distinct lower covers $v,w$ are
incomparable. Order reflection makes their labels incomparable under
inclusion, so monotonicity prevents any node from one image from
being comparable with a node from the other.

The union of the images is therefore an antichain of size
$\sum_{v\in\operatorname{Pred}(u)}L_\B(v)$. In a finite tree each
node has a maximal descendant, and incomparable nodes have no common
descendant.
Thus
\[
 L_\B(u)\ge
 \sum_{v\in\operatorname{Pred}(u)}L_\B(v).
\]
For minimal $u$, nonemptiness and finiteness give $L_\B(u)\ge1$.
Induction along the outer poset yields $L_\B(u)\ge h(u)$.

For the node bound, consider, for every $x\preceq u$, the subset
\[
 S_x(u)=\iota_{xu}(\operatorname{Max}K_x)\subseteq K_u.
\]
It has $L_\B(x)$ elements, all with label $\Lambda(x)$.
Order reflection implies that $\Lambda(x)\ne\Lambda(y)$ whenever
$x\ne y$, so these subsets are pairwise disjoint. Therefore
\[
 |K_u|\ge\sum_{x\preceq u}L_\B(x)
           \ge\sum_{x\preceq u}h(x).
\]

Suppose now that $C=C(u)$ has no least element. The roots in $C$
share a label $R_C$, and $R_C\subseteq\Lambda(v)$ for every $v\in C$.
If $r_u\in S_x(u)$, then $\Lambda(x)=R_C\subseteq\Lambda(v)$ for
every $v\in C$. Order reflection would make $x$ the least element
of $C$. Thus $r_u$ contributes one more node.

Proposition~\ref{prop:saturated-representation} attains both bounds.
Summing over $u$, each term $h(x)$ occurs once for each $u\in\uparrow x$,
and each $\delta_C$ occurs $|C|$ times.
\end{proof}

\begin{theorem}[Uniqueness of optimal tree representations]
\label{thm:rigidity}
Assume that $M$ has an order-reflecting atomic valuation. Suppose an
atomic-prevalent tree representation $\B$ attains the node bound
of Theorem~\ref{thm:optimal-representation} at every outer world.
For each comparability component $C$ without a least element, let
$R_C$ be the common atomic label of its roots. Then
\[
 R_C\subseteq\bigcap_{u\in C}\Lambda(u).
\]
Give each empty root in the saturated-path representation the label
$R_C$ of its component. There is a unique family of rooted,
label-preserving tree isomorphisms from $\B$ to this representation
commuting with all transition maps. Conversely, every choice of
$R_C$ satisfying the displayed inclusion gives a representation
attaining both bounds at every world.

For the canonical valuation $V(p_x)=\uparrow x$, the optimal
representation is unique up to a unique isomorphism over the outer
frame. The same classification holds for representations minimizing
the total number of generation points.
\end{theorem}

\begin{proof}
Equality in the node bounds, together with the proof of
Theorem~\ref{thm:optimal-representation}, gives
$L_\B(x)=h(x)$ for every $x$. It also gives the disjoint
decomposition
\[
 K_u=
 \begin{cases}
  \displaystyle\coprod_{x\preceq u}S_x(u),&\delta_{C(u)}=0,\\
  \displaystyle\{r_u\}\,\sqcup\coprod_{x\preceq u}S_x(u),
     &\delta_{C(u)}=1,
 \end{cases}
 \qquad
 S_x(u)=\iota_{xu}(\operatorname{Max}K_x).
\]
A point in $S_x(u)$ has label $\Lambda(x)$, which determines $x$ by
order reflection. Call $x$ its endpoint. Distinct points with the same
endpoint are incomparable because $\iota_{xu}$ is an order embedding
and their preimages are maximal in $K_x$.

For a nonminimal $x$, consider
\[
 A_x=\coprod_{v\in\operatorname{Pred}(x)}S_v(x).
\]
It is an antichain with $\sum_{v\in\operatorname{Pred}(x)}h(v)=h(x)$
members, as many as there are maximal nodes in $K_x$. Its members
have pairwise disjoint, nonempty sets of maximal descendants. Each
such set must therefore be a singleton, and together they exhaust
$\operatorname{Max}K_x$.

Take $a\in S_v(x)$ and let $y$ be its maximal descendant.
Their labels $\Lambda(v)$ and $\Lambda(x)$ are distinct, so $a<y$.
If $a<z<y$, then $z$ has an endpoint $w$. Monotonicity of labels
and order reflection give $v\preceq w\preceq x$. As $v$ is a lower
cover of $x$, either $w=v$ or $w=x$. The first case contradicts
incomparability of distinct nodes with endpoint $v$.
The second contradicts maximality of $z\in S_x(x)$.
Hence $a$ is the immediate predecessor of $y$.

We now assign a saturated path to each maximal node of $K_x$ by
induction on $x$. At a minimal $x$, the decomposition of $K_x$ gives
one maximal node, which we assign the path $(x)$. This node is the
root if $x$ is least in its component, and the unique child of the
root otherwise. At a nonminimal $x$, each maximal node has an
immediate predecessor $\iota_{vx}(a)$ with $v\in\operatorname{Pred}(x)$
and $a\in\operatorname{Max}K_v$. Append $x$ to the path already
assigned to $a$. The bijection with $A_x$ shows that this procedure
gives every saturated path to $x$ exactly once.

In $K_u$, send each $\iota_{xu}(a)\in S_x(u)$ to the path of $a$,
and send the additional root, when present, to the empty path.
The disjoint decomposition gives a bijection. The image of
$\iota_{xu}$ is downward closed, so the ancestors of $\iota_{xu}(a)$
are precisely the images of the ancestors of $a$. Thus the bijection
sends an immediate predecessor to the path obtained by deleting the
last world. It preserves the root, the order in both directions, and
the atomic labels. Coherence of the embeddings makes the bijections
commute with each $\iota_{uv}$.

A rooted, label-preserving isomorphism must preserve the sequence of
endpoints along the chain from the root to each node, omitting the
adjoined root when present. This sequence is the node's assigned
path, so the isomorphism is unique.

For the converse, give each adjoined root any label contained in
$\bigcap_{u\in C}\Lambda(u)$. Every maximal node of $K_u$ still has
label $\Lambda(u)$, so prevalence and the compressed valuation are
preserved. The sizes of the fibers are unchanged. For the canonical
valuation, an atom $p_x$ common to the component would satisfy
$x\preceq u$ for every $u\in C$, making $x$ its least element.
Thus the intersection is empty in each component without a least
element. Finally, since every fiber satisfies the node bound, the
sum of the bounds is attained exactly when each fiber attains its
own bound.
\end{proof}

\begin{remark}[Scope of the lower bounds]
The saturated-path construction applies to every monotone valuation.
The lower bounds use order reflection to distinguish the images of
maximal nodes from different worlds. At the other extreme, if the
valuation is constant on each comparability component, a single node
per fiber suffices.
\end{remark}

\begin{example}[Chains]
For an $n$-world linear outer frame with an order-reflecting valuation,
$h(u)=1$ at every world and the component has a least element.
If $u_i$ is the $i$th world, every atomic-prevalent representation satisfies
$|K_{u_i}|\ge i$, and nested chains attain this bound. The minimum
total number of generation points is $n(n+1)/2$.
\end{example}

\begin{example}[Successive diamonds]
\label[example]{ex:diamond-representation-cost}
For $d\ge1$, let the outer frame have worlds
\[
 c_0,c_1,\ldots,c_d,\quad a_1,b_1,\ldots,a_d,b_d
\]
and covers
\[
 c_{i-1}\prec a_i,\quad c_{i-1}\prec b_i,\quad
 a_i\prec c_i,\quad b_i\prec c_i
 \qquad(1\le i\le d).
\]
Give it the canonical valuation $V(p_x)=\uparrow x$.
There are $3d+1$ outer worlds. The saturated-chain counts are
\[
 h(c_i)=2^i,\qquad h(a_i)=h(b_i)=2^{i-1}.
\]
Consequently every exact atomic-prevalent tree representation satisfies
\[
 |\operatorname{Max}K_{c_d}|\ge2^d,
 \qquad |K_{c_d}|\ge2^{d+2}-3.
\]
Both bounds are attained. The minimum total number of generation
points is
\[
 18\cdot2^d-9d-17.
\]
Indeed, the optimal fiber sizes are $1$ at $c_0$,
$5\cdot2^{i-1}-3$ at each of $a_i,b_i$, and $2^{i+2}-3$ at $c_i$.
Figure~\ref{fig:diamonds} shows the top fiber for $d=2$.
\end{example}

\begin{figure}[tb]
\centering
\begin{tikzpicture}[x=0.8cm,y=0.78cm,
 dot/.style={circle,fill=black,inner sep=1.5pt},
 edge/.style={-{Stealth[length=3pt]},thin},
 every label/.style={font=\small}]
\node[dot,label=below:$c_0$] (o) at (0,0) {};
\node[dot,label=left:$a_1$] (a) at (-0.8,1) {};
\node[dot,label=right:$b_1$] (b) at (0.8,1) {};
\node[dot,label=left:$c_1$] (m) at (0,2) {};
\node[dot,label=left:$a_2$] (c) at (-0.8,3) {};
\node[dot,label=right:$b_2$] (d) at (0.8,3) {};
\node[dot,label=above:$c_2$] (t) at (0,4) {};
\foreach \a/\b in {o/a,o/b,a/m,b/m,m/c,m/d,c/t,d/t}
 \draw[edge] (\a)--(\b);
\node[font=\small,align=center] at (0,-1.25) {Outer frame\\7 worlds};
\begin{scope}[xshift=6.5cm]
\node[dot,label=below:$c_0$] (O) at (0,0) {};
\node[dot,label=left:$a_1$] (A) at (-1.6,1) {};
\node[dot,label=right:$b_1$] (B) at (1.6,1) {};
\node[dot,label=left:$c_1$] (M1) at (-1.6,2) {};
\node[dot,label=right:$c_1$] (M2) at (1.6,2) {};
\node[dot,label=left:$a_2$] (C1) at (-2.3,3) {};
\node[dot,label=right:$b_2$] (D1) at (-0.9,3) {};
\node[dot,label=left:$a_2$] (C2) at (0.9,3) {};
\node[dot,label=right:$b_2$] (D2) at (2.3,3) {};
\foreach \n/\x in {T1/-2.3,T2/-0.9,T3/0.9,T4/2.3}
 \node[dot,label=above:$c_2$] (\n) at (\x,4) {};
\foreach \a/\b in {O/A,O/B,A/M1,B/M2,M1/C1,M1/D1,M2/C2,M2/D2,C1/T1,D1/T2,C2/T3,D2/T4}
 \draw[edge] (\a)--(\b);
\node[font=\small,align=center] at (0,-1.25) {Optimal top tree fiber\\13 nodes, 4 leaves};
\end{scope}
\end{tikzpicture}
\caption{Two successive diamonds and the optimal tree over $c_2$ for an order-reflecting valuation. Each tree node is marked with the last world on its path. The two paths to $c_1$ remain distinct, and each extends in two ways to $c_2$.}
\label{fig:diamonds}
\end{figure}

\begin{example}[Boolean outer frames]
On the Boolean lattice $U=\mathcal P(\{1,\ldots,m\})$, assign atom
$p_i$ at $S$ exactly when $i\in S$. This valuation is order-reflecting.
Here $h(S)=|S|!$, so every exact atomic-prevalent tree representation has at least
$m!$ leaves in its top fiber and at least
\[
 \sum_{j=0}^m\binom mj j!
\]
nodes there. The saturated-path representation, whose nodes record
ordered lists of distinct acquired atoms, attains both bounds.
\end{example}

\subsection{Merging histories with the same atomic labels}

Under a general monotone valuation, distinct saturated paths may
record the same sequence of changes in atomic labels. Identifying
such paths can reduce the size of the fibers.

\begin{proposition}[Representation by reduced label histories]
\label[proposition]{prop:reduced-label-histories}
Let $M$ have a monotone atomic valuation, and put
$R_C=\bigcap_{v\in C}\Lambda(v)$ for each comparability component
$C$. There is an exact atomic-prevalent tree representation in which
$K_u$, for $u\in C$, consists of the empty history labelled $R_C$
and the reduced label histories of saturated paths from minimal
worlds to worlds $x\preceq u$.

To reduce a history, replace each run of equal labels by one copy
and delete the first label if it equals $R_C$. Paths yielding the
same reduced sequence give a single node. If
\[
 d_u=\left|\{\Lambda(x):x\preceq u\}\setminus\{R_C\}\right|,
\]
then its fiber size satisfies
\[
 |K_u|\le
 \min\left\{\delta_C+\sum_{x\preceq u}h(x),\,2^{d_u}\right\}.
\]
For a finite alphabet, put $m_u=|\Lambda(u)\setminus R_C|$.
Every branch has at most $m_u$ edges, and
\[
 |K_u|\le (m_u+1)^{m_u}.
\]
\end{proposition}

\begin{proof}
Order the reduced histories by prefix. Each nonempty prefix occurs
by truncating a path at the first occurrence of the prefix's last
label. Together with the empty history, the sequences thus form a
rooted tree. Each sequence is strictly increasing under inclusion,
and its first label, if present, properly contains $R_C$.
Label a nonempty history by its final entry.

When $u\preceq v$, each path used in $K_u$ also occurs in $K_v$.
The inclusions of histories therefore give coherent, label-preserving
order embeddings with downward-closed images. Every label in $K_u$
is contained in $\Lambda(u)$. Extending a path to $u$ and reducing
its label sequence gives an extension of its history labelled
$\Lambda(u)$. The empty history has such an extension as well,
obtained from any saturated path to $u$, including when the reduced
sequence is empty and $\Lambda(u)=R_C$. This gives atomic prevalence
and exact compression.

Reduction maps the saturated-path tree of
Proposition~\ref{prop:saturated-representation} onto this tree.
When $C$ has a least element $b$, one has $R_C=\Lambda(b)$ and the
root path $(b)$ maps to the empty history. This gives the first size
bound. A strictly inclusion-ordered sequence is uniquely determined
by its set of entries, giving at most $2^{d_u}$ histories.

For the finite-alphabet claim, every proper inclusion adds at least
one atom from $\Lambda(u)\setminus R_C$, so the sequence has length
at most $m_u$. Encode a history by assigning to each of these $m_u$
atoms the index of the step at which it first occurs, or $0$ if it
never occurs. These values belong to $\{0,\ldots,m_u\}$ and
determine the history, proving the final bound.
\end{proof}

\begin{remark}
For a finite alphabet the construction is effective from explicit
atomic labels. Over a countably infinite alphabet, restriction to any
finite set of atoms gives the same construction for the compressed
model on that set.
\end{remark}

\subsection{The cost of requiring trees}

The proofs of maximal-stage reduction and compression under atomic
prevalence use the existence of maximal extensions in each finite
fiber. They also apply to finite rooted posets, where incomparable
nodes can have a common upper bound. This changes the number of
nodes needed to represent $M$.

\begin{theorem}[Sharp bounds for rooted-poset representations]
\label{thm:poset-representation}
Allow the fibers to be finite rooted posets, with the same bundle-map
requirements. Every finite Kripke model has an exact atomic-prevalent
representation with
\[
 |K_u|=\delta_{C(u)}+|\downarrow u|.
\]
If the valuation reflects the order, this is the minimum possible
size of each $K_u$, and one representation attains all the minima.
\end{theorem}

\begin{proof}
Fix a component $C$. For $u\in C$ take $K_u=\downarrow u$ with
its inherited order, adjoining a common bottom element if $C$ has
no least element. Give each world $x\in K_u$ the label $\Lambda(x)$
and any adjoined bottom the empty label. Take inclusions as the
transition maps. The greatest node of $K_u$ is $u$ itself, with
label $\Lambda(u)$, so atomic prevalence holds and compression is
exact.

For the lower bound, choose one maximal node of $K_x$ for each
$x\preceq u$ and map it into $K_u$. By
Lemma~\ref{lem:maximal-node-labels}, its image has label $\Lambda(x)$.
Order reflection distinguishes these labels, giving at least
$|\downarrow u|$ nodes. As in Theorem~\ref{thm:optimal-representation},
the root supplies one further node if $C$ has no least element.
\end{proof}

For the successive diamonds of Example~\ref{ex:diamond-representation-cost},
the minimum size of the top fiber is $3d+1$ among rooted posets and
$2^{d+2}-3$ among trees. The difference comes from the two paths
through each diamond, which can meet again in a poset.

\section{Validity, recognition and finite computation}\label{sec:effectivity}

\subsection{Validity without prevalence}

Write $\models_{\mathrm{pt}}A$ if every generation point of every verification bundle forces $A$, and $\models_{\exists}A$ if $A$ is assertible at every outer world of every verification bundle.

\begin{theorem}[Unrestricted bundle validity]\label{thm:unrestricted-validity}
For every $A\in\Lsf$,
\[
 \models_{\mathrm{pt}}A
 \quad\Longleftrightarrow\quad
 \models_{\exists}A
 \quad\Longleftrightarrow\quad
 \IPC\vdash c(A).
\]
The same equivalences hold over finite bundles. Whenever $\IPC\nvdash c(A)$, there is a finite atomic-prevalent bundle with an outer world at which $A$ is not assertible.
\end{theorem}
\begin{proof}
Every fiber is nonempty, so pointwise validity implies assertibility at every outer world. If $\IPC\nvdash c(A)$, the finite model property gives a finite Kripke model with a world $u$ refuting $c(A)$ \citep{TroelstraVanDalen1988}. By \cref{prop:saturated-representation,thm:prevalence-projection}, this model is the compression of a finite atomic-prevalent bundle in which $A$ is not assertible at $u$.

It remains to show that $\IPC\vdash c(A)$ implies $\models_{\mathrm{pt}}A$. We argue by induction on $A$. Neither an atom nor $\bot$ is an $\IPC$ theorem. If a conjunction is provable, then both conjuncts are provable. If a disjunction is provable, the disjunction property gives a provable disjunct. The induction hypothesis gives pointwise validity in both cases.

Suppose $A=C\Rightarrow D$ and $\IPC\vdash c(C)\to c(D)$. Fix a generation point $(u,k)$ and an extension $(v,l)\succeq_g(u,k)$ forcing $C$. Choose a maximal $m\ge_v l$. Persistence and \cref{thm:maximal-reduction} give $M_{\B}^{\max},(v,m)\forces c(C)$. By intuitionistic soundness, this point also forces $c(D)$. Applying the reduction again gives $(v,m)\gforces_{\B}D$. Thus $m$ witnesses the consequent in the fiber required by \eqref{eq:gimplication}.
\end{proof}

The pointwise equivalence in \cref{thm:unrestricted-validity} concerns theorems. With premises, modus ponens can fail at a generation point. Take one outer world $u$ with fiber $r<a$. Let $p$ hold at both nodes and $q$ only at $a$. Then
\[
 (u,r)\gforces_{\B}p,\qquad
 (u,r)\gforces_{\B}p\Rightarrow q,\qquad
 (u,r)\not\gforces_{\B}q.
\]
The witness for $q$ lies at $a$.

\begin{corollary}\label[corollary]{cor:pspace}
Pointwise validity and assertibility validity over all verification bundles are PSPACE-complete, as is validity of $c(A)$ in the compressions of all atomic-prevalent bundles. In each case, replacing $\to$ by $\Rightarrow$ in an $\IPC$ calculus axiomatizes the valid formulas of $\Lsf$.
\end{corollary}
\begin{proof}
Both $c$ and its inverse are length-preserving renamings computable in linear time. Apply \cref{thm:unrestricted-validity,prop:saturated-representation,thm:prevalence-projection} and the PSPACE-completeness of intuitionistic propositional validity \citep{Statman1979}.
\end{proof}

\subsection{Recognizing exact compression in a finite bundle}

Fix a finite set $P$ of atoms and take all theories in the language over $P$. Write $N=\Comp(\B)$, and let $E$ be bisimilarity on the disjoint union $M_{\B}^{\max}\sqcup N$.

\begin{proposition}\label[proposition]{prop:recognition-test}
Exact compression over $P$ holds if and only if the following two conditions hold for every $u\in U$:
\begin{enumerate}[label=(\roman*)]
\item some $x\in\pi^{-1}(u)$ satisfies $x\mathrel E u$;
\item every $x\in\pi^{-1}(u)$ has a successor $x'\ge x$ in $M_{\B}^{\max}$ with $x'\mathrel E u$.
\end{enumerate}
\end{proposition}
\begin{proof}
By maximal-stage reduction, compression is exact at $u$ precisely when $\Th_N(u)$ equals the union of the theories of the points over $u$ in $M_{\B}^{\max}$. By \cref{lem:union-of-theories}, this equality holds precisely when one of these theories equals $\Th_N(u)$ and all are contained in it. In finite models, equality of point theories is bisimilarity. By \cref{lem:theory-inclusion}, inclusion in $\Th_N(u)$ is equivalent to having a successor bisimilar to $u$.
\end{proof}

\begin{theorem}[Recognition and separating formulas]\label{thm:recognition}
Given the order and atomic tables of $M_{\B}^{\max}$ and $\Comp(\B)$ and the projection $\pi$, one can decide exact compression in time $O(dn^2+n^4)$, where $n=|T_{\B}|+|U|$ and $d=|P|$. This bound excludes the cost of constructing the tables from the bundle. If compression fails, one can construct a formula witnessing its failure. The witness has polynomial size as a directed acyclic graph and length at most $2^{O(n\log n)}$ as an ordinary formula, counting each atom as one symbol.
\end{theorem}
\begin{proof}
Partition the $n$ points by their atomic labels. At each round refine the current partition $\mathcal P_i$ by the signature
\[
 \left([x]_{\mathcal P_i},\ \{[y]_{\mathcal P_i}:x\le y\}\right).
\]
There are at most $n-1$ proper refinements. In the stable partition, points in the same block agree on atoms and can match each other's successors block by block. Conversely, bisimilar points remain together at every round. The stable partition therefore consists of the $E$-classes. Comparing the initial labels takes $O(dn^2)$ time. Computing each signature as a set of blocks and comparing all pairs of signatures takes $O(n^3)$ per round. Given $E$, the conditions of \cref{prop:recognition-test} can be checked in $O(n^3)$ time.

For each pair of points, record a separating formula when the two points first fall into different blocks. In the initial partition, an atom separates them. At a subsequent round, interchange $x$ and $y$ if necessary so that some $x'\ge x$ has no match above $y$ in the preceding partition. For each $y'\ge y$, choose an earlier formula separating $x'$ and $y'$. Place the formula in $\Gamma$ if it holds at $x'$, and in $\Delta$ if it holds at $y'$. Then
\[
 (\bigwedge\Gamma)\to(\bigvee\Delta)
\]
holds at $y$, since every $y'\ge y$ either fails a conjunct or forces a disjunct. It fails at $x$, as witnessed by $x'$. There are at most $\binom{n}{2}$ pairs, each requiring at most $n$ previous formulas. Reusing those formulas gives a graph of polynomial size. If $L_i$ bounds the expanded lengths through round $i$, then $L_{i+1}\le nL_i+O(n)$. After at most $n-1$ refinements this gives the claimed exponential bound.

If (ii) fails at $x\in\pi^{-1}(u)$, apply the construction in \cref{lem:theory-inclusion} to the separators for $u$ and the successors of $x$. It gives a formula $\alpha$ true at $x$ and false at $u$. Thus $c^{-1}(\alpha)$ is assertible at $u$ although $N,u\not\forces\alpha$. If (ii) holds everywhere but (i) fails at $u$, each theory over $u$ is properly contained in $\Th_N(u)$. For each $x\in\pi^{-1}(u)$, the recorded separator for $x$ and $u$ is then true at $u$ and false at $x$. Their conjunction holds at $u$ and fails at every maximal stage over $u$. By maximal-stage reduction its inverse under $c$ is not assertible there. Both constructions add at most $O(n)$ connectives and preserve the size bounds.
\end{proof}

For a finite model over infinitely many atoms, the semantic criterion still holds. Applying the partition algorithm in that setting requires an effective test for equality of complete atomic labels.

\subsection{Finite forcing tables}

Let $N=|P_{\B}|$, and write $F(A)$ for the set of generation points forcing $A$. Let $G(x,y)$ mean that $y$ is a generation extension of $x$, and let $T(y,z)$ mean that $z$ extends $y$ within its fiber. For a relation $R$, write $\downarrow_R S=\{x:\exists y\in S\ R(x,y)\}$.

\begin{proposition}\label[proposition]{prop:model-checking}
For every $C,D\in\Lsf$,
\[
 F(C\Rightarrow D)
 =P_{\B}\setminus\downarrow_G
       \bigl(F(C)\setminus\downarrow_TF(D)\bigr).
\]
Given the two relation matrices and the atomic tables, one can compute the truth sets of all $s$ subformulas in $O(sN^2)$ time using $O(N^2+sN)$ working space, apart from input parsing.
\end{proposition}
\begin{proof}
A point $y$ belongs to $F(C)\setminus\downarrow_TF(D)$ precisely when it forces $C$ and has no extension in its fiber forcing $D$. By \eqref{eq:gimplication}, the implication fails at $x$ precisely when some such $y$ is a generation extension of $x$. Each of the two lower closures takes one scan of a relation matrix. The remaining connectives require only pointwise operations, and each subformula occupies one row of $N$ truth values.
\end{proof}

\section{Consequences for verification semantics}\label{sec:consequences}

At a maximal stage, generation forcing agrees with intuitionistic forcing in $M_{\B}^{\max}$. Projecting all the maximal stages of a fiber onto their outer world may lose information even when its atomic valuation records every atom verified somewhere in the fiber. For a finite bundle, conjunction requires that one maximal stage realize the greatest theory in its fiber. Once such theories exist, implication requires that their selection lift future types. Atomic prevalence makes all maximal stages over a world agree with that world on every formula. Conversely, exact compression in every one-world restriction already implies prevalence.

There is a corresponding distinction between tree and poset representations. When atomic labels reflect the outer order, coherence forces a tree to retain distinct branches for distinct saturated paths to $u$. If the comparability component has no least element, its common root contributes one further node. The classification in \cref{thm:rigidity} describes the representations attaining the node bounds at every world. In a rooted poset, incomparable histories can have a common continuation, reducing the sharp node bound to $|\downarrow u|+\delta_C$.

\appendix
\section{A uniform bounded arithmetic definition}\label{app:arithmetic}

We define a single predicate $\operatorname{Force}(e,a,x)$ whose arguments code a finite bundle, a formula, and a generation point. Work in the language of $0,1,+,\cdot,\le$ and $E(t)=2^t$. A $\Delta_0(\exp)$ formula has only bounded quantifiers in this language. We take elementary arithmetic $\mathsf{EA}$ to have the usual arithmetic and exponentiation axioms and induction for these bounded formulas.

\subsection{Codes and bounded access}

Use the injective pairing
\[
 \langle a,b\rangle=(a+b)^2+a.
\]
Each component is bounded by the pair code, so bounded search recovers both components of a valid code. We code tuples by nesting pairs to the right. To test bit $i$ of $B$, define
\begin{equation}\label{eq:bit-definition}
 \operatorname{Bit}(B,i)
 \iff \exists q\le B\ \exists r<2^i\
          (B=q2^{i+1}+2^i+r).
\end{equation}
For fixed-width fields, write $\operatorname{Field}(B,j,w,z)$ for
\begin{equation}\label{eq:field-definition}
 z<2^w\ \land\
 \exists q\le B\ \exists r<2^{wj}\
 (B=q2^{w(j+1)}+z2^{wj}+r).
\end{equation}
Both predicates are $\Delta_0(\exp)$, with each power of two written as a term using $E$.

Number the $N$ generation points of a finite bundle from $0$ to $N-1$. Over atoms $p_0,\ldots,p_{d-1}$ its relation tables have the code
\[
 e=\langle N,d,G,T,V\rangle,
\]
where $N\ge1$, $G,T<2^{N^2}$, and $V<2^{dN}$. Bit $xN+y$ of $G$ records whether $y$ is a generation extension of $x$. The same bit of $T$ records whether $y$ extends $x$ in its own fiber. Bit $jN+x$ of $V$ records whether $x$ forces $p_j$. The outer order, fiber orders and embeddings determine $G$ by \eqref{eq:gorder}.

A formula code is
\[
 a=\langle s,w,O,L,R,J\rangle.
\]
The subformula table has $s\ge1$ entries in topological order, ending with the formula to be evaluated. Choose a field width $w\ge1$ with $2^w\ge s+d+5$. For $i<s$, the $i$th three-bit field $O_i$ of $O<2^{3s}$ is one of $0,1,2,3,4$, denoting $\bot$, an atom, $\wedge$, $\vee$, and $\Rightarrow$, respectively. In the corresponding $w$-bit fields of $L,R,J<2^{ws}$, a binary entry has child indices $L_i,R_i<i$, and an atom has index $J_i<d$. The other fields of that entry are ignored. Several entries may refer to the same child.

Let $\operatorname{Well}(e,a)$ assert that the tuple components and their fields satisfy these bounds and tag conditions. It accepts arbitrary relations $G,T$ of the stated dimensions. The recursive equations below determine a truth table for every such input. Their interpretation as generation forcing applies when the relations and valuations come from a bundle.

\subsection{One formula for all finite inputs}

Let $S<2^{Ns}$ encode a candidate truth table and abbreviate
\[
 B_S(i,x)\iff\operatorname{Bit}(S,iN+x).
\]
The bounded predicate $\operatorname{Correct}(e,a,S)$ imposes the equation for tag $O_i$ at each $i<s$ and $x<N$. The first four tags give
\[
\begin{array}{c|l}
 O_i& \text{required equation}\\\hline
 0&\neg B_S(i,x)\\
 1&B_S(i,x)\leftrightarrow\operatorname{Bit}(V,J_iN+x)\\
 2&B_S(i,x)\leftrightarrow(B_S(L_i,x)\land B_S(R_i,x))\\
 3&B_S(i,x)\leftrightarrow(B_S(L_i,x)\lor B_S(R_i,x)).
\end{array}
\]
For tag $4$, the equation is
\begin{equation}\label{eq:arithmetic-implication}
\begin{split}
 B_S(i,x)\ \longleftrightarrow\
 \forall y<N\,\bigl(&\operatorname{Bit}(G,xN+y)\land B_S(L_i,y)\\
 &\Longrightarrow\exists z<N\,
       (\operatorname{Bit}(T,yN+z)\land B_S(R_i,z))\bigr).
\end{split}
\end{equation}
Define
\begin{equation}\label{eq:uniform-force}
\begin{split}
 \operatorname{Force}(e,a,x)\iff{}&
 \operatorname{Well}(e,a)\land x<N\ \land\\
 &\exists S<2^{Ns}\,
    \bigl(\operatorname{Correct}(e,a,S)
             \land B_S(s-1,x)\bigr),
\end{split}
\end{equation}
Here bounded quantifiers recover the components of $e$ and $a$, and $s-1$ denotes the unique $t<s$ satisfying $t+1=s$. The bound $2^{Ns}$ on the entire table is a term in the language. Hence \eqref{eq:uniform-force} defines one $\Delta_0(\exp)$ formula with free variables $e,a,x$.

\begin{theorem}[Uniform arithmetic evaluation]\label{thm:arithmetic}
For every well-formed pair $(e,a)$, there is exactly one $S<2^{Ns}$ satisfying $\operatorname{Correct}(e,a,S)$, and $\mathsf{EA}$ proves this assertion. If $e$ presents a finite bundle and $a$ codes $A$, then for each generation point $x<N$ the following equivalence holds in the standard natural numbers:
\[
 \operatorname{Force}(e,a,x)\quad\Longleftrightarrow\quad x\gforces_{\B}A.
\]
\end{theorem}

\begin{proof}
Fix a bounded formula $\theta(j)$, allowing parameters. For each $t$ we first construct the unique $D<2^t$ with $\operatorname{Bit}(D,j)\leftrightarrow\theta(j)$ for $j<t$. Start with $D=0$ at $k=0$. At step $k$ add $2^k$ if $\theta(k)$ holds, and retain $D$ otherwise. The induction assertion
\[
 \exists D<2^k\ \forall j<k\,
       (\operatorname{Bit}(D,j)\leftrightarrow\theta(j))
\]
is bounded. For uniqueness, two such codes agree modulo $2^k$ for $k=0$. If they agree modulo $2^k$ and have the same $k$th bit, they agree modulo $2^{k+1}$. Bounded induction gives agreement modulo $2^t$, hence equality below $2^t$. All remainder and bit calculations here are provable in $\mathsf{EA}$ by bounded induction.

Let $\operatorname{Partial}(e,a,S,i)$ assert correctness of the first $i$ rows. Induct on $i\le s$ with the bounded assertion
\[
 \exists S<2^{iN}\ \operatorname{Partial}(e,a,S,i).
\]
For $i=0$, take $S=0$. At step $i<s$, each child index is less than $i$, so the right-hand side of the equation for row $i$ defines a bounded predicate of $x<N$ with the partial table $S$ as a parameter. Binary comprehension supplies its row code $D<2^N$. The code
\[
 S'=S+2^{iN}D<2^{(i+1)N}
\]
retains all earlier rows and appends row $i$. This proves existence in $\mathsf{EA}$. By the same bounded induction, any two correct tables agree through each row. Binary uniqueness then gives equality. For a bundle in the standard model, induction on the row index identifies each bit with forcing at the corresponding point. In the implication case, \eqref{eq:arithmetic-implication} is exactly the generation clause \eqref{eq:gimplication}.
\end{proof}

\bibliographystyle{plainnat}
\bibliography{references}
\end{document}