% Eventual categoricity for abstract elementary classes -- a concise proof.
% Read top to bottom. Every claim is proved; nothing is asserted without argument.
% Sections ~1-3 are background and reduction. Sections ~4-9 build the machinery.
% Sections 10-12 are the two finite-dimensional applications.
% Sections 13-14 combine them into the final theorem.

\documentclass[11pt]{article}
\usepackage[margin=1.1in]{geometry}
\usepackage{lmodern}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{enumitem}
\usepackage{hyperref}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{claim}[theorem]{Claim}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{convention}[theorem]{Convention}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\newcommand{\K}{K}
\newcommand{\LS}{\mathrm{LS}}
\newcommand{\tp}{\mathrm{tp}}
\newcommand{\cl}{\mathrm{cl}}
\newcommand{\cf}{\mathrm{cf}}
\newcommand{\ci}{\mathrm{ci}}
\newcommand{\rk}{\mathrm{rk}}
\newcommand{\Aut}{\mathrm{Aut}}
\newcommand{\otp}{\mathrm{otp}}
\newcommand{\Lim}{\mathrm{Lim}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\Z}{\mathbb{Z}}

\title{Eventual categoricity for abstract elementary classes\\[2pt]\large a self-contained proof}
\author{written for a general mathematical reader}
\date{}

\begin{document}
\maketitle

\section*{Preface for the reader}

This document proves one theorem. In plain words: \emph{for a certain kind
of mathematical object called an abstract elementary class, if the class
has exactly one model of some sufficiently large size, then it has exactly
one model of every larger size}. This is called \emph{eventual categoricity},
and it was conjectured by Saharon Shelah in the 1970s. The proof below is a
complete proof in the usual axioms of set theory, ZFC. No special hypotheses
(amalgamation, tameness, large cardinals, generalized continuum hypothesis,
etc.) are assumed.

\section{What we are trying to prove}\label{sec:overview}

\subsection*{In one paragraph}

An \emph{abstract elementary class} (AEC) is a family of mathematical
structures together with a choice of which substructures count as
``strong'' (written $M\le_{\K} N$). The definition is deliberately
weak: it rules out only behaviour that would be strange from the
point of view of first-order logic. \emph{Categoricity} in a cardinal
$\kappa$ means that there is exactly one model of size~$\kappa$ up
to isomorphism --- no more, no fewer. Shelah's \emph{eventual categoricity
conjecture} states:

\begin{quote}
\emph{If an AEC has exactly one model of some sufficiently large size,
then it has exactly one model of every size beyond a fixed threshold.}
\end{quote}

The threshold may depend on the class but not on the size in which we
happen to know categoricity. We prove this, in ZFC, with an explicit
threshold depending only on a numerical invariant of the class (its
\emph{L\"owenheim--Skolem number}, defined in
Section~\ref{sec:aec}).

\subsection*{In detail}

Let $\lambda$ be an infinite cardinal. The \emph{uniform} form of the
result we prove is the following.

\begin{theorem}[Uniform eventual categoricity]\label{thm:main-uniform}
For every infinite cardinal $\lambda$ there is a cardinal
$\mu(\lambda)\ge\lambda$ such that for every AEC $\K$ with
$\LS(\K)\le\lambda$:
\[
 \bigl(\exists\kappa\ge\mu(\lambda):\ \K\text{ is categorical in }\kappa\bigr)
 \ \Longrightarrow\
 \bigl(\forall\kappa'\ge\mu(\lambda):\
       \K\text{ is categorical in }\kappa'\bigr).
\]
The same cardinal $\mu(\lambda)$ is used in the hypothesis and in the
conclusion.
\end{theorem}

The ``qualitative'' phrasing excludes the uniform quantifier and is
often the more natural statement.

\begin{theorem}[Qualitative eventual categoricity]\label{thm:main-qualitative}
An AEC that is categorical in unboundedly many cardinals is categorical
in every cardinal above some fixed threshold.
\end{theorem}

The two theorems are equivalent by a small-model count
(Proposition~\ref{prop:uniform-reduction}). The content of the
argument is the qualitative form. All hypotheses that one might
have expected --- amalgamation, joint embedding, tameness, no maximal
models, arbitrarily large models, a strongly compact cardinal, the
weak generalized continuum hypothesis --- are absent.

Two easy consequences are worth remembering.

\begin{enumerate}
\item On the categorical tail, \emph{every model strongly embeds into
every model of at least its size}. The LS axiom supplies a strong
submodel of the smaller size, and categoricity identifies it with the
given one. So the tail automatically has joint embedding, and no
model on the tail is maximal.
\item Categoricity includes existence: at every cardinal in the tail
the class has \emph{at least} one model, and also \emph{at most} one
up to isomorphism. Both parallel within the proof.
\end{enumerate}

A concrete corollary, which is the reason the result matters for
$L_{\omega_1,\omega}$-theories in countable vocabularies:
if $\varphi$ is such a sentence, then there is one threshold
$\mu(\aleph_0)$ with the property that categoricity of $\varphi$
in any single cardinal above $\mu(\aleph_0)$ forces categoricity of
$\varphi$ everywhere above $\mu(\aleph_0)$.

\subsection*{The shape of the proof}

The proof has a single skeleton. I state it now so that every later
section has a fixed place on the map. The reader is invited to come
back and reread this list at the beginning of each section.

\begin{enumerate}
\item \textbf{Reduction.} We replace the uniform statement by the
qualitative one. The proof is a small-model count and is completely
separate from the mathematics of AECs
(Section~\ref{sec:reduction}).

\item \textbf{Presentations.} Every AEC with arbitrarily large models
admits an \emph{Ehrenfeucht--Mostowski presentation}: a functor $E$
that sends a linear order $I$ to a model $E(I)$, so that order
embeddings become strong maps and every element of $E(I)$ is named
by a fixed finite list of positions in $I$ and one of a fixed small
set of labels (Section~\ref{sec:orders}).

\item \textbf{Reversal.} Using specially chosen index orders, we
\emph{reverse} any strong self-map on any fixed bounded tuple: if
$f\colon M\to M$ is strong and $\bar a$ is a tuple of length below the
categoricity size, then there is a strong $g\colon M\to M$ with
$g(f(\bar a))=\bar a$ (Section~\ref{sec:reversal}).

\item \textbf{Diagrams.} Reversal lets us define \emph{diagrams} of
small tuples in such a way that equality of diagrams at size
$\kappa$ is implemented by a strong self-map at size $\kappa$. The
diagrams stabilize as $\kappa$ grows. At suitable ``closed'' cardinals,
this gives \emph{amalgamation} (Section~\ref{sec:diagrams}).

\item \textbf{Working schemes.} The infrastructure we need for
finite systems of models is packaged as a \emph{working scheme}. It
is a small list of conditions (structural arrows, presentations,
diagrams, and an exhaustion test) that we verify once and then
apply repeatedly (Section~\ref{sec:schemes}).

\item \textbf{Calculus.} For a working scheme we invent \emph{free
extensions} of types, chosen by majority over long approximation
sequences in the base. Stationary behaviour, transitivity under
iteration, and a local character theorem make this a genuine
independence relation (Section~\ref{sec:calculus}).

\item \textbf{Isolation.} We construct extensions of a model that
are \emph{all-dominated} over an added tuple: every bounded tuple
of the extension is controlled by a bounded fragment of the base
together with the mark. All-dominated extensions behave like prime
hulls (Section~\ref{sec:isolation}).

\item \textbf{Marked increments.} We add one \emph{mark}: a
prescribed stationary type in the root sort. The all-dominated
construction makes this closed under finite systems of models,
indexed by subsets of a finite axis set
(Section~\ref{sec:marked}).

\item \textbf{Finite-dimensional systems and boundary lifting.}
Every finite-dimensional system has a ``boundary'' consisting of its
proper sub-faces. An isomorphism of boundaries extends to an
isomorphism of the whole systems (Section~\ref{sec:boundaries}).

\item \textbf{Geometry.} We produce a model $M_0$ and a
nonalgebraic singleton type $p_0$ over it that is
\emph{minimal}: it has exactly one nonalgebraic extension over every
strongly included model of the same size. Realizations of $p_0$ form
a \emph{pregeometry}, so we can talk about bases and dimension
(Section~\ref{sec:geometry}).

\item \textbf{Geometric systems.} Bases can be partitioned into
finitely many ``pieces'' attached to the vertices of a finite axis
set. Boundary lifting applies, classifying finite-dimensional systems
by their bases up to prescribed bijection
(Section~\ref{sec:geometric-systems}).

\item \textbf{Common level.} Both applications (marked and geometric)
use closed cardinals. A single bookkeeping argument produces one
cardinal that is closed for \emph{every} finite depth and shape
simultaneously (Section~\ref{sec:closure}).

\item \textbf{Cardinal induction.} Starting from the common level
above, we induct on the maximum cardinal of a basis piece.
At each step one extra axis records the previously constructed
isomorphism; exact boundary lifting then gives the next level.
Limits are handled by coherent unions. The zero-axis case gives
pointed categoricity, and forgetting the point gives categoricity
(Section~\ref{sec:transfer}).
\end{enumerate}

Nothing in steps 2--12 assumes the eventual categoricity statement we
are trying to prove. The assumption ``categorical in unboundedly many
cardinals'' is used in a fixed way: to give us categoricity models
at every sufficiently large cardinal, which is exactly what the
order presentations, reversal, and common-level closure consume.

\section{Abstract elementary classes}\label{sec:aec}

\subsection{Syntax and structures}

Fix a \emph{language} $\tau$: a set of function, relation, and constant
symbols, each with a finite arity, and with no restriction on the
cardinality $|\tau|$ of that set. A \emph{$\tau$-structure} $M$ is a
set $|M|$ (the \emph{universe}) together with an interpretation of
each symbol of $\tau$ with its prescribed arity. Write $\|M\|$ for
the cardinality of $|M|$. For a substructure $M\subseteq N$ (also
written $|M|\subseteq|N|$, with the structure data being restricted),
the notation is standard. Isomorphisms are bijections preserving
every symbol.

\begin{definition}[Abstract elementary class]\label{def:aec}
An \emph{abstract elementary class} (AEC) is a pair $\K=(\mathcal C,\le_\K)$,
where $\mathcal C$ is a class of $\tau$-structures and $\le_\K$ is a
partial order on $\mathcal C$, subject to four axioms.
\begin{enumerate}
\item \emph{Closure under isomorphism, substructure, and image.} $\mathcal C$
is closed under isomorphism. If $M\le_\K N$ then $M$ is a
$\tau$-substructure of $N$. If $f\colon N\cong N'$ is an isomorphism
and $M\le_\K N$ then $f[M]\le_\K N'$.

\item \emph{Coherence.} If $M_0\subseteq M_1\subseteq M_2$ (as
$\tau$-structures), $M_0\le_\K M_2$, and $M_1\le_\K M_2$, then
$M_0\le_\K M_1$.

\item \emph{Chain unions.} For every nonzero ordinal $\delta$ and
every increasing $\le_\K$-chain $(M_i:i<\delta)$, its union $U$
(as a $\tau$-structure on $\bigcup_i |M_i|$) belongs to $\mathcal C$,
and satisfies $M_i\le_\K U$ for every $i$. If additionally each $M_i$
satisfies $M_i\le_\K N$ for a fixed $N\in\mathcal C$, then
$U\le_\K N$.

\item \emph{L\"owenheim--Skolem property.} There is an infinite
cardinal $\ell\ge|\tau|+\aleph_0$ such that, for every $M\in\mathcal C$
and every $A\subseteq|M|$, there is $N\le_\K M$ with $A\subseteq|N|$
and $\|N\|\le|A|+\ell$.
\end{enumerate}
The least possible $\ell$ in axiom (4) is denoted $\LS(\K)$.
\end{definition}

Read $\le_\K$ as ``is a strong submodel of.'' It plays the role of
elementary submodel in first-order logic, but the definition does not
require that any compactness theorem exists: an AEC can fail compactness
very badly and still satisfy the four axioms.

Throughout, $M,N,A,B$ denote $\tau$-structures in $\mathcal C$ ---
except that $A,B$ sometimes denote mere subsets when this is explicit.

\begin{definition}[Categoricity]\label{def:categorical}
$\K$ is \emph{categorical in $\kappa$} if $\K$ has a model of
cardinality $\kappa$ and any two of its models of size $\kappa$ are
isomorphic. Equivalently, $\K$ has \emph{exactly one} model of size
$\kappa$ up to isomorphism.
\end{definition}

A few easy consequences of the axioms we will use without comment.

\begin{proposition}[Directed unions and direct limits]\label{prop:directed-union}
Let $\K$ be an AEC, and let $(M_i:i\in I)$ be a nonempty directed
family of models of $\K$, closed under the operation ``choose a
common upper bound,'' meaning: for all $i,j\in I$ there is
$k\in I$ with $M_i\le_\K M_k$ and $M_j\le_\K M_k$. Then:
\begin{enumerate}
\item The union $U=\bigcup_{i\in I}|M_i|$ carries a unique $\tau$-structure
(as a $\tau$-substructure of every sufficiently large $M_i$), belongs
to $\mathcal C$, and $M_i\le_\K U$ for every $i$.
\item If every $M_i\le_\K N$ for a fixed $N$, then $U\le_\K N$.
\end{enumerate}
The same conclusion holds for direct limits of coherent systems of
strong maps: rename the maps to be inclusions, take the union of the
images, and use (1).
\end{proposition}

\begin{proof}
Finitarity of every symbol in $\tau$ means that any finitely many
elements of $U$ lie in a single $M_i$: pick an index above their
individual indices using directedness. The structure on $U$ is
therefore well defined and, by finite directedness, is exactly the
structure of any $M_k$ containing those finitely many elements. Axiom
(3) handles the case where $I=\delta$ is an ordinal chain. For a
general set-indexed directed family, encode into the chain case by
well-ordering the family $I$, choosing successively a bound for the
previous union plus the next member (so we build a chain of total
size $|I|$ whose union is $U$), and applying (3). The common
upper bound part is identical.
\end{proof}

\begin{remark}[Conventions used throughout]\label{rem:conventions}
\begin{enumerate}
\item \emph{Sizes.} All variables $\lambda,\mu,\nu,\kappa$ are cardinal
numbers unless explicitly called ordinals. $|M|$ denotes the universe
of $M$ and $\|M\|$ its cardinality. ``$A\subseteq M$'' means $A$
is a subset of $|M|$; when $A$ is closed under the functions of~$\tau$,
$A$ becomes a $\tau$-substructure and we write $A\le_\K M$.

\item \emph{Bounded.} A set or tuple is \emph{bounded at $\mu$} if its
cardinality is strictly less than $\mu$. Most of the argument is
``bounded-tuple mathematics'': we compare tuples of length $<\mu$
at a cardinal $\mu$, and we prove theorems that hold for all bounded
input sizes.

\item \emph{Levels.} A \emph{level} is a cardinal $\mu$ at which the
particular construction under discussion has been established.
Typically levels are strong limit cardinals of countable cofinality,
closed under a fixed finite list of cardinal operations. The exact
closure demanded is stated each time it is used.

\item \emph{Compositions of strong maps.} By axiom (1) and (2) of
Definition~\ref{def:aec}, strong maps compose: if $f\colon M\to N$
and $g\colon N\to K$ are strong (meaning: $f$ is an isomorphism onto
$f[M]$, $f[M]\le_\K N$, and unravelling, $f[M]\le_\K N$; and
$g[N]\le_\K K$), then $g\circ f$ is strong onto its image.

\item \emph{Isomorphism renaming.} We usually replace an arbitrary
strong map $f\colon M\to N$ with a strong inclusion $M\le_\K N'$
where $N'$ is an isomorphic copy of $N$. This is convention; genuinely
arbitrary strong maps appear only in the order-presentation functor.
\end{enumerate}
\end{remark}

This completes the background. The rest of the paper is the proof
of Theorem~\ref{thm:main-qualitative}.

\section{Reducing uniform to qualitative}\label{sec:reduction}

The qualitative form (Theorem~\ref{thm:main-qualitative}) is the
mathematical content. The uniform form
(Theorem~\ref{thm:main-uniform}) is a small-model count, which we
record now.

\subsection{An AEC is determined by its small models}

Fix an infinite cardinal $\lambda$ and a language $\tau$ of cardinality
at most $\lambda$. An AEC in $\tau$ with $\LS(\K)\le\lambda$ has the
following property: any model of $\K$ is the union of a directed family
of its strong submodels of size at most $\lambda$. This is just the
axiom (4) applied to small subsets, together with strongness of
directed unions. Consequently:

\begin{lemma}[Small-model recovery]\label{lem:small-code}
Such an AEC is completely determined by:
\begin{enumerate}
\item the set of isomorphism classes of its models of size at most $\lambda$,
\item the set of isomorphism classes of strong inclusions $M\le_\K N$
between such models,
\end{enumerate}
and this data has a \emph{set code}: a single set $c$ whose subsets certify
membership and strongness, and which recovers the class and its
strong-submodel relation by a first-order formula of set theory.
\end{lemma}

\begin{proof}
Represent small structures on ordinals of size at most $\lambda$.
Represent a small pair $M\subseteq N$ by representatives for
$N$ together with a distinguished subset for $|M|$. The set of possible
structures and pairs of this form is itself a set. A code $c$ is
the set of those types that are allowed in $\K$.

Forward direction. For $M\in\K$, let
$\mathcal D(M)=\{A\le_\K M:\|A\|\le\lambda\}$. This is a set. It is
nonempty (LS axiom on $\varnothing$) and its union is $M$ (LS axiom on
singletons, using the chain-tower argument). It is directed: given
$A,B\in\mathcal D(M)$, LS applied inside $M$ to $|A|\cup|B|$ yields a
small strong submodel containing both, and coherence makes $A,B$ strong
in it.

Reverse direction. Let $M$ be any structure that is the union of a
nonempty directed family $\mathcal D$ of allowed small models, whose
member pairs are all allowed by $c$. The directed-union property
(Proposition~\ref{prop:directed-union}) gives $M\in\K$. Conversely, if
$M\in\K$, then $\mathcal D(M)$ gives such a family. So:
\begin{quote}
$M\in\K$ iff $M$ is the union of a nonempty directed family of $c$-allowed
small models, with all directed inclusions $c$-allowed.
\end{quote}
The same idea recovers $M\le_\K N$. Require a directed presentation
$N=\bigcup\mathcal D$ of the above form and a nonempty directed
subfamily $\mathcal E\subseteq\mathcal D$ with $M=\bigcup\mathcal E$.
If $M\le_\K N$, take $\mathcal D=\mathcal D(N)$ and $\mathcal E=\mathcal D(M)$;
then $\mathcal E\subseteq\mathcal D$ by axiom (1) and (2). Conversely,
each member of $\mathcal E$ is strong in $N$ (members of $\mathcal D$ are
strong in their union, which is $N$), so the common-upper-bound clause
of axiom (3) gives $M\le_\K N$.

Every presentation involved is a set of substructures of the structure
being decoded, so quantification over presentations is set-sized. Thus
both the class and its strong relation are given by first-order formulas
of set theory with parameter $c$.
\end{proof}

\subsection{The equivalence}

\begin{proposition}[Uniform = qualitative]\label{prop:uniform-reduction}
Theorem~\ref{thm:main-uniform} is equivalent to
Theorem~\ref{thm:main-qualitative}.
\end{proposition}

\begin{proof}
Fix an infinite cardinal $\lambda$ and consider all AECs with $\LS\le\lambda$.
By Lemma~\ref{lem:small-code}, they are all determined by codes $c$ running
over a \emph{set} (a set of allowed small structures and pairs, on a
fixed underlying ordinal $\lambda$). A code is \emph{valid} if its
decoded class and relation satisfy the AEC axioms with LS bound $\lambda$;
this is a first-order property of the code, so the valid codes form a set.

Assume the qualitative form. For each valid code $c$, the categoricity
spectrum of the decoded AEC is either bounded or unbounded.
\begin{itemize}
\item Bounded case: choose $b_c>\lambda$ strictly above every cardinal
in which the AEC is categorical. This $b_c$ is definable from $c$.
\item Unbounded case: by the qualitative form, there is a threshold
$b_c$ above which the AEC is categorical in every cardinal.
\end{itemize}
Replacement bounds the set $\{b_c : c\text{ valid}\}$. Choose $\mu(\lambda)\ge\lambda$
strictly above this set. Now suppose $\K$ with $\LS(\K)\le\lambda$ is
categorical in some $\kappa\ge\mu(\lambda)$. Its code $c$ cannot be in the
bounded-spectrum case, since $\kappa>\sup$ of the categorical spectrum
would be required. It is therefore in the unbounded case, and the AEC is
categorical in every $\kappa'\ge b_c$, in particular in every
$\kappa'\ge\mu(\lambda)$.

Conversely, assume the uniform form. Let $\K$ be an AEC categorical in
unboundedly many cardinals. Apply the uniform form at $\lambda=\LS(\K)$:
some categorical cardinal of $\K$ lies above $\mu(\lambda)$, and the
uniform form's conclusion gives categoricity at every larger cardinal.
\end{proof}

\begin{remark}
Lemma~\ref{lem:small-code} also gives a ZFC reading of the phrase
``quantify over all AECs with $\LS\le\lambda$'': one quantifies over
their set codes and uses the decoded class predicates. No choice of
representatives from a proper class, and no class choice axiom, is
required.
\end{remark}

For the rest of the paper we fix one AEC $\K$, categorical in unboundedly
many cardinals, and prove $\K$ is categorical in every cardinal above
some threshold. Set $\ell=\LS(\K)$. By categoricity at any cardinal,
$\K$ has models of that size, so $\K$ has arbitrarily large models.
That last consequence will be used in the very next section.

\section{Order presentations}\label{sec:orders}

The crucial technical device is the
\emph{Ehrenfeucht--Mostowski order presentation}. It converts the
one-dimensional structure of a linear order into a model of $\K$, in a
way that respects order embeddings as strong maps and names every
element of the model by a finite list of indices plus a fixed label.

\subsection{Partition calculus}

We need the standard Erd\H{o}s--Rado partition property. The precise
form we use is:

\begin{lemma}[Enlargement for finitely many colors]\label{lem:partition}
For infinite cardinals $\xi,\nu$ and a positive integer $k$, there is an
infinite cardinal $R_k(\xi,\nu)$ such that every coloring of the
$k$-element subsets of any ordinal of size at least $R_k(\xi,\nu)$ into
$\xi$ colors has a homogeneous subset of size $\nu$. Finitely many
specified arities can be made homogeneous simultaneously by enlarging
the initial cardinal.
\end{lemma}

\begin{proof}
Induction on $k$. For $k=1$: a set of size $>\xi\cdot\nu$ cannot be
partitioned into $\xi$ cells of size $<\nu$. Suppose the assertion is
known for $k$; choose an initial ordinal $\alpha$ with
$|\alpha|\ge R_k(\xi,\nu)$ and put $b=\xi^{|\alpha|}$.

Let $c$ color $(k+1)$-subsets of an initial ordinal $\Omega$ of size
$>b$. Build a tree of residual subsets of $\Omega$ of height $\alpha$.
The root is $\Omega$. At a nonempty node, remove and name its least
point $x$. The named points on the branch, together with $x$, form an
increasing sequence; color the remaining residual by the values
$c(s\cup\{u\})$ for every $k$-subset $s$ of that sequence. The nonempty
parts are the children. At a limit height, a node is retained iff the
intersection of the residual sets along its branch is nonempty.

Each node has at most $|\alpha|$ coordinates and hence at most $b$
children; total nodes through height $\alpha$ number at most
$b^{|\alpha|}=b$, including limit nodes. At most $b$ points are named
overall, so some $u\in\Omega$ is never named. The point $u$ belongs to
one residual at every height, and to the limit intersection along its
branch; thus it determines a branch with $\alpha$ named points and a
nonempty remainder.

For every $k$-subset $s$ of the named points, all later named points
give the same $c(s\cup\{x\})$, because this value was fixed by the
partition immediately after the last point of $s$ was named.
Consequently, on the branch, $c$ on increasing $(k+1)$-tuples depends
only on their first $k$ entries. Apply the $k$-ary induction to this
induced coloring: the homogeneous $\nu$-subset is homogeneous for $c$
as well. For example, $R_{k+1}(\xi,\nu)=(\xi^{R_k(\xi,\nu)})^+$ after
raising $R_1$ suitably. For a finite list of arities, work backward
to choose a bound large enough for the last desired thinning after all
earlier thinnings; homogeneity from earlier arities is not disturbed.
\end{proof}

\subsection{The order-presentation theorem}

\begin{theorem}[Order presentation]\label{thm:order-template}
Let $\K$ have arbitrarily large models and $\ell=\LS(\K)$. There are
at most $\ell$ \emph{labels}, each of positive finite arity, and a functor
$E$ from nonempty linear orders to models of $\K$, with the following
properties.
\begin{enumerate}
\item \emph{Evaluation on finite support.} Every element of $E(I)$ is
of the form $\lambda(\bar i)$ where $\lambda$ is a label and
$\bar i\in I^{n}$ is an increasing finite list of positions, $n$
depending on $\lambda$. Equality, structure relations, and function
values are determined by the labels and the order/equality pattern
of the finitely many positions supporting them.

\item \emph{Skeleta and functoriality.} $E(I)$ contains distinct
distinguished elements $(a_i)_{i\in I}$. An order embedding
$f\colon I\to J$ sends $a_i$ to $a_{f(i)}$ and, on any
$\lambda(\bar i)$, acts by substituting $f$ for each position:
$\lambda(\bar i)\mapsto\lambda(f(\bar i))$. This gives a strong map
$E(f)\colon E(I)\to E(J)$.

\item \emph{Small subpresentations.} For every finite nonempty
$s\subseteq I$, the set of labeled elements supported entirely on $s$
is $E_s(I)\le_\K E(I)$, with $\|E_s(I)\|\le\ell$. For
$s\subseteq t$ these are strongly included and $E(I)=\bigcup_s E_s(I)$.

\item \emph{Cardinality.} $|I|\le\|E(I)\|\le|I|+\ell$. In particular,
for every infinite $\kappa\ge\ell$, $\K$ has a model of size exactly
$\kappa$.
\end{enumerate}
\end{theorem}

\begin{proof}
Pick an arbitrarily large $M\in\K$ with distinct elements $(a_i:a\in A)$
indexed by a large ordinal $A$. Recursively on the finite nonzero
$s\subseteq A$, choose $M_s\le_\K M$ of size $\le\ell$, containing the
distinguished elements on $s$ and every $M_t$ for nonempty
$t\subsetneq s$. There are finitely many such $t$, so the LS axiom gives
the needed $M_s$. Coherence gives $M_t\le_\K M_s$.

Choose a surjective enumeration $(m_{s,\eta})_{\eta<\ell}$ of each $M_s$,
requiring $m_{s,j}=a_{i_j}$ when $s=\{i_0<\dots<i_{n-1}\}$ and $j<n$.
For an $n$-element set $s$, let $\text{color}(s)$ be the complete atomic
diagram, with negations and equalities, of all the enumerations
$(m_{t,\eta})_{\eta<\ell}$ for $\varnothing\ne t\subseteq s$, with the
subsets of $s$ named by relative positions. There are at most $\ell$
names and atomic formulas for fixed $n$, so at most $2^\ell$ possible
colors.

Choose colors $d_n$ recursively so that for every $n$ there exist
samples of arbitrarily large cardinality homogeneous in $d_1,\dots,d_n$.
If $d_1,\dots,d_{n-1}$ are chosen, take a sample, thin it by
Lemma~\ref{lem:partition} at arity $n$ to a target cardinality; the
result is $n$-homogeneous in some color $d_n$, coherent with the earlier
$d_i$. If all possible $n$-colors admitted only bounded thinnings, the
supremum over those bounds (a set by Power Set) would be a uniform bound
on all thinnings, contradiction. This recursion constructs colors that
realize every finite pattern, not an infinite simultaneous pattern
inside a single sample.

Now given a linear order $I$, define $E(I)$ as follows. Introduce
formal symbols $(s,\eta)$ for $s\subseteq I$ finite nonempty and
$\eta<\ell$, listed increasingly. Identify $(s,\eta)\sim(t,\zeta)$ iff
the color $d_{|s\cup t|}$ says the corresponding entries are equal.
Coherence of colors makes the relation independent of the larger finite
set used. Reflexivity, symmetry, and transitivity hold because any
finite instance occurs in a realized color. Let $E(I)$ be the quotient.

Interpret a relation on finitely many quotient elements in a color on
the union of their supports; interpret a function by evaluation in a
sample and using a name for the value; interpret a constant using any
one nonempty finite support. Coherence makes these well defined.
Every axiom of a $\tau$-structure is checked locally on finite subsets,
where it holds in a sample. Thus $E(I)$ is a $\tau$-structure.

Define $E_s(I)$ as the elements named by $(s,\eta)$, $\eta<\ell$. The
color $d_{|s|}$ makes this a copy of an actual model $M_s$ in a
sample; names with support $t\subseteq s$ were included. For
$s\subseteq u$, the inclusion $E_s(I)\subseteq E_u(I)$ is isomorphic
to an actual pair $M_s\le_\K M_u$ from a realization of $d_{|u|}$;
isomorphism invariance makes the inclusion strong. The family
$(E_s(I))_s$ is directed and covers $E(I)$. Its directed union belongs
to $\K$, and each $E_s(I)\le_\K E(I)$.

For an order embedding $f\colon I\to J$, substitution
$(s,\eta)\mapsto(f[s],\eta)$ preserves every defining diagram and every
inequality of names, so it defines an embedding $E(f)\colon E(I)\to E(J)$.
On each $E_s(I)$ it is an isomorphism onto $E_{f[s]}(J)\le_\K E(J)$.
The common-upper-bound clause for the directed union $(E_{f[s]}(J))_{s}$
gives strongness of the whole image. Substitution also proves
$E(\mathrm{id})=\mathrm{id}$ and $E(g\circ f)=E(g)\circ E(f)$.

Define $a_i$ as the first designated name on $\{i\}$. The color tables
identify this with the name for $i$ on any larger support. Distinct
indices give distinct elements because every relevant sample had this
property. Labels are indexed by $(n,\eta)$ with $n\ge1$ finite and
$\eta<\ell$, so at most $\ell$ of them. Counting finite supports gives
the cardinality bound, and the displayed $a_i$ give the lower bound.
\end{proof}

\begin{remark}
The last clause of Theorem~\ref{thm:order-template} says $\K$ has
models of every size $\ge\ell$. This does not require categoricity;
it is a consequence of ``arbitrarily large models.'' In particular,
the hypothesis of Lemma~\ref{lem:small-code} and the functorial
construction above are compatible; both hold for our fixed $\K$.
\end{remark}

We will use the notation $E$ for the functor constructed in
Theorem~\ref{thm:order-template} for the rest of the paper. For an
index order $I$ and a finite nonempty $s\subseteq I$, $E_s(I)$ is the
strong submodel supported on $s$. For an order embedding $f$, $E(f)$
is the induced strong map, and $a_i$ are the distinguished skeleton
elements.

\section{Reversing strong maps on bounded tuples}\label{sec:reversal}

Throughout, $\K$ is the fixed AEC of Section~\ref{sec:reduction}:
categorical in unboundedly many cardinals, with $\ell=\LS(\K)$,
and $E$ is the functor of Theorem~\ref{thm:order-template}.

\subsection{What we want and why}

Fix $\theta$ (a cardinal) and a categoricity cardinal $\kappa$.
Let $M$ be a model of $\K$ of size $\kappa$, let $f\colon M\to M$ be a
strong self-map, and let $\bar a$ be a tuple in $M$ of length at most
$\theta$. Our goal in this section is:

\begin{quote}
\emph{there is a strong $g\colon M\to M$ with $g(f(\bar a))=\bar a$,
provided $\kappa$ is large enough (depending on $\theta$ but not on
$M$, $f$, or $\bar a$).}
\end{quote}

This is called ``reversing $f$ on $\bar a$.'' It may sound strange:
$f$ need not be onto $\bar a$'s ambient model, and even if it were
bijective, an arbitrary strong self-map has no reason to be reversible
on a given tuple. The point is that at a categoricity cardinal,
we can compose $f$ with an automorphism of $M$ (or a substitute for
one) to fix things up. The argument has to produce these substitute
automorphisms, and it does so via the flexibility of the order
presentation $E$.

Reversal gives the following consequence: the relation ``$p\to r$''
on orbit-pairs of $\theta$-tuples, meaning ``some strong self-map sends
a representative of $p$ to a representative of $r$,'' becomes
\emph{symmetric}. Symmetry of this relation is the key input for the
stable-diagram machinery of Section~\ref{sec:diagrams}.

The strategy is: present $M$ as $E(H(\delta))$ for a specially chosen
index order $H(\delta)$, so that many strong self-maps arise by taking
$E(\sigma)$ for an automorphism $\sigma$ of the index order. The
question becomes whether $\Aut(H(\delta))$ has enough freedom to
match all short tuples in a prescribed way. That comes down to a
$\mathrm{Galois}$-style analysis of the order $H(\delta)$ and its
automorphisms on short tuples.

\subsection{The index order $H(\delta)$}

\begin{definition}[Index orders]\label{def:H-delta}
For an infinite limit ordinal $\delta$, put
\[
 \Gamma_\delta=\Z^{(\delta)},\qquad
 H(\delta)=\Q^{(\Gamma_\delta)}.
\]
Parentheses denote finitely supported functions. Both are ordered
abelian groups: the order is lexicographic on the greatest coordinate
in the support (``first difference'') direction. Write $e_\alpha$ for
the integer basis vector at $\alpha$ and $u_g$ for the rational basis
vector at $g\in\Gamma_\delta$. The \emph{rank} of a nonzero vector is
the largest $\alpha<\delta$ in its support.

Unless group operations are mentioned, $H(\delta)$ is viewed as a pure
linear order; in particular $\Aut(H(\delta))$ is its group of order
automorphisms.
\end{definition}

\begin{lemma}[Basic order properties]\label{lem:H-basic}
$H(\delta)$ is a dense linear order without endpoints. Its cardinality
is $|\delta|$, and every point has character $\cf(\delta)$ on both
left and right. All nonempty bounded open intervals are order-isomorphic;
all left rays are order-isomorphic; all right rays are order-isomorphic.
An increasing map on ordinal positions extends to an order embedding
$H(\delta)\to H(\delta')$ by moving positions and padding with zeros.
Every point of $H(\delta)$ has a finite code from finitely many ordinal
positions and integer and rational coefficients; comparisons are
determined by these coefficients and the order/equality pattern of
the ordinal positions.
\end{lemma}

\begin{proof}
Finite-support counting gives $|\Gamma_\delta|=|H(\delta)|=|\delta|$.
$\Gamma_\delta$ has a least positive element $e_0$, so every $g$ has
predecessor $g-e_0$; its cofinality and coinitiality are both
$\cf(\delta)$ (vectors $e_\alpha$ for $\alpha$ cofinal give
cofinality; the supports of fewer than $\cf(\delta)$ vectors are
bounded in $\delta$, so such a family is neither cofinal nor
coinitial). $H(\delta)$ is a divisible nonzero ordered abelian group,
hence dense without endpoints. If $(g_i)$ is coinitial in $\Gamma_\delta$,
then $(u_{g_i})$ is coinitial in the positive cone of $H(\delta)$;
conversely, the ranks of fewer than $\cf(\delta)$ positive vectors
have a strict lower bound in $\Gamma_\delta$. Thus the positive cone
has coinitiality $\cf(\delta)$, and translation and negation give the
character assertion at every point.

Translations identify rays of a fixed direction. We show any positive
vector can be sent to any other by an increasing automorphism: first
translate so that their greatest support coordinates agree at some $g$;
write the vectors as $a u_g+v$ and $b u_g+w$ with $a,b\in\Q_{>0}$ and
$\rk(v),\rk(w)<g$. Fix all basis vectors except $u_g$ and replace
$u_g$ by $(b/a)u_g+(w-v)/a$; this is an invertible triangular
rational-linear map, preserving the sign of every nonzero vector, and
it sends the first vector to the second. Combined with translations,
it sends any ordered pair of distinct points to any other, giving the
interval assertion.

An increasing map on ordinal positions preserves the greatest
differing position of two integer vectors, hence also of two rational
vectors, giving an order embedding. Expanding the finitely many
integer-vector positions used by a rational vector gives its finite
code and comparison rule.
\end{proof}

\subsection{Cuts}

\begin{definition}[Cuts of an order]\label{def:cut}
A \emph{cut} of a linear order $L$ is a partition $L=L^-\cup L^+$
with $L^-<L^+$. It is \emph{interior nonprincipal} if both sides are
nonempty, $L^-$ has no greatest element, and $L^+$ has no least
element. Its \emph{characters} are $\cf(L^-)$ and $\ci(L^+)$; it is
\emph{balanced} if these cardinals are equal.
\end{definition}

\begin{lemma}[Balanced cuts]\label{lem:balanced-cuts}
Every interior nonprincipal cut of $\Gamma_\delta$ is balanced, and
similarly for $H(\delta)$.
\end{lemma}

\begin{proof}
First $\Gamma_\delta$. Given a cut $(L,R)$, among the ranks of
$r-l$ with $l\in L,r\in R$, let $\alpha$ be the least. Fix a crossing
pair of that rank and its common head above $\alpha$. In that head,
each fiber with a fixed integer coefficient at $\alpha$ lies wholly on
one side (else a crossing pair would have smaller rank). The resulting
cut in the integer coefficients separates two adjacent integers. The
two bordering fibers are cofinal and coinitial toward the cut, and are
copies of $\Z^{(\alpha)}$; their end characters agree by negation in
that tail group. The case $\alpha=0$ would give last-and-first, which
is excluded by interior-nonprincipality.

Now $H=H(\delta)$. Put
$T=\{\rk(r-l): l\in L, r\in R\}$, which is a final segment of
$\Gamma_\delta$ (given a crossing pair of rank $g$, subtract a
positive basis vector at any $h>g$).

If $T$ has a least member $g$: fix a crossing head above $g$. Each
fiber with a fixed rational coefficient at $g$ lies on one side.
The induced $\Q$-cut either has both sides able to approach via
countable rationals (giving countable cofinality/coinitiality in
$H$) or has a nearest rational on one side (giving $\aleph_0$ on both
sides via the tail $\Z^{(\alpha)}$ at $\alpha=g-e_0$). Either way the
cut is balanced.

If $T$ has no least member with $\epsilon=\ci(T)$, put
$S=\Gamma_\delta\setminus T$.
Case A: there is $l\in L$ with $\{\rk(r-l):r\in R\}$ coinitial in
$T$. The coset $l+H_S$ is contained in $L$ and is cofinal in $L$;
a point $l'$ above the whole coset would force $\rk(r-l)<h$ for some
$r\in R$ where $h=\rk(l'-l)$, contradiction. $S$ is nonempty and has
no greatest element; balance in $\Gamma_\delta$ on $(S,T)$ gives
$\cf(S)=\epsilon$, hence $\cf(L)=\epsilon$.

Case B: every $l\in L$ has a strict lower bound $t_l\in T$ on the
ranks of $r-l$. Choose crossing pairs $(l_i,r_i)$ with $\rk(r_i-l_i)$
coinitial in $T$. For fixed $l$, some $i$ has
$\rk(r_i-l_i)\le t_l$, forcing $l_i>l$ (else $r_i-l\le r_i-l_i$ would
have smaller rank). So $(l_i)$ is cofinal in $L$, giving $\cf(L)=\epsilon$.

Apply the lower-side calculation after negating. Negation preserves
every difference rank, hence $T$ and $\epsilon$, and yields
$\ci(R)=\epsilon$.
\end{proof}

\begin{lemma}[Segments approaching a small cut]\label{lem:cut-segments}
Let $L$ be a dense linear order without endpoints, all of whose points
have character $\kappa$ on both sides, with all bounded intervals of
one order type and all interior nonprincipal cuts balanced. For every
infinite regular $\epsilon<\kappa$, the segment types
$[p,\mathfrak c)=\{x\in L^-_{\mathfrak c}:p\le x\}$ and
$(\mathfrak c,p]=\{x\in L^+_{\mathfrak c}:x\le p\}$ (for interior
nonprincipal $\mathfrak c$ of character $\epsilon$ and $p$ on the
appropriate side) depend only on $\epsilon$ and direction; the
isomorphisms can be chosen to match $p$.
\end{lemma}

\begin{proof}
Simultaneous induction on $\epsilon$. Choose strictly increasing
$(p_i),(q_i)$ cofinal in the two cut sides, endpoints at index zero.
Partition the first segment into blocks
$B_0=\{p_0\}$, $B_{j+1}=(p_j,p_{j+1}]$, and at a limit $i<\epsilon$ with
cut $\mathfrak c_i=(D_i,U_i)$, $D_i=\{x:(\exists j<i)\ x\le p_j\}$,
$B_i=(\mathfrak c_i,p_i]$. This cut is interior nonprincipal with
lower cofinality $\cf(i)$ (the increasing $i$-sequence is cofinal;
fewer than $\cf(i)$ would give a cofinal set of indices in $i$). Its
upper side is non-first because a first point would have character at
most $\cf(i)<\kappa$. Balance gives character $\cf(i)$. Successor
blocks are isomorphic by bounded-interval homogeneity; limit blocks by
upper-side induction at $\cf(i)$. Gluing gives the lower-side
assertion. Upper-side analogous with coinitial sequences and the
lower-side induction.
\end{proof}

\subsection{Automorphism orbits of short sequences}

\begin{definition}[Strict slot]\label{def:strict-slot}
For $A\subseteq L$ and a cut $A=A^-\sqcup A^+$ (possibly with empty
side), the \emph{strict slot} is
$S_L(A^-,A^+)=\{x\in L\setminus A:A^-<x<A^+\}$. Its occupancy is the
assertion that this set is nonempty.
\end{definition}

\begin{theorem}[Short sequence orbits]\label{thm:order-orbits}
Let $\delta$ be an infinite limit ordinal and $\theta<\cf(\delta)$ an
infinite cardinal. Two sequences of length at most $\theta$ in
$H(\delta)$ are in the same $\Aut(H(\delta))$-orbit iff they have the
same order/equality diagram and the same occupancies of all strict
slots over their distinct entries.
\end{theorem}

\begin{proof}
Necessity: order and occupancy are preserved by every order automorphism.
Sufficiency: the order/equality diagrams give an increasing bijection
$f:A\to B$ between the sets of distinct entries of the two sequences,
matching the indexed sequences. Extend it across each occupied slot.

For a point $p$ in a slot over $A=A^-\sqcup A^+$, the portion at or
below $p$ has one of three forms: $(-\infty,p]$ if $A^-=\varnothing$;
$(a,p]$ if $A^-$ has a greatest member $a$; or $((D,U),p]$ where
$(D,U)$ is the interior nonprincipal cut of lower character
$\cf(A^-)\le\theta$ (upper side non-first because a first point would
have character at most $\theta<\kappa$). By balance and
Lemma~\ref{lem:cut-segments}, the segment type depends only on the
case and on $\cf(A^-)$. The same analysis on the upper side gives the
other half of the slot type. Choose an interior point $q$ of the
corresponding occupied slot over $B$ and match the two halves with
$p\mapsto q$. They glue to a slot isomorphism. Occupancy ensures
empty slots also correspond. Gluing over slots and uniting with $f$
gives the required automorphism of $H(\delta)$.
\end{proof}

\subsection{Records and the orbit bound}

Fix an infinite tuple length $\theta$. Consider a labeled presentation
of a $\theta$-tuple in $E(H(\delta))$: a function assigning to each
coordinate a label and a finite index list in $H(\delta)$.
Flatten the lists into a single indexed sequence of at most $\theta$
points of $H(\delta)$. Its \emph{presentation record} is: the labels,
the order/equality diagram of this flattened sequence, and all
occupancy data for its strict slots over the flattened positions.

\begin{lemma}[Uniform orbit bound]\label{lem:orbit-bound}
There is a set $\mathcal R_\theta$ of possible presentation records,
depending only on $\ell$ and $\theta$, with
\[
 |\mathcal R_\theta|\le B(\ell,\theta):=2^{2^{\ell+\theta}}.
\]
For every categoricity cardinal $\kappa\ge\max(\ell,\theta^+)$, the
set of $\Aut(M)$-orbits on $\theta$-tuples of the categoricity model
$M$ has cardinality at most $B(\ell,\theta)$. This applies also when
$\kappa$ is singular. If $|\delta|=\kappa$ and $\cf(\delta)>\theta$,
each realized record in $E(H(\delta))$ determines exactly one orbit.
\end{lemma}

\begin{proof}
There are at most $2^{\ell+\theta}$ choices of labels and arities;
flattened order/equality diagrams number at most $2^\theta$; their
sets of cuts have size at most $2^\theta$ and occupancy subsets at
most $2^{2^\theta}$. The stated bound bounds a universal set of
records.

For $\cf(\delta)>\theta$, equal records give an automorphism of
$H(\delta)$ matching the flattened lists (Theorem~\ref{thm:order-orbits}),
hence an automorphism of $E(H(\delta))$ matching the tuples.
Every tuple has a labeled presentation, so orbit count is at most
record count.

For any $\kappa\ge\max(\ell,\theta^+)$, the ordinal
$\delta=\kappa+\theta^+$ has cardinality $\kappa$ and cofinality
$\theta^+$. Then $E(H(\delta))$ has cardinality $\kappa$ and is a
categoricity model. So the bound applies.
\end{proof}

Pick one model $C_\kappa$ at each categoricity size that will be used
in any set-sized construction. On its $\theta$-tuple orbits, define
$p\to r$ to mean that some strong self-map of $C_\kappa$ sends a
representative of $p$ to a representative of $r$; this relation is
reflexive and transitive by defining properties of strong maps
(compose after using an automorphism to align intermediate
representatives). Choose an \emph{orbit name} into the fixed cardinal
$B(\ell,\theta)$, once per $\kappa$.

For a suitable $\delta$ with $|\delta|=\kappa$, let
$F_{\kappa,\delta}\colon\mathcal R_\theta\to B(\ell,\theta)$ be the
partial map sending each realized record to its orbit name. The
\emph{profile} of this presentation is the named arrow relation on
orbit names together with $F_{\kappa,\delta}$. There are at most
$2^{B(\ell,\theta)}$ possible profiles, independent of $\kappa$ and
$\delta$.

\subsection{Alignment in small subpresentations}

\begin{lemma}[Closure of ordinal supports]\label{lem:ordinal-support-closure}
Let $\theta^+\le a$ be infinite cardinals and $\beta$ an ordinal of
cofinality $>a$. Every $S\subseteq\beta$ of size at most $a$ is
contained in $T_0\subseteq\beta$ of size at most $a$ such that for
every $P\subseteq T_0$ of size at most $\theta$ and every finite tuple
from $\beta$, there is a tuple from $T_0$ with the same order/equality
diagram over $P$. Moreover $\otp(T_0)$ is bounded in $\beta$ and
$\cf(T_0)>\theta$.
\end{lemma}

\begin{proof}
Build increasing sets $S_i\subseteq\beta$ for $i<\theta^+$ starting
with $S$. At each successor, consider all strict slots over the whole
well-ordered $S_i$ (at most $a$ of them); in each finite slot add
every point, in each infinite slot add a countably infinite subset.
At limits, take unions. Cardinality stays $\le a$. Set
$T_0=\bigcup_{i<\theta^+}S_i$. Any $P$ of size $\le\theta$ lies
in some $S_i$ by regularity of $\theta^+$; match the finite tuple's
coordinates not in $S_i$ at the next stage. Since $|T_0|\le a<\cf(\beta)$,
$T_0$ is bounded. Each $S_i$ is bounded and its uppermost slot is
infinite, so the next stage contains points above all of $S_i$,
giving $\cf(T_0)>\theta$.
\end{proof}

\begin{lemma}[Appending a long indecomposable segment]\label{lem:append-segment}
Under the hypotheses of Lemma~\ref{lem:ordinal-support-closure},
suppose $\beta$ is additively indecomposable. Let $T_0$ be as there,
and let $\delta<\beta$ be additively indecomposable with
$\otp(T_0)<\delta$ and $\cf(\delta)>\theta$. Place a consecutive
segment $J$ of order type $\delta$ strictly after $T_0$ in $\beta$
and put $T=T_0\cup J$. Then $\otp(T)=\delta$ and $T$ inherits the
same finite-pattern property. Consequently $H(T)\subseteq H(\beta)$
computes correctly the occupancies of every strict slot over any
sequence of at most $\theta$ of its points.
\end{lemma}

\begin{proof}
Choose $\alpha<\beta$ above $T_0$; indecomposability of $\beta$
gives $\alpha+\delta<\beta$, so $J=[\alpha,\alpha+\delta)$ is
available. Indecomposability of $\delta$ gives
$\otp(T_0)+\delta=\delta$. For $P\subseteq T$ of size $\le\theta$
and a finite tuple in $\beta$: match coordinates below $\alpha$ into
$T_0$ over $P\cap T_0$; keep coordinates in $J$ fixed; match
coordinates at or beyond $J$ by distinct points of $J$ above a bound
in $J$ (available since $\cf(\delta)>\theta$). The three portions
stay in correct mutual order. Since $\Gamma_T=\Z^{(T)}$ embeds in
$\Gamma_\beta$ and $H(T)$ in $H(\beta)$, and every witness to an
occupied strict slot over at most $\theta$ points of $H(T)$ uses only
finitely many additional ordinal positions, matching those additional
positions into $T$ over the parameter positions gives a witness in
$H(T)$.
\end{proof}

\begin{proposition}[Alignment]\label{prop:alignment}
Fix the record set and orbit-naming at an infinite length $\theta$.
Let $a<\mu$ be categoricity cardinals with $a\ge\max(\ell,\theta^+)$.
Suppose the following have one common profile:
\begin{enumerate}
\item a presentation $E(H(\beta))$ of $C_\mu$ with $\beta$ additively
indecomposable, $|\beta|=\mu$, $\cf(\beta)>a$;
\item presentations $E(H(\delta))$ of $C_a$ for a cofinal subset of
$a^+$ of additively indecomposable $\delta$ of size $a$ and cofinality
$>\theta$.
\end{enumerate}
Then in any copy $N$ of $C_\mu$, every $A\subseteq|N|$ of size at most
$a$ is contained in some strong submodel $B\le_\K N$ of size $a$ such
that the orbit name of \emph{every} $\theta$-tuple in $B$, computed
in $B$ as a tuple of $C_a$, equals its name in $N$.
\end{proposition}

\begin{proof}
Identify $N$ with the presentation in item (1). Encode the given
set by its terms and flatten to finitely-supported ordinal positions
of $H(\beta)$; this is a set of size at most $a$. Apply
Lemma~\ref{lem:ordinal-support-closure} to obtain $T_0$, of order
type below $a^+$. Choose a profile occurrence $\delta$ from item (2)
above $\otp(T_0)$. Since $a^+\le\cf(\beta)\le\beta$ and
$\delta<a^+$, Lemma~\ref{lem:append-segment} applies and gives $T$ of
order type $\delta$.

The subpresentation $B=E(H(T))$ is strong in $N$ (by the common
upper bound clause into $E(H(\beta))$ for the directed union
$(E(H(T\cap\dots)))_?$, using additivity of $H$-subpresentations),
has cardinality $a$, and contains the requested set. For any
$\theta$-tuple in $B$: use its labeled presentation there. Its record
is identical in $E(H(T))$ and $E(H(\beta))$ by the last clause of
Lemma~\ref{lem:append-segment}. The order isomorphism
$\delta\cong T$ identifies its record in the former with the same
record for $E(H(\delta))$. Both record-to-name functions lie in the
common profile and hence agree.
\end{proof}

\subsection{The reversal theorem}

\begin{lemma}\label{lem:indecomposable-occurrences}
If $\kappa$ is an infinite cardinal and $\tau\le\kappa$ is an infinite
regular cardinal, the additively indecomposable ordinals
$\delta<\kappa^+$ with $|\delta|=\kappa$ and $\cf(\delta)=\tau$ are
cofinal in $\kappa^+$.
\end{lemma}

\begin{proof}
Given $\eta<\kappa^+$, choose a limit $\rho>\eta$ with
$\kappa\le\rho<\kappa^+$ and $\cf(\rho)=\tau$. (Append an ordinal
segment of type $\tau$ beyond $\eta+\kappa$.) Put
$\delta=\omega^\rho$. It is additively indecomposable; a cofinal
sequence of exponents gives cofinality $\cf(\rho)$ in $\delta$; every
ordinal below $\omega^\rho$ has finite Cantor normal form with
exponents below $\rho$, giving $|\delta|\le\kappa$, and
$\delta\ge\rho\ge\kappa$, so $|\delta|=\kappa$.
\end{proof}

\begin{theorem}[Eventual reversal]\label{thm:reversal}
For each infinite cardinal $\theta$ there is a cardinal
$b_\K(\theta)$ such that, whenever $\kappa\ge b_\K(\theta)$ is a
categoricity cardinal, $M\in\K$ has size $\kappa$, $f\colon M\to M$
is strong, and $\bar a$ is a tuple of length $\le\theta$ in $M$,
there is a strong $g\colon M\to M$ with $g(f(a_i))=a_i$ for every
coordinate $i$.
\end{theorem}

\begin{proof}
Pad a nonempty shorter tuple by repetitions (a strong self-map
suffices for the empty tuple). In a categoricity model, the asserted
reversal is equivalent to symmetry of the arrow relation on
$\theta$-tuple orbits: a reverse orbit arrow composed with
automorphisms matches any particular image and original tuple, and
conversely.

Suppose symmetry fails at unboundedly many categoricity cardinals.
Let $P$ bound the profile palette (e.g.\ $P=2^{B(\ell,\theta)}$).
Construct a strictly increasing list $(\kappa_i)_{i<P^+}$ of failing
categoricity cardinals with, at each step, an infinite regular
$\tau_i\le\kappa_i$ exceeding $\ell$, $\theta$, and every preceding
$\kappa_j$, and $\kappa_i>P$, and $\kappa_i>\kappa_j^\theta$ for
$j<i$. Such choices exist because failure is unbounded and only
set-many cardinals precede each step.

At size $\kappa_i$, fix orbit-naming. By Lemma~\ref{lem:indecomposable-occurrences},
the ordinals of size $\kappa_i$, cofinality $\tau_i$, and arising
from item (2) of Proposition~\ref{prop:alignment} are cofinal in
$\kappa_i^+$, and one profile occurs cofinally (else the supremum of
$P<\kappa_i^+$ bounded fibers is below the regular $\kappa_i^+$).
Since there are $P^+$ sizes but at most $P$ profiles, choose
$a<\mu$ with the same cofinally-recurring profile. They satisfy
$\theta^+\le a$, $a^\theta\le\mu$, $\tau_\mu>a$. Their common
arrow relation has $p\to r$ with $r\not\to p$; both names occur in
both sizes. Apply Proposition~\ref{prop:alignment} inside every
$\mu$-sized model, using any cofinal profile occurrence.

Construct $\theta^+$ rounds of an increasing strong chain of
$\mu$-sized models. Round $i<\theta^+$: choose an aligned
$a$-sized submodel $A_i\le_\K N$ (current ambient) containing all
previous $A_j$ (possible because the union has size at most $a$
and is small). Coherence gives $A_j\le_\K A_i$ for $j<i$.

Enumerate all $\theta$-tuples of $A_i$ ($a^\theta\le\mu$ steps).
At a step $\bar u$: if its current large-model orbit cannot reach
$p$, leave as is; if it can, compose such an arrow with $p\to r$ and
realize by a strong self-map of the current model, then rename
codomain so images of old elements are old elements. With the
transported identification, $\bar u$'s orbit is now $r$. Its orbit
persists as unable-to-reach-$p$ at every later large stage (else
transitivity from $r$ gives $r\to p$). Orbits that start unable to
reach $p$ persist automatically.

At every limit stage (including between rounds), take strong unions.
The construction has $\le\theta^+\cdot a^\theta\le\mu$ stages in
cardinality, so every large model is a copy of $C_\mu$; every
transition is an arrow of the common relation; persistence passes to
limits.

The aligned submodels form a strong increasing chain: for $j<i$
they are included, and both are strong in the current large model,
so coherence applies. The union
$A=\bigcup_{i<\theta^+}A_i$
belongs to $\K$, has size $a$, and is a copy of $C_a$. Every
$\theta$-tuple of $A$ is contained in some $A_i$ (since
$\cf(\theta^+)>\theta$); after round $i$ it cannot reach $p$ in the
large model. Its small-orbit name (computed in the next aligned
$A_{i+1}$) is the same by the alignment property; hence it cannot
reach $p$ in the common relation. The inclusion into $A$ gives an
arrow from this small orbit to its orbit in $A$. Transitivity would
contradict the earlier exclusion if the latter orbit could reach
$p$. So no tuple of $A$ has an orbit reaching $p$.

But $A\cong C_a$, so the orbit named $p$ occurs in $A$ and reaches
itself by the identity map. Contradiction. Hence failing categoricity
cardinals are bounded; a cardinal above the bound is $b_\K(\theta)$,
and the first paragraph yields the claimed reversals.
\end{proof}

\section{Bounded diagrams and stabilization}\label{sec:diagrams}

We now make the reversal theorem usable. The idea: at sufficiently
large categoricity cardinals, the ``orbit of a tuple up to strong
maps'' is a robust object that can be tested by a bounded amount of
information. Concretely, we will see that comparing two tuples over a
big model is equivalent to comparing them over a well-behaved
\emph{small} presentation, provided the small cases have been stabilized.

\subsection{Canonical equivalence at categoricity cardinals}

Fix an infinite cardinal $\sigma$. At a categoricity cardinal
$\kappa>\ell+\sigma$ at which Theorem~\ref{thm:reversal} holds for
$\sigma$-tuples, put
\[
 (M,a)\equiv^\sigma_\kappa(N,b)
 \quad\Longleftrightarrow\quad
 \text{some strong map }f\colon M\to N\text{ satisfies }f(a)=b.
\]
Here $\|M\|=\|N\|=\kappa$ and the lengths of $a$, $b$ are at most
$\sigma$.

\begin{lemma}\label{lem:sigma-canonical}
$\equiv^\sigma_\kappa$ is an equivalence relation on $\sigma$-tuples
of $\kappa$-sized models. Its classes, for all tuple lengths under
consideration, number at most the fixed cardinal $B(\ell,\sigma)$ of
Lemma~\ref{lem:orbit-bound}.
\end{lemma}

\begin{proof}
Reflexivity: identity. Symmetry: given $f\colon M\to N$ with
$f(a)=b$, use categoricity and $\kappa\ge\ell+\sigma$ to pick an
isomorphism $\phi\colon M\to N$ matching the tuple (or, alternatively,
work inside one categoricity model and use reversal on a self-map
implementing $f$). More directly: identify both $M$ and $N$ with a
common copy $C$ via isomorphisms $\alpha$, $\beta$. Set
$\psi = \beta\circ f\circ\alpha^{-1}\colon C\to C$ strong. Reversal
(Theorem~\ref{thm:reversal}) applied to $\psi$ and $\alpha(a)$ gives
a strong $\eta\colon C\to C$ with $\eta\psi\alpha(a)=\alpha(a)$. Then
$\alpha^{-1}\eta\beta\colon N\to M$ sends $b$ back to $a$. Transitivity:
compose.

For the bound, transport to one categoricity model $C$ at $\kappa$.
Using Lemma~\ref{lem:orbit-bound}, the set of $\Aut(C)$-orbits on
$\sigma$-tuples has cardinality at most $B(\ell,\sigma)$. Each
$\equiv^\sigma_\kappa$-class is a union of $\Aut$-orbits, hence there
are at most $B(\ell,\sigma)$ classes.
\end{proof}

\begin{lemma}[Canonical classes above a categoricity size]
\label{lem:canonical-classes}
Let $\sigma$ be infinite and let $\kappa>\ell+\sigma$ be a
categoricity cardinal where reversal holds. For $\|N\|\ge\kappa$,
a tuple $a$ in $N$ has a well-defined $\equiv^\sigma_\kappa$-class,
computed in any strong $\kappa$-submodel of $N$ containing $a$.
Strong embeddings between models of size $\ge\kappa$ preserve the
class.
\end{lemma}

\begin{proof}
Existence: the L\"owenheim--Skolem axiom inside $N$ supplies a strong
$\kappa$-submodel $A\le_\K N$ containing $a$. Independence of the
choice: given two such $A_0,A_1\le_\K N$, LS inside $N$ once more
gives $B\le_\K N$ of size $\kappa$ containing $A_0\cup A_1$; coherence
gives $A_0,A_1\le_\K B$, both of size $\kappa$, so they are isomorphic
categoricity models. The inclusion of $A_0$ into $B$ then $A_1$ is a
strong map witnessing $\equiv^\sigma_\kappa$ between the two
candidates.

Preservation: given a strong $f\colon N\to N'$ of models of size
$\ge\kappa$, the LS axiom gives strong $\kappa$-submodel inclusions
$A\le_\K N$, $A'\le_\K N'$ with $f[A]\subseteq A'$; coherence gives
$f|_{A}\colon A\to A'$ strong, which is exactly a witness for
preservation.
\end{proof}

\subsection{Bounded diagram homogeneity}

For a well-ordered presentation $I$ of a model, and a tuple $d$ in an
extension, we want to test the joint type of $d$ with bounded tuples
from $I$. The next lemma is the key engine: bounded tests suffice.

\begin{definition}[Bounded diagram]\label{def:bounded-diagram}
Let $A\le_\K B$, let $I$ well-order a presentation $E(I)$ of $A$, and
let $d$ be a tuple in $B$ of length $\le\sigma$. For a subset
$X\subseteq|A|$, write $D(d,X;B)$ for the complete diagram of $d$
with parameters from $X$ computed inside $B$: the assignment, to each
atypical joint list of formulas over $X$ with $d$, of its truth value.
\end{definition}

\begin{theorem}[Stabilization]\label{thm:stabilization}
For every infinite cardinal $\sigma$ there is a cardinal
$\beta_\K(\sigma)$ such that, at every categoricity cardinal
$\kappa\ge\beta_\K(\sigma)$ and every $A\le_\K B$ at categoricity
size, the following hold. Let $d,e$ be tuples of length $\le\sigma$
in $B$. Suppose that $D(d,X;B)=D(e,X;B)$ for every bounded
$X\subseteq A$ (that is, $|X|<\kappa$). Then there is an automorphism
of $B$ over $A$ taking $d$ to $e$.
\end{theorem}

\begin{proof}[Sketch of proof]
Encode $d,e$ and their bounded diagrams symbolically in an
increasing approximation to $B$. The matching is a back-and-forth at
size $\kappa$; by reversal (Theorem~\ref{thm:reversal}) the ``orbit
matching'' relation stays symmetrical at every bounded stage. Each
stage requires only the stabilisation of the $\sigma$-tuple canonical
classes (Lemma~\ref{lem:canonical-classes}) plus a bounded-in-$\sigma$
count of possible joint patterns. Since reversal gives the symmetry
that makes ``arrow-matchable records'' into an equivalence for
tuples over $B$ (not just over categoricity copies), the sequence
of back-and-forth approximations closes at some stage. The threshold
$\beta_\K(\sigma)$ is chosen so that $\kappa$ exceeds all the orbit
counts, which depend only on $\ell$ and $\sigma$.
\end{proof}

The point: for bounded diagram comparison, we may work entirely with
bounded tests. This is what allows the working scheme below to define
its diagram clause over well-ordered presentations, without needing to
quantify over the full model diagram.

\begin{corollary}[Uniqueness of lifts]\label{cor:lift-unique}
Let $\mu>\beta_\K(\sigma)$ be a categoricity cardinal, $A\le_\K B$ of
size $\mu$, and $d$ a bounded tuple in $B$. The family
$(D(d,X;B))_{X\subseteq A,|X|<\mu}$ determines the full comparison
$D(d,A;B)$ and is determined by it. Moreover, any family of partial
diagrams agreeing on the intersections of its bounded tests lifts to
a unique full comparison.
\end{corollary}

\begin{proof}
The first sentence is a rephrasing of Theorem~\ref{thm:stabilization};
to be sure that $D$ detects the full comparison, restrict to a
$\sigma$-sized subtuple of $d$, and note that the join over all bounded
$X$ recovers the atomic diagram with each element. Uniqueness for the
second sentence is a Zorn amalgamation of the partial placements, using
bounded compactness: a family of bounded tests is compatible iff every
subfamily is realized, and Zorn provides a maximal amalgam. Maximality
is impossible to fail: if the maximal partial placement misses some
element of $A$, then $X$ plus that element is still bounded, and the
corresponding test extends it.
\end{proof}

\subsection{Bounded placement and compactness}

The following consequence is used repeatedly in the calculus and the
isolation arguments.

\begin{theorem}[Compactness for bounded placements]
\label{thm:compact-placement}
Let $\mu>\ell$ be an infinite cardinal and let $\chi<\mu$ satisfy
$\chi^\sigma=\chi$ for all $\sigma<\mu$ in a fixed set of arities.
Suppose $A\le_\K B$ is a strong inclusion of categoricity models of
size $\mu$ and $d$ is a bounded tuple in $B$. For every
$\chi$-bounded subfamily of the bounded tests over $A$ that is
jointly realized in some extension of $A$, there is a $\mu$-sized
extension $A\le_\K B'$ of $A$ and a tuple $d'$ in $B'$ realizing all
of them simultaneously.
\end{theorem}

\begin{proof}[Sketch of proof]
Work in a well-ordered presentation of $A$. Each test constrains
$d$ at finitely many positions and formulas; only finitely many
elements of $A$ are named in each test. The union of the named
parameters over the $\chi$-bounded subfamily has size $\le\chi$. Realize
the joint diagram of $d$ over that union in a $\chi^+$-sized strong
extension of the induced subpresentation (using LS and saturation of the
categoricity model). Then take an LS-enlargement to size $\mu$: the
bounded extension is realized at size $\chi^+$, and pulling back
through the LS embedding into a $\mu$-submodel of the categoricity
model gives the required placement.
\end{proof}

\subsection{Further consequences}

The orbit bound of Lemma~\ref{lem:orbit-bound} also bounds orbits
over bounded parameters; we will need this in Section~\ref{sec:marked}
when comparing marked pairs.

\begin{lemma}[Bounded parameter orbits]
\label{lem:parameter-orbits}
Fix an infinite cardinal $\sigma$ and a categoricity cardinal
$\kappa>\ell+\sigma$ at which stabilization holds. Let $A\le_\K B$
have size $\kappa$, and let $C$ be a bounded subset of $A$ of size
$\le\sigma$. The number of orbits of $\sigma$-tuples of $B$ over $C$
(under automorphisms of $B$ fixing $C$ pointwise) is at most the
fixed bound $B(\ell,\sigma)^+$.
\end{lemma}

\begin{proof}[Sketch of proof]
Each orbit over $C$ is contained in an orbit over $\varnothing$: the
set of all $\Aut(B)$-orbits on $\sigma$-tuples partitions the tuples,
and fixing $C$ further refines this partition. By
Lemma~\ref{lem:orbit-bound} there are at most $B(\ell,\sigma)$
$\Aut$-orbits, and each splits into at most $2^{|C|+\sigma}$ orbits
over $C$ (pick witnesses for each formula with parameters from $C$
and count them). Combined bound is $B(\ell,\sigma)^+$.
\end{proof}

\begin{theorem}[Amalgamation over a bounded tuple]
\label{thm:bounded-amalgamation}
Fix a categoricity cardinal $\kappa$ above the stabilization threshold.
Let $M$ be a model of $\K$ of size $\kappa$, $d$ a bounded tuple in
$M$, and $M\le_\K N$ an extension of size $\kappa$. There are a model
$M'$ of size $\kappa$ with $M\le_\K M'$, an isomorphism
$\alpha\colon N\cong_\K M'$ over $M$ (that is, $\alpha$ restricts to
the identity on all of $M$), and a bounded tuple $d'$ in $M'$ extending
$d$ such that the joint diagram of $d,d'$ in $M'$ agrees with the joint
diagram of $d,\alpha^{-1}(d')$ in $N$. In other words, any bounded
configuration of $d$ in an extension of $M$ can be realized inside
a size-$\kappa$ extension of $M$, with $d$ fixed.
\end{theorem}

\begin{proof}
The map $\alpha$ is a strong inclusion $M\le_\K M'$ traced back from
$N$: take $\alpha = \id_M\colon M\to N$ with codomain the obvious copy
of $N$ inside an isomorphic envelope. Then bounded tuples are just
bounded tuples; the diagram condition is a tautology.
\end{proof}

\begin{remark}
Theorem~\ref{thm:bounded-amalgamation} is elementary in form, but its
scope matters: it says that in any extension of $M$ at all, a bounded
tuple's diagram is fully captured by a size-$\kappa$ enlargement. Every
subsequent model we build can therefore be of size at most $\kappa$
above the working base, and no extra cardinals are introduced.
\end{remark}


\section{Working schemes}\label{sec:schemes}

Sections~\ref{sec:calculus}--\ref{sec:boundaries} prove a series of
theorems in a general framework: ``if a category satisfies the working
package described here, then its version of a free extension, an
isolation, a marked pair, and a boundary lift all exist.'' The single
model scheme, the marked schemes obtained from it, and the geometric
systems of the second half are all recorded as instances, and the
instances inherit the machinery. The point of isolating the framework
is that we do not re-prove the same back-and-forth ten times.

\subsection{Levels and closure}\label{sub:levels}

\begin{convention}[Levels]\label{conv:level}
An \emph{eligible level} is an infinite cardinal that belongs to some
fixed class on which a particular construction has been established.
Unless we say otherwise, an eligible level is a strong limit cardinal
of countable cofinality. A set is \emph{bounded at $\mu$} if its
cardinality is strictly less than $\mu$. If $u$ is a cardinal-valued
function, \emph{strict closure of $\mu$ under $u$} means
$u(\theta)<\mu$ for every cardinal $\theta<\mu$. Bounds may include
fixed parameters, may be increased to infinite cardinals, and may be
replaced by monotone majorants.
\end{convention}

\begin{convention}[Eligible-subclass hypothesis]\label{conv:eligible-subclass}
Let $S$ be an unbounded class of eligible levels. When we assert that
an unbounded class of refinements of $S$ remains eligible, we assume in
addition that $S$ contains a fixed definable unbounded subclass $T$
closed under suprema of strictly increasing countable sequences. This
is a hypothesis on the \emph{supply of levels}, not a consequence of
unboundedness alone. The reason: a theorem that proves its conclusion
at every level strongly closed under bounds does not by itself prove
that every unbounded class of levels has an unbounded subclass closed
under those bounds, since membership in the class is exactly what we
are establishing. The subclass $T$ supplies this membership once and
for all, and the individual closure operations in this section refine
$T$ into smaller classes that are still unbounded in $T$.
\end{convention}

\subsection{Systems and arrows}\label{sub:systems}

\begin{definition}[System]\label{def:system}
Let $I$ be a finite set of \emph{axes}. A \emph{system} on $I$ has one
vertex for each subset $s\subseteq I$, and each vertex is a $\K$-model
$X_s$ that is infinite if $s\ne\varnothing$. For every inclusion
$s\subseteq t$ of subsets, there is a specified $\K$-strong map
$\iota_{s,t}\colon X_s\to X_t$, subject to $\iota_{s,s}=\id$ and
$\iota_{s,u}=\iota_{t,u}\circ\iota_{s,t}$ whenever $s\subseteq t\subseteq u$.

A system is \emph{typed} if on each vertex a finite number of subsets
of its universe, called \emph{distinguished data}, is singled out, one
set per entry of a fixed finite data scheme. All distinguished data are
preserved by every strong map in the system.
\end{definition}

We treat a system as a many-sorted structure with the vertex universes
as sorts and the maps $\iota_{s,t}$ as function symbols. A
\emph{system embedding} is a commuting family of $\K$-strong maps that
also preserves every distinguished datum. It is an \emph{arrow} if it
satisfies any additional condition stated for the specific application.
At the moment there is none; later one more condition (relative
independence) will be required for the geometric application.

An \emph{isomorphism} is an arrow whose underlying vertex maps are
bijections onto the whole target vertices. We denote by $\|\mathfrak X\|$
the maximum (equivalently, in contexts where they are all equal, the
common) cardinality of the vertex models of $\mathfrak X$.

\begin{remark}
We do not require anything about intersections $\iota_{s,t}[X_s]\cap
\iota_{s,u}[X_u]$ of images within a vertex: the definition of a system
and of an arrow leaves it unconstrained. When we later prove a criterion
for a componentwise map to be an arrow, the criterion does not need
to know about such intersections either.
\end{remark}

\subsection{The working package}\label{sub:package}

Let $\mathcal C$ be a category whose objects are systems at some
eligible level, and whose arrows are system embeddings of the previous
paragraph satisfying possibly some extra condition. Fix also a class
$\mathcal B$ of \emph{bounded term lists} in $\mathcal C$: each is a
joint list of elements from the vertex universes, tagged by occurrence
sort, together with a set of distinguished positions; ``bounded''
means of cardinality strictly less than the level.

For a system $\mathfrak X\in\mathcal C$ at level $\mu$, a bounded term
list $u$ in $\mathfrak X$, and a system embedding
$\mathfrak X\to\mathfrak Y$, write $D_{\mathcal C}(u;\mathfrak Y)$ for
the \emph{joint diagram} of $u$ in $\mathfrak Y$: the assignment
to every atomic formula with parameters from $u$ (in the many-sorted
language of $\mathcal C$), together with the equality pattern of
distinguished data attached to $u$, of its truth value in
$\mathfrak Y$. Two bounded lists are \emph{$D_{\mathcal C}$-equal}
if their diagrams agree.

\begin{definition}[Working package]\label{def:working-package}
A category $\mathcal C$ with a class $\mathcal B$ of bounded term lists
satisfies the \emph{working package} at a class $S$ of eligible levels
provided all of the following hold.
\begin{enumerate}
\item \emph{Structural condition.} Objects and arrows are as in
Definition~\ref{def:system}; the arrows preserve distinguished data,
and every arrow's vertex maps are $\K$-strong.
\item \emph{Presentations.}
\begin{enumerate}
  \item[(2a)] There is a fixed scheme of finite-support terms and a
  template $F$ on linear orders, and for every well-order $I$ of
  eligible cardinality $\mu\in S$, $F(I)$ is an object of
  $\mathcal C$ at level $\mu$.
  \item[(2b)] For any order embedding $f\colon I\to J$, substitution of
  positions along $f$ induces an arrow $F(f)\colon F(I)\to F(J)$,
  including between different eligible levels; $F(\id)=\id$ and
  $F(g\circ f)=F(g)\circ F(f)$.
  \item[(2c)] For every object $\mathfrak X\in\mathcal C$ at level
  $\mu\in S$, some well-order $I$ of cardinality $\mu$ has
  $\mathfrak X\cong F(I)$.
  \item[(2d)] \emph{Mixed downward closure.} For eligible $\nu\le\mu$
  in $S$ and a set $A$ of at most $\nu$ vertex occurrences of an
  object $\mathfrak X$ at level $\mu$, there is an arrow
  $F(J)\to\mathfrak X$ from a level-$\nu$ presentation $F(J)$
  containing $A$ in its image. Distinguished data are included as
  part of the request.
\end{enumerate}
\item \emph{Diagram condition.} Bounded lists have joint diagrams as
above; for any order embedding inducing an arrow between presentations,
the diagrams of corresponding terms agree up to that arrow. There is
a cardinal function $b_F$ (depending only on $F$ and on the bounded
input arity) such that two bounded lists in a presentation at level
$\mu\in S$, both of size $\le\sigma$ with $\sigma<\mu$, are
$D_{\mathcal C}$-equal iff they are $D_{\mathcal C}$-equal at all
test arities $\le b_F(\sigma)$. This gives a fixed, level-independent
definition of $D_{\mathcal C}$ at bounded input sizes.
\item \emph{Exhaustion criterion.} Suppose $f\colon \mathfrak X\to
\mathfrak Y$ is a commuting family of $\K$-strong vertex maps. Enumerate
in each vertex of $\mathfrak X$ a nested family of small strong
submodels with union the whole vertex. If the images of these
submodels under $f$ are strong in the target vertices and $f$ agrees
with a $D_{\mathcal C}$-equality on every bounded term list in the
enumerations, then $f$ is an arrow of $\mathcal C$.
\item \emph{Isomorphism at a level.} Any two objects of $\mathcal C$ at
the same eligible level $\mu\in S$ are isomorphic. (Equivalently, the
empty bounded list has one diagram in the whole category at $\mu$, and
the $D_{\mathcal C}$-equality of the empty list forces an isomorphism.)
\end{enumerate}
\end{definition}

The clauses (2a)--(2d) can be read as: well-ordered presentations exist
and are unique at level; they are functorial under order maps; every
object is such a presentation; and top-down requests reduce to
bottom-up at smaller levels. Clause (3) is the ``diagrams at one level
are determined by their bounded instances'' statement, made concrete
via the fixed test-arity function $b_F$. Clause (4) is the standard way
a bound-in-one-shape construction climbs to an arrow at larger
shapes: the two conditions on strong submodels catch every strength
condition vertexwise, and the diagram-equality condition catches the
algebraic compatibility between vertices.

\subsection{Mixing levels}

The mixed-arrow part of Definition~\ref{def:working-package} deserves
its own statement: we frequently compare a small object at level $\nu$
with a large one at level $\mu>\nu$, and want to argue componentwise
strongness at the small level only.

\begin{lemma}\label{lem:mixed-levels}
Let $\mathcal C$ be a working scheme at a class $S$ of levels. Suppose
$\nu\le\mu$ are in $S$, $F(J_0)\to F(J_1)$ is an arrow at these two
levels, and $u$ and $v$ are bounded term lists in $F(J_0)$ of the
same sizes. Then $D_{\mathcal C}(u;F(J_1))=D_{\mathcal C}(v;F(J_1))$
iff $D_{\mathcal C}(u;F(J_0))=D_{\mathcal C}(v;F(J_0))$ for all
arities below $\nu$, provided the arities in question are below the
test bound for $\nu$.
\end{lemma}

\begin{proof}[Sketch of proof]
One direction is preservation of diagrams under an arrow (clause (3)).
For the converse, use mixed downward closure (2d) to factor
$\nu\to\mu$ through a level-$\nu$ presentation of the smaller base,
then apply preservation and reflections at that smaller level.
\end{proof}

\subsection{Refining the eligible levels}\label{sub:refining}

The subsequent constructions each refine the eligible class by adding
more closure requirements. Since they are all fixed operations on
cardinal functions, and the base class contains an unbounded definable
subclass closed under suprema of strictly increasing countable
sequences, the refinement stays unbounded.

More precisely:

\begin{lemma}[Closure points exist]\label{lem:closure-points}
Let $(u_i : i\in A)$ be a fixed, set-indexed family of cardinal-valued
functions. Above any prescribed cardinal there is a cardinal
$\mu$ of countable cofinality that is a strong limit and satisfies
$u_i(\theta)<\mu$ for all $\theta<\mu$ and all $i\in A$.
\end{lemma}

\begin{proof}
Define an increasing sequence of cardinals
$\kappa_0<\kappa_1<\cdots$ by
\[
 \kappa_{n+1}
 \;=\;
 \max\bigl(2^{\kappa_n},\ \sup\{u_i(\theta):i\in A,\ \theta\le\kappa_n\}\bigr)^+.
\]
Replacement bounds the supremum at each step. Set
$\mu=\sup_{n<\omega}\kappa_n$. Then $\cf(\mu)=\aleph_0$ and $\mu$ is
a strong limit; given $\theta<\mu$, pick $n$ with $\theta\le\kappa_n$;
then $u_i(\theta)\le\sup\{u_i(\theta'):\theta'\le\kappa_n\}
 \le\kappa_{n+1}<\mu$.
\end{proof}

\begin{lemma}[Closure refines supply]\label{lem:refine-supply}
Under the eligible-subclass hypothesis, any finite or set-sized list
of closure conditions on levels leaves an unbounded class of levels
satisfying all of them and still containing an unbounded definable
subclass closed under suprema of strictly increasing countable
sequences.
\end{lemma}

\begin{proof}
The intersection of the base class $T$ with the class of points
produced by Lemma~\ref{lem:closure-points} is unbounded in $T$, as the
sequence $\kappa_n$ may be chosen inside $T$ (by induction on $n$,
using that $T$ is unbounded and closed under suprema of strictly
increasing countable sequences). The resulting $\mu$ is the supremum
of a strictly increasing countable sequence in $T$. Finite and
set-sized intersections preserve closedness under countable suprema.
\end{proof}

\subsection{The single-model scheme is a working scheme}

Let $\K$ be our fixed AEC of Section~\ref{sec:reduction}, categorical in
unboundedly many cardinals. The \emph{single-model scheme} has
$I=\varnothing$ (so there is one vertex, the whole model) and no
distinguished data; arrows are just $\K$-strong maps. Its template is
the $E$ of Theorem~\ref{thm:order-template}; we may take it as the
template $F$ of the working package.

\begin{proposition}\label{prop:base-scheme}
Let $S_0$ be the class of categoricity cardinals of $\K$ at which the
reversal theorem (Theorem~\ref{thm:reversal}) holds for every bounded
input size and where the refinement of Lemma~\ref{lem:refine-supply}
can be applied with all the cardinal functions that occur in the
statements of Theorems~\ref{thm:stabilization} and
\ref{thm:compact-placement}. Then $S_0$ is unbounded, and the
single-model scheme is a working scheme at $S_0$.
\end{proposition}

\begin{proof}
Unboundedness of $S_0$: reversal itself is eventually true (Theorem
\ref{thm:reversal}), and $S_0$ is a union of intervals of categoricity
cardinals above each of the countably many thresholds that appear in
the finitely many lemma statements. Each threshold is fixed once and
for all; the class of cardinals above a fixed threshold that are also
categoricity cardinals and satisfy the countable closure of
Lemma~\ref{lem:refine-supply} is unbounded because categoricity is
assumed at unboundedly many cardinals and the closure operation
produces new categoricity cardinals by replacing any cardinal in
$S_0$ with a limit of categoricity cardinals above it.

The working-package clauses.
(1) The structural condition holds by construction (one vertex, no
distinguished data).

(2a)--(2c) are exactly Theorem~\ref{thm:order-template}: the functor
$E$ has well-ordered presentations at every level, is functorial, and
every $\K$-model at a categoricity cardinal is isomorphic to some
$E(I)$.

(2d) mixed downward closure: given a model $\mathfrak X$ at level
$\mu$ and a subset $A$ of size $\le\nu$, LS inside $\mathfrak X$
produces a strong submodel $A_0\le_\K\mathfrak X$ containing $A$,
and we present $A_0$ as $E(J)$ for a well-ordered $J$ of size $\nu$
using Theorem~\ref{thm:order-template} and coherence.

(3) the diagram condition is provided by Theorem~\ref{thm:stabilization}
and Corollary~\ref{cor:lift-unique}: for $\sigma$-sized bounded lists,
two are $D_{\K}$-equal iff they agree on all $\sigma$-bounded tests,
with the bound $\beta_\K(\sigma)$ supplied by those results. As
$b_F(\sigma)$ we take the maximum of $\sigma$ and the test costs.

(4) the exhaustion criterion: a componentwise map between
single-model vertices is just a strong map on the whole model. Suppose
$f\colon M\to N$ agrees with the bounded diagram data on every bounded
list of $M$. To show $f[M]\le_\K N$, use the LS axiom inside $N$ to
enlarge $f[M]$ to a strong $\mu$-submodel $N_0\le_\K N$, then note
coherence gives $f[M]\le_\K N_0\le_\K N$ because $f[M]$ is
unchanged under $N_0\le_\K N$ (the inclusion is strong). The
small strong submodel enumeration condition on $f[M]$ uses the LS
axiom on $M$ itself: any bounded subset of $f[M]$ is the image of
some bounded subset of $M$, which lies in a small strong submodel
of $M$ whose image under $f$ is itself small and strong in $N$ by
the diagram condition. The identity inclusion $N_0\le_\K N$ then
makes $f[M]\le_\K N$.

(5) the isomorphism clause is categoricity: exactly one model per
categoricity cardinal, so any two objects of the single-model scheme
at the same level are isomorphic.
\end{proof}

\begin{remark}\label{rem:base-scheme-consequence}
Proposition~\ref{prop:base-scheme} is the ``use the working package''
statement for our starting AEC. Everything in Sections~\ref{sec:calculus}
through~\ref{sec:boundaries} applies to $\K$ itself: free extensions
of types, stationary approximations, isolation, all-dominated
extensions, and each new working scheme constructed by adjoining a
dimension.
\end{remark}


\section{The calculus of free extensions}\label{sec:calculus}

Throughout this section, $\mathcal C$ is a working scheme in the sense
of Definition~\ref{def:working-package}, with a fixed template $F$, its
class $S$ of eligible levels containing a definable unbounded subclass
$T$ closed under suprema of strictly increasing countable sequences, and
all further closure refits stated when used. Bounds always depend only
on fixed scheme data and on bounded input arities.

\subsection{Approximation sequences}

The first main result of this section is that types over whole models
have free extensions that are compatible with strong maps, and that they
are computed by averaging over a long sequence in the base.

\begin{definition}[Approximation sequence]\label{def:approx-seq}
An \emph{approximation sequence} for $p=\tp(v/A)$ at query size $\tau$
is an indexed family $I=(v_i : i<\kappa)$ in $A$, each $v_i$ having the
same index set as $v$, such that the concatenation of the family is
bounded and, for every $Z\subseteq A$ of size at most $\tau$,
\[
 \bigl|\{i<\kappa:D(v_i,Z)\ne p\mathord{\upharpoonright} Z\}\bigr|
 \le |Z|+\aleph_0.
\tag{$*$}
\]
Here $p\mathord{\upharpoonright} Z$ denotes its joint diagram. A
sequence is always indexed: different indices may carry the same tuple.
We use the same terminology for all projections of the displayed tuple.
Whenever $\kappa>|Z|+\aleph_0$, the unique value assumed outside at
most $|Z|+\aleph_0$ indices is the \emph{majority value} of the sequence
on $Z$.
\end{definition}

\begin{lemma}[Uniform approximations]\label{lem:approximations}
Let $|v|\le\sigma$ and $\tau\ge\aleph_0$ be bounded. At sufficiently
closed levels there are approximation sequences for $p=\tp(v/A)$ at
size $\tau$ of every prescribed bounded infinite length $\kappa$. They
satisfy $(*)$ simultaneously for all subtuples of $v$. The construction
has bounds depending only on $\sigma,\tau,\kappa$ and the fixed scheme.

In particular, taking $\tau=c(\sigma)$ and $\kappa=c(\sigma)^+$, the
concatenated sequence has a uniform bounded length depending only on
$\sigma$ and the fixed scheme. Its diagram is a code for $p$ in the
precise transport sense proved in Theorem~\ref{thm:free-extension} below.
\end{lemma}

\begin{proof}[Sketch of proof]
Present $A$ on a padded dense order rich enough for every support size
used below (obtainable by enriching the order-template construction of
Theorem~\ref{thm:order-template} with finitely many extra labels; the
extra labels are fixed once and for all). The presentation is an object
of the current scheme, and no additional categoricity is needed here.
The bounded-placement result (Theorem~\ref{thm:compact-placement})
places $p$ correctly at size $\tau$.

Keep every extra supporting position that belongs to the old chart.
Partition the other supporting positions into clusters according to
their strict cut over the entire old order. For every pair of distinct
cuts choose an old position separating them. Include the shared
supporting positions as well. This gives a bounded anchor set of size
at most $\sigma+\aleph_0$. Each unshared cluster belongs to a
different strict slot over the anchors.

In each such anchor slot, choose $\kappa$ pairwise disjoint convex
regions in the old order; in the $i$th region, put a copy of the
corresponding cluster with its internal order. The prescribed richness
supplies these patterns; its required arity is bounded in terms of
$\sigma+\kappa$. Use the original labels and the unchanged shared
positions to obtain $v_i\in A$.

Choose a query $Z$ with one finite support for each element. If these
supports avoid every region used for the $i$th copies, then each copied
cluster and the original cluster can differ relative to the query only
by passing whole blocks of parameter positions. There are no hits or
separations inside a cluster. Their anchor slots are disjoint, so
Lemma~\ref{lem:parameter-orbits} (of Section~\ref{sec:diagrams}) gives
$D(v_i,Z)=p\mathord{\upharpoonright} Z$. Every supporting position of
$Z$ belongs to at most one of the regions, and therefore excludes at
most one index $i$. Finitarity of supports gives at most
$|Z|+\aleph_0$ excluded indices. The same set of good indices works for
every subtuple of $v$. Only bounded support patterns, the fixed labels,
rich orders at bounded arities, and the compact-placement bounds were
used. This proves the uniformity assertions.
\end{proof}

\subsection{Free extension}\label{sub:free-extension}

\begin{theorem}[Stationary free extension]\label{thm:free-extension}
Let $A\to B$ be an arrow at a sufficiently closed level, and let
$p=\tp(v/A)$ where $|v|\le\sigma$. There is a specified actual type
$p^B$ over $B$, called its \emph{free lift}, extending $p$. At every
query size whose approximation and testing costs are bounded at the
originating level, it is computed by transporting sufficiently long
approximations in $A$. At one level this includes every bounded query
size; in a mixed-level use the costs must remain below the level of
$A$. It has the following properties.
\begin{enumerate}
\item The answer is independent of the approximation sequence, its
length, and the auxiliary test size.
\item Free lifts commute with restriction of the tuple, are invariant
under isomorphisms, and satisfy $(p^B)^C=p^C$ whenever
$A\to B\to C$.
\item If $A$ has an eligible size $\nu$ and $B$ has a larger eligible
size, the construction still works for $|v|<\nu$, with its construction
thresholds and approximation lists below $\nu$.
\item A sequence from Lemma~\ref{lem:approximations} at the fixed
threshold $c(\sigma)$ is bounded code data. If an equally indexed
sequence in any sufficiently closed eligible object has the same
diagram, it determines a unique corresponding type there by the same
rule.
\end{enumerate}
\end{theorem}

\begin{proof}[Sketch of proof]
Well-definedness. Fix $\tau=c(\sigma)$ large enough that the possibility
set tested below is a set of size $\le 2^\tau$. Let
$I=(v_i:i<\kappa)$ be an approximation sequence at $\tau$, with
$\kappa>\tau$. For each bounded query $Z\subseteq B$, we know the
pattern of $D(v_i,Z)$ as $i$ varies; the majority value is well defined
by $(*)$ and is by construction the intended answer $p^B\mathord{\upharpoonright} Z$.
Formally, move $Z$ into $A$ over the approximation sequence: by bounded
diagram homogeneity, there are cardinality- and order-preserving moves
of each $Z$-element's support into a support of the sequence, and the
diagram at the moved query $Z'$ is the diagram at $Z$. Then
$D(v_i,Z)$ agrees with $D(v_i,Z')$ at all but finitely many $i$, hence
has a majority, which by $(*)$ equals $p\mathord{\upharpoonright} Z' = p\mathord{\upharpoonright} Z$.

For independence of the sequence, take a second $I'$ of the same length
and set $\kappa>\tau$; move $Z$ into $A$ over $I\cup I'$; on that
moved query both majorities compute $p$ and hence agree. This proof
requires saturation over the concatenation of the sequences; it does
not require the approximation estimate to hold for a query containing
that concatenation. The averaging queries still have size at most
$\tau$. The same argument compares different query bounds on their
common domain. It also proves coherence under restrictions and
reindexing of queries.

Existence of an actual type. Use $\tau=c(\sigma)$ and $\kappa=\tau^+$.
In a well-ordered chart of $B$, prescribe the majority answers on
every query of size at most $\tau$. For each single query these are
realized by some $v_i\in A\subseteq B$, since fewer than $\kappa$
indices are exceptional. Thus they have local placements.
Lemma~\ref{lem:compact-placement} (of Section~\ref{sec:diagrams})
gives a placement realizing all of them in an order enlargement of $B$.
This is an actual tuple in an extension object, and the bounded-test
uniqueness of Corollary~\ref{cor:lift-unique} makes its type unique
once the test size exceeds the stabilisation threshold. This type is
$p^B$. Its restriction to $A$ equals $p$ by the same testing criterion.

Properties (1)--(4) are now routine from the construction:
independence of the sequence is already shown; restriction and
isomorphism invariance follow by taking sub-sequences and pushing
through the isomorphism; the mixed-level part uses the same rule with
the relevant bounds taken below $\nu$; the code-data property is a
formal consequence of Theorem~\ref{thm:stabilization}.
\end{proof}

\subsection{Products and independence}\label{sub:products}

\begin{definition}[Free product]\label{def:product}
Let $A\to B$ be an arrow at a fixed eligible level. Let $p$ and $q$ be
types over $A$ in disjoint tuples, with free lifts $p^B$ and $q^B$. We
say that a tuple $(x,y)$ realizes the \emph{free product} $p\otimes q$
over $A$ if $x$ is a realization of $p$ with $\tp(y/A,x)=q^{A[x]}$, where
$A[x]$ is a copy of $A$ extended by $x$ (using the ambient level).
\end{definition}

\begin{proposition}[Products are symmetric, transitive, associative]\label{prop:products}
In a working scheme, at sufficiently closed levels, the free product
construction has the following properties.
\begin{enumerate}
\item \emph{Base change.} If $x/B$ is free from $A$ and $x,d$ have
product type over $B$, then $x$ and $(d,e)$ have product type over $A$
for every bounded tuple $e$ from $B$.
\item \emph{Symmetry.} For bounded tuples $x,y$ of size $\le\sigma$
with free lifts over $A$, $p\otimes q = q\otimes p$ as actual types
over $A$.
\item \emph{Transitivity.} If $p,q,r$ are bounded types over $A$ at
one level, then $(p\otimes q)\otimes r=p\otimes(q\otimes r)$ and
$p\otimes q\subseteq(p\otimes q)\otimes r$ with $r$-marginal = $r$
over the initial base.
\item \emph{Associativity.} Combined with (3), products of finitely
many factors are well defined up to commuting.
\end{enumerate}
\end{proposition}

\begin{proof}
Base change: two realizations of $p$ can be identified over $A$ by
amalgamation. In a common model containing their witnessing extensions,
the free lifts of $q$ agree by stationarity and restriction. A second
type-identifying amalgamation identifies the realizations of $q$.
This proves independence of the choices.

Symmetry: fix a bounded query $Z$ in $A$, and put
$e=|Z|+|x|+|y|+\aleph_0$. Choose approximation sequences
$(a_i : i<\kappa)$ for $p$ and $(b_j : j<\lambda)$ for $q$ sufficient
for queries of size $e$, where $\kappa=e^+$ and $\lambda=\kappa^+$.
All these cardinals lie below a sufficiently closed level.

For the array $M_{ij}=D(a_i,b_j,Z)$, first realize $x$ and freely
realize $y$: the resulting answer $R$ is the iterated majority in $i$
commuting with the majority in $j$. Except at at most $e$ columns,
the column majority is $R$, and in each such column at most $e$
entries differ from $R$. Reversing the realization order gives an
answer $S$: except at at most $e$ rows, its row majority is $S$, with
at most $e$ exceptions in each such row. The bounds concern the size
of $(x,Z)$ or $(y,Z)$, not the lengths of the sequences.

There are $\kappa$ good rows. Their exceptional columns together number
at most $\kappa e=\kappa<\lambda$, choose a column outside this set and
outside the at most $e$ bad columns. Every good-row entry in that
column equals $S$, whereas all but at most $e$ entries equal $R$. As
$\kappa>e$, some entry has both values. Thus $R=S$. Testing then gives
symmetry of the joint types.

For transitivity, take the two sequences just used in $A$ and a
sequence $K\subseteq A$ approximating the actual old product. Choose
their accuracy at common sufficient threshold. Given a query $Z$ in
the enlarged base $B$, move it into $A$ over these three whole
sequences. Both successive free evaluations over $B$ are the iterated
majority of the same array $D(a_i,b_j,Z)$. Transitivity permits the
original sequence for the second factor to be used after the first
has been realized. The query movement identifies this array with the
old array in $A$, where it computes $p\otimes q$. The sequence $K$
evaluates that old product and computes its free lift on the original
query. The answers therefore agree. Testing proves the formula.

Associativity: realize $x,y,z$ successively along a chain of free
lifts from $A$. The first two form $p\otimes q$, and $z$ is free over a
model containing them, so the joint type is $(p\otimes q)\otimes r$.
Over a model containing $x$, the last two have type
$q^B\otimes r^B=(q\otimes r)^B$ by symmetry-transitivity over $B$,
so the same joint type is $p\otimes(q\otimes r)$. This proves
associativity. Projection follows from the projection property of
free lifts in successive realizations. Associativity and binary
symmetry permit every permutation of a finite list of factors.

Base change (second assertion of (1)): use symmetry and a
type-identifying amalgam to realize the given joint type by first
putting $d$ in a model containing $B$ and then realizing $x$ freely
over it from $B$. Since $x/B$ is free from $A$, transitivity makes
this last realization free from $A$. The tuple $(d,e)$ is in the
intervening model. The amalgam identifies the full original tuple
over $B$, and hence retains its actual joint type over $A$.
\end{proof}

\subsection{Local character}\label{sub:local-character}

\begin{proposition}[Local character of freeness]\label{prop:local-character}
Let $(A_i : i<\delta)$ be an increasing chain of objects at one
eligible level $\mu$, whose union $A$ has size $\mu$, and let $\delta$
be a nonzero limit ordinal. If $p=\tp(v/A)$ and either $v$ is finite
or $|v|<\cf(\delta)$, then $p$ is free from some $A_i$. If, in
addition, every restriction $\tp(v/A_i)$ is free from a fixed base
$X\le_\K A_0$, then $p$ is free from $X$.
\end{proposition}

\begin{proof}
Pass to a cofinal chain indexed by the regular cardinal
$\gamma=\cf(\delta)$. Choose a sufficient testing size
$\chi\ge c(|v|+\aleph_0)$ below $\mu$. If $\gamma$ is larger than
the size of an approximation sequence for $p$ at that threshold, the
whole sequence lies in one stage. Its exception estimate is still
correct on all queries in $A$, so Lemma~\ref{lem:average-descent}
below, at the same level, applies.

In the other case $\gamma<\mu$. Choose a regular $\kappa<\mu$ above
$\gamma,\chi,|v|$, and take $\kappa$ approximations inside $A$. Every
whole approximation tuple belongs to some stage (finiteness, or the
hypothesis $|v|<\gamma$). If every stage contained fewer than $\kappa$
of the tuples, regularity of $\kappa$ and $\gamma<\kappa$ would make
their union contain fewer than $\kappa$ tuples. Thus one stage contains
$\kappa$ of them. Pass to those indices. The exception estimate
survives unchanged, and Lemma~\ref{lem:average-descent} again identifies
$p$ as the free lift from that stage.

For the final assertion, local character makes $p$ free from some
$A_i$. Its restriction there is free from $X$ by hypothesis.
Transitivity in Theorem~\ref{thm:free-extension} makes $p$ free
from $X$.
\end{proof}

\begin{lemma}[Average descent]\label{lem:average-descent}
Let $A\to B$ have eligible sizes $\nu\le\mu$, and let $q=\tp(d/B)$ be
actual, with $|d|=\sigma<\nu$. Choose $\chi\ge c(\sigma)$ below $\nu$.
Suppose that a bounded sequence $I=(d_i:i<\kappa)$ in $A$, with
$\chi+\aleph_0<\kappa<\nu$, has majority value $q\mathord{\upharpoonright} Z$
on every query $Z\subseteq B$ of size at most $\chi$, with at most
$|Z|+\aleph_0$ exceptions. Then $q$ is the free lift of its actual
$\nu$-restriction to $A$.
\end{lemma}

\begin{proof}[Sketch of proof]
Apply Theorem~\ref{thm:free-extension} at the smaller level $\nu$, then
push forward along $A\to B$; the majority condition is exactly the
hypothesis that checks the "code" clause of the free lift. Uniqueness
is by clause (4) of Theorem~\ref{thm:free-extension}.
\end{proof}


\subsection{Universal strips}\label{sub:universal-strip}

For the marked-increment construction we need to be able to enlarge a
base model so that every same-level extension of it embeds inside the
enlargement, with the enlargement differing from the base only in a
bounded way.

\begin{proposition}[Universality of a fresh strip]\label{prop:universal-strip}
Let $\mathcal C$ be a working scheme with template $F$. In addition to
$F$, use a presentation-template $G$ with the following properties: it
has a fixed set of finite-support labels; every $G(J)$ used below, for
an order of size $\mu$, is an object of $\mathcal C$ at level $\mu$;
order embeddings give arrows; the diagrams of its term lists are
natural, including in the order enlargements and padded orders used
below. Require $\mu$ to exceed the cardinality of the label set of $G$
and to be closed under the bounds below with that cardinal as input.
Put $A=G(J)$. Insert into $J$ a fresh convex strip $V$ of size $\mu$
with countably many disjoint convex sub-strips, each of size $\mu$, and
denote the resulting object $A^+=G(J+V)$. Then every same-level
extension of $A$ embeds into $A^+$ over $A$. In particular this applies
to $G=F$ and to well-ordered presentations.
\end{proposition}

\begin{proof}[Sketch of proof]
A same-level extension $A\le_\K B$ of $A$ is itself at level $\mu$, so
by the categorical clause of the working package it is isomorphic to
$G(J')$ for some order $J'$ of size $\mu$. Write $J'$ as
$J\sqcup K$ (a disjoint union of orders refining a common prefix,
which is possible by renaming); we identify $A\subseteq B$ with
$G(J)\subseteq G(J')$.

Realize a bounded type $p(v/A)$ in one fresh sub-strip $V_0$ of $A^+$.
Choose a testing threshold $\chi\ge c(|v|+\aleph_0)$ large enough for
$|v|$ and the labels of $G$. Take a sequence $I$ in $A$ approximating
$p$ at query size $\chi$. Represent its entries by $G$-terms, and
collect their old supports in $S_0\subseteq J$. Apply support closure
(Lemma~\ref{lem:support-closure}, below) with the side of $V_0$
recorded, to obtain a bounded $S\subseteq J$ with the property that
any query of at most $\chi$ old positions can be moved into $S$ over
any subset of $S$ of size at most $\chi$. Include the approximation
supports as the fixed set in that lemma.

Let $P_S$ be the set of all $G$-terms on $S$. It is bounded since $G$
has a bounded set of finite-support labels. The natural parameter
diagram of $P_S$ is the same in $A$ and in $G(S\cup V_0)$. The latter
is a level object because $|V_0|=\mu$. Saturation there realizes the
desired whole joint diagram of $(v,P_S)$, giving a tuple $w$ whose
supporting positions belong to $S\cup V_0$. Only at most
$|v|+\aleph_0\le\chi$ of its supporting positions are old; call them
$R\subseteq S$. Move every bounded old query into $S$ over $R$ and use
uniform testing at $\chi$. The diagram of $w$ over the moved query
equals the diagram of $v$ over the original query. We have therefore
realized $p$ inside $G(S\cup V_0)\subseteq A^+$, fixing $A$ pointwise.

Iterate over an enumeration of the bounded tuple types over $A$ (there
are at most $2^{|A|}$ of them; but for our purposes only the ones
realized in $B$ matter, of which there are at most $\mu$). Each is
realized in a distinct fresh sub-strip $V_n$; disjointness of the
sub-strips makes the realizations independent over $A$. After
$\mu$ steps, the resulting object contains a copy of $B$ over $A$,
by induction on the well-ordered enumeration of bounded types realized
in $B$. Since the working package's categorical clause identifies all
level-$\mu$ objects, this is the desired embedding.
\end{proof}

\subsection{Approximate retractions}\label{sub:retractions}

\begin{corollary}[Approximate retractions]\label{cor:retractions}
Let $A\le_\K B$ have eligible cardinality $\mu$ of countable
cofinality. There is a family of arrows
$r_j\colon B\to A$ ($j<\mu$) such that, for every $a\in A$,
the set
\[
 \{j<\mu:\ r_j(a)\ne a\}
\]
is finite.
\end{corollary}

\begin{proof}[Sketch of proof]
Present $A=G(J)$ and, using Proposition~\ref{prop:universal-strip},
embed $B$ over $A$ into $A^+=G(J+V)$ where $V$ is a fresh strip of size
$\mu$. Enumerate a family of disjoint sub-strips of $V$ by ordinals
$j<\mu$. For each $j<\mu$ define $r_j\colon A^+\to A$ as follows: a
$G$-term whose $V$-support lies in the $j$-th sub-strip is mapped to
the corresponding $G$-term on a fixed fresh initial segment of $A$ that
encodes that sub-strip's position; a $G$-term with support in $J$ stays
fixed. This is a $G$-term substitution, hence a $\mathcal C$-arrow
(working-package clauses (2a)--(2b)). Pulling back along
$B\subseteq A^+$ gives the arrow $r_j\colon B\to A$.

Every $a\in A$ has a finite-support $G(J)$-representation with empty
$V$-part, so $r_j(a)=a$ for every $j$; the failure set
$\{j<\mu: r_j(a)\neq a\}$ is empty. This is the form in which the
corollary is used: for any bounded $Z\subseteq A$, all but
$|Z|+\aleph_0$ of the $r_j$ fix $Z$ pointwise.

The genuine content is in the images $r_j(b)$ for $b\in B\setminus A$:
if $b$ has $G$-term representation with finite $V$-support, then all the
$r_j(b)$ lie in a common bounded submodel of $A$ (essentially
$G$-terms on $J$ plus the $V$-support reindexed into the fixed initial
segment of $A$). The downward-transfer argument of
Section~\ref{sub:downward-transfer} averages over this bounded list.
\end{proof}

\subsection{Support closure}\label{sub:support-closure}

\begin{lemma}[Support closure]\label{lem:support-closure}
Let $\chi$ be a bounded infinite cardinal. Let $J$ be a rich dense
linear order (as supplied by the order template), $S_0\subseteq J$ a
bounded subset, and $T^*\subseteq J$ a further fixed set with
$|S_0|+|T^*|<\mu$. Let $V$ be a fresh convex strip of size $\mu$
disjoint from $J$. Then there is a bounded $S\subseteq J$ with
$S_0\subseteq S$ such that, for every subset $P\subseteq S$ of size at
most $\chi$ and every finite tuple in $J\cup V$, there is a tuple in
$S\cup V$ with the same order/equality diagram over $P$ that fixes
$T^*$ pointwise.
\end{lemma}

\begin{proof}[Sketch of proof]
Iterate the enrichment from Lemma~\ref{lem:ordinal-support-closure};
because $|S_0|+|T^*|<\mu$ and $\mu$ has countable cofinality with
sufficiently large closure, the resulting union is bounded in $J$ and
exhibits the required matching. Positions that lie in $V$ are kept
where they are (not moved into $S$), and the order/equality pattern is
preserved because $V$ is convex and disjoint from $J$.
\end{proof}

\section{Isolation and dominated extensions}\label{sec:isolation}

Throughout this section, $\mathcal C$ is again a working scheme in the
sense of Definition~\ref{def:working-package}, with the refinement
process of Section~\ref{sub:refining} applied. A tuple is
\emph{bounded} at a level $\mu$ if its cardinality is less than $\mu$.

Our goal is a strong statement about extending models: we want
extensions $A\le_\K B$ in which every bounded tuple of $B$ is
\emph{controlled} by the pair $(A,b)$, where $b$ is a fixed mark.
Controls means that the joint type of $(b,c)$ over a small fragment
of $A$ determines the joint type over all of $A$. Such extensions are
\textit{all-dominated}; they play the role of (mild) prime hulls.

\subsection{Free isolation}\label{sub:free-isolation}

\begin{lemma}[Free isolation]\label{lem:free-isolation}
Let $A\le_\K B$ be an arrow, $b$ a bounded tuple in $B$, and $q$ a
bounded type in the free lift from $B$ (so $q^B$ is a stationarily
determined type over $B$). If $q$ is isolated relative to $b$
over $A$, then $q^B$ is isolated relative to $b$ over $B$ with an
isolation radius controlled by $\ell$, $\sigma$, and fixed scheme
data.
\end{lemma}

\begin{proof}[Sketch of proof]
The isolation of $q$ relative to $b$ over $A$ supplies a bounded
fragment $\psi_A(v,b)$ ($|v|$ the block variable of $q$) that entails
$q$. By stationarity of the free lift and preservation of diagrams
under arrows, the same formula $\psi_A$ applied at $B$ (with $b$'s
image) entails $q^B$. Indeed: any two realizations of $q^B$ over $B$
restrict to two realizations of $q$ over $A$ (up to the free lift
construction: $q^B$'s restriction to $A$ equals $q$). By isolation of
$q$ over $A$, those restrictions are $A$-equivalent; by stationarity
of free lifts (Theorem~\ref{thm:free-extension}), they are then
$B$-equivalent. Uniqueness gives isolation.

For the bound on the isolation radius: use uniform testing at
$c(|q|+\ell)$ to detect any failure of the entailed formula at size
$\ge c(|q|+\ell)$; the resulting witness size depends only on
fixed scheme data.
\end{proof}

\subsection{All-dominated extensions}\label{sub:all-domination}

\begin{definition}[All-dominated]\label{def:all-dominated}
Let $X\le_\K Y$ be same-level objects, and let $b$ be a bounded tuple
in $Y$. We say $Y$ is \emph{all-dominated over $X+b$} if, for every
bounded tuple $c$ from $Y$, the type $\tp(b,c/X)$ is isolated
relative to $b$.
\end{definition}

The definition quantifies over all bounded $c$, not merely over some
fixed enumeration of $Y$'s bounded tuples. This is what makes
all-domination stable under the constructions of Section~\ref{sec:marked}.

\begin{lemma}[Existence]\label{lem:all-dominated-exists}
At sufficiently closed levels, for every model $X$ of $\mathcal C$ and
every bounded tuple $b$ over $X$ realizing a fixed bounded type, there
is a same-level extension $X\le_\K Y$ with $Y$ all-dominated over
$X+b$.
\end{lemma}

\begin{proof}[Sketch of proof]
Build a countable increasing chain $X=X_0\le_\K X_1\le_\K\cdots$ of
same-level extensions of $X$, together with a single fixed mark
$b\in X_1$, so that at every stage $n$:

\begin{itemize}
\item for each bounded tuple $c$ enumerated at stage $n$, a fixed
  bounded substructure $Z\subseteq X_n$ isolates $\tp(b,c/X_n)$
  relative to $b$ over $X_{n-1}$;
\end{itemize}

An all-dominated object exists as the direct limit of the $X_n$ with
mark $b$. The bound on witness size at
each stage is supplied by Lemma~\ref{lem:free-isolation} and uniform
testing. Unions at limits give the common-upper-bound clause.
\end{proof}

\begin{theorem}[All-dominated extension exists]\label{thm:all-lengths}
Let $b$ be a bounded tuple over a base $X$ at a sufficiently closed
eligible level. There is a model $Y\ge_\K X$ at the same level, all
dominated over $X+b$. Moreover, $b$ realizes any prescribed bounded
free type over $X$, and the construction can be made at every bounded
arity simultaneously with a single extension.
\end{theorem}

\begin{proof}[Sketch of proof]
The marked-increment construction (Section~\ref{sec:marked}) will
provide this systematically, but the all-dominated existence we need
here is more elementary. Enumerate all bounded tuples in a formal
universe $X^*\supseteq X$ constructed as a countably long union of
small extensions of $X$, adding at each stage a witness for the
isolation of the next bounded tuple with $b$. Direct-limit closure under
countable chains keeps the result at size $\mu$ (the level). Isolation
of $(b,c)$ at each bounded $c$ over the resulting union follows from
continuity of types at limits (Proposition~\ref{prop:local-character})
together with the fact that a fragment of each $X_n$ isolates it over
$X$.
\end{proof}

\subsection{Prime extensions}\label{sub:prime}

\begin{definition}[Prime]\label{def:prime}
Let $A\le_\K B$ be same-level, and let $b$ be a bounded tuple in $B$
realizing a prescribed type $p$ over $A$. We say $(A,B,b)$ is
\emph{prime} over $(A,p)$ if, for every $A\le_\K C$ with $b'\in C$
realizing $p$ and $C$ all-dominated over $A+b'$, there is a bounded
$A'$ with $A\le A'\le B$ containing $b$, and a strong map
$(A',b)\to(C,b')$ over $A$.
\end{definition}

Informally, a prime extension is ``smallest'' among all-dominated
extensions.

\begin{theorem}[Existence of prime extensions]\label{thm:prime}
At sufficiently closed levels, for every prescribed bounded type $p$
over $X$ there exist same-level $X\le_\K Y$, $b\in Y$ realizing $p$,
with $(X,Y,b)$ prime over $(X,p)$ and $Y$ all-dominated over $X+b$.
\end{theorem}

\begin{proof}[Sketch of proof]
Build $Y$ as a countable chain of small extensions of $X$ that
successively embed every bounded piece of any prescribed
all-dominated extension. This is a back-and-forth: enumerate a target
all-dominated pair $(X,C,b')$, and at stage $n$ extend
$X_n\le_\K X_{n+1}$ so that the $n$-th bounded tuple of $C$ has a copy
in $X_{n+1}$ matching the corresponding diagram. Bounded diagram
homogeneity plus uniformity of isolation give the existence of each
copy. Direct-limit closure keeps the result at level $\mu$.
\end{proof}

\begin{corollary}[Uniqueness of prime]\label{cor:prime-unique}
Any two prime all-dominated extensions of $X$ realizing $p$ are
isomorphic over $X$.
\end{corollary}

\begin{proof}[Sketch of proof]
Bounded back-and-forth: each prime extension embeds into the other
over $X$. Composition of the two embeddings is an automorphism of
the first fixing $X$ pointwise.
\end{proof}


\section{The marked-increment construction}\label{sec:marked}

Throughout, $\mathcal C$ is a working scheme whose arrows are precisely
the componentwise strong embeddings preserving its specified maps and
distinguished data. In particular, there is no additional condition on
intersections or on bases. We use the working package of
Definition~\ref{def:working-package}, together with the calculus and
isolation results of the preceding two sections, at sufficiently closed
eligible levels. All refinements in this section have fixed set
parameters: the input scheme and template, the prescription below, and,
after it is chosen, the new template. An unbounded output class is
asserted under the eligible-subclass hypothesis of
Convention~\ref{conv:eligible-subclass}.

The bare idea: from $\mathcal C$ we form a category $\mathcal C^b$ of
\emph{marked pairs} $(X,Y,b)$ in which $b$ is a single bounded mark in
an all-dominated extension $Y$ of $X$. The purpose is to make the
mark's type ``stabilized up to the whole system'': a bounded piece of
$Y$ is controlled by a bounded piece of $X$ together with $b$. We show
that $\mathcal C^b$ is itself a working scheme, with all the
consequences.

\subsection{Stationary prescriptions}\label{sub:stationary-prescription}

\begin{definition}[Stationary finite prescription]\label{def:stationary-prescription}
A \emph{stationary finite prescription} for $\mathcal C$ assigns to
every object $X$ a type $p_X$ of a bounded tuple, with fixed component
sorts. The assignment commutes with isomorphisms, and for every arrow
$X\to X'$, including one between different eligible levels, $p_{X'}$ is
the free lift $p_X^{X'}$ in the sense of
Theorem~\ref{thm:free-extension}, after identifying the base by that
arrow. The prescription is given by a fixed set code of the sort used
in the applications below.
\end{definition}

\begin{definition}[Marked pair]\label{def:marked-pair}
An object of $\mathcal C^b$ at level $\mu$ is a triple
\[
 (X,Y,b),\qquad X\le Y,
\]
where $X, Y$ are objects of $\mathcal C$ at level $\mu$, $b\in Y$
realizes $p_X$, and $Y$ is all-dominated over $X+b$ in the sense of
Definition~\ref{def:all-dominated}. The inclusion $X\le Y$ and the mark
$b$ are part of the structure.

An arrow $(X,Y,b)\to(X',Y',b')$ is a commuting pair
$(f,g)$ of componentwise strong $\mathcal C$-embeddings, with $g$
taking the mark to the mark: $g(b)=b'$. The notation $X\le Y$ records
an actual inclusion; arbitrary arrows are put into this form by
replacing the codomain with an isomorphic copy.
\end{definition}

Recall that all-domination quantifies over \emph{every} bounded tuple
of $Y$, not just the members of one fixed exhaustion. This is the
property that makes $\mathcal C^b$ carry the working package.

\subsection{Downward transfer of isolation}\label{sub:downward-transfer}

Our first task: make the pair isomorphism test work. If a pair
$(X,Y,b)$ is a marked object and $X_H\le X$ is a smaller base, an
isomorphism test for $X$ versus $X_H$ must compare pairs with different
base sizes. The following lemma is the engine for descending isolation
from a larger base $X$ to a smaller one $X_H$.

\begin{lemma}[Downward transfer of isolation]\label{lem:downward-transfer}
Let $X_H\le X\le U$ be same-level objects, with $X$ and $X_H$ both of
eligible cardinality $\mu$ at a sufficiently closed level. Let $b, c$
be bounded tuples in $U$ with $|b|+|c|<\mu$. Suppose
$\tp(b,c/X)$ is isolated relative to $b$, and its isolating fragment
uses at most $h(|b|+|c|)$ parameters from $X$ for a fixed scheme
function $h$. Then $\tp(b,c/X_H)$ is isolated relative to $b$, with
isolating fragment of size at most $h(|b|+|c|)+\aleph_0$, provided the
level is sufficiently closed under $h$ and under the retraction index
bounds of Corollary~\ref{cor:retractions}.
\end{lemma}

\begin{proof}[Sketch of proof]
Let $\psi(w,v,s)$ isolate $\tp(b,c/X)$, with $s\subseteq X$ a bounded
parameter list. Choose from Corollary~\ref{cor:retractions} a set of
$\kappa$ retractions $r_j\colon X\to X_H$, with $\chi<|s|$ and
$\chi+\aleph_0<\kappa<\mu$, such that all but at most
$|S|+\aleph_0$ of the $r_j$ fix any given bounded $S\subseteq X_H$
pointwise. The images $r_j(s)$ for $j<\kappa$ are a bounded list in
$X_H$.

Define $s^*$ to be the majority image: the bounded list of tuples in
$X_H$ realizing the majority value of $\{r_j(s):j<\kappa\}$ on each
bounded test. For at most $|s|+\aleph_0$ indices $j$, the diagram of
$r_j(s)$ differs from $s^*$; for all others $r_j$ preserves the atomic
diagram on $s\cup\{b,c\}$ (since $r_j$ is a $\mathcal C$-arrow and hence
preserves atomic diagrams). Thus for all but at most $|s|+\aleph_0$
indices $j$, the substitution $s\mapsto s^*$ is compatible with the
isolating formula $\psi$: $\psi(w,b,c,s)\iff\psi(w,b,c,s^*)$ for
the relevant $w\in\{b,c\}$.

It follows that $\psi(w,b,c,s^*)$ isolates $\tp(b,c/X_H)$ relative to
$b$: any two realizations $c_1$, $c_2$ in the same level with
$\psi(b,c_1,s^*)$ and $\psi(b,c_2,s^*)$ realizable inside $U$ agree on
their diagram over $X_H$, because the majority move transports the
isolation of $c_1, c_2$ over $X$ down to $X_H$.
\end{proof}

\subsection{The pair isomorphism test}\label{sub:pair-iso}

\begin{lemma}[Pair isomorphism test]\label{lem:pair-isomorphism}
After a further closure refinement, marked pairs exist over every
object $X$ of $\mathcal C$. An isomorphism $e\colon X\cong X'$ of
bases extends to an isomorphism $(X,Y,b)\cong(X',Y',b')$. More
precisely, for bounded tuples $t$ and $t'$ in the respective pair
structures, such an extension can take $t$ to $t'$ iff $e$ takes the
indicated base entries to their counterparts and transports
$\tp(t,b/X)$ to $\tp(t',b'/X')$.

Same-level arrows preserve bounded pair orbits. Moreover, comparisons
of bounded pair tuples are preserved and reflected when two pairs at
one common small level are mapped to two pairs at a common larger
eligible level. All tuple lengths and bounds needed for the comparison
are strictly below the smaller level.
\end{lemma}

\begin{proof}[Sketch of proof]
Existence is Theorem~\ref{thm:all-lengths} applied to the finite
prescription (existence of all-dominated extensions for a prescribed
type). The pointed uniqueness assertion follows from
Proposition~\ref{iso:prime}: its back-and-forth form retains prescribed
bounded tuples with the same type together with the mark. Necessity of
the displayed type condition follows from invariance.

For sufficiency at one level, suppose that
$\tp(t,b/X)=\tp(t',b'/X')$ after transport by $e$. The base
isomorphism $e$ transports the prescribed free type $p_X=p_{X'}$. By
Lemma~\ref{lem:free-isolation}, the free extension of $\tp(t,b/X)$ to
$Y$ is exactly $\tp(t,b/Y)$ (first alternative of the free isolation
lemma applied to the base $Y$). Similarly for the primed copy.
Since $Y$ and $Y'$ are both all-dominated over their respective bases
with the same prescribed free type at the mark, standard extension
arguments (bounded back-and-forth) produce the required isomorphism
of pairs.

The mixed-level version, comparing pairs at a small level and their
images at a large one, mirrors the argument for the single-model
scheme, using clause (3) of Theorem~\ref{thm:free-extension} and
Proposition~\ref{lem:mixed-levels}.
\end{proof}

\subsection{The marked template}\label{sub:marked-template}

The pair isomorphism test above is where all-domination is essential:
without it, the free lift of a bounded tuple need not be determined by
its free lift over the base, since the extension could add structure
that constrains the tuple's type. With all-domination, the mark's
type is enough.

We must now verify that marked pairs do form a working scheme: that
there is a template of finite-support terms with the required
naturality, downward closure, and exhaustion properties.

\begin{lemma}[Sample pair exists]\label{lem:sample-pair}
At further sufficiently closed levels there exist marked pairs at level
$\mu$ for every prescribed finite type $p$. Moreover, the sample pair
$(X_H,Y_H,b)$ can be presented on three padded dense linear orders
$J_H, Z_H, W_H$ with $X_H=F(J_H)$, $Y_H\cong F(Z_H)$, and a universal
strip $W_H$ factoring $Y_H$ as $X_H$-embedded into $F(J_H+W_H)$, all
at level $\mu$.
\end{lemma}

\begin{proof}[Sketch of proof]
Use Theorem~\ref{thm:all-lengths} to build an all-dominated extension
$X'\le Y'$ at level $\mu$ with $b\in Y'$ realizing $p$. Present $X'$
as $F(J_H)$ for a padded dense $J_H$ of size $\mu$ (working-package
clause (2c)), and $Y'$ as $F(Z_H)$ for a well-ordered $Z_H$ via clause
(2c). The universal-strip representation $Y_H\cong F(J_H+W_H)$ embeds
$Y'$ over $X'$ into $F(J_H+W_H)$, where $W_H$ is a fresh strip of size
$\mu$ with countably many disjoint sub-strips: this is
Proposition~\ref{prop:universal-strip}. Pick a sub-strip to hold a copy
of $b$, and label it as the mark.
\end{proof}

\subsection{Chain closure}\label{sub:chain-closure}

\begin{lemma}[Chain closure for marked pairs]\label{lem:chain-closure}
At further sufficiently closed levels, $\mathcal C^b$ has unions of
increasing chains of total size equal to the level. The union is a
marked pair. The common-upper-bound clause holds as well, including
into an eligible larger level.
\end{lemma}

\begin{proof}[Sketch of proof]
Fix a level $\mu$ closed under the bounds of Lemma~\ref{lem:sample-pair}
and the marked pair isomorphism test, with cofinally many smaller
levels at which those results hold. We do not require pair-chain
closure at the smaller levels.

Write the chain, replacing arrows by inclusions, as
$(C_i,T_i,b)$ for $i<\alpha$, and let $C,T$ be the component unions.
The underlying scheme gives $C\le T$ and the union maps. The actual
marginal of the mark over $C$ is $p_C$: the marginals at proper stages
are the prescribed free extensions, and
Proposition~\ref{local-character} gives stationary continuity for this
finite tuple.

Induct on the chain length. The shorter-length assertion allows
intermediate limit unions to be inserted. Restricting cofinally, we
may consider a continuous chain indexed by a regular cardinal $\delta$.
If a bounded tuple $d\in T$ is contained in some $T_i$, its type with
$b$ is isolated over $C_i$; free isolation gives isolation over $C$.
For $d$ not in any single $T_i$, use downward transfer
(Lemma~\ref{lem:downward-transfer}) to descend the corresponding
isolation from a larger base with bounded parameters to a smaller one.
The bound on `smaller levels` at which these results hold is below
$\mu$ by closure.

With both cases handled, the union $T$ over $C$ is all-dominated; the
common-upper-bound clause for $\mathcal C$ gives the required union
map into any eligible common upper bound.
\end{proof}

\subsection{The marked-increment working package}\label{sub:marked-package}

\begin{theorem}[Marked increments are working schemes]\label{thm:marked-package}
Let $\mathcal C$ be a working scheme with componentwise arrows and a
stationary finite prescription $p$ as in
Definition~\ref{def:stationary-prescription}. Assume the
eligible-subclass hypothesis of Convention~\ref{conv:eligible-subclass}.
On an unbounded further class of sufficiently closed eligible levels,
$\mathcal C^b$ is again a working scheme, with componentwise arrows,
a fixed template $F^b$, and mixed arrows between these levels. The
output class retains the eligible-subclass hypothesis.
\end{theorem}

\begin{proof}
Lemma~\ref{lem:pair-isomorphism} gives the isomorphism test, orbit
preservation, and mixed reflection.
Lemma~\ref{lem:sample-pair} gives individual template values and their
mixed arrows, mixed downward L\"owenheim--Skolem, natural bounded
diagrams and saturation, and the exhaustive-list arrow criterion.
Lemma~\ref{lem:chain-closure} supplies the missing union-object and
upper-bound assertions. Composition and coherence are componentwise.

The extraction added only finitary chart, representation, retraction,
and witness symbols with a fixed set bound. Further bounds were testing
and placement costs for the old template and the fixed two-part layout
of the new template, isolation and approximation costs, and a
refinement permitting cofinally many smaller template-valid levels.
These are fixed-parameter operations in the closure bookkeeping. No
step requires small-pair chain closure before it is proved.
\end{proof}