==== TABLE OF CONTENTS ====
Eventual-Categoricity-for-Abstract-Elementary-Classes//01-introduction.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//02-reduction-orders.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//03-reversal.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//04-diagrams.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//05-working-schemes.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//06-calculus.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//07-isolation.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//08-marked-increments.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//09-marked-boundaries.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//10-geometry.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//11-geometric-systems.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//12-geometric-boundaries.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//13-uniform-closure.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//14-cardinal-transfer.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//main.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//proof-route.tex
Eventual-Categoricity-for-Abstract-Elementary-Classes//references.bib
===========================

==== BEGIN Eventual-Categoricity-for-Abstract-Elementary-Classes//01-introduction.tex ====
\section{Introduction}\label{main:introduction}

Categoricity asks whether cardinality determines a model up to isomorphism.
For abstract elementary classes, the eventual categoricity conjecture predicts
that uniqueness in one sufficiently large cardinal forces uniqueness in every
cardinal above a uniform threshold. We prove this prediction in ZFC, with the
threshold depending only on a bound for the L\"owenheim--Skolem number.

\subsection{The statement}

We specify the axioms, including the union clause used throughout the proof.
All structures have sets as their universes, and all languages are set-sized
and finitary. We write $|M|$ for the universe of a structure and $\|M\|$ for
its cardinality.

\begin{definition}[Abstract elementary class]\label{main:aec}
An \emph{abstract elementary class} (AEC) is a pair $K=(\mathcal C,\le_K)$,
where $\mathcal C$ is a class of structures in a fixed language $\tau$ and
$\le_K$ is a partial order satisfying the following conditions.
\begin{enumerate}[label=\textup{(\arabic*)}]
\item The class is closed under isomorphism. If $M\le_K N$, then $M$ is a
$\tau$-substructure of $N$. If $f:N\cong N'$ and $M\le_K N$, then
$f[M]\le_K N'$.
\item \emph{Coherence:} if $M_0$ is a $\tau$-substructure of $M_1$, and
$M_0\le_K M_2$ and $M_1\le_K M_2$, then $M_0\le_K M_1$.
\item For every nonzero ordinal $\delta$ and increasing chain
$(M_i:i<\delta)$ under $\le_K$, its union $U$ belongs to $\mathcal C$ and
$M_i\le_K U$ for all $i<\delta$. If also $M_i\le_K N$ for every $i$, then
$U\le_K N$.
\item There is an infinite cardinal $\ell\ge |\tau|+\aleph_0$ such that,
for every $M\in\mathcal C$ and $A\subseteq |M|$, there is $N\le_K M$ with
$A\subseteq |N|$ and $\|N\|\le |A|+\ell$.
\end{enumerate}
The least possible $\ell$ is denoted $\LS(K)$. A \emph{strong map} is an
isomorphism onto a strong substructure of its codomain. The class is
\emph{categorical in $\kappa$} if it has a model of cardinality $\kappa$ and
all its models of that cardinality are isomorphic.
\end{definition}

The chain axioms equivalently give unions and the common-upper-bound clause
for nonempty set-indexed directed systems of strong inclusions. We also use
the corresponding direct limits of coherent strong maps, obtained by
renaming their injective images. No intersection axiom is included.

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

In particular, Theorem~\ref{main:uniform} resolves Shelah's eventual
categoricity conjecture positively. No amalgamation, joint embedding,
tameness, no-maximal-models, or arbitrarily-large-models hypothesis is
assumed. The starting categoricity cardinal may be a successor, a regular
limit, or a singular cardinal. The theorem asserts the existence of a
threshold, without prescribing a numerical bound for it.

On the resulting categorical tail, every model strongly embeds into every
model of at least its cardinality. Indeed, the L\"owenheim--Skolem axiom
supplies a strong submodel of the smaller cardinality, and categoricity
identifies it with the given model. Taking a larger target gives proper
strong extensions and a common target for any two models. Thus the tail
has joint embedding and no maximal models.

It is useful to separate the uniform quantifier from the main structural
argument.

\begin{theorem}[The qualitative form]\label{main:qualitative}
An AEC categorical in unboundedly many cardinals is categorical on a tail of
the cardinals.
\end{theorem}

Here ``unbounded'' means unbounded in the class of all cardinals, and a tail
contains every cardinal above some fixed cardinal. The set-coding argument
in Proposition~\ref{found:uniform-reduction} proves the equivalence of the
two theorems. Once that reduction is made, arbitrarily large models are
available. The order construction in Theorem~\ref{found:order-template}
then supplies actual models at every sufficiently large cardinal; subsequent
categoricity arguments concern both existence and uniqueness.

The uniform theorem applies in particular to sentences of
$L_{\omega_1,\omega}$ in countable languages, where countable conjunctions
and disjunctions are allowed but quantifier strings are finite.
For such a sentence $\varphi$, choose a countable fragment containing it
and order its models by elementarity for that fragment. This is an AEC
with L\"owenheim--Skolem number $\aleph_0$
\cite[Example~2.0.2]{BoneyVasey2017Survey}. The models and their
isomorphisms are unchanged, so the same $\mu(\aleph_0)$ works for all
these sentences. The prescribed $\beth_{\omega_1}$ threshold in the
classical infinitary formulation remains a separate question
\cite[Conjecture~1.1]{BoneyVasey2015}.

\subsection{History and scope}

Morley's categoricity theorem gives the countable first-order prototype:
a countable theory categorical in one uncountable cardinal is categorical
in every uncountable cardinal \cite{Morley1965}.  Its structural approach
connects uniqueness of models with stability and dimension.  The geometry
of strongly minimal sets, developed by Baldwin and Lachlan
\cite[Sections~1--2]{BaldwinLachlan1971}, provides a central antecedent for
classification by bases.  In an AEC, elementary compactness and the
first-order description of types are not part of the axioms.  The
corresponding amalgamation, independence, and geometry therefore require
separate constructions.

Shelah's eventual categoricity conjecture asks for an eventual dichotomy
between categoricity and noncategoricity; see
\cite[Conjecture~N.4.2]{Shelah2009} and \cite{BoneyVasey2015}.
The equivalent formulation using one threshold depending on an LS bound
is discussed in \cite[Remark~1.3]{VaseyUniversalI}.  Our set-coding
argument makes that reduction explicit: it treats bounded categoricity
spectra as well as classes categorical at unboundedly many cardinals.
An explicit numerical threshold is a further question, separate from the
existential threshold in Theorem~\ref{main:uniform}; compare
\cite[Conjecture~N.4.3(1)(b)]{Shelah2009}.
Under CH, the companion \cite[Theorem~1.1]{OpenAI2026CHThreshold}
constructs an AEC $K$ with $\LS(K)=\aleph_0$ that is categorical on a
higher tail but not at $\beth_{(2^{\aleph_0})^+}=\beth_{\omega_2}$,
ruling out this prescribed endpoint for arbitrary AECs.

Substantial special cases have been established. Makkai and Shelah
proved transfer from sufficiently large successor categoricity for
$L_{\kappa,\omega}$-theories when $\kappa$ is strongly compact
\cite[Conclusion~5.1]{MakkaiShelah1990}. Grossberg and VanDieren
obtained upward categoricity transfer from one sufficiently large successor
cardinal for tame AECs with amalgamation, joint embedding, and arbitrarily
large models \cite[Theorem~5.2]{GrossbergVanDieren2006}.
Boney subsequently derived tameness from strongly compact cardinals and,
combining it with the Grossberg--VanDieren transfer, established eventual
categoricity for arbitrary AECs with a successor starting cardinal under
a proper class of strongly compact cardinals \cite{Boney2014}.
These results explain the importance of removing restrictions on the
starting cardinal as well as structural hypotheses on the class.

Universal classes admit
a ZFC transfer without assuming amalgamation
\cite[Theorem~7.3]{VaseyUniversalII}.  Tameness, amalgamation, and primes
give another transfer \cite[Theorem~3.8]{VaseyTamePrimes}.
Shelah and Vasey prove a ZFC categoricity theorem for excellent AECs and
obtain broader results using strongly compact cardinals, or the weak
generalized continuum hypothesis (WGCH), that is,
$2^\kappa<2^{\kappa^+}$ for every infinite cardinal $\kappa$, together
with amalgamation
\cite[Theorem~14.2 and Corollaries~14.7, 14.10]{ShelahVasey2024}.
Under WGCH, amalgamation, and arbitrarily large models, Vasey also gives
a classification of categoricity spectra
\cite[Corollary~9.7]{VaseySpectrum}.  These hypotheses supply substantial
structure. Here the amalgamation, bounded-tuple calculus, and geometry
needed for the working schemes are constructed at selected levels from
the AEC axioms and unbounded categoricity.

The proof uses several established methods in forms that are proved
locally.  Order presentations originate in the work of Ehrenfeucht and
Mostowski \cite{EhrenfeuchtMostowski1956}; their AEC formulation and
functorial maps are developed in
\cite[IV.0.8--IV.0.9 and IV.0.12]{Shelah2009}.  We retain a finite-support
presentation throughout the proof.  Its extraction uses classical
partition-calculus methods \cite{ErdosRado1956}, while the later
isolation argument uses Fodor's pressing-down method \cite{Fodor1956}.
Stationary independence and local character are central to Shelah's good
frames \cite[II.2.1]{Shelah2009}.  Sections~\ref{calc:section-calculus}
and~\ref{iso:section-isolation} establish the bounded-tuple calculus,
relative isolation, and dominated extensions required for the systems
used here.

A version-sensitive issue matters for the order argument.  Boney and
Vasey \cite[Fact~1.4 and the discussion of Claim~1.5, pp.~3--4]{BoneyVasey2015}
identify a gap in the unrestricted syntactic-characterization claim of
Shelah's Chapter~IV and withdraw an earlier attempted repair.  Their
valid variants with exponentiation or cofinality assumptions do not
cover all the starting cardinals of Theorem~\ref{main:uniform}.  We prove
the required reversal of strong maps directly in
Theorem~\ref{found:reversal}.

Finite systems and dimension-raising arguments have a long history in
nonelementary categoricity.  Shelah's existence and uniqueness methods
\cite[Sections~3--5]{Shelah1983B} are antecedents of the passage from
one additional dimension to a larger cardinal.  The modern treatment in
\cite[Definition~8.16 and Lemma~11.6]{ShelahVasey2024} distinguishes
amalgamated completion from strong uniqueness onto a prescribed target.
Both properties are needed below and are proved separately.  Our final
cardinal induction uses exact boundary maps for systems whose basis
pieces may have different cardinalities.

Esp\'indola has announced eventual categoricity for arbitrary AECs and
further accessible-category results \cite{Espindola2019}, and subsequently
an explicit-threshold categoricity theorem \cite[Theorem~4.1]{Espindola2023}.
These are separate public claims.  The argument here constructs its
working-scheme calculus, isolation, marked and geometric boundary lifting,
and common-level closure directly.  None of these interfaces is imported
from those preprints.

\subsection{Proof overview}

By the set-coding reduction in Section~\ref{found:section-reduction-orders},
it suffices to fix one AEC $\K$ categorical in unboundedly many cardinals
and prove categoricity on a tail.  The proof first builds structure at
selected cardinals, called working levels, and only at the end transfers
it to every larger cardinal.  A tuple is bounded at a level $\mu$ when
its length is strictly less than $\mu$.

\paragraph{From orders to comparison of tuples.}
An order presentation $E$ assigns a model to a linear order: each element
is represented by a label and finitely many indices, and an order embedding
induces a strong map by substituting indices.  Section~\ref{found:section-reversal}
uses specially chosen orders to control the automorphism orbits of short
tuples.  A small subpresentation can be aligned with a larger presentation
so that all its short tuples have matching orbit records.  An elimination
chain then proves that a strong map can be reversed on any prescribed
short tuple.  The small model supplies the alignment; the larger model
accommodates the enumeration of the small model's tuples.  This avoids an
exponentiation hypothesis at the categoricity cardinal.

In Section~\ref{lev:section-diagrams}, the resulting equivalence classes
of tuples under strong maps stabilize as the categoricity cardinal
increases.  These are
the comparison diagrams used later.  Finite supports give two further
tools: a bound on the parameter sets needed to distinguish comparisons,
and simultaneous placement of coherent bounded prescriptions.  Together
they yield amalgamation and homogeneity for bounded tuples at suitable
countably cofinal closure levels.

\paragraph{A calculus that can be applied to systems.}
The same tools will be needed for finite systems of models, not only for
individual models.  Section~\ref{lev:section-working-schemes} records their
precise hypotheses as a working scheme: a finite system shape, specified
arrows, one finite-support presentation, and compatible tuple comparisons.
Sections~\ref{calc:section-calculus} and~\ref{iso:section-isolation} derive
the calculus from this package.  A type over a base is determined by
identification of tuples in an amalgam over that base.  Its distinguished
free extensions are computed by long approximation sequences already in
the base.  The isolation construction gives extensions controlled by
a specified mark: the full type of each additional bounded tuple, together
with the mark, is determined by the mark's type and a bounded fragment of
the base.  Such extensions have the primeness and uniqueness needed for
iteration.

\paragraph{Marked systems detect growth of a geometry.}
Section~\ref{mark:section-increments} shows that adjoining a finite mark
and an extension controlled in this way again gives a working scheme.
Iterating produces a model at each subset of a finite axis set, with
commuting strong maps.  Its boundary consists of the proper-subset
vertices and their maps.  Section~\ref{iter:section-boundaries} first
completes a compatible boundary map into a common extension, then extends
a boundary isomorphism onto the prescribed target.  The return-tree
argument keeps full maps coherent along individual branches but retains
only boundary maps in the common accumulator.  This distinction lets the
orbit bound control joint comparisons across different faces, including
their actual equalities.

Section~\ref{geom:section-geometry} chooses a minimal singleton type,
one with a unique nonalgebraic extension over each relevant base.  Its
realizations form the points of a pregeometry, with independence defined
by finite products of the type.  We retain a distinguished strong copy of
its base model $M_0$, with a fixed diagram for its enumeration, in the
later models; these are the pointed models used below.  Exact lifting for all finite marked
systems at one common level rules out a proper strong extension with no
new points.  A downward construction then extends this no-growth
conclusion to arbitrary larger cardinalities.  Thus the geometry detects
every proper extension, and its basis cardinality equals model
cardinality above the resulting threshold.

\paragraph{From geometric systems to a categorical tail.}
Sections~\ref{sys:section-geometric-systems} and~\ref{exact:section-boundaries}
organize bases into finitely many pieces assigned to vertices.  Tiled
order presentations give systems with these pieces; a paired induction
establishes their working packages and classification by prescribed
basis maps.  A second boundary argument gives exact lifting for every
finite geometric shape at suitable levels.

The two finite-dimensional applications require separate common-level
choices.  Section~\ref{close:section-uniform} supplies both: fixed set codes
for all finite constructions and their bound requests produce a level
where every finite depth is available.  The geometric application is made
after the marked application has supplied the no-growth threshold.
Finally, Section~\ref{tail:section-transfer} starts from a common geometric
level and inducts on the maximum cardinality of the basis pieces,
simultaneously for all finite shapes.  One additional axis records the
previously constructed isomorphism at each extension step; coherent
unions handle limits. The zero-axis case gives pointed categoricity.
The L\"owenheim--Skolem axiom and categoricity at one fixed smaller
cardinal place the chosen base pattern in every sufficiently large model.
Forgetting that base gives the qualitative theorem, and the set-code
reduction gives the uniform theorem.

Figure~\ref{fig:proof-route} summarizes the proof and the two uses of
common-level closure.

\input{figures/proof-route}

\subsection{Conventions}

All size variables are cardinals unless explicitly called ordinals.
An assertion about bounded tuples at a level $\mu$ concerns tuples of
length strictly below $\mu$. Eligible working levels have countable
cofinality and are strong limits closed under the displayed bounds.
Whenever smaller adequate levels are needed cofinally below a working
level, that requirement is stated and included in the closure bookkeeping.
Automorphisms of an index order always mean automorphisms of its pure
linear order. Charts, auxiliary hulls, and basis choices are not added to
the structures whose isomorphisms are being compared.
==== END Eventual-Categoricity-for-Abstract-Elementary-Classes//01-introduction.tex ====

==== BEGIN Eventual-Categoricity-for-Abstract-Elementary-Classes//02-reduction-orders.tex ====
\section{Set codes and models indexed by orders}
\label{found:section-reduction-orders}

We first separate the uniformity over AECs from the transfer argument for
one AEC. All directed families below are nonempty and set-indexed. We
begin by deriving the directed forms of the chain axioms in
Definition~\ref{main:aec}.

\begin{lemma}[Directed unions and coherent direct limits]
\label{found:directed-colimits}
If a nonempty set of models is directed under strong inclusion, its
union belongs to $\K$ and every member is strong in the union. If
every member is strong in a common model $N$, its union is strong in
$N$. More generally, a coherent diagram of strong maps indexed by a
nonempty directed partial order has a direct limit in $\K$, with
strong canonical maps. Every compatible family of strong maps from
the diagram into a model induces a strong map from the direct limit.
\end{lemma}

\begin{proof}
The union is a well-defined $\tau$-structure: finitely many
arguments are contained in one family member, and any two
choices of such a member agree after passing to a common
strong upper member. Here finitarity is used for functions
and relations alike.
We prove the union and common-upper-bound assertions together by
induction on the cardinality of the family. A finite directed
family has a member containing every other member, so its union is
that member. A countable directed family has a cofinal increasing
sequence: enumerate the family and successively choose a member
above the previous choice and the next enumerated member. The
chain axioms apply to this sequence, including their
common-upper-bound clause.

Suppose the family is indexed by a set $I$ of uncountable
cardinality $\kappa$, and the two assertions hold for smaller
families. Choose an operation assigning to each pair of indices
an index of a strong upper bound. Express $I$ as the union of an
increasing continuous sequence $(I_\alpha)_{\alpha<\cf(\kappa)}$
of nonempty subsets of size less than $\kappa$, each closed under
that operation. To obtain this sequence, enumerate $I$ by
$\kappa$, use a cofinal sequence of ordinals below $\kappa$
to specify the required initial segments, close each stage
under the binary operation by countably many iterations, and
take unions at limit stages. A union of fewer than
$\cf(\kappa)$ sets of size less than $\kappa$ still has size
less than $\kappa$; countable closure preserves the size of
each infinite stage. This construction also works when
$\kappa$ is a successor cardinal, using $\kappa$ many stages.

Let $U_\alpha$ be the union of the family on $I_\alpha$. The
induction hypothesis gives $U_\alpha\in\K$. For $\alpha<\beta$,
every member indexed by $I_\alpha$ is strong in $U_\beta$.
The inductive common-upper-bound assertion therefore gives
$U_\alpha\leq_\K U_\beta$. The chain axioms now give the
required union over $I$. If the original family is strong in
$N$, induction first gives $U_\alpha\leq_\K N$ for every
$\alpha$, and the chain common-upper-bound clause gives the
same conclusion for their union. This completes the induction.

For a diagram $(M_i,f_{ij})$ indexed by a directed partial order,
form the quotient of the disjoint union of its underlying sets
by
\[
(i,x)\sim(j,y)
\quad\Longleftrightarrow\quad
(\exists k\geq i,j)\ f_{ik}(x)=f_{jk}(y).
\]
Directedness and coherence make this an equivalence relation.
The canonical map from each $M_i$ is injective. Interpret any
finitary function or relation in a common later model containing
representatives of its arguments; coherence and the fact that
the maps are structure embeddings make this interpretation
well-defined. The images of the $M_i$ are models forming a
directed family of strong inclusions. The first assertion puts
their union, which is the quotient just constructed, in $\K$
and makes all canonical maps strong.

Finally, compatible strong maps $g_i:M_i\longrightarrow N$
induce a map on that quotient. It is injective: if two images
agree, compare their representatives in a common later $M_k$
and use injectivity of $g_k$. The same argument gives a
structure embedding. Its image is the directed union of the
strong submodels $g_i[M_i]$ of $N$, so the
common-upper-bound assertion makes the induced map strong.
The quotient construction also gives uniqueness, and hence
the stated direct-limit property.
\end{proof}

\begin{lemma}[Recovery from small models and pairs]
\label{found:small-code}
Fix an infinite cardinal $\lambda$ and a finitary language $\tau$ of
cardinality at most $\lambda$. An AEC in $\tau$ with
$\LS(\K)\leq\lambda$ is determined by its models of cardinality at most
$\lambda$ and its strong inclusions between such models, both taken up to
isomorphism. These data have a set code, and the recovered class and
strong-submodel relation are uniformly first-order definable in set
theory from that code.
\end{lemma}

\begin{proof}
Represent small structures on ordinals of cardinality at most $\lambda$.
Represent a small pair $M\subseteq N$ by such a representative for $N$
together with the distinguished subset that is the domain of $M$.
The possible structures and pairs form sets. A code specifies which
structure types and which pair types are allowed. Testing whether a
given small structure or pair has an allowed type is a set-theoretic
condition: quantify over the relevant isomorphisms.

For an actual $M\in\K$, let
\[
\mathcal D(M)=\{A\leq_\K M:\|A\|\leq\lambda\}.
\]
This is a set. It is nonempty by the LS axiom applied to the empty set,
and its union is $M$ by the LS axiom applied to singletons. If
$A,B\in\mathcal D(M)$, the LS axiom inside $M$ supplies a small strong
submodel containing $|A|\cup|B|$. Coherence makes both $A$ and $B$ strong
in that submodel. Thus $\mathcal D(M)$ is directed.

Conversely, suppose a structure $M$ is the union of a nonempty directed
family of small structures whose membership and pair inclusions are
allowed by the code of $\K$. These are actual members and strong
inclusions of $\K$, so the directed-union axiom gives $M\in\K$.
Consequently the following condition recovers membership, including for
structures not already assumed to belong to $\K$:
\begin{quote}
$M$ is a union of a nonempty directed family of allowed small models,
with all its directed inclusions allowed by the small-pair code.
\end{quote}

To recover the strong relation, require a directed presentation
$N=\bigcup\mathcal D$ of this kind and a nonempty directed subfamily
$\mathcal E\subseteq\mathcal D$ with $M=\bigcup\mathcal E$.
If $M\leq_\K N$, use $\mathcal D=\mathcal D(N)$ and
$\mathcal E=\mathcal D(M)$; transitivity makes the second a subfamily
of the first. In the reverse direction, every member of $\mathcal E$
is strong in $N$ by the union clause for $\mathcal D$. The
common-upper-bound clause for $\mathcal E$ then gives $M\leq_\K N$.

Each presentation can be quantified over as a set of substructures of
the structure being decoded. All the preceding conditions are thus
first-order set-theoretic formulas with the small code as parameter.
They recover both the class and the order, as asserted.
\end{proof}

The equivalence below is the usual Hanf-number reduction; compare
\cite[Remark~1.3]{VaseyUniversalI}. We spell out the set coding to make
the uniform quantifier explicit.

\begin{proposition}[The uniform reduction]
\label{found:uniform-reduction}
The uniform assertion in Theorem~\ref{main:uniform} is equivalent to
the following qualitative assertion:
\begin{quote}
Every AEC categorical in unboundedly many cardinals is categorical in
all cardinals above some bound depending on that AEC.
\end{quote}
\end{proposition}

\begin{proof}
At a fixed LS bound $\lambda$, the languages can be renamed into a
fixed set of symbols with specified finite arities. By
Lemma~\ref{found:small-code}, the possible AECs in those languages are
determined by members of a set of small codes. A code is valid exactly
when its decoded class and relation satisfy the AEC axioms with LS
bound $\lambda$. This is a first-order condition on the code, so the
valid codes form a set.

Assume the qualitative assertion. For each valid code $c$, its
categoricity spectrum is either bounded or unbounded. In the bounded
case choose the least infinite cardinal $b_c$ strictly above every
categoricity cardinal. In the unbounded case choose the least infinite
cardinal $b_c$ such that the decoded AEC is categorical in every
cardinal at least $b_c$. These choices are definable, and the second
choice exists by the qualitative assertion. Replacement bounds the
set of all $b_c$. Choose a cardinal $\mu(\lambda)\geq\lambda$ strictly
above that set of bounds. If an AEC with LS number at most $\lambda$
is categorical at some $\kappa\geq\mu(\lambda)$, its code cannot be
in the bounded-spectrum case. It is therefore categorical at every
$\kappa'\geq b_c$, in particular at every
$\kappa'\geq\mu(\lambda)$. This is exactly the same threshold in
the premise and conclusion.

Conversely, for an AEC categorical unboundedly often, apply the uniform
assertion with $\lambda=\LS(\K)$. Some categoricity cardinal crosses
the resulting threshold, and the asserted tail follows.
\end{proof}

\begin{remark}
Lemma~\ref{found:small-code} also supplies the usual ZFC interpretation
of quantification over AECs: 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 needed. Below we fix one
AEC categorical unboundedly often and write $\ell=\LS(\K)$. It has
arbitrarily large models because categoricity includes existence.
\end{remark}

\subsection{A finite-arity partition argument}

The following end-homogeneous argument belongs to classical partition
calculus; compare Erd\H{o}s and Rado
\cite[Theorem~39 and its corollary]{ErdosRado1956}.  We prove the
finite-arity form and bounds used by the order-template construction.

\begin{lemma}
\label{found: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 an ordinal of cardinality at least
$R_k(\xi,\nu)$ into $\xi$ colors has a homogeneous subset of
cardinality $\nu$. Finitely many specified arities can be made
homogeneous simultaneously by enlarging the initial cardinal.
\end{lemma}

\begin{proof}
For $k=1$, a set of cardinality greater than $\xi\cdot\nu$ cannot be
partitioned into $\xi$ sets all of cardinality less than $\nu$.
Suppose the assertion is known for $k$. Choose an infinite initial
ordinal $\alpha$ large enough for that $k$-ary assertion with target
$\nu$, and put $b=\xi^{|\alpha|}$. Consider a coloring $c$ of the
$(k+1)$-element subsets of an ordinal $\Omega$ with $|\Omega|>b$.

Construct a tree of residual subsets of $\Omega$ through height
$\alpha$. Its root is $\Omega$. At a nonempty node, name and remove
its least point $x$. The previously named points on its branch,
together with $x$, form an increasing sequence. Partition the
remaining residual set according to all values
\[
u\longmapsto c(s\cup\{u\}),
\qquad
s\text{ a $k$-subset of that sequence}.
\]
The nonempty parts are the children. At a limit height, a branch has
as its residual set the intersection of the earlier residual sets;
retain the node precisely when this intersection is nonempty.

At each node there are at most $|\alpha|$ coordinates to record and
hence at most $b$ children. The total number of possible nodes
through height $\alpha$ is at most
$b^{|\alpha|}=b$. This includes the limit nodes, which are specified
by their branches. At most $b$ points are removed as node labels.
Choose $u\in\Omega$ which is never removed. At every height it
belongs to one residual set; at limit heights it belongs to the
intersection on that branch. Consequently it determines a branch
with $\alpha$ named points and nonempty remainder.

For every $k$-subset $s$ of these named points, all later named points
give the same value of $c(s\cup\{x\})$: that value was fixed by the
partition immediately after the last point of $s$ was named.
Therefore $c$ on increasing $(k+1)$-tuples from the branch depends
only on their first $k$ entries. Apply the $k$-ary induction
hypothesis to this induced coloring on the branch. Its homogeneous
$\nu$-subset is homogeneous for $c$ as well. For example, the
recursion just proved allows
$R_{k+1}(\xi,\nu)=(\xi^{R_k(\xi,\nu)})^+$ after increasing the
initial $R_1$ as needed.

For a finite list of arities, work backward to choose a bound large
enough for the last desired thinning after all the earlier ones.
Successive thinning preserves homogeneity already obtained. This
proves the final assertion.
\end{proof}

\subsection{A fixed presentation on every order}

The construction is an Ehrenfeucht--Mostowski presentation
\cite{EhrenfeuchtMostowski1956}; for its AEC form compare
\cite[Definition~IV.0.8 and Claims~IV.0.9, IV.0.12]{Shelah2009}.
We include the finite-support construction in the label notation used below.

\begin{theorem}[Order presentation]
\label{found:order-template}
Suppose $\K$ has arbitrarily large models and $\LS(\K)=\ell$.
There are at most $\ell$ labels, each of positive finite arity, and a
functor $E$ from nonempty linear orders and order embeddings to
$\K$ and strong maps, with the following properties.
\begin{enumerate}
\item Every element of $E(I)$ is a label evaluated on an increasing
finite list from $I$. Equality and all structure relations and
function values are determined by the labels and the order/equality
pattern of the finitely many indices involved.
\item $E(I)$ contains distinct distinguished elements $(a_i)_{i\in I}$.
An order embedding $f:I\longrightarrow J$ sends $a_i$ to $a_{f(i)}$,
and its action on any labeled element is position substitution.
\item For every finite nonempty $s\subseteq I$, the elements labeled
on $s$ form a strong submodel $E_s(I)$ of cardinality at most $\ell$.
For $s\subseteq t$ these submodels are strongly included, and
$E(I)=\bigcup_s E_s(I)$.
\item $|I|\leq\|E(I)\|\leq |I|+\ell$. In particular, for every
infinite $\kappa\geq\ell$, $\K$ has a model of cardinality exactly
$\kappa$.
\end{enumerate}
Here a subpresentation is identified with its image under the
canonical strong map when an inclusion of underlying universes is
convenient.
\end{theorem}

\begin{proof}
Take an arbitrarily large $M\in\K$ and distinct elements
$(a_i)_{i\in A}$ indexed by a large ordinal $A$. Recursively on the
positive finite size of $s\subseteq A$, choose $M_s\leq_\K M$ of
cardinality at most $\ell$ containing the displayed elements on $s$
and every $M_t$ for nonempty $t\subsetneq s$. There are only finitely
many such $t$, so the LS axiom applies with bound $\ell$. Coherence
gives $M_t\leq_\K M_s$.

Choose a surjective enumeration
$(m_{s,\eta})_{\eta<\ell}$ of each $M_s$, allowing repetitions. If
$s=\{i_0<\cdots0},\quad \rk(v),\rk(w)0$.
It sends the first displayed vector to the second. Combining this
map with translations sends any ordered pair of distinct points to
any other such pair. Restricting gives the interval assertion.

Finally, an increasing map on ordinal positions preserves the
greatest differing position of two integer vectors. The induced
map on these integer vectors preserves the greatest differing
position of rational vectors as well. This proves the embedding
claim. Expanding the finitely many integer-vector positions used
by a rational vector gives the asserted finite code and comparison
rule.
\end{proof}

\begin{lemma}[Balance of cuts]
\label{found:balanced-cuts}
Every interior nonprincipal cut of $\Gamma_\delta$, and every such
cut of $H(\delta)$, is balanced.
\end{lemma}

\begin{proof}
First consider a cut $(L,R)$ of $\Gamma_\delta$. Among the ranks of
$r-l$, with $l\in L$ and $r\in R$, choose the least ordinal
$\alpha$. Fix one 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: a crossing pair
within a fiber would have smaller rank. The resulting cut in the
integer coefficients separates two adjacent integers. A point
with a head above the fixed head would exceed the fixed upper
point, and a point with a head below it would precede the fixed
lower point. The two bordering fibers are therefore cofinal
and coinitial toward the original cut, and their tails are
copies of $\Z^{(\alpha)}$. Their end
characters agree by negation in that tail group. The case
$\alpha=0$ would give a last lower and a first upper point, and
is excluded. This proves balance in $\Gamma_\delta$.

Now let $(L,R)$ be an interior nonprincipal cut of $H=H(\delta)$,
and put
\[
T=\{\rk(r-l):l\in L,\ r\in R\}\subseteq\Gamma_\delta.
\]
This is a final segment: from a crossing pair of rank $g$, subtract
a positive basis vector at any $h>g$ from its lower point. The new
pair still crosses and has rank $h$.

Suppose first that $T$ has a least member $g$. Fix a crossing head
above $g$. Every fiber with a fixed rational coefficient at $g$
lies on just one side of the cut. Otherwise a crossing difference
would have rank below $g$. The induced cut of $\Q$ is nonempty
and proper. If neither coefficient side has a nearest rational,
countable rational approximations are cofinal and coinitial in
the original cut. If the lower coefficients have a greatest
member, the entire fiber at that coefficient lies on the lower
side and is cofinal there. Its tail, supported below $g$, has
greatest available rank $g-e_0$, and the vectors
$n u_{g-e_0}$ and $-n u_{g-e_0}$ show that both its end characters
are $\aleph_0$. On the upper side, rational coefficients decreasing
to the greatest lower coefficient give coinitiality $\aleph_0$.
If instead the upper coefficients have a least member, the
reversed calculation gives cofinality and coinitiality
$\aleph_0$. These cases exhaust the rational cuts, so the original
cut is balanced.

Suppose that $T$ has no least member, and let
$\epsilon=\ci(T)$. Put $S=\Gamma_\delta\setminus T$ and let
$H_S$ be the subgroup supported on $S$. We prove that the lower
character is $\epsilon$ by separating two cases.

Assume there is $l\in L$ for which
\[
\{\rk(r-l):r\in R\}
\quad\text{is coinitial in }T.
\]
The coset $l+H_S$ is contained in $L$, since a crossing within it
would have rank in $S$. It is cofinal in $L$. In fact, if a point
$l'\in L$ lay above the entire coset, $l'-l$ would have positive
rank $h\in T$. Choose $r\in R$ with $\rk(r-l)l'$. The set $S$ is nonempty, since
otherwise the cofinal coset would be the singleton $\{l\}$.
It has no greatest member: if $s$ were greatest, $s+e_0$ would
be the least member of $T$. Balance in $\Gamma_\delta$, applied
to $(S,T)$, gives $\cf(S)=\epsilon$. The cofinality of $H_S$ at
its upper end equals $\cf(S)$. A cofinal set of ranks gives
cofinal positive basis vectors, while fewer ranks are bounded
and cannot give a cofinal family of vectors. Hence
$\cf(L)=\epsilon$ in this case.

In the other case, each $l\in L$ has a bound $t_l\in T$ strictly
below all ranks $\rk(r-l)$, $r\in R$. Choose crossing pairs
$(l_i,r_i)$, $i<\epsilon$, whose ranks are coinitial in $T$.
For fixed $l\in L$, choose $i$ with
$\rk(r_i-l_i)\leq t_l$. If $l_i\leq l$, then
$0\theta$, each realized
record in $E(H(\delta))$ determines exactly one such model orbit.
\end{lemma}

\begin{proof}
The finitely many positions belonging to each tuple entry can
be indexed in $\theta\times\omega$. Choices of arities and
labels number at most $2^{\ell+\theta}$. The flattened
order/equality diagrams number at most $2^\theta$; their sets
of cuts have size at most $2^\theta$, and occupancy subsets
number at most $2^{2^\theta}$. The displayed generous bound
therefore bounds a universal record set.

For a fixed $\delta$ with $\cf(\delta)>\theta$, equal records
give an order automorphism matching the flattened lists by
Theorem~\ref{found:order-orbits}. Applying $E$ gives an
automorphism of the model matching the tuples. Hence a
realized record determines one model orbit. Every tuple has
a labeled presentation, so the number of orbits is bounded
by the number of records.

For any $\kappa\geq\max(\ell,\theta^+)$, the ordinal
$\delta=\kappa+\theta^+$, with ordinal addition here, has
cardinality $\kappa$ and cofinality $\theta^+$. The model
$E(H(\delta))$ has cardinality $\kappa$ and is therefore a
copy of the categoricity model. This proves the bound without
any condition on $\cf(\kappa)$.
\end{proof}

Choose a model $C_\kappa$ at each categoricity size needed in a
given set-sized construction. On its $\theta$-tuple orbits put
$p\longrightarrow r$ when some strong self-map sends a
representative of $p$ to a representative of $r$. This relation
is reflexive and transitive: compose maps after using an
automorphism to align the intermediate representatives.
Choose an injection of the orbit set into the fixed cardinal
$B=B(\ell,\theta)$, once for each $\kappa$. These are its
\emph{orbit names}. For any copy of $C_\kappa$, a tuple's
name is independent of the isomorphism used to $C_\kappa$,
because two such isomorphisms differ by an automorphism.

For a suitable $\delta$ of size $\kappa$, let $F_{\kappa,\delta}$
be the partial function from $\mathcal R_\theta$ to $B$ sending
each realized record to its orbit name. The \emph{profile}
of this presentation consists of its named arrow relation
and $F_{\kappa,\delta}$. The profiles belong to a fixed set
of cardinality at most $2^B$; in particular this bound is
independent of $\kappa$ and $\delta$.

\subsection{Preserving every short record in a small subpresentation}

\begin{lemma}[Closure of ordinal supports]
\label{found:ordinal-support-closure}
Let $\theta^+\leq a$ be infinite cardinals and let $\beta$ be
an ordinal of cofinality greater than $a$. Every subset
$S\subseteq\beta$ of size at most $a$ is contained in a set
$T_0\subseteq\beta$ of size at most $a$ with the following
property: for every $P\subseteq T_0$ of size at most $\theta$
and every finite tuple from $\beta$, there is a tuple from
$T_0$ having the same order/equality diagram over $P$.
Moreover $T_0$ is bounded in $\beta$ and has cofinality
greater than $\theta$ in its induced order.
\end{lemma}

\begin{proof}
Construct increasing sets $S_i\subseteq\beta$ for $i<\theta^+$,
starting with $S$. At a successor stage consider all strict
slots over the entire well-ordered set $S_i$. There are at
most $|S_i|+1\leq a$ of them. In each finite slot add every
point; in each infinite slot add a countably infinite subset.
Together with $S_i$ this realizes every finite order/equality
pattern over $S_i$ which occurs in $\beta$. At limits take
unions. The cardinality stays at most $a$ throughout.

Set $T_0=\bigcup_{i<\theta^+}S_i$. Every set
$P\subseteq T_0$ of size at most $\theta$ is contained in
some $S_i$, by regularity of $\theta^+$. For a given finite
tuple, keep any coordinates already in $S_i$ and match its
other coordinates in their respective slots using the next
stage. This proves the asserted property over $P$.
Since $|T_0|\leq a<\cf(\beta)$, $T_0$ is bounded in
$\beta$. Each $S_i$ is bounded too, and its uppermost slot
is infinite. The next stage therefore contains points above
all of $S_i$. Every at-most-$\theta$ subset of $T_0$ is
bounded in this way, proving $\cf(T_0)>\theta$.
\end{proof}

\begin{lemma}[Appending a long indecomposable segment]
\label{found:append-segment}
Under the hypotheses of Lemma~\ref{found: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 set $T=T_0\cup J$.
Then $\otp(T)=\delta$, and $T$ has the same finite-pattern
matching property over its at-most-$\theta$ subsets.
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$.

Fix a parameter subset $P\subseteq T$ of size at most
$\theta$ and a finite tuple in $\beta$. Match the
coordinates below $\alpha$ into $T_0$ over $P\cap T_0$
using Lemma~\ref{found:ordinal-support-closure}. Keep
coordinates in $J$ fixed. The parameters in $J$, together
with these finitely many retained coordinates, are bounded
in $J$ because $\cf(\delta)>\theta$. Match all coordinates
at or beyond the end of $J$ by suitably many distinct
points of $J$ above that bound, retaining any repetitions.
The three portions stay in their correct mutual order,
and this gives the required finite tuple over $P$.

Here $\Gamma_T=\Z^{(T)}$ is identified with its image in
$\Gamma_\beta$, and $H(T)=\Q^{(\Gamma_T)}$ with its image
in $H(\beta)$. A sequence of at most $\theta$ points of
$H(T)$ uses at most $\theta$ ordinal positions in its
finite codes. A witness in $H(\beta)$ to an occupied
strict slot uses only finitely many additional ordinal
positions. Match those into $T$ over all the parameter
positions and retain the integer and rational
coefficients. Lemma~\ref{found:order-basic} makes every
comparison with the sequence unchanged. The resulting
point of $H(T)$ witnesses that slot. The reverse
implication follows from inclusion.
\end{proof}

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

\begin{proof}
Identify $N$ with the presentation in the first item.
Represent the requested set by labeled elements and
collect the ordinal positions in the finite codes of
their indices. There are at most $a$ positions. Apply
Lemma~\ref{found:ordinal-support-closure} to obtain
$T_0$. Its order type is below $a^+$. Choose a
profile occurrence $\delta$ from the second item above
$\otp(T_0)$. Since $a^+\leq\cf(\beta)\leq\beta$ and
$\delta\eta$ with $\kappa\leq\rho<\kappa^+$ and
$\cf(\rho)=\tau$, for example by appending an ordinal
segment of type $\tau$ beyond $\eta+\kappa$.
Set $\delta=\omega^\rho$. It is additively
indecomposable. A cofinal sequence of exponents gives
a cofinal sequence in $\omega^\rho$ by continuity of
exponentiation. Fewer than $\cf(\rho)$ ordinals below
$\omega^\rho$ have all their Cantor-normal-form
exponents bounded below $\rho$, and are therefore
bounded in $\omega^\rho$. This proves
$\cf(\delta)=\cf(\rho)=\tau$.
Every ordinal below $\omega^\rho$
has a finite Cantor normal form with exponents below
$\rho$. Thus $|\delta|\leq\max(\aleph_0,|\rho|)=\kappa$.
Since $\delta\geq\rho\geq\kappa$ and $\rho>\eta$,
we have $|\delta|=\kappa$, $\delta<\kappa^+$, and
$\delta>\eta$.
\end{proof}

\begin{theorem}[Eventual reversal at categoricity cardinals]
\label{found:reversal}
For each infinite cardinal $\theta$ there is a cardinal
$b_\K(\theta)$ such that, whenever
$\kappa\geq b_\K(\theta)$ is a categoricity cardinal,
$M\in\K$ has size $\kappa$, $f:M\longrightarrow M$
is strong, and $\bar a$ is a tuple of length at most
$\theta$ in $M$, there is a strong
$g:M\longrightarrow M$ with
\[
g(f(a_i))=a_i
\quad\text{for every coordinate }i.
\]
The bound concerns all sufficiently large categoricity
cardinals, of arbitrary cofinality. No equality of the
form $\kappa^\theta=\kappa$ is assumed.
\end{theorem}

\begin{proof}
It suffices to treat length exactly $\theta$; pad a
nonempty shorter tuple by repetitions, and use any
strong self-map for the empty tuple. In a categoricity
model, the asserted reversal is equivalent to symmetry
of the arrow relation on its $\theta$-tuple orbits.
Indeed a reverse orbit arrow can be precomposed and
postcomposed with automorphisms to match the particular
image tuple and original tuple. The converse follows
by applying reversal to a map witnessing an arrow.

Suppose that symmetry fails at unboundedly many
categoricity cardinals. Let $P$ be an infinite cardinal
bounding the profile palette; for example take $P=2^B$.
Choose a strictly increasing list of failing
categoricity cardinals $(\kappa_i)_{iP,\qquad
\kappa_i>\kappa_j^\theta\quad(ja.
\]
Their common named arrow relation has $p\longrightarrow r$
but no $r\longrightarrow p$. Both names occur in
both sizes. Proposition~\ref{found:alignment} applies
inside every $\mu$-sized model, using any of its
cofinal profile occurrences.

We construct $\theta^+$ rounds of an increasing strong
chain of $\mu$-sized models. At the start of round
$i<\theta^+$, choose an aligned $a$-sized submodel
$A_i$ containing all previous $A_j$. This is possible
because their union has cardinality at most $a$.
They are all strong in the current large model, and
coherence will make $A_j\leq_\K A_i$ for $j\theta$. After
round $i$ it cannot reach $p$ in a large model.
At the next aligned small model its small orbit
has the same name, and therefore cannot reach $p$
in the common relation. The inclusion of that small
model into $A$ gives an arrow from this earlier
small orbit to its orbit in $A$. If the latter
could reach $p$, transitivity would contradict the
former exclusion. Thus no tuple in $A$ can have
an orbit reaching $p$.

But $A\cong C_a$, so the orbit named $p$ occurs in
$A$; it reaches itself by the identity map. This
contradiction proves that the failing categoricity
cardinals are bounded. A cardinal above their bound
is $b_\K(\theta)$, and the first paragraph gives
the claimed reversals, including all shorter lengths.
\end{proof}
==== END Eventual-Categoricity-for-Abstract-Elementary-Classes//03-reversal.tex ====

==== BEGIN Eventual-Categoricity-for-Abstract-Elementary-Classes//04-diagrams.tex ====
\section{Stable diagrams and amalgamation at closed levels}
\label{lev:section-diagrams}

Throughout this section, \(\K\) is the AEC fixed after
Proposition~\ref{found:uniform-reduction}: it is categorical in unboundedly
many cardinals, and \(\ell=\LS(\K)\). We use the order presentation \(E\)
of Theorem~\ref{found:order-template}. A tuple may have any set as its
index set. Comparisons between tuples always specify the identification
of their index sets. Reindexing by an ordinal, padding, and repetitions
do not change any of the arguments below.

The goal is to turn bounded-tuple reversal into amalgamation at selected
levels.  We first stabilize tuple comparisons across categoricity sizes,
then use the order presentation to test and realize those comparisons
over an entire base.  Amalgamation will be a conclusion of this process.

\subsection{Stabilization of strong-map classes}

Fix an infinite cardinal \(\sigma\). At a categoricity cardinal
\(\kappa>\ell+\sigma\) where Theorem~\ref{found:reversal} holds for
\(\sigma\)-tuples, put
\[
 (M,a)\equiv^\sigma_\kappa(N,b)
 \quad\Longleftrightarrow\quad
 \text{some strong map }f:M\longrightarrow N\text{ satisfies }f(a)=b.
\]
Here \(\|M\|=\|N\|=\kappa\), and the lengths of the displayed
tuples are at most \(\sigma\).
This is an equivalence relation. Reflexivity is immediate. Categoricity
allows one to regard all the maps as maps between copies of one model;
reversal then gives symmetry, and composition gives transitivity.
Using structures with universe \(\kappa\), or one fixed representative
and its tuples, its classes form a set. Their number, for all the tuple
lengths under consideration, is bounded by the fixed cardinal supplied
by Lemma~\ref{found:orbit-bound}. Denote an infinite such bound by
\(B_\sigma\). It depends on \(\ell,\sigma\), not on \(\kappa\).

\begin{lemma}[Canonical classes above one categoricity size]
\label{lev:canonical-classes}
For \(\|N\|\ge\kappa\), a tuple \(a\) in \(N\) has a well-defined
\(\equiv^\sigma_\kappa\)-class: compute it in any strong
\(\kappa\)-submodel containing \(a\). Strong embeddings between models
of size at least \(\kappa\) preserve this class.
\end{lemma}

\begin{proof}
The downward LS axiom supplies the submodel, after adding
\(\kappa\) many elements to the requested set if necessary. If
\(M_0,M_1\le_\K N\) are two such submodels, apply LS to
\(|M_0|\cup|M_1|\). It gives \(M_2\le_\K N\) of size \(\kappa\)
containing both. Coherence gives \(M_i\le_\K M_2\). The two occurrences
of \(a\) therefore have the same class. For a strong embedding
\(f:N\to N'\), the image of a witnessing submodel is a strong
\(\kappa\)-submodel of \(N'\), so the same observation proves
preservation. All these comparisons take place inside a given ambient
model; no amalgamation property is used.
\end{proof}

\begin{proposition}[Stable diagrams]
\label{lev:stabilization}
There is a definable, nondecreasing cardinal function \(t\), with
\(t(\sigma)>\ell+\sigma\) a categoricity cardinal for every infinite
\(\sigma\), having the following properties.
\begin{enumerate}
\item Tuples of length at most \(\sigma\) in models of size at least
\(t(\sigma)\) have canonical diagrams. Equality of diagrams is
preserved by every strong embedding between such models, and there
are at most \(B_\sigma\) diagrams at these lengths.
\item Diagrams include atomic diagrams, respect reindexing and
restriction, and are compatible when the bound \(\sigma\) is
increased. We denote equality by \(D(a;M)=D(b;N)\), suppressing the
bound when it is understood.
\item If \(\kappa\ge t(\sigma)\) is a categoricity cardinal, equality
of diagrams between tuples in \(\kappa\)-models is implemented by
a strong map between those models.
\item A possible diagram of a pair of tuples \((a,c)\), of total
length at most \(\sigma\), can be realized over any tuple with the
diagram of \(a\) in any categoricity model of size at least
\(t(\sigma)\). ``Possible'' means that the diagram occurs in a
model in the domain of its definition.
\end{enumerate}
\end{proposition}

\begin{proof}
If \(\gamma\ge\kappa\) are categoricity cardinals above the reversal
threshold, Lemma~\ref{lev:canonical-classes} associates a
\(\kappa\)-class to every \(\gamma\)-class. This gives a projection
\(\pi_{\gamma\kappa}\), and these projections compose. They are
surjective. Indeed, a \(\kappa\)-model is isomorphic to \(E(I)\) for
\(|I|=\kappa\); extend \(I\) to an order of size \(\gamma\) and use
the strong order map. Every tuple class in the smaller model then
occurs in the larger one. This argument supplies the needed extension
without a no-maximal-model assumption.

These projections are eventually all bijective. Otherwise, construct
a sequence of categoricity cardinals with more than \(B_\sigma\)
successive noninjective projections, and choose one final
categoricity cardinal \(\rho\) above the entire sequence. For each
noninjective projection, surjectivity supplies a pair of
\(\rho\)-classes which agree when projected to the earlier stage and
differ when projected to the later stage. Pairs selected at distinct
stages are distinct: after a pair has separated it remains separated
under every later refinement. This gives more than
\(B_\sigma\) pairs from a set of size at most \(B_\sigma\), a
contradiction. The construction uses only a set-length sequence of
cardinals and choices from sets.

Choose a categoricity cardinal \(c_\sigma\) beyond this stabilization
and reversal threshold. The canonical \(c_\sigma\)-class defines
the desired diagram on models of size at least \(c_\sigma\).
The bijective projections show that its equality can equally be
computed at every later categoricity cardinal. If two tuple bounds
are used, compare them at a categoricity cardinal above both
thresholds. Restriction of strong maps then gives the same
restricted equivalence. Atomic formulas and their negations are
preserved because strong maps are structure embeddings.

For definiteness, thresholds can be chosen as least cardinals having
the stated eventual properties. Choose \(t(\sigma)\) to be the
least categoricity cardinal strictly above \(\ell+\sigma\) and
above all the thresholds \(c_\tau\) for infinite \(\tau\le\sigma\).
This is a nondecreasing definable function. The preceding arguments
prove the first three assertions.

For the fourth, first put a realization of \((a,c)\) into a strong
\(c_\sigma\)-submodel. If the originally chosen ambient size is
smaller than a desired target categoricity size, this categorical
submodel can be extended to that size by the order presentation.
If the original ambient size is larger, LS gives a submodel of the
desired size containing the realization. Thus the joint diagram
has a realization in a model of the target categoricity size.
Apply the third assertion to the first tuple and the specified tuple
in the target. The resulting strong map transports the whole
realization as required.
\end{proof}

\begin{proposition}[Categoricity at countably cofinal closure points]
\label{lev:closure-categoricity}
Suppose \(\zeta>\ell\) is an infinite cardinal of countable
cofinality and
\[
 t(\sigma)<\zeta\qquad\text{for every infinite }\sigma<\zeta.
\]
Then \(\K\) is categorical in \(\zeta\). Moreover any diagram match
between bounded tuples in two \(\zeta\)-models extends to an
isomorphism between those models. Here and throughout the paper,
bounded at a level means of cardinality strictly less than that level.
\end{proposition}

\begin{proof}
Existence follows from \(E(I)\) for \(|I|=\zeta\). Let \(M,N\)
have size \(\zeta\), and choose countable increasing exhaustions of
their underlying sets by sets of size less than \(\zeta\).
Start with the prescribed bounded diagram match, or with the empty
match. At a forward step, enumerate together the current source
tuple and the next part of the exhaustion of \(M\). Its length and
the length of the current target tuple are bounded by an infinite
\(\sigma<\zeta\). Put the data on each side inside a strong
submodel of size \(t(\sigma)<\zeta\). Their current tuples have
the same diagram. Proposition~\ref{lev:stabilization} gives a
strong map of these submodels matching those tuples. Its values
on the new entries extend the match, and the enlarged tuples
again have equal diagrams. At the next step interchange \(M,N\).

Only finitely many previously chosen bounded tuples are used at
each step, so their combined length stays below \(\zeta\).
The union of the countable sequence of partial matches is a
bijection \(|M|\to|N|\). Every finite tuple and every value of a
finitary function occur at some step, where the atomic diagram
is preserved. The bijection is therefore a structure isomorphism.
\end{proof}

The closure cardinals in Proposition~\ref{lev:closure-categoricity}
are unbounded. For example, starting above any specified cardinal,
choose a strictly increasing sequence \((\alpha_n:n<\omega)\)
such that \(\alpha_{n+1}\) exceeds all \(t(\sigma)\) for
\(\sigma\le\alpha_n\). Its supremum has the required closure and
countable cofinality. Including \(2^{\alpha_n}\) in these requirements
makes the supremum a strong limit. We will use these stronger
closure points below.

\subsection{Natural diagrams and interchange of blocks}

\begin{definition}[Natural and placed diagrams]
\label{lev:natural-diagrams}
Consider a set-sized list of terms in an order presentation. Each
term consists of a label and an increasing finite list of positions.
Extend the order to size at least the threshold for the list and
compute its diagram there. The result is its \emph{natural diagram}.
If \(A=E(I)\), a \emph{placement} of an additional tuple \(d\)
over \(A\) is a labeled representation in an order extension of
\(I\), retaining the positions and chosen representations of the
parameters in \(A\). Its \emph{placed comparison over \(A\)} is
the natural diagram of \((d,a_A)\), where \(a_A\) is a fixed
enumeration of \(A\).
\end{definition}

The natural diagram is independent of the extension used. Indeed,
linear orders amalgamate over a common suborder: for each cut of
the suborder, place the remaining portions of the two orders in
that cut while preserving each portion's order. Extending the
amalgam further if necessary gives a common sufficiently large
presentation. Strong order maps and
Proposition~\ref{lev:stabilization} identify the two diagrams.
The same argument shows that only the labels and the joint
order/equality pattern of their supports matter. All diagrams
with parameters use matching parameter enumerations. One may
instead list all labels on the base order, allowing repetitions:
restriction gives an enumeration of the elements, and reinserting
the repetitions is forced by their equalities.

A placed comparison over a whole \(\mu\)-model is evaluated in a
sufficiently large presentation. It is not, by this definition,
an assertion that the original \(\mu\)-model itself lies above the
threshold for diagrams of length \(\mu\).

\begin{lemma}[Orbits over parameters]
\label{lev:parameter-orbits}
Let \(\sigma\) be infinite and suppose
\[
 \chi^\sigma=\chi,
 \qquad \chi\ge \ell+2^{2^\sigma}.
\]
At every sufficiently large categoricity cardinal, there are at
most \(\chi\) automorphism orbits of \(\sigma\)-tuples over any
specified set of at most \(\chi\) parameters.
\end{lemma}

\begin{proof}
Present the categoricity model as \(E(H(\delta))\), choosing
\(|\delta|\) to be its cardinality and \(\cf(\delta)>\chi\).
This is possible at every sufficiently large cardinal, including
singular cardinals. Fix term representations of the parameters,
and let \(S\subseteq H(\delta)\) be their support set. Its size
is at most \(\chi\). Every member of \(S\) is coded by a finite
list of ordinals and integer and rational coefficients. The union
of its ordinal supports consequently also has size at most
\(\chi\).

For one further position, its finite ordinal support has at most
\(\chi\) possible order/equality patterns over these old ordinal
supports. The discrete coefficients contribute only countably
many choices for each finite code. Such a pattern determines
all comparisons of the new position with \(S\). For at most
\(\sigma\) new positions, include their mutual comparisons,
their identifications with old positions, and the term labels.
There are at most \(\chi^\sigma=\chi\) choices so far.

To apply Theorem~\ref{found:order-orbits}, also record which strict
slots over the old and new positions are realized in
\(H(\delta)\). The old support \(S\) is fixed. A slot over \(S\)
not containing a new position is unchanged. At most \(\sigma\)
old slots contain new positions, and inside each there are at
most \(2^\sigma\) cuts of the new support to test. The new flags
therefore have at most \(2^{2^\sigma}\le\chi\) possible values.
The full record has at most \(\chi\) possibilities.

The combined list of old and new positions has size at most
\(\chi<\cf(\delta)\). Theorem~\ref{found:order-orbits} extends
equality of full records to an order automorphism fixing \(S\)
pointwise. Its induced automorphism of the presentation fixes
the parameters and matches the tuples. Thus the number of
structure-automorphism orbits is at most the number of records.
\end{proof}

\begin{lemma}[Disjoint block transpositions]
\label{lev:block-transpositions}
Take two set-sized families of labeled terms. In disjoint convex
regions of their joint support order, suppose each region consists
of two adjacent blocks, one used only by the first family and one
only by the second. Interchange the blocks in every such region,
retaining their internal orders and all positions outside the
regions. The joint natural diagram is unchanged.
\end{lemma}

\begin{proof}
Suppose the original and modified diagrams were different. Let
\(\sigma\) bound the two lists, their supports, and the shared
positions. Choose \(\chi\ge\ell+2^{2^\sigma}\) with
\(\chi^\sigma=\chi\), for instance by taking a sufficiently
large power of two.

In each region repeat the pair of blocks along an arbitrary
linear order \(L\). If the first family's block was on the left,
use the order \(L\) for the repetitions; if it was on the right,
use the reverse of \(L\). Write \(d_i\) for the first-family
tuple using the blocks at index \(i\), and \(e_j\) for the
second-family tuple using the blocks at index \(j\); retain all
the shared positions outside the regions. For \(ij\)
it is the modified one. Comparisons within either family and
across distinct regions do not change.

Let \(\epsilon\) be the least infinite cardinal satisfying
\(2^\epsilon>\chi\). The binary tree \(2^{<\epsilon}\) has
at most \(\chi\) nodes: for \(\alpha<\epsilon\) each level has
size at most \(\chi\), and \(\epsilon\le\chi\). Give it
lexicographically ordered divider points, one between the two
successor subtrees at each node. Explicitly, encode branch
digits by \(-1,1\), and encode the divider at a node \(s\)
by the sequence \(s\) followed by \(0\), using
\(-1<0<1\) in lexicographic comparison. Adjoin one point for every
branch in \(2^\epsilon\). Distinct branch points determine
distinct strict cuts over the divider points. Use this as the
order \(L\).

The tuples \(e_j\) at the divider indices, together with the
fixed shared data, use at most \(\chi\) parameters. If two
branch-indexed tuples \(d_i\) were in the same automorphism
orbit over these parameters, their diagrams with every divider
tuple would agree. A divider between the two branches gives
the two different diagrams, a contradiction. Hence there are
more than \(\chi\) such orbits. Pad the constructed order to a
sufficiently large categoricity size and apply
Lemma~\ref{lev:parameter-orbits}. This is impossible.
\end{proof}

\subsection{Bounded tests over a well-ordered presentation}

The next elementary set-theoretic observation will also be used for
the more elaborate layouts of later sections.

\begin{lemma}[Ordinal-vector witnesses]
\label{lev:ordinal-vectors}
Let \(C\) be a set, and let \(U\) be a definable class of functions
\(C\to\Ord\), with fixed set parameters allowed in its definition.
There is a set \(U_0\subseteq U\) such that each \(u\in U\)
dominates some \(v\in U_0\) coordinatewise.
\end{lemma}

\begin{proof}
The assertion is immediate if \(C\) is empty or \(U\) is empty.
Well-order \(C\), and suppose no such set exists. For every
ordinal \(\beta\), the set \(U\cap V_\beta\) fails to generate
\(U\) upwards. There is therefore an element of \(U\) which
dominates none of its members. Let \(h(\beta)>\beta\) be the
least ordinal such that one such witness lies in \(V_{h(\beta)}\).
This is a definable ordinal function.

Take an ordinal length \(\lambda\) satisfying the partition
relation for pairs, \(|C|\) colors, and an infinite homogeneous
set, supplied by Lemma~\ref{found:partition}. Define increasing
ordinals \(\beta_i\), for \(i\le\lambda\), recursively, with
\(\beta_{i+1}>h(\beta_i)\) and with limit values above all earlier
values. Choice for a set-indexed collection of nonempty subsets
of \(V_{\beta_\lambda}\) now selects witnesses \(u_i\) which
dominate no member of \(U\cap V_{\beta_i}\), for \(i<\lambda\).
For \(iu_j(c)\). Color the pair \(i\ell+\sigma\) satisfy \(\chi^\sigma=\chi\). Suppose that
for every \(X\subseteq A\) of size at most \(\chi\) a possible
joint diagram \(q_X(d,X)\) is prescribed, where \(d\) has length
at most \(\sigma\). Assume these prescriptions restrict
coherently and that their parameter diagrams are the natural
ones of \(X\). Then one placement of \(d\) over \(I\) realizes
all the prescriptions.
\end{proposition}

\begin{proof}
Fix one term representation per parameter in \(A\). Write
\(S_X\subseteq I\) for the supports of \(X\). For one set
\(X\), its prescription has a placement. To see this, extend
\(I\) to a sufficiently large categoricity size and use
Proposition~\ref{lev:stabilization} to realize the possible
joint diagram over the actual parameter tuple. The realization
has term representations in that presentation.

A support profile over \(X\) records the labels for \(d\),
its formal support order \(T_0\) of size at most \(\sigma\),
and comparisons and coincidences with \(S_X\). A well-order
of size at most \(\chi\) has at most \(\chi\) cuts. Hence
there are at most \(\chi^\sigma=\chi\) profiles. The positions
of \(T_0\) in one strict slot over \(S_X\) form a cluster.
Each profile has a continuation over \(I\) which leaves
every such cluster intact: insert the cluster at a single
cut of \(I\) extending its specified cut over \(S_X\).

Call a hit of a new parameter support on \(T_0\), or the
separation of two positions in one cluster by a new parameter
support, a new event. For \(X'\supseteq X\), all continuations
of a profile with no new event over \(S_{X'}\) have the same
natural diagram over \(X'\). Within each old slot, the whole
cluster can only change its position across a block of new
parameter positions. The slots are disjoint, so
Lemma~\ref{lev:block-transpositions} applies simultaneously.

Suppose no placement solves all the prescriptions. Start with
any \(X_0\) of size at most \(\chi\). Given \(X_i\), choose
for every profile over \(X_i\) a continuation with no new
event over all of \(I\). It fails a prescription on some set
of at most \(\chi\) parameters. Adjoin one such failing set
for each profile to obtain \(X_{i+1}\). At limits take unions,
and carry out \(\sigma^+\) stages. Every set constructed,
including \(X_* = \bigcup_{i<\sigma^+}X_i\), has size at most
\(\chi\), because \(\sigma^+\le\chi\).

Take a placement realizing \(q_{X_*}\). At each stage its
profile over \(X_i\) was considered. If it had no new event
between \(S_{X_i}\) and \(S_{X_{i+1}}\), the preceding
no-event comparison would identify its diagram on the
selected failing set with that of the chosen continuation.
This contradicts its realization of \(q_{X_*}\). Thus it
has a new event at every stage. A support position can be
newly hit only once, and a pair can be newly separated only
once. There are at most \(\sigma+\sigma^2=\sigma\) such
events. They cannot occur at \(\sigma^+\) different stages.
\end{proof}

\begin{lemma}[Unique lifts of bounded diagrams]
\label{lev:placed-lifts}
Let \(\mu>\ell\) be a strong-limit cardinal of countable
cofinality strictly closed below itself under \(t\) and \(g\).
Let \(A\le_\K B\) have size \(\mu\), and identify
\(A=E(I)\) for a well-order \(I\) of size \(\mu\). For a
tuple \(d\) in \(B\) of length at most \(\sigma<\mu\), the
diagrams
\[
 D(d,X;B),\qquad X\subseteq A,\quad |X|<\mu,
\]
lift to one placed comparison over all of \(A\), uniquely
as a comparison diagram. Restricting a lifted tuple gives
the lift of its restricted diagram.
\end{lemma}

\begin{proof}
The displayed bounded diagrams are defined, since their
thresholds lie below \(\mu\), and they agree on the parameters
with the natural diagrams. For every sufficiently large
\(\chi<\mu\) with \(\chi^\sigma=\chi\),
Proposition~\ref{lev:compact-placement} gives a placement
realizing the tests of size at most \(\chi\). Such \(\chi\)
are cofinal below \(\mu\): use \(\chi=2^\alpha\) for
\(\sigma\le\alpha<\mu\), enlarging \(\alpha\) as necessary.

Once \(\chi\ge g(\sigma)\), any two resulting placements
have the same full comparison by Proposition~\ref{lev:testing}.
Fix one of them. Every bounded test is covered by a larger
choice of \(\chi\), whose placement has that same full
comparison. The fixed placement consequently realizes every
bounded test. The same argument gives uniqueness. A
restriction realizes the restricted tests and hence, by
uniqueness, is their lift.
\end{proof}

\subsection{Amalgamation and type counts}

\begin{theorem}[Amalgamation at closed levels]
\label{lev:amalgamation}
There is an unbounded class of strong-limit cardinals \(\mu\)
of countable cofinality with the following properties.
\begin{enumerate}
\item \(\K\) is categorical in \(\mu\), and any two
\(\mu\)-sized strong extensions of a \(\mu\)-model have a
strong amalgam of size \(\mu\).
\item If \(A\le_\K B_0,B_1\) all have size \(\mu\), and
\(d_i\in B_i\) are tuples of the same length at most
\(\sigma<\mu\), there is such an amalgam identifying
\(d_0\) with \(d_1\) if and only if
\[
 D(d_0,X;B_0)=D(d_1,X;B_1)
 \quad\text{for every }X\subseteq A,
 \quad |X|\le g(\sigma).
\]
\item There are at most \(\mu\) singleton types over each
\(\mu\)-model, where type means identification in an amalgam
over that model.
\end{enumerate}
One may take every sufficiently large strong-limit cardinal
of countable cofinality strictly closed under \(t\) and \(g\).
\end{theorem}

\begin{proof}
Such levels are unbounded by the countable closure construction
following Proposition~\ref{lev:closure-categoricity}.
Categoricity at them has already been proved. Identify a
given base with \(A=E(I)\), where \(I\) is a well-order of
size \(\mu\). Extend \(I\) to an order \(J\) whose cardinality
\(\gamma\) is a categoricity cardinal at least \(t(\mu)\),
and let \(G=E(J)\). Thus \(A\) is strongly included in its
specified position in \(G\).

We show that every \(\mu\)-sized strong extension \(B\) of
\(A\) embeds strongly into \(G\) over \(A\). Choose
\(M_n\le_\K B\), increasing with union \(B\), with
\(\|M_n\|<\mu\). This follows by LS from a countable
exhaustion of \(B\), containing the preceding submodel at
each step; coherence makes the chain strong. Choose compatible
enumerations \(d_n\) of these models, so that each earlier
list is a sublist of the next.

Lemma~\ref{lev:placed-lifts} assigns coherent placed comparisons
to \((d_n,A)\). Each is realized over \(A\) in \(G\), and
the realizations can retain the previous assignments. More
explicitly, realize the corresponding term pattern in an
order extension of size \(\gamma\). Its parameter tuple
\(A\), and then its tuple \((A,d_{n-1})\), have the same
diagram as the already assigned ones. Their length is at
most \(\mu\), so Proposition~\ref{lev:stabilization} at
\(\gamma\ge t(\mu)\) supplies the strong map realizing the
new list while fixing these previous data.

It remains to verify strongness of the copied small models;
atomic agreement by itself would not suffice. Fix \(n\),
and bound the length of \(d_n\) by an infinite
\(\sigma_n<\mu\). Choose the categoricity cardinal
\(\rho=t(\sigma_n)<\mu\). LS puts the original enumeration
inside \(B_n'\le_\K B\) of size \(\rho\), and the copied
enumeration inside \(G_n'\le_\K G\) of that size. Coherence
gives \(M_n\le_\K B_n'\). The copied and original lists
have the same bounded diagram; Proposition~\ref{lev:stabilization}
gives a strong map \(B_n'\to G_n'\) with exactly the prescribed
values on \(d_n\). Its restriction shows that the copied
\(M_n\) is a strong submodel of \(G\).

The copied models are nested, and coherence makes their
inclusions strong. Their union is a strong submodel of \(G\)
by the chain and common-upper-bound axioms. It is the image
of an embedding of \(B\). Every element of \(A\) eventually
occurs in some \(d_n\), and its equality with that parameter
is part of the lifted comparison. The embedding therefore
fixes \(A\). Performing this construction for \(B_0,B_1\)
in the same \(G\) gives an amalgam. LS supplies a strong
\(\mu\)-submodel of \(G\) containing both images; coherence
makes it a strong amalgam of the required size.

For the second assertion, any identifying amalgam preserves
the displayed bounded diagrams, giving necessity. Conversely,
Proposition~\ref{lev:testing} identifies the placed lifts
of \(d_0,d_1\) over \(A\). Realize this common lift once
in \(G\). On each side start the preceding countable
construction with the specified tuple already assigned,
and choose every small-model enumeration to contain that
tuple. Homogeneity over \(A\) and the old assignments works
exactly as above. The two resulting embeddings identify the
tuples, and the same LS shrinking applies.

For a singleton, a placement uses one label on a finite
support. Relative to the well-order \(I\), each support
position is either an old position or lies in one of its
\(|I|+1\) cuts. Together with the finitely many mutual
comparisons and the label, these data have at most
\(\mu\) possibilities. They determine the full natural
comparison. The second assertion identifies exactly the
types with equal comparison, proving the bound.
\end{proof}

Amalgamation has thus been obtained at the stated levels from the
AEC axioms and unbounded categoricity. We have not assumed that
all models of intermediate cardinalities amalgamate. The next
section records precisely the level-by-level properties that
will be required of later categories of finite systems.
==== END Eventual-Categoricity-for-Abstract-Elementary-Classes//04-diagrams.tex ====

==== BEGIN Eventual-Categoricity-for-Abstract-Elementary-Classes//05-working-schemes.tex ====
\section{Working schemes and uniform comparison of diagrams}
\label{lev:section-working-schemes}

We isolate the conditions used when the preceding constructions are applied
to finite systems of models.  The definition includes the hypotheses that
must be checked for a new system; it does not infer them merely from
categoricity of its vertices.

\subsection{Systems and the working package}

\begin{convention}[Closure below a level]
\label{lev:level-convention}
An eligible level is an infinite cardinal belonging to the class of
cardinals on which the particular construction under consideration has
been established.  Except when explicitly discussing preliminary levels,
we use strong limit levels of countable cofinality.  A list is
\emph{bounded at $\mu$} if its cardinality is strictly less than $\mu$.
If $u$ is a cardinal-valued function, strict closure under $u$ means
\[
  u(\theta)<\mu
  \qquad\text{for every infinite cardinal }\theta<\mu.
\]
Bounds may include fixed parameters, may be increased to infinite
cardinals, and may be replaced by monotone majorants.
\end{convention}

A system has finitely many vertices, each a $\K$-model, and specified
maps between specified vertices.  We code it as a many-sorted structure,
with one sort for each occurrence of a vertex and function symbols for
the specified maps.  An element occurring in two vertices therefore
has two occurrences in the code, related by the specified map when
appropriate.  Distinguished lists are coded by names.  A system
embedding consists of commuting embeddings on its vertices, preserving
these names.  An \emph{arrow} is such an embedding whose vertex maps are
strong, together with any additional condition stated for the scheme.
The geometric application will have one such additional condition.
No condition on intersections of images is implicit in this definition.
An isomorphism means a structural isomorphism onto the entire system.

\begin{definition}[Working package]
\label{lev:working-package}
Fix an unbounded definable class $S$ of eligible levels, a finite system
shape, and a set-sized finite-support term template $F$.  A
\emph{working scheme} consists of classes $\mathcal C_\mu$, for $\mu\in S$,
arrows between their objects, and comparisons $D$ of bounded lists,
with the following properties.  Every vertex of an object in
$\mathcal C_\mu$ has cardinality $\mu$.
\begin{enumerate}
\item \emph{Structural arrows and unions.}
Arrows include all structural isomorphisms, compose, and are invariant
under isomorphisms.  They are coherent: if $X$ is a subsystem of $Y$,
and both inclusions into $Z$ are arrows, then $X\to Y$ is an arrow.
For an increasing nonempty chain of objects at level $\mu$, whose
union has total cardinality $\mu$, the union is an object at that level
and the inclusions into it are arrows.  If all members of the chain
map by the inclusions into one object $Z$ at an eligible level
$\nu\geq\mu$, then the inclusion of the union into $Z$ is an arrow.

\item \emph{Presentations and mixed downward closure.}
For every well-order $I$ of eligible cardinality $\mu$, $F(I)$ is an
object of $\mathcal C_\mu$.  Its elements are represented by labels
applied to finite increasing lists from $I$; equality, the symbols of
the system structure, and the specified maps are evaluated from the
labels and the finite order and equality patterns.  Substitution of
positions along an order embedding induces an arrow, including when
the source and target levels differ.  Every object at a level is
isomorphic to a well-ordered presentation.  If $\nu\leq\mu$ are eligible
and $A$ is a set of at most $\nu$ vertex occurrences in an object of
level $\mu$, there is an arrow inclusion of an object of level $\nu$
containing $A$.  Fixed distinguished data are included in this request.

\item \emph{Diagrams, homogeneity, and saturation.}
For each index set of bounded cardinality there is an equivalence
relation, denoted by equality of $D$-diagrams, on the corresponding
lists in all eligible objects large enough for that index set.
It includes the atomic diagram of the entire coded system, respects
restrictions and reindexing, and sends every list to a $D$-equal list
under every arrow, including mixed-level arrows.  At each level,
two bounded lists have the same diagram if and only if a structural
isomorphism between their objects takes one list to the other.
The number of diagrams at a fixed arity has a set-sized bound
independent of the level.  A possible joint diagram of bounded length
extending the diagram of an actual bounded list is realized over that
list at its level.  Here ``possible'' includes a diagram witnessed at
any larger eligible level, provided the total requested length is
bounded at the receiving level.  On term lists diagrams are natural:
they depend only on labels and the order and equality pattern of all
positions used, including in comparisons between eligible levels.

\item \emph{Exhaustion criterion for arrows.}
Suppose a map is obtained from compatible diagram matches on increasing
bounded lists which exhaust its domain object.  Include in these lists,
for every vertex $V$, nested enumerations of strong submodels
$V_n\leq_\K V$ of sizes below the source level, with union $V$.
The image of each such enumeration must enumerate a strong submodel
of the corresponding target vertex.  Under these conditions the map
is an arrow.  Component strongness follows from the chain union and
common-upper-bound axioms of $\K$; an additional arrow condition, when
present, must be proved for this construction separately.
\end{enumerate}
The empty list is included in the third condition, and has one
diagram.  Consequently all objects at any one eligible level are
isomorphic.
\end{definition}

The mixed downward assertion in the second condition usually needs no
separate construction.  In a chart for the large object, choose finite
supports for the requested occurrences.  Their union has size at most
$\nu$; enlarge it to a suborder of size $\nu$ and use the presentation
arrow.  If an already given small object is also to be included, put
supports for all its occurrences into the request and use coherence.

The assertion about images of small strong submodels in the fourth
condition is also a precise obligation, rather than a claim that
arbitrary structural embeddings are strong.  At one level it follows
when the bounded enumeration is carried by a diagram match, since that
match is implemented by an isomorphism of the containing objects.
For a mixed-level use, first place the smaller containing object in a
large presentation by an order arrow.  Diagram preservation and an
isomorphism at the receiving level then show that the matched small
submodel has strong image.  Finally, the union of these strong images
is strong in the target by the common-upper-bound clause.  This proves
the componentwise part of the criterion in precisely the situations
in which it will be used.

\subsection{Refining the eligible levels}
\label{lev:refining-levels}

The later scheme constructions refine the class of levels on which the working
package is available. The following hypothesis ensures that the required
refinements still leave an unbounded supply of levels.

Here and below every bound being closed under is given by a fixed
set-theoretic definition with set parameters.  To see the elementary
closure construction explicitly, start above a prescribed cardinal and
choose strictly increasing infinite cardinals $\kappa_n$ such that
\[
 \kappa_{n+1}>2^{\kappa_n}
 \quad\text{and}\quad
 \kappa_{n+1}>
 \sup\{u_i(\theta):\theta\leq\kappa_n,\ i\in A\},
\]
where $A$ is the fixed set of functions to be accommodated.  Replacement
makes the displayed supremum a set-sized ordinal.  The cardinal
$\mu=\sup_{n<\omega}\kappa_n$ has countable cofinality, is a strong limit,
and is strictly closed under every $u_i$.

There are two distinct uses of this observation.  If a theorem proves
its conclusion at every such closure point, it establishes eligibility
of $\mu$.  If eligibility is already restricted to an unbounded class
$S$, closing under the least member of $S$ above $\theta$ ensures only
that $S\cap\mu$ is unbounded in $\mu$; it does not by itself prove
$\mu\in S$.  Membership at the limiting cardinal must come from the
relevant theorem or from an already established closure property of
$S$.  In particular, if $S$ is unbounded and closed under suprema of
strictly increasing countable sequences, we may choose the $\kappa_n$
inside $S$ in the construction above.  The resulting $\mu$ then belongs
to $S$ and has cofinally many smaller members of $S$.  This is the
meaning of requiring sufficiently many smaller eligible levels; an
arbitrary unbounded class of cardinals is not silently assumed to have
this property.

\begin{convention}[Supply of eligible levels]
\label{lev:eligible-subclass}
For the generic scheme refinements below, we use the following
\emph{eligible-subclass hypothesis} whenever an unbounded class of
refined levels is asserted.  The input eligible class $S$ must contain
a fixed definable unbounded subclass $T$ closed under suprema of
strictly increasing countable sequences.  In addition to the input
scheme's individual conditions, this is a hypothesis on the supply
of eligible levels; arbitrary unboundedness of $S$ does not imply it.
\end{convention}

This hypothesis persists through every finite list of the stated
refinements.  For a fixed definable bound function, choose successive
members of $T$ beyond all its values on the ordinals below the previous
member, and take their countable supremum.  This gives arbitrarily
large members of $T$ strictly closed under that bound.  The intersection
with the bound-closure class is still closed under strictly increasing
countable suprema.  A threshold only removes an initial segment.
For a limit-point refinement of a current class containing such a $T$,
use $\{\mu\in T:\sup(T\cap\mu)=\mu>0\}$; it is unbounded and has the same countable closure,
and is contained in the required limit-point class.  Repeat for the
finite refinement list, including the finitely many bound functions
then required.  Thus an unbounded subclass with the same property
remains available, including for larger auxiliary-level choices.

\paragraph{Advance notation for common levels.}
\label{lev:closure-preview}
For a definable class $A$ of ordinals, write
\[
 \Lim(A)=\{\mu:\sup(A\cap\mu)=\mu>0\}.
\]
Here is the hierarchy that will organize the two applications of
Section~\ref{close:section-uniform}.  That section constructs one fixed
bound majorant $\Phi$ for each application.  Its initial class $G_0$
consists of the strong limit cardinals $\mu$ of countable cofinality with
$\Phi(\alpha)<\mu$ for every ordinal $\alpha<\mu$; subsequent classes are
\[
 G_{j+1}=G_j\cap\Lim(G_j)\quad(j<\omega),
 \qquad G_\omega=\bigcap_{j<\omega}G_j.
\]
This is advance notation: the definition of $\Phi$ and the proof that
each $G_j$ is unbounded and closed under strictly increasing countable
suprema are given in that section.  A member of $G_{j+1}$ is thus both
a member of $G_j$ and a limit of smaller members of $G_j$.

In those applications, the input class contains $G_j$ for some finite
$j$.  This subclass serves as $T$, and the finite refinements retain a
later $G_k$.  These subclasses supply the required levels; they are not inserted as
additional class parameters into the definitions of bounds. Those
definitions, given in Section~\ref{close:section-uniform}, use fixed
formulas for the required working assertions and for the finite
refinements already described.  Without the eligible-subclass hypothesis, the generic
proofs assert their conclusions at levels satisfying their displayed
bound and limit-point requirements, but do not assert that those
levels are unbounded.

\subsection{Directed unions and rich orders}

\begin{lemma}[Directed unions and padded presentations]
\label{lev:directed-unions}
Assume the structural union and presentation conditions of
Definition~\ref{lev:working-package} at a level $\mu$.
Every nonempty directed family of inclusion subobjects at that level,
whose union has total cardinality $\mu$, has an object as its union,
with arrow inclusions and the common-upper-bound conclusion, including
into an eligible larger level.

Consequently $F(I)$ is an object whenever $I$ has eligible cardinality
$\mu$ and contains a well-ordered subset of cardinality $\mu$.
We call such an order \emph{padded}.  Order embeddings between padded
orders induce arrows, also between different eligible levels.
If the diagram conditions of the package hold, diagrams on bounded
term lists in padded orders are natural as well.
\end{lemma}

\begin{proof}
We first prove the directed assertion by induction on the cardinality
of an indexing set.  A finite directed family has a member containing
all its members.  A countable directed family has a cofinal increasing
sequence, obtained by successively choosing an upper bound for the
previous choice and the next enumerated member.  The chain assertion
gives its union and its common-upper-bound property.

For an uncountable indexing cardinal $\tau$, fix a binary operation on
the indexing set selecting an upper bound for each pair.  Write the
indexing set as an increasing union of sets of size less than $\tau$,
and close each under this operation.  This closure adds only countably
many stages and preserves the bound of being smaller than $\tau$.
The sets can be chosen nested, and their union is the whole indexing
set.  By the inductive assertion each corresponding smaller directed
family has an object as its union.  That union still has cardinality
$\mu$: it contains a member of cardinality $\mu$ and is contained in
the given total union of cardinality $\mu$.  The common-upper-bound
part of the inductive assertion makes these unions a chain of arrows.
The chain assertion now gives the total union.  Applying the same
common-upper-bound clauses to a specified ambient object proves the
last assertion, including the mixed-level version.

Fix a well-ordered subset $J_0\subseteq I$ of size $\mu$.  Let
$\mathcal J$ consist of all well-ordered subsets of $I$ of size $\mu$.
A union of two well-ordered subsets is well-ordered: in any nonempty
subset take the smaller of the minima supplied by its two nonempty
intersections.  Thus $\mathcal J$ is directed under inclusion.  Every
finite subset of $I$ is contained in a member, namely its union with
$J_0$.  The finite-support description of the template identifies
\[
                  F(I)=\bigcup_{J\in\mathcal J}F(J).
\]
The union has cardinality $\mu$, and the directed assertion applies.
For an order embedding $I\to I'$, first restrict to well-ordered
suborders of the source.  Their images are well-ordered; if necessary,
enlarge each image by a padding subset in the target.  The known order
arrows and the common-upper-bound assertion give the induced map on
the total union as an arrow.

Finally, two occurrences of the same bounded support pattern in
orders can be identified by amalgamating the orders over that
suborder.  Such an amalgamation is obtained cut by cut: retain the
common suborder and put the points from each of the two orders in
their prescribed cuts, keeping their own orders within each cut.
Append a well-order of sufficiently large eligible cardinality to
make the amalgam padded.  The two order arrows identify the term
lists there.  Diagram preservation proves their naturalness.
\end{proof}

When the chain assertion for a newly defined scheme is still being
proved, the lemma is used only for an underlying scheme whose chain
assertion has already been established.  Directed unions are not used
to presume the assertion under proof.

\begin{lemma}[Rich padded orders]
\label{lev:rich-orders}
Let $\eta$ be infinite.  There is a dense linear order $Q_\eta$ without
endpoints of cardinality $2^\eta$ such that every cut given by at most
$\eta$ parameters on either side is filled.  Equivalently, every
extension of an order pattern with at most $\eta$ old and at most
$\eta$ added positions can be realized over its old positions.
If $\mu$ is a strong limit cardinal and $\eta<\mu$, there is a padded
order with these properties of cardinality $\mu$.  No restriction on
$\cf(\mu)$ is needed for this assertion.
\end{lemma}

\begin{proof}
Put $\xi=2^\eta$, so that $\xi^\eta=\xi$ and $\eta^+\leq\xi$.
Starting with an order of size $\xi$, repeatedly fill every cut
specified by disjoint sets $A|F|+\beta$.  The diagram of $c$ has a witness
at $\alpha$.  If its original witness is at a larger level, use
saturation at $\alpha$ with the empty tuple as base.  If its witness
is at a smaller level, first extend that object to a presentation
at a level at least $\alpha$ using an order arrow.  This gives a
choice of $\alpha$ uniform over all diagrams of the specified arity.
Choose a well-ordered chart for this new witness and fix
representations of $c$.  Let $J$ be the union of their finite supports, with its inherited
well-order.  In the presentations $F(J+H)$ name the terms representing
$c$ on $J$.  Regard this as a template in the variable order $H$:
any term using positions from both parts becomes a label recording
its original label and its finitely many fixed positions from $J$,
applied to its remaining positions from $H$.  Terms supported wholly
on $J$ are labels of arity zero.  The new collection of labels has
cardinality at most $|F|+|J|+\aleph_0$ and is fixed independently of
the level.  Order maps on $H$, extended by the identity on $J$,
induce arrows preserving the names.

Naturality gives the prescribed diagram on the named list in every
sufficiently large such presentation.  Homogeneity for $c$ shows
that every object with such a named realization is isomorphic to one
of these presentations.
Define its diagram on a further list $a$ to be the old diagram on
the combined list $(c,a)$.  The old package gives exactly restriction
compatibility, the uniform bound, preservation, homogeneity, and
saturation for these diagrams.  The same support construction gives
mixed downward closure, now including the named terms.  Chain unions
and the exhaustion criterion retain the names, so they are inherited.

For the final assertion suppose a sublist enumerates
$M\leq_\K V$ in the original witness, which may be at a level
larger than $\alpha$.  Embed that original system and the new
level-$\alpha$ witness into objects of a common larger eligible
level.  Mixed preservation and homogeneity there give an
isomorphism matching their named lists.  The original copy of $M$
has strong image in that large vertex.  This image is exactly the
substructure enumerated inside the embedded level-$\alpha$ vertex,
so coherence makes it strong in that vertex as well.  It is a
$\K$-model because its complete atomic enumeration is isomorphic
to $M$.  Thus strong naming already holds in the uniformly small
witness.  Above $\alpha$, order arrows and the same homogeneity
argument preserve it.  The argument applies to every named
vertex model and specified map.
Thus the new presentations satisfy the intended strong naming
condition, not just the atomic diagram of the enumeration.
\end{proof}

\subsection{Two routes to working diagrams}

The next statement records the exact diagram input that may be used
for a new scheme.  In its first route the role of
Theorem~\ref{found:reversal} is an explicit hypothesis; it is not
assumed for a new category without proof.

\begin{proposition}[Obtaining the diagram clause]
\label{lev:scheme-diagram-routes}
Suppose a finite-system scheme has the structural and presentation
conditions of Definition~\ref{lev:working-package}, and is categorical
at its eligible levels.  For an unbounded supply after refinement,
assume the eligible-subclass hypothesis of
Convention~\ref{lev:eligible-subclass}.  Either of the following inputs
supplies the diagram clause, after the indicated closure refinements.
\begin{enumerate}
\item For each infinite $\sigma$, at all sufficiently large eligible
levels, the relation of being sent to another list by an arrow is
reversible on lists of cardinality at most $\sigma$, and their orbit
sets have a bound depending only on $\sigma$ and the fixed scheme.
In this case take stabilization bounds and require enough smaller
levels below the receiving level for the bounded arities in use.

\item Same-level arrows preserve isomorphism orbits of bounded lists,
and comparisons of such orbits in well-ordered charts are independent
of the eligible level.  More precisely, for each arity, equivalence
of two term patterns by an isomorphism in their respective charts is
the same relation on patterns whenever both patterns are bounded at
the levels under comparison.
\end{enumerate}
The componentwise exhaustion condition follows whenever arrows have
only componentwise strongness as their additional structural content.
For any other arrow condition its exhaustion assertion remains a
separate obligation.
\end{proposition}

\begin{proof}
For the first route, fix an arity bound $\sigma$.  At a sufficiently
large eligible cardinal $\kappa$, arrow comparison on lists of this
arity is reflexive and transitive, and reversal makes it symmetric.
A list in a larger object can be put into a level-$\kappa$ subobject.
Two choices of that subobject are included in a third by mixed
downward closure and coherence.  Their arrow classes therefore agree.
This defines the level-$\kappa$ comparison in all larger objects and
shows that it is preserved under mixed arrows.

If $\gamma\geq\kappa$ is another sufficiently large eligible cardinal,
there is consequently a projection from the $\gamma$ comparison
classes to the $\kappa$ comparison classes.  This projection is onto:
an object at level $\kappa$ embeds into one at level $\gamma$ by
identifying it with a chart and using an order arrow.  The projections
compose.  Let $b$ bound the numbers of classes.  If strict refinement
continued arbitrarily high, recursively choose $b^+$ many successive
strict refinements and then an eligible cardinal above all the
chosen levels.  At each strict refinement some pair of classes at
this final level has equal images before the refinement and unequal
images after it.  A fixed pair can witness this only once, since
unequal images cannot merge in a refinement.  There are at most
$b^2=b$ pairs, a contradiction.  Thus the comparisons stabilize.

Their stabilized equality is canonical, and comparisons at different
arities commute with restriction: raise the cardinal beyond the
stabilization thresholds for both arities and restrict an arrow
implementing the longer comparison.  Atomic diagrams are preserved
by arrows.  A prescribed bounded extension is realized over an actual
list in a sufficiently high same-level object by placing a witness
and the actual list into objects of one common eligible size and
using the reversible comparison to map the witness list to the actual
one.  This gives the joint extension as well.

At a receiving level $\mu$ of countable cofinality, close below $\mu$
under these thresholds and under choices of a sufficiently large
smaller eligible cardinal for each arity.  Enumerate each of two
objects by countably many nested bounded lists.  To extend a match,
choose a smaller eligible cardinal containing all the old and newly
requested entries and above their stabilization thresholds.  Put the
data into subobjects at that cardinal and implement the equal
stabilized diagrams by an arrow in the desired direction.  Alternate
the direction of extension and include the next enumeration list on
each side.  The union is a bijection preserving and reflecting every
atomic formula, hence an isomorphism of systems.  Starting with a
given equal-diagram tuple makes it part of that isomorphism.  The
same smaller-level construction realizes a possible bounded extension
diagram over an actual tuple.  Order arrows and order amalgamation
give naturality.  These arguments use both eligibility of $\mu$ and
the availability of smaller eligible cardinals, as distinguished in
Section~\ref{lev:refining-levels}.

For the second route, instances of the same well-ordered pattern
have the same orbit.  Indeed two well-orders amalgamate over a common
suborder into a well-order: in each cut of the common well-order
concatenate the two remaining well-ordered pieces, then retain the
common points between successive cuts.  Enlarge to an eligible size
if necessary.  The induced order arrows and same-level orbit
preservation identify the two instances.  The assumed independence
of orbit comparison from the level therefore defines diagrams on
well-ordered patterns.  The set of such patterns at a fixed arity
gives a uniform bound.

For a mixed arrow from level $\nu$ to level $\mu$, include the image
of its whole source in a level-$\nu$ subpresentation of the target.
Coherence factors the arrow through that subpresentation.  Same-level
orbit preservation computes the comparison there, and the assumed
agreement of chart comparisons computes the same diagram in the
target.  This proves mixed preservation.  For saturation, take a
well-ordered support pattern witnessing the desired joint diagram
in a larger object.  Its support has cardinality below the receiving
level, so it embeds into a well-order of that level.  The old subtuple
has the diagram of the prescribed actual tuple; an isomorphism at
the receiving level carries the new realization over that tuple.
The orbit hypothesis itself supplies homogeneity.  Naturality on
padded orders follows from Lemma~\ref{lev:directed-unions}.

In either route, diagrams on bounded enumerations of small vertex
submodels have strong images by homogeneity, with the preliminary
order embedding in the mixed-level case.  The AEC union axioms give
the asserted componentwise exhaustion condition.
\end{proof}

\subsection{A set-theoretic code for diagram equality}

The next construction supplies one definition of comparison that can
be used uniformly with a finite descriptor for the scheme.  It does
not define truth for a varying family of proper-class predicates.

A code for a finite-support template consists of its set-sized
finitary language, sorts and specified-map symbols, its labels and
their finite arities, and tables evaluating the function symbols,
equality, and relations on finite ordered support patterns.  A
function table supplies a label and sublist for its output within
the union of its inputs' supports; its arity-zero case is included.
Adjoin labels of arity zero for closed terms if necessary.  This
does not increase the infinite bound on the language and label set.
Fixed names, including
the labels of arity zero in Proposition~\ref{lev:named-package}, are
part of this code.  The usual consistency requirements say that the
evaluated equality is an equivalence relation and a congruence, that
the function tables are total and correctly sorted, and that the
evaluations agree under passage to larger finite support
patterns.  These are tests on sets.  A coherent code constructs a
structure $F(I)$ on any set-sized order $I$ by taking the quotient
of the set of labeled finite lists by the evaluated equality.  This
construction makes sense whether or not $F(I)$ is an object of a
working scheme at that size.

For an arity bound $\sigma$, a \emph{pattern} records an indexed list
of labels, finite increasing support lists for them, and the order
on the union of these supports.  Use canonical support universes
of cardinality at most $\sigma$ and index sets of cardinality at most
$\sigma$.  These codes form a set, denoted by $\mathcal P_F(\sigma)$.
Two codes representing the same terms need not be identified in
advance.  The comparison below handles such duplicate representations.
When names are represented by reserved support positions instead of
labels of arity zero, include their fixed support in every pattern
and every support map; the test bounds must then also dominate its
cardinality.

\begin{proposition}[Uniform coding of working diagrams]
\label{lev:diagram-coding}
There is a fixed first-order set-theoretic definition $D_F$ of an
equivalence relation on term patterns, uniform in a coherent
finite-support template code $F$.  There is a definable cardinal
bound $b_F(\sigma)$ such that, on $\mathcal P_F(\sigma)$, a single
back-and-forth test with bound at least $b_F(\sigma)$ computes $D_F$.
These definitions do not require the system axioms at the cardinals
used for the tests.

Suppose, in addition, that $F$ presents a working scheme at unboundedly
many eligible strong limit levels of countable cofinality.  At every
eligible level $\mu>|F|$ strictly closed under $b_F$, the working
diagram of a bounded term list is exactly its $D_F$-comparison class.
The same definition therefore computes the diagrams of every such
scheme, including the schemes with fixed named data.
\end{proposition}

\begin{proof}
Fix an infinite $\eta$ at least the cardinality of the template code
and of the patterns to be tested.  For two set structures $A,B$ in
its language, form the set of all pairs of tuples of the same index
set of cardinality at most $\eta$.  Index sets can be taken to be
ordinals below $\eta^+$, reindexing concatenations when necessary.
Let $R_0$ consist of the pairs with the same atomic diagram.  Having
defined $R_\alpha$, retain in $R_{\alpha+1}$ just those pairs
$(a,b)\in R_\alpha$ such that every added tuple of cardinality at
most $\eta$ on either side has a matching added tuple on the other
side with the extended pair in $R_\alpha$.  At a limit take the
intersection of all preceding relations.

This decreasing recursion stabilizes.  If its state set has
cardinality $\tau$, there cannot be a strict decrease at every
successor stage below $\tau^+$, since each strict decrease removes
a previously unremoved state.  Equality at one successor stage
gives a fixed point.  Write $R_\infty$ for the stabilized relation.
In particular, from a pair in $R_\infty$ every allowed extension has
a matching extension still in $R_\infty$; quantification over all
ranks is not being exchanged with an existential choice without
this fixed-point argument.  Reflexivity and symmetry follow from
the construction.  Transitivity follows by composing matches:
the composition of two relations having the atomic and extension
properties again has those properties, and is contained in the
largest such relation $R_\infty$.  This also proves invariance under
isomorphisms.

Use orders satisfying Lemma~\ref{lev:rich-orders}, and realize the
two indicated patterns in their term structures.  Declare
$p\equiv_{F,\eta}q$ when their tuple pair belongs to $R_\infty$.
Every support pattern of size at most $\eta$ embeds into such an
order, by the successive insertion assertion in that lemma.

The definition is independent of the rich orders and of the
realizations of an individual pattern.  To prove this, relate two
term tuples when their representations are carried to each other
by an order isomorphism between support sets of size at most $\eta$.
This relation has atomic matching by the definition of the template.
An added tuple has at most $\eta$ new support positions.  Order
richness extends the support map to these positions on the other
side, in either direction.  Thus this relation has the extension
property and is contained in $R_\infty$.  Replacing an instance of
either pattern by another instance and using transitivity proves
independence for the comparison of two possibly different patterns.

If $\eta'\geq\eta$, orders rich for $\eta'$ are also rich for $\eta$,
and their back-and-forth test with the larger moves implies the test
with the smaller moves.  Independence of the chosen orders gives
\[
              \equiv_{F,\eta'}\ \subseteq\ \equiv_{F,\eta}
\]
on patterns in the common domain.  Define $D_F$ to be agreement at
every sufficiently large test bound $\eta$.

Here is both uniform definability and the promised single bound.
In defining the test at $\eta$ it is enough to use rich orders of
cardinality $2^\eta$ on a fixed standard universe, whose existence
was proved in Lemma~\ref{lev:rich-orders}.  All their order relations,
the realizations of the patterns, the associated term structures,
and the states of the recursion are sets.  The recursion up to the
successor cardinal of its state set defines $R_\infty$ by an ordinary
first-order set-theoretic formula.  Independence means that one may
quantify over the rich orders and realizations in that set, without
making a uniform class choice of an order.

For each pair in $\mathcal P_F(\sigma)^2$ which fails some test,
take its least failing infinite cardinal above the fixed input bounds.
This is a uniquely defined ordinal when it exists.  Replacement
collects these witnesses into a set.  Choose $b_F(\sigma)$ above
their supremum, above $\sigma$, and above the template and naming
bounds.  Monotonicity proves
\[
 p\mathrel{D_F}q
 \quad\Longleftrightarrow\quad
 p\equiv_{F,b_F(\sigma)}q,
 \qquad p,q\in\mathcal P_F(\sigma).
\]
The same holds at every larger test bound.  Taking suprema over
smaller arities makes $b_F$ monotone if desired.  Notice that the
cardinality of the set of patterns justifies taking the set of
separation witnesses; it does not assert an a priori numerical
upper bound on their ranks.  A code failing the coherence tests may,
if a total definition on all set codes is desired, be assigned the
discrete comparison and a fixed default bound.  This convention has
no mathematical role for a coherent template.

We now compare with the working diagrams.  First suppose two bounded
patterns have equal working diagrams.  Fix any test bound $\eta$.
Choose an eligible level large enough for the patterns and $\eta$,
and use a rich padded order of that level from
Lemma~\ref{lev:rich-orders}.  Lemma~\ref{lev:directed-unions} makes
its term structure an object of the scheme.  Naturalness transfers
the equal working diagrams to realizations of the two patterns
there.  The package gives an isomorphism taking one realization to
the other.  It passes the back-and-forth test at $\eta$.  Independence
of rich orders now gives $p\equiv_{F,\eta}q$.  Since $\eta$ was
arbitrary, equal working diagrams imply $D_F$-equivalence.

Conversely fix an eligible $\mu$ as in the statement and two objects
of that level with bounded lists whose patterns are $D_F$-equivalent.
Choose countable nested bounded enumerations exhausting both objects.
We construct compatible matches containing these enumerations,
maintaining $D_F$-equivalence of their term patterns.  Suppose the
current lists have been matched, and a next bounded list on one side
is requested.  Let an infinite $\rho<\mu$ bound the cardinality of the combined
old and requested lists.  Choose
\[
          b_F(\rho)\leq\eta<\mu.
\]
This is possible by strict closure.  At the same level $\mu$, form
rich padded presentations for this test.  Realize the current
patterns there.  Naturality and homogeneity for the working diagrams
give isomorphisms from the current objects to these presentations
taking their current lists to the chosen realizations.

Transport the requested list through the first isomorphism.  The
current pair passes the test at $\eta$, so the fixed-point extension
property supplies a matching list in the other rich presentation.
Choose finite-support term representations for the extended lists.
Their patterns pass the $\eta$-test; because
$\eta\geq b_F(\rho)$, they are $D_F$-equivalent.  Transport the
matching list back to the actual target object.  The isomorphisms
used in this transport preserve working diagrams, which were
already shown to imply $D_F$-equivalence.  Transitivity therefore
gives the required $D_F$-equivalence for the extended actual lists,
independently of their chosen representations.

Repeat with the sides reversed and with the next lists in the two
enumerations.  All stages have cardinality below $\mu$; only their
countable union exhausts the objects.  Atomic matching ensures that
the compatible assignments define a well-defined injective map, and
the alternating exhaustion makes it onto every sort.  Every atomic
instance involves finitely many entries and occurs at one stage,
so the resulting bijection is a structural isomorphism.  It carries
the original list to the other list.  The working package therefore
identifies their working diagrams, as required.
\end{proof}

\begin{remark}[What the code does and does not establish]
\label{lev:coding-interface}
The code $F$, its finite shape, and its fixed naming data are set
parameters.  The recursion in Proposition~\ref{lev:diagram-coding}
is a recursion on a set of states of set structures.  Its definition
is the same formula for every such parameter, including templates
arising after a finite number of later constructions.  It therefore
introduces no satisfaction predicate for arbitrary class definitions.
The bound $b_F(\sigma)$ depends on the full fixed descriptor; names
or labels of unbounded size cannot be omitted from that input.

The identification of $D_F$-equivalence with equality of working diagrams
uses an already established working package, including its actual
isomorphism assertion.  It supplies a
uniform way to express that package in subsequent closure tests; it
is not a substitute for proving homogeneity, chain closure, or an
additional arrow condition for a new scheme.  The later simultaneous
closure argument must still prove that its descriptors and its bound
recipes are uniformly set-theoretically definable and that their
requested bounds exist on relevant inputs.
\end{remark}
==== END Eventual-Categoricity-for-Abstract-Elementary-Classes//05-working-schemes.tex ====

==== BEGIN Eventual-Categoricity-for-Abstract-Elementary-Classes//06-calculus.tex ====
\section{The one-dimensional calculus}
\label{calc:section-calculus}

Throughout this Section, $\mathcal C$ is a scheme satisfying the working
package of Definition~\ref{lev:working-package}.  Its fixed presentation is
denoted by $F$, and $b$ is an infinite cardinal bounding the set of labels
and the finite amount of structural data in the scheme.  We use the
occurrence sorts of that Definition: a tuple in several vertices is a
tuple of tagged occurrences, and a map of systems commutes with every
specified structural map.  No choice of a hull or a basis is part of a
diagram.  A level is an eligible strong limit cardinal of countable
cofinality.  All further closure requirements below are requirements on
functions of bounded arities and fixed scheme data.
For the supply of unbounded refinements and larger auxiliary levels,
we use the eligible-subclass hypothesis of
Convention~\ref{lev:eligible-subclass}: the input class contains a fixed
definable unbounded subclass closed under suprema of strictly increasing
countable sequences.  This subclass is used only to supply levels;
the bounds below depend on fixed scheme data and bounded arities.

Stationary independence and local character are central to the theory of
good frames; see \cite[II.2.1]{Shelah2009}.  The assertions below are
proved from the working package for bounded tuples and finite systems.
Their role is to supply the independence and descent properties needed
for the next isolation construction.

A \emph{query} is an enumerated parameter set $Z$ together with the
diagram of the displayed tuple and that enumeration.  Repetitions in an
enumeration are allowed.  Saying that an answer is correct on $Z$ means
equality of the whole joint diagram, rather than equality only on finite
subtuples.  At a level $\mu$, every tuple or query called bounded has
cardinality less than $\mu$.

\subsection{Testing, placement, and amalgamation}

\begin{lemma}[Parameter orbits for a scheme]
\label{calc:parameter-orbits}
Fix an infinite $\sigma$.  If
$\chi>b+\sigma$ and $\chi^\sigma=\chi$, then, at every sufficiently closed
level greater than $\chi$, there are at most $\chi$ diagrams of
$\sigma$-tuples over a fixed parameter tuple of length at most $\chi$.
Moreover, natural diagrams are unchanged by simultaneous disjoint block
transpositions: within each of a family of disjoint convex regions,
interchange an adjoining block belonging exclusively to the first tuple
family with one belonging exclusively to the second, retaining each
block's internal order.
\end{lemma}

\begin{proof}
Present the parameter object on a well-order.  After choosing one term
representation of each parameter, its supporting positions form a
well-ordered set of size at most $\chi$.  There are at most $\chi$ slots
and positions relative to this set.  Labels, comparisons and coincidences
for at most $\sigma$ additional positions therefore have at most
$\chi^\sigma=\chi$ possibilities.  Equal profiles give equal natural
diagrams.  The diagram-isomorphism clause of the working package turns
this into the asserted orbit bound over the actual parameters.

Here are the hypotheses needed for the block argument in
Lemma~\ref{lev:block-transpositions}.  We have just proved its parameter
orbit bound.  Repeating the two blocks along an arbitrary order is
permitted after padding: the scheme has the union and common-upper-bound
clauses, so Lemma~\ref{lev:directed-unions} supplies the padded
presentations and their order arrows.  Naturalness compares the two
patterns at a common higher eligible level.  If the transposition changed
a diagram, the repeated patterns would distinguish cuts by whether the
first block preceded or followed a parameter block.  A binary tree of
least height $\epsilon$ with $2^\epsilon>\chi$ has at most $\chi$
nonterminal nodes and more than $\chi$ branches.  Divider points at those
nodes give at most $\chi$ parameter blocks and more than $\chi$ different
diagrams over them.  The preceding orbit bound gives a contradiction.
The repetition uses only a set of positions, so a higher eligible level
can contain the entire test.  This proves the assertion also when there
are boundedly many simultaneous transpositions.
\end{proof}

\begin{definition}[Natural parameter layouts]
\label{calc:natural-layout}
A natural parameter layout consists of finitely many well-ordered
segments, a fixed finite set of colors and their prescribed order, and
specified families of terms on specified collections of those positions.
Its parameters are all the designated terms; vertex sorts may be among
the designations.  The data must have the following monotonicity
property: after freezing bounded extra supports, increasing the ordinal
lengths of the remaining slots gives an embedding of layouts that
preserves the designated parameter terms.  Bounded frozen parameters
are permitted and count towards the input arity.  The layout, labels and
color conventions are fixed set data.

The whole object $F(H)$, with $H$ well-ordered, is a natural layout.
Unions of designated vertex sorts generated on specified segments are
further examples.  An arbitrary subset of the parameters in an unrelated
target chart is not asserted to be a natural layout.
\end{definition}

\begin{proposition}[Uniform testing for natural layouts]
\label{calc:testing}
\label{calc:layout-testing}
For each fixed natural layout there is a monotone cardinal function
$g(\sigma)$ with the following property.  Two placed comparison types of
tuples of length at most $\sigma$ over that layout are equal if and only
if they agree on parameter queries of size at most $g(\sigma)$.
The bound is independent of the eligible level.  The extra tuple supports
may lie in a non-well-ordered extension of the layout.  The assertion is
uniform when the fixed layout and frozen bounded data range over a fixed
set of descriptors of bounded size.
\end{proposition}

\begin{proof}
Amalgamate the orders containing the two placements over the parameter
order.  Freeze the labels of the two tuples, their combined ordered
support $T$, the coincidences with old positions, and the colors.  There
are set-many such frozen patterns at the prescribed bound.  The
unfrozen well-ordered parameter positions are described by a vector of
ordinal lengths, one coordinate for each strict slot and each prescribed
segment.  There are set-many coordinates, even when $T$ itself is not
well-ordered.  By the monotonicity requirement in
Definition~\ref{calc:natural-layout}, a pointwise increase embeds the old
layout and its designated terms into the new one.  Unequal comparisons
remain unequal because diagrams are preserved by the induced arrows.

For a fixed frozen pattern, apply
Lemma~\ref{lev:ordinal-vectors} to the upward closure, among all ordinal
vectors, of its valid unequal configurations.  It gives a set of
generators, which can be chosen from valid unequal configurations.  Each
generator has a set-sized parameter order.  Take a cardinal above the
sizes of the terms on all these orders, then above the resulting bounds
for all the frozen patterns.  An unequal configuration contains one of
the generating configurations and is consequently witnessed on at most
that many parameters.  Increasing the bound monotonically gives $g$.
This is precisely the ordinal-vector proof of
Proposition~\ref{lev:testing}; its required ingredients here are natural
diagrams, their preservation, and the explicit monotonicity of the
layout, all verified above.  Taking the same supremum over a set of
descriptors proves the last assertion.
\end{proof}

\begin{lemma}[Compact placement for a scheme]
\label{calc:compact-placement}
Let $P$ be any chosen parameter set in a well-ordered presentation, with
one fixed term representation for each parameter.  Let $v$ have length
at most $\sigma$, and let
\[
 \chi>b+\sigma,\qquad \chi^\sigma=\chi.
\]
Suppose that coherent diagrams for $(v,X)$ are prescribed for every
$X\subseteq P$ of size at most $\chi$, and that each individual
prescription has a placement.  At a sufficiently closed eligible level
containing the data, one order enlargement realizes all these
prescriptions simultaneously.  The same assertion holds with bounded
frozen data, after adding its size to $\sigma$.

For a padded order that need not be well-ordered, it suffices instead to
have locally possible coherent prescriptions on every bounded subset
and closure under the profile-count growth used in the proof.  The
conclusion then holds simultaneously at any one specified bounded test
size.  All the bounds are uniform in the fixed scheme and layout data.
\end{lemma}

\begin{proof}
For $X\subseteq P$, let $S_X$ be the union of its chosen supports.  A
profile records the labels of $v$, its formal ordered support, and all
comparisons and coincidences with $S_X$.  If $|X|\le\chi$, there are at
most $\chi$ profiles.  In each strict slot over $S_X$, all the new
positions there form one cluster.  A profile has a continuation over the
whole old order with no new event: place each cluster intact into a
single strict slot of the old order extending its slot over $S_X$.
Order enlargement supplies positions if necessary.  A new event on
enlarging $X$ means a new hit of an old position or a separation of two
previously unseparated new positions by an old position.

Two continuations with no new event over $S_Y$, for $Y\supseteq X$,
have the same diagram over $Y$.  Indeed, their differences consist of
moving whole clusters past blocks of parameter supports.  The regions
belong to distinct slots, so the block transpositions in
Lemma~\ref{calc:parameter-orbits} apply simultaneously.

If simultaneous realization fails, choose $X_0$ of size at most $\chi$.
For each profile over $X_i$, choose a no-new-event continuation and one
prescribed query where it fails.  Adjoin those queries to $X_i$ to obtain
$X_{i+1}$; at limits take unions.  There are at most $\chi$ profiles,
each chosen query has size at most $\chi$, and $\sigma^+\le\chi$.
Thus every $X_i$, including $X_{\sigma^+}$, has size at most $\chi$.
Choose a placement realizing the prescription on $X_{\sigma^+}$.
At every earlier step this placement must have a new event, since
otherwise the no-event comparison would transfer the chosen failure to
it.  There are at most $\sigma$ possible hits and at most $\sigma$
pairs of new positions.  Each event can occur for the first time only
once.  This contradicts the $\sigma^+$ steps.

In a non-well-ordered chart, the number of profiles over $X_i$ is at most
$2^{|X_i|+\sigma+b}$.  Starting with the desired test size, use this as
the next cardinal bound and include a failed query of at most that
original test size for every profile.  The larger sets $X_i$ have
prescriptions because those were supplied on all bounded subsets.
More explicitly, start with an infinite $\beta_0$ above the desired
test size and set $\beta_{i+1}=2^{\beta_i+\sigma+b}$, taking suprema
at limits.  Require the single bound
$\sup_{i\le\sigma^+}\beta_i$ to be strictly below the level.
This is closure under the whole indicated recursion, rather than
merely closure under each individual exponentiation.  It keeps the
final set bounded even though the level has countable cofinality.
Its prescription
is available by hypothesis, and the identical event count is a
contradiction.  This is a set recursion depending only on the starting
arity and fixed data.
\end{proof}

For later reference, fix a convenient explicit threshold for the whole
object layout.  Increase $g$ so that $g(\sigma)\ge b+\sigma$, and put
\begin{equation}
\label{calc:test-threshold}
 c(\sigma,\tau)=2^{g(\sigma)+b+\sigma+\tau},
 \qquad c(\sigma)=c(\sigma,\aleph_0).
\end{equation}
These cardinals exceed the displayed arities and satisfy
$c(\sigma,\tau)^\sigma=c(\sigma,\tau)$.  We close levels under these
functions and their successors, as well as under the diagram and rich
order bounds at the resulting arities.  For a different fixed natural
layout, use its testing function in the same formula.

\begin{lemma}[Placed comparisons of actual tuples]
\label{calc:placed-comparisons}
Suppose $A\to N$ is an arrow between same-level objects and $v$ is a
bounded tuple in $N$.  Its diagrams over bounded subsets of $A$ have a
placed comparison over a well-ordered presentation of $A$.  This
comparison is unique as a diagram over all of $A$.  Two such actual
tuples have equal comparisons if and only if their diagrams agree over
queries in $A$ of size at most $g(|v|+\aleph_0)$.
The conclusion also holds over any natural parameter layout for which
the same coherent local diagrams are given.
\end{lemma}

\begin{proof}
A single bounded request is possible in a presentation: the parameter
diagram is preserved by the arrow, and saturation realizes its desired
extension over the actual parameters in a level object.  Apply
Lemma~\ref{calc:compact-placement} at
$\chi=c(|v|+\aleph_0,\tau)$, for any desired bounded query size $\tau$.
Two outputs agree on all tests of size at most $g(|v|+\aleph_0)$, and
Proposition~\ref{calc:testing} identifies their full placed comparisons.
For any bounded query, choose $\tau$ large enough to include it.  The
unique comparison therefore computes every actual bounded diagram.
This argument does not require an amalgamation relation on types.
\end{proof}

\begin{theorem}[Amalgamation and types for a scheme]
\label{calc:scheme-amalgamation}
At sufficiently closed levels, $\mathcal C$ has amalgamation.  If
$A\to B_0,B_1$ are arrows and $v_i$ are equally indexed bounded tuples
in $B_i$, then an amalgam over $A$ identifying $v_0$ and $v_1$ exists
if and only if their diagrams agree on all parameter queries in $A$ of
size at most $g(|v_i|+\aleph_0)$.

Consequently $\tp(v/A;B)$, defined by identification in an amalgam over
$A$, is an equivalence class.  It is determined by these bounded
diagrams and has an order placement.  Restriction of a type means
restriction of its actual tuple and parameter diagrams.
\end{theorem}

\begin{proof}
Write arrows as inclusions by taking renamed copies.  We prove the
stronger construction with a prescribed identification of bounded
tuples; omit the tuples for ordinary amalgamation.  Let the target
initially be $N_0=B_1$.  Choose increasing bounded lists $d_n$ exhausting
$B_0$, starting with $d_0=v_0$ (or the empty list when no identification
is prescribed).  In each vertex also choose an
increasing countable exhaustion by strong submodels of cardinality less
than the level, and include their enumerations in the $d_n$'s.  Such
exhaustions exist by the component LS property, coherence and
$\cf(\mu)=\omega$.

We construct targets $N_n$ and compatible images of $d_n$.  The invariant
is equality of all bounded joint diagrams of $(d_n,A)$ with their
original diagrams in $B_0$.  For the prescribed initial tuple this is
the hypothesis and Lemma~\ref{calc:placed-comparisons}; the empty initial
tuple is automatic.

Suppose an image of $d_n$ has been chosen.  In a well-ordered chart of
$N_n$, regard $A$ and this whole image as the parameter set $P$.
For a bounded subset of $P$, its required joint diagram with $d_{n+1}$
is read in $B_0$, interpreting the old image as $d_n$.  This prescription
is well-defined on repetitions and coincidences by the invariant.
It is locally possible: equality on the old parameters and saturation
give a realization in $N_n$.  Choose a test cardinal of the form
\eqref{calc:test-threshold}, large enough also for the length of $d_n$,
and apply Lemma~\ref{calc:compact-placement}.  The resulting tuple lies
in an order enlargement $N_{n+1}$ and retains the old assignments.

To verify the invariant, use a natural well-ordered chart of the
\emph{source} $A$.  Both the desired tuple and the newly placed tuple
have comparisons there by Lemma~\ref{calc:placed-comparisons}.  Their
agreement on the chosen tests includes the testing bound for the joint
arity, so Proposition~\ref{calc:testing} makes their comparisons equal.
They therefore agree on every bounded query in $A$.  We have not
applied uniform layout testing to the possibly unnatural image of $A$
in the target chart; compact placement alone was used on that image.

Take the union of the countable target chain.  Its total size is $\mu$,
so the union and upper-bound clauses of the package give an object and
an arrow from $B_1$.  The assignments define a map from $B_0$ into this
union.  They match diagrams on increasing lists that exhaust $B_0$ and
include the component strong-submodel exhaustions.  The image of each
such small submodel is strong: the matching diagram of its enumeration
is implemented by an isomorphism between its original containing
object and the target object.  The arrow criterion
of the package consequently makes this map an arrow, including any
extra basis condition already checked for the current scheme.  The
initial tuples have the same image.  Necessity of diagram equality
follows from preservation in any amalgam.

Amalgamation makes the identification relation transitive: amalgamate
two witnesses over their common intervening object.  Reflexivity and
symmetry follow from identity maps and interchange of the two legs.
The equivalence and testing descriptions now follow from the proved
criterion and Lemma~\ref{calc:placed-comparisons}.
\end{proof}

\begin{corollary}[Realization into a larger level]
\label{calc:mixed-realization}
Let $\nu<\mu$ be sufficiently closed eligible levels.  If $A\to B$ are
$\nu$-objects and $A\to N$ is an arrow into a $\mu$-object, then there
is an arrow $B\to N$ extending the given arrow on $A$.  One may prescribe
the image of a tuple of length less than $\nu$ whose diagrams over
queries in $A$ below $\nu$ already match.  Types of tuples of length
less than $\nu$ over $A$ obtained in a larger object are actual
$\nu$-types, and the mixed diagram comparisons at those arities agree.
\end{corollary}

\begin{proof}
Use the countable exhaustion in the preceding proof, with all source
lists and testing thresholds below $\nu$.  Perform the compact
placement in a chart of $N$.  The placed tuple, all of $A$, and the
previously assigned list together have cardinality at most $\nu$, which
is bounded at $\mu$.  Saturation at $\mu$ therefore realizes their
whole joint diagram back in the actual $N$, fixing the existing
parameters.  Continue there, without enlarging the final target.
For component strongness, first place the source object at level $\mu$
by a presentation arrow.  Mixed preservation and an isomorphism of
$\mu$-objects implementing the matching enumeration show that every
small source strong submodel has strong image in $N$.  The exhaustion
criterion now gives the arrow.

To interpret a tuple of length less than $\nu$ over $A$ inside a larger
object, take a $\nu$-subobject containing $A$ and the tuple, using mixed
LS.  Coherence makes it an extension of $A$.  Mixed preservation
identifies its diagrams with those in the larger object.  The testing
criterion shows independence of the chosen subobject.  This also
justifies the source-level type comparisons used during the construction.
\end{proof}

\subsection{Approximations and stationary free extensions}

Amalgamation has made types over a whole object available.  We now choose
their free extensions by means of sequences in the base: on each bounded
parameter query, almost all entries of the sequence give the same answer.
The next two results construct these sequences and show that their answers
determine an actual type, independently of the choices.

\begin{definition}[Approximation sequence]
An 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$,
\begin{equation}
\label{calc:exception-estimate}
 \bigl|\{i<\kappa:D(v_i,Z)\ne p\mathord\upharpoonright Z\}\bigr|
 \le |Z|+\aleph_0.
\end{equation}
Here $p\mathord\upharpoonright Z$ denotes its joint diagram, and 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 called its \emph{majority value} on $Z$.
\end{definition}

\begin{lemma}[Uniform majority approximations]
\label{calc:approximations}
Let $|v|\le\sigma$ and let $\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 \eqref{calc:exception-estimate} simultaneously
for all subtuples of $v$.  The construction has bounds depending only
on $b,\sigma,\tau,\kappa$, rather than on the level or the type.

In particular, take $\tau=c(\sigma)$ and
$\kappa=c(\sigma)^+$.  The concatenated sequence then 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{calc:free-extension} below.
\end{lemma}

\begin{proof}
By the rich-order and padding constructions of
Lemmas~\ref{lev:rich-orders} and~\ref{lev:directed-unions}, present $A$
on a padded dense order sufficiently saturated for every support size
used below.  The presentation is an object of the current scheme;
categoricity in the package gives an isomorphism with $A$.
Lemma~\ref{calc:placed-comparisons}, or its compact-placement proof in
the padded chart, 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 now belongs to a
different strict slot over the anchors.

In each such anchor slot, choose $\kappa$ pairwise disjoint convex
regions in the old order and, 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$ and one finite support for each of its elements.
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{calc:parameter-orbits} 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}

\begin{theorem}[Stationary free extension]
\label{calc: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
desired 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 used in its construction.
\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$.  The restriction to
$A$ is the actual $\nu$-type of
Corollary~\ref{calc:mixed-realization}.
\item A sequence from Lemma~\ref{calc: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
majority prescription.  Arrows carrying one such sequence to another
carry the corresponding type to its free lift.  In particular an
isomorphism carrying the code sequence transports the type.
\end{enumerate}
We say that an actual type over $B$ is \emph{free from $A$} when it is
the free lift of its restriction to $A$.
\end{theorem}

\begin{proof}
First fix a query bound $\tau$ and take an approximation sequence
$I=(v_i:i<\kappa)$ in $A$ with $\kappa>\tau+\aleph_0$.  Given a
query $Z$ in $B$ of size at most $\tau$, saturation moves it into $A$
over the entire sequence: there is $Z_0\subseteq A$, with the same
enumeration, such that
\begin{equation}
\label{calc:query-move}
 D(I,Z)=D(I,Z_0).
\end{equation}
The total length $|I|+|Z|$ is bounded.  For mixed levels it is bounded
at the originating level, and the mixed saturation clause applies.
Define the answer on $Z$ to be the majority of $D(v_i,Z)$, equivalently
the answer $p\mathord\upharpoonright Z_0$.  Equation
\eqref{calc:query-move} preserves every entry of the sequence, so this
definition is independent of the chosen $Z_0$ and retains the same
exception estimate.

If $I'$ is another sufficiently long approximation sequence, move $Z$
into $A$ over $I\cup I'$.  On that moved query both majorities compute
the original $p$.  Thus the answers agree.  This proof requires
saturation over the concatenation of the sequences; it does not
require either approximation estimate to hold for a query containing
that concatenation.  The averaging queries still have size at most
$\tau$.  The identical argument compares different query bounds on
their common domain.  It also proves coherence under restrictions and
reindexing of queries.

We next obtain 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{calc:compact-placement} gives a placement
realizing all of them in an order enlargement of $B$.  This is an
actual tuple in an extension object, and
Theorem~\ref{calc:scheme-amalgamation} makes its type unique, since
$\tau\ge g(\sigma)$.  This type is $p^B$.  Its restriction to $A$
equals $p$ by the same testing criterion.

For a larger desired bounded query size $\tau'$, repeat with a power
closed bound at least $c(\sigma,\tau')$.  The comparison of sequences
just proved identifies the resulting type with $p^B$ on the initial
testing threshold and hence everywhere.  In a mixed-level use, this
additional direct majority evaluation is asserted only when its costs
remain below the originating level.  The type itself is already
actual over $B$, and its diagrams at larger arities are those of this
actual type; no averaging inside a smaller model at unbounded arities
is being asserted.

Restriction to a subtuple commutes with every majority evaluation.
Choose the threshold large enough for both arities and use testing to
obtain equality of types.  Isomorphism invariance follows by applying
the isomorphism to the sequences and their query diagrams.
For transitivity, let $J\subseteq B$ be a canonical approximation
sequence for $p^B$ at a sufficient fixed threshold, and retain an
original sequence $I\subseteq A$ at that threshold.  The latter
computes $p^B$ on queries in $B$ by the construction.  Move a query in
$C$ into $B$ over $I\cup J$.  The two sequences give the same answer
there, because each computes $p^B$.  The first also computes $p^C$,
and the second computes $(p^B)^C$.  Testing proves transitivity.
All these sequence lengths can be chosen as the uniform bounds in
Lemma~\ref{calc:approximations}, below the smallest originating level.
This proves the mixed-level assertions as well.

Finally, suppose $J\subseteq B$ has the same whole diagram as a fixed
code $I\subseteq A$ at threshold $c(\sigma)$.  For each query $Z$ in
$B$ of that size, saturation realizes $D(J,Z)$ over $I$ in $A$.
The resulting majority is therefore well-defined, with the same
exception estimate.  For each query one of the entries of $J$ realizes
the answer in $B$.  Coherence, compact placement and testing give an
actual unique type, as in the preceding construction.  Moving queries
over code sequences shows that an arrow carrying $J$ into a larger
object gives exactly its free lift there.  The code length and every
threshold used here depend only on $\sigma$ and the fixed scheme,
which proves the final assertion.
\end{proof}

\begin{lemma}[An average criterion for descent]
\label{calc: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}
Let $p=q\mathord\upharpoonright A$ and choose a canonical sequence
$J\subseteq A$ approximating $p$ at size $\chi$.  For a query
$Z\subseteq B$ of that size, mixed saturation moves it to $Z_0$ in
$A$ over the whole $I\cup J$.  The total length is less than $\nu$.
The majority from $I$ on $Z$ computes $q$, and on $Z_0$ computes $p$.
These answers agree by diagram preservation.  The majority from $J$
on $Z_0$ also computes $p$, and on $Z$ computes $p^B$.
Hence $q$ and $p^B$ agree on all $\chi$-queries.  Apply the testing
criterion.  The same proof works for an arbitrary longer indexed
family whenever a bounded subsequence of the displayed length retains
the exception estimate.
\end{proof}

\subsection{Products and local character}

\begin{proposition}[Products of bounded types]
\label{calc:products}
For bounded types $p(x),q(y)$ over $A$, realize $p$ in an extension
$B\ge A$ and then realize $q^B$ in a further extension.  The joint
type of $(x,y)$ over $A$, denoted $p\otimes q$, is independent of all
choices.  Binary products are symmetric, with the indicated
permutation of coordinates.  Finite products associate, are
permutation invariant, and commute with coordinate projections.
Furthermore
\begin{equation}
\label{calc:free-product-formula}
 (p\otimes q)^B=p^B\otimes q^B.
\end{equation}
These assertions hold across eligible levels when all originating
arities and uniform testing costs are bounded at the smallest level.

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$.
\end{proposition}

\begin{proof}
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 in the definition.

We give the cardinal calculation for 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^+,\qquad \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 obtained by first taking
the majority in $i$ and then 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$.  Since $\lambda>\kappa$, 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$.  This explains why two equally sized sequences
would not suffice for the argument.  Testing gives symmetry of
the joint types.

For \eqref{calc:free-product-formula}, take the two sequences just
used in $A$ and a sequence $K\subseteq A$ approximating the actual
old product.  Choose their accuracy at a common sufficient test
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 factor 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.  All the
lists fixed during the query movement are bounded, including in the
mixed case.

Now 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 the formula just proved.
Thus the same joint type is $p\otimes(q\otimes r)$.  This proves
associativity.  Projection follows from the projection property of
free lifts in each successive realization.  Associativity and the
binary symmetry permit every permutation of a finite list of factors.

For the final assertion, 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 itself free from $A$, transitivity makes this last
realization free from $A$.  The tuple $(d,e)$ is in the intervening
model, so the definition of product gives the assertion.  The amalgam
identifies the full original tuple over $B$, and hence retains its
actual joint type over $A$.
\end{proof}

\begin{proposition}[Local character and continuity]
\label{calc: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\leq 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{calc:average-descent}, at the same level, applies.

In the other case $\gamma<\mu$.  Choose a regular
$\kappa<\mu$ above $\gamma,\chi,|v|$ and the needed bounds, and
take $\kappa$ approximations inside $A$.  Every whole approximation
tuple belongs to some stage: this uses 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{calc: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{calc:free-extension} makes $p$ free
from $X$.
\end{proof}

\subsection{Universal strips and approximate retractions}

The remaining construction provides maps from an extension back into its
base which fix each individual base element at all but finitely many
indices.  It
will allow isolation to descend from a larger level without requiring a
bounded tuple to lie in one stage of a countable exhaustion.

\begin{lemma}[Closure of a bounded support set]
\label{calc:support-closure}
Let $J\subseteq J^*$ be linear orders, let $V$ be a convex strip in
$J^*$, and put $J_0=J\setminus V$.  Allow any fixed finite coloring
of positions in $J_0$, including their side of $V$.  Let
$T^*\subseteq J^*$ and $S_0\subseteq J_0$ be bounded sets.  Given
an infinite $\chi$, choose an infinite $\lambda$ with
\[
 \lambda\ge\chi+|T^*|+|S_0|,
 \qquad \kappa=2^\lambda.
\]
There is $S\subseteq J_0$, of size at most $\kappa$, containing
$S_0\cup(T^*\cap J_0)$, with this property: for every
$R\subseteq S$ of size at most $\chi$ and every indexed tuple $Q$
of at most $\chi$ positions from $J_0$, there is an equally indexed
tuple $Q'$ in $S$ having the same order, equality and color pattern
over $R\cup T^*$.  In particular all positions named by $R$ are
fixed whenever they occur in $Q$.

At a strong limit level with the displayed input bounded, $S$ is
bounded.  The assertion needs no well-order hypothesis on $J$.
\end{lemma}

\begin{proof}
Build $S_\alpha$ for $\alpha<\chi^+$, starting with the required
set.  At a successor stage, for every $R\subseteq S_\alpha$ of
size at most $\chi$, and every order, equality and color pattern of
at most $\chi$ further positions over $R\cup T^*$ that is actually
realized in $J_0$, choose one realizing tuple and adjoin its positions.
Use unions at limits.  If $|S_\alpha|\le\kappa$, the number of
choices of $R$ is at most $\kappa^\chi=\kappa$, and the number of
patterns for each $R$ is at most $2^\lambda=\kappa$.  Each chosen
tuple adds at most $\chi$ positions.  Consequently every stage and
their union have size at most $\kappa$.

For $R$ contained in the final union, regularity of $\chi^+$ puts
all of $R$ into a single stage.  The actual tuple $Q$ witnesses that
its pattern was among the requirements processed at the next stage.
Its chosen witness is the required $Q'$.  Equality with elements of
$R$ and $T^*$ is part of the pattern, so it is preserved literally.
This also covers arbitrary enumerations and repetitions in $Q$.
\end{proof}

\begin{proposition}[Universality of a fresh strip]
\label{calc:universal-strip}
Let $\mathcal C$ already satisfy the working package.  In addition to
its fixed template $F$, one may use a presentation $G$ with the
following properties: it has a fixed set of finite-support labels;
every presentation $G(J)$ used below, for an order of size $\mu$, is
an object of $\mathcal C$ at level $\mu$; order embeddings give
$\mathcal C$-arrows; and the diagrams of its term lists are natural,
including in the order enlargements and padded orders used.  Assume
also that these labels represent every element of $G(J)$.
Require $\mu$ to exceed the cardinality of the label set of $G$ and
to be closed under the bounds below with that cardinal included in
their fixed input data.

Put $A=G(J)$.  Insert into $J$ a fresh convex strip of size $\mu$
with countably many disjoint convex substrips, each of size $\mu$,
and denote the resulting object by $A^+$.  Then every same-level
extension of $A$ embeds into $A^+$ over $A$.  In particular this
applies to $G=F$ and to well-ordered presentations.  No separate
union or categoricity assertion for a category of $G$-presentations
is required.
\end{proposition}

\begin{proof}
We first realize a bounded type $p(v/A)$ using just one fresh
substrip $V$.  Choose a testing threshold $\chi\ge c(|v|+\aleph_0)$
large enough also for $|v|$ and the number of 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 Lemma~\ref{calc:support-closure}, with
the side of $V$ recorded, to obtain a bounded $S\subseteq J$.
Its closure permits every at-most-$\chi$ old query pattern to move
into $S$ over any at-most-$\chi$ subset of $S$.  The approximation
supports, which may be larger than $\chi$, can instead be included
as the fixed set $T^*$ in that Lemma.  Thus all of them are fixed
during every such movement.

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)$.
The latter is a level object because $|V|=\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$.
Only at most $|v|+\aleph_0\le\chi$ of its supporting positions
are old; call them $R\subseteq S$.

For any query $Z$ in $A$ of size at most $\chi$, move its chosen
support tuple into $S$ over $R$ and the fixed approximation
supports, preserving the side of $V$.  Let $Z'$ be the resulting
term tuple.  All comparisons with the new supporting positions
of $w$ in $V$ are forced by that side.  Naturalness therefore gives
\[
 D(w,Z)=D(w,Z'),\qquad D(I,Z)=D(I,Z').
\]
The majority from $I$ computes $p$ on both queries.  The chosen
realization of $(v,P_S)$ gives $D(w,Z')=p\mathord\upharpoonright Z'$.
It follows that $D(w,Z)=p\mathord\upharpoonright Z$.
Testing of actual types, using a natural $F$-chart of $A$ if $G$
differs from $F$, proves $\tp(w/A)=p$.  Naturality of $G$ was used
only for the displayed support movements; the testing and saturation
are those already proved in $\mathcal C$.

Now let $B\ge A$ be arbitrary and choose increasing bounded lists
$d_n$ exhausting it, including countable strong-submodel
exhaustions in every vertex.  Use the first substrip to realize the
type of $d_0$ over $A$.  At subsequent step $n$, the target base consists
of $A$ and the whole previously used substrips.  Suppose $d_n$ has
already been assigned there with its correct type over $A$.
Theorem~\ref{calc:scheme-amalgamation} amalgamates $B$ with this
target base over $A$, identifying that entire assigned tuple.
In this amalgam, $d_{n+1}$ has an actual bounded type over the
target base.  Apply the one-substrip construction to the next fresh
substrip.  Since its type includes equality with the already
assigned coordinates, the new assignment extends the previous one.
The final union of the assignments lands in $A^+$.  The arrow
criterion applies to the included strong-submodel exhaustions, so
it is an arrow $B\to A^+$ over $A$.
\end{proof}

\begin{corollary}[Approximate retractions]
\label{calc:retractions}
For same-level $A\le B$ there are arrows
$(r_i:B\to A:i<\mu)$ such that, for every $a\in A$,
\[
 \bigl|\{i<\mu:r_i(a)\ne a\}\bigr|<\aleph_0.
\]
The maps are not asserted to fix all of $A$ at once.
\end{corollary}

\begin{proof}
Present $A$ by $F$ on a well-order consisting of $\mu$ disjoint
convex blocks $J_i$, each of cardinality $\mu$ and itself containing
countably many convex substrips of that size.  The whole order still
has cardinality $\mu$, and the working package identifies its
presentation with $A$.  Let $A_i$ be the presentation on the
complement of $J_i$.  It is a level subobject of $A$.
Proposition~\ref{calc:universal-strip}, with $J_i$ as the inserted
strip, embeds $B$ into $A$ over $A_i$; call the arrow $r_i$.
Choose one finite supporting set for $a$.  It meets only finitely
many $J_i$.  For every other index, $a\in A_i$ and $r_i(a)=a$.
\end{proof}

\begin{lemma}[Descent through approximate retractions]
\label{calc:retraction-descent}
Let $A\le U$ be objects at an eligible level $\mu$, and let
$A'\le U'$ be objects at an eligible level $\nu\le\mu$, with
compatible arrows $A'\le A$ and $U'\le U$.  Suppose there are
arrows $(r_i:U\to A:i<\nu)$ such that every $a\in A$ is fixed
for all but finitely many $i$, and $r_i[U']\subseteq A'$ for all
$i<\nu$.  Then for every tuple $d$ in $U'$ of length less than
$\nu$, its actual type over $A$ is the free lift of
$\tp(d/A';U')$.  All comparisons are comparisons of the working
diagrams, including mixed-level diagrams at arities bounded at $\nu$.
\end{lemma}

\begin{proof}
Coherence makes $r_i\mathord\upharpoonright U':U'\to A'$ an
arrow: its image and $A'$ are subobjects of $A$, and its image is
contained in $A'$.  Put $\sigma=|d|+\aleph_0$, choose
$\chi\ge c(\sigma)$ below $\nu$, and choose
$\chi^+\le\kappa<\nu$.  Retain any $\kappa$ indices and form
$I=(r_i(d))$ on them.  This is a bounded concatenated list in $A'$.

For a query $Z\subseteq A$ of size at most $\chi$, at most
$|Z|+\aleph_0$ indices fail to fix every element of $Z$.  At every
other index, arrow preservation gives
\[
 D(r_i(d),Z)=D(r_i(d),r_i(Z))=D(d,Z).
\]
Thus $I$ has the required majority estimate for the actual type
over $A$.  On queries in $A'$ the same identity is a comparison at
level $\nu$, using the restricted arrows.  Mixed preservation
identifies it with the larger-level identity.

Apply Lemma~\ref{calc:average-descent} to $A'\le A$.  Its
restriction type is precisely $\tp(d/A';U')$, by
Corollary~\ref{calc:mixed-realization}.  The conclusion is therefore
the stated free lifting of the actual type, including tuples that
span a chosen resolution of $U'$.
\end{proof}

The preceding calculus will be applied only after the working package
has been established for the relevant scheme.  Its approximation,
testing and support-closure bounds are functions of fixed scheme data
and bounded input arities.  This is the uniformity needed when the
schemes are iterated at finite depths.
==== END Eventual-Categoricity-for-Abstract-Elementary-Classes//06-calculus.tex ====

==== BEGIN Eventual-Categoricity-for-Abstract-Elementary-Classes//07-isolation.tex ====
\section{Isolation and dominated extensions}
\label{iso:section-isolation}

Throughout this section, $\mathcal C$ is a working scheme in the sense of
Definition~\ref{lev:working-package}. We use the refinements of the eligible
levels required in Section~\ref{calc:section-calculus}. All objects and
extensions in a displayed type are at one eligible level, unless a change of
level is stated. We retain the eligible-subclass hypothesis of
Convention~\ref{lev:eligible-subclass}; every larger auxiliary sufficiently
closed level below is chosen in its unbounded refined subclass.
A type over an object at a smaller eligible level is computed
in a section of that level; Corollary~\ref{calc:mixed-realization} makes this
independent of the section. A tuple is bounded when its cardinality is less
than the level of its base. We write $p^{\mathrm{fr}}_B$ for the free lift
$p^B$ of Theorem~\ref{calc:free-extension} when its role needs emphasis.

We will repeatedly use the following convention concerning bounds. A request
involving a tuple of cardinality $\sigma$ is first enlarged to an infinite
arity at least $\sigma$. The testing, compact-placement, and approximation
bounds of Section~\ref{calc:section-calculus} are then applied at that arity.
There are only finitely many such enlargements in each argument below. A
source level is required to be strictly closed under those bound functions.
Thus, when a tuple is bounded at a smaller level, every test used to determine
its type may be taken below that smaller level, even if the receiving object
is at a much larger eligible level. This does not assert saturation over an
unbounded parameter set.

Our goal is an extension controlled by a given mark, with an embedding
into every ambient object realizing that mark's type.  Relative isolation
will give this control on bounded tuples.  The main existence argument
first treats one bound on tuple length and then obtains all bounded
lengths in a single extension.

\subsection{Relative isolation}

\begin{definition}\label{iso:relative-isolation}
Let $q=\tp(u,c/A)$ and $p=\tp(u/A)$, where the concatenation $(u,c)$ is
bounded. We say that $q$ is \emph{isolated relative to $u$} if there is a
bounded set $Z\subseteq A$ such that, for every $q'=\tp(u',c'/A)$,
\[
 \tp(u'/A)=p\quad\text{and}\quad
 D(u',c',Z)=D(u,c,Z)
 \quad\Longrightarrow\quad q'=q.
\]
Here and below a parameter set in a diagram is supplied with a fixed
enumeration, and the same enumeration is used on both sides. We call $Z$ an
\emph{isolating fragment}. A projection retains the entire tuple $u$ unless
explicitly stated otherwise.
\end{definition}

\begin{lemma}\label{iso:free-isolation}\label{iso:upward-transfer}
The following hold at sufficiently closed eligible levels.
\begin{enumerate}
\item A projection of a relatively isolated type is relatively isolated.
\item Suppose $A\leq B$, $q=\tp(u,c/A)$ is isolated relative to $u$, and an
actual coupling over $B$ satisfies
\[
 \tp(u/B)=\tp(u/A)^{\mathrm{fr}}_B.
\]
Then
\[
 \tp(u,c/B)=q^{\mathrm{fr}}_B.
\]
Moreover this type is isolated relative to $u$, using the same isolating
fragment as $q$.
\end{enumerate}
The second assertion also holds when $A$ is at a smaller eligible level than
$B$, provided $(u,c)$ and the required uniform bounds are below the level of
$A$.
\end{lemma}

\begin{proof}
For the first assertion, write $c=(c_0,c_1)$ and let $Z$ isolate $q$.
Suppose $(u',c'_0)$ has the prescribed marginal on $u$ and the same diagram
as $(u,c_0)$ over $Z$. In a model containing $A,u',c'_0$, bounded saturation
extends this diagram by a tuple $c'_1$ so that
\[
 D(u',c'_0,c'_1,Z)=D(u,c_0,c_1,Z).
\]
Isolation identifies the full type over $A$, and its projection identifies
$\tp(u',c'_0/A)$.

For the second assertion, fix an isolating fragment $Z$. It is enough to
compare the actual joint type over $B$ with $q^{\mathrm{fr}}_B$ on the
uniform testing arity for $(u,c)$. Enlarge that arity to include $Z$ and
choose approximation lists in $A$ for both $q$ and $p=\tp(u/A)$, long enough
to evaluate all the comparisons just specified. Let $t$ be a test tuple
from $B$ at this enlarged arity. Bounded saturation moves $t$ to a tuple
$t'$ in $A$, preserving its diagram over $Z$ and both approximation lists.

Choose a realization $u_0$ of $p$ over $A$. The free evaluation of $p$ gives
\[
 D(u,t,Z)=D(u_0,t',Z).
\]
Saturation over the bounded list $(u_0,t',Z)$ supplies $c_0$ such that
\[
 D(u_0,c_0,t',Z)=D(u,c,t,Z).
\]
In particular $(u_0,c_0)$ agrees with $q$ on $Z$ and has marginal $p$.
Isolation gives $\tp(u_0,c_0/A)=q$. Consequently the actual answer to the
query $t$ is the answer that $q$ gives to $t'$. Because the query was moved
over the approximation list for $q$, that is also the free evaluation of
$q$ on $t$. The testing theorem identifies the types over $B$.

Now let a competing type over $B$ have the same marginal on $u$ and agree
with the displayed type on $Z$. Its restriction to $A$ is $q$. The argument
just given identifies it with $q^{\mathrm{fr}}_B$, proving isolation there.
In the mixed-level case, perform these comparisons at the uniform test
bound below the source level. Mixed realization supplies the required
sections, and the same argument applies to those diagrams.
\end{proof}

\begin{proposition}\label{iso:alternative}
There is a bound function $h$, depending only on the fixed working scheme,
with the following property. Put
$\sigma=|u,c|+\aleph_0$. At sufficiently closed eligible levels, precisely
one of the following alternatives holds for $q=\tp(u,c/A)$:
\begin{enumerate}
\item $q$ is isolated relative to $u$ by a fragment of size at most
$h(\sigma)$;
\item there are an extension $A\leq B$ at the same level and an extension
$q_B$ of $q$ such that
\[
 q_B\ne q^{\mathrm{fr}}_B,
 \qquad
 q_B\mathbin{\upharpoonright}u
   =\tp(u/A)^{\mathrm{fr}}_B.
\]
\end{enumerate}
In particular, every relatively isolated type has an isolating fragment
bounded by $h(\sigma)$, uniformly in the level and in the type.
\end{proposition}

\begin{proof}
Choose an infinite $\chi$ large enough for the testing theorem at arity
$\sigma$, for the approximation lists for $q$ and its marginal $p$, and
for the finitely many joint comparisons made below. These choices are
uniform in $\sigma$. Increasing $\chi$ if necessary, all the supports in
the chosen approximation lists have cardinality at most $\chi$.

Present $A=F(I)$ on a well-order of the level cardinality $\mu$. We may
choose $I$ to have more than $\sigma$ disjoint consecutive blocks, each
of order type and cardinality $\mu$: this is still a well-order of
cardinality $\mu$, and all such presentations are objects at this level.
Let $J_0$ consist of the supports of the approximation lists, together
with an initial segment of order type $\chi^+$ in every candidate block.
Its size has a bound depending only on $\sigma$. Let $Z_0$ be the set of
all term values on $J_0$. Since the label set is fixed, the same is true
of $|Z_0|$.

If $Z_0$ isolates $q$, we have the first alternative. Suppose it does not.
Choose $q^1\ne q^0=q$ with the same marginal $p$ and the same diagram on
$Z_0$. By Lemma~\ref{calc:compact-placement}, give both types placements
over the displayed presentation of $A$, and amalgamate their support
orders over $I$. The combined new support has cardinality at most
$\sigma$. Each new support position either hits the interior of one
candidate block or determines an interior cut of at most one such block.
We can therefore choose a candidate block $J$ whose interior contains
neither a hit nor a cut of either placement.

Set $A_*=F(J_0\cup J)\leq A$. This object has cardinality $\mu$. The
restrictions of $q^0$ and $q^1$ to $A_*$ are equal. To check this, take a
test at the fixed sufficient arity. Move every position of the test
lying in $J$ into the initial $\chi^+$ part of $J$, preserving the order
and equality pattern of the test. This can be done above any positions
of that initial part which need to remain in the pattern: fewer than
$\chi^+$ positions have been specified. Leave the positions outside
$J$ unchanged. No position of either candidate separates the interior
of $J$, so the move preserves the natural diagram with either candidate.
The moved query uses only $J_0$ and therefore has the same answer for
$q^0$ and $q^1$. The testing theorem proves equality over $A_*$.

The approximation lists for $q^0$ and $p$ lie in $A_*$. Their majority
evaluations show that $q^0$ and $p$ over $A$ are free from $A_*$. Also,
an isomorphism $f:A_*\simeq A$ may be chosen to fix those bounded lists,
by bounded diagram homogeneity. The transport assertion for free types
then gives
\[
 f\bigl(q^0\mathbin{\upharpoonright}A_*\bigr)=q.
\]
Transport the inclusion $A_*\leq A$ along $f$, viewing its larger object
as an extension $B$ of the original base $A$. Transport $q^1$ as well.
Its restriction is $q$ because the two restrictions to $A_*$ agree. Its
marginal is the free lift of $p$. Its joint type is not free, since the
unique free lift before transport was $q^0$, distinct from $q^1$.
This is the second alternative.

Choose $h(\sigma)$ to bound the size of $Z_0$ for these uniform choices.
Lemma~\ref{iso:free-isolation} excludes the second alternative when $q$
is isolated, even if an initially given isolating fragment was larger.
This proves both exclusivity and the asserted uniform bound.
\end{proof}

\subsection{Primeness and descent of isolation}

\begin{definition}\label{iso:all-dominated-definition}
Let $X\leq Y$ be same-level objects and let $b$ be a bounded tuple in
$Y$. We say that $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 quantifier over all bounded tuples is part of this definition. It is
not enough to verify isolation for individual entries, or for the tuples
in one chosen countable exhaustion of $Y$.

\begin{proposition}\label{iso:prime}
Let $Y$ be all-dominated over $X+b$ at a sufficiently closed eligible
level $\mu$.
\begin{enumerate}
\item If an extension $N$ of $X$ contains a tuple $b'$ of the same type
over $X$, there is an arrow $Y\longrightarrow N$ over $X$ sending $b$
to $b'$. The target may be at a larger eligible level. A prescribed
bounded tuple match can be retained whenever its joint type with $b$
over $X$ already agrees.
\item Two all-dominated objects over the same data $X+b$ are isomorphic
over those data. The isomorphism may retain a prescribed bounded tuple
match of the kind just described.
\item In an actual coupling, if a bounded tuple $x$ has product with
$b$ over $X$, then $\tp(x/Y)$ is free from $X$.
\end{enumerate}
\end{proposition}

\begin{proof}
Choose increasing bounded lists $c_n$, $n<\omega$, exhausting $Y$;
include $b$, the prescribed initial data, and exhaustions of every vertex
by smaller strong submodels. Suppose the image of $c_n$ has already been
chosen with the correct full type over $X$. Let $Z_{n+1}\subseteq X$
isolate $\tp(b,c_{n+1}/X)$. The old image and the source list have the
same diagram over $Z_{n+1}$. Saturation in $N$ extends this bounded match
to $(b,c_{n+1},Z_{n+1})$. Relative isolation makes its full type over $X$
correct. Taking the union gives a map on all of $Y$ fixing $X$: whenever
an entry of $X$ occurs in a list, its equality with the corresponding
parameter is part of its full type. The strong-submodel exhaustions and
the map criterion in the working package show that this map is an arrow.
This proves the first assertion, also into a larger target because every
saturation request is bounded at the source level.

For the second assertion, perform the same construction alternately on
the two sides, at each step including the next list in the chosen
exhaustion on the side to be covered. Both objects have isolation for
the enlarged bounded list. The construction therefore continues in both
directions and its union is an onto structural isomorphism.

For the third assertion, use symmetry and the definition of product to
choose a model $W\geq X$ containing $x$ over which $b$ is free from $X$.
Type-identifying amalgamation brings $W$ and the actual coupling into a
common extension, identifying $x$ and $b$ over $X$. For every bounded
$c$ in $Y$, Lemma~\ref{iso:free-isolation} says that $(b,c)/W$ is free
from $X$. Hence $x$ and $(b,c)$ have product over $X$. Symmetry and
projection give the free evaluation of $x$ on every bounded test $c$
from $Y$. The testing theorem identifies $\tp(x/Y)$ with the free lift
of $\tp(x/X)$.
\end{proof}

\begin{lemma}\label{iso:downward-transfer}
Suppose $A\leq B$ are objects at eligible levels $\nu\leq\mu$,
$|u,c|<\nu$, and the actual type
\[
 q_B=\tp(u,c/B)
\]
is the free lift of $q_A=\tp(u,c/A)$. If $q_B$ is isolated relative to
$u$, then $q_A$ is isolated relative to $u$. Here $\nu$ is sufficiently
closed for the uniform bounds at $|u,c|+\aleph_0$.
\end{lemma}

\begin{proof}
By Proposition~\ref{iso:alternative}, choose a large-base isolating
fragment $W\subseteq B$ with
\[
 |W|\leq h(|u,c|+\aleph_0)<\nu.
\]
Let $w$ enumerate $W$. The type $\tp(w/A)$ is a small-level type,
computed by taking a level-$\nu$ section containing $A$ and $w$.
Choose a sufficiently long bounded approximation list $(w_i)_{i<\tau}$
for this type inside $A$, where $\tau<\nu$. Enlarge its testing bound
to include the arities of $w$ and $(u,c)$ and choose $\tau$ larger than
the two exception bounds that will occur below. Put
\[
 Z=\bigcup_{i<\tau}\ran(w_i)\subseteq A.
\]
This is a bounded fragment.

Let $q'_A$ have the same marginal on $u$ as $q_A$ and agree with it over
$Z$. Lift $q'_A$ freely to $B$. The marginal on $u$ then agrees with
the marginal of $q_B$. In either free coupling, symmetry identifies the
joint diagram with $w$ by the majority evaluation of $\tp(w/A)$ against
the candidate tuple. Thus all but the prescribed bounded number of
$i<\tau$ give the diagram of that candidate with $w$. Choose one index
outside the two exception sets. The candidates agree on $w_i$, because
$w_i$ lies in $Z$, so their free lifts agree on $w$. Isolation of $q_B$
identifies the free lifts, and restriction identifies $q'_A$ with $q_A$.
Every approximation and comparison here has size below $\nu$; no
approximation to the whole of $B$ is used.
\end{proof}

\subsection{Existence with a prescribed bound on tuple length}

We first isolate the continuity requirement on the marked marginal. This
will let us identify exactly where the proof for a finite mark must be
supplemented for a long independent list.

\begin{definition}\label{iso:marginal-continuity}
A bounded marginal type $p$ satisfies the \emph{continuity condition used
here} if the following holds at every sufficiently closed eligible level
to which $p$ is freely lifted. Suppose
\[
 X_0\leq X_1\leq\cdots\leq X_i\leq\cdots\quad(i<\delta)
\]
is a continuous chain at that level, its union is an object at that level,
and a fixed realization $b$ in a coupled extension satisfies
\[
 \tp(b/X_i)=\tp(b/X_0)^{\mathrm{fr}}_{X_i}
 \qquad(i<\delta).
\]
Then the same equality holds over $\bigcup_{i<\delta}X_i$.
The type at $X_0$ is required to be the appropriate free lift of $p$.
\end{definition}

Every finite-tuple marginal has this property. At a limit, local character
for the finite tuple gives freeness from some earlier stage, and
transitivity gives freeness from $X_0$. This is a direct application of
Proposition~\ref{calc:local-character}, including when the chain has small
cofinality.

\begin{proposition}\label{iso:finite-existence}
Let $\lambda$ be a sufficiently closed eligible level, let $X$ be an
object there, and let $p=\tp(b/X)$ be a finite-tuple type. For every
infinite $\theta<\lambda$ there is a same-level extension $X\leq U$
containing a realization of $p$ such that
\[
 \tp(b,c/X)\text{ is isolated relative to }b
 \quad\text{for every }c\in U\text{ with }|c|\leq\theta.
\]
More generally the assertion holds for a bounded mark $b$ satisfying
Definition~\ref{iso:marginal-continuity}, with $|b|\leq\theta$.
The closure requirements at the output level are uniform functions of
bounded arities; they do not require $\theta$ to have been fixed before
the level was chosen.
\end{proposition}

\begin{proof}
We prove the more general statement. Fix a bounded approximation list
$I_p$ in $X$ which determines $p$ at a sufficient testing arity. Choose
a much larger eligible level $\kappa$ and a cardinal $\rho$ such that
\[
 \lambda<\rho=\rho^\lambda,
 \qquad \rho^+<\kappa.
\]
Require $\rho$ to dominate the approximation and small-hull costs at
arity $\lambda$, and choose $\kappa$ after those set-sized bounds. Such
choices exist: first choose a sufficiently large power $2^\xi$ with
$\xi\geq\lambda$ for $\rho$, and then choose an eligible $\kappa$
above $\rho^+$ and all remaining bounds. Extend $X$ by a presentation
arrow to a level-$\kappa$ object $X_0$, and choose $Y_0\geq X_0$
containing a realization $b$ of the free lift of $p$.

We construct continuous pairs
\[
 X_i\leq Y_i\qquad(i\leq\rho^+)
\]
at level $\kappa$, with a single fixed $b$ in all the upper objects.
The invariant on the marked marginal is
\begin{equation}\label{iso:matrix-marginal}
 \tp(b/X_i)=\tp(b/X_0)^{\mathrm{fr}}_{X_i}.
\end{equation}
For $i<\rho^+$, we also keep increasing continuous sets
\[
 R_i\subseteq X_i,\qquad S_i\subseteq Y_i,\qquad
 R_i\subseteq S_i,\qquad |R_i|,|S_i|\leq\rho,
\]
with $I_p\subseteq R_i$ and $b\subseteq S_i$. They are bookkeeping
sets, not additional structure on the objects.

Here are the two closure requirements at a stage $i$ with
$\cf(i)>\lambda$.
\begin{enumerate}
\item Any specified at-most-$\lambda$ sets of base and top parameters
from $R_i,S_i$ are contained in a pair $A\leq V$ of level-$\lambda$
subobjects of $X_i\leq Y_i$, with $A\subseteq R_i$ and
$V\subseteq S_i$.
\item Every tuple $d$ of length at most $\lambda$ from $S_i$ has a
sequence of at least $\lambda$ copies inside $R_i$ computing its
actual type over $X_i$ on all tests of size less than $\lambda$.
For every subtuple and each such parameter test $Z$, all but at most
$|Z|+\aleph_0$ of the copies give its joint $D$-diagram.
\end{enumerate}

We explain how to arrange the requirements; in particular, they do not
amount to assuming a small saturated submodel. At successor stages,
process all at-most-$\lambda$ lists in the current parameter sets.
There are at most $\rho^\lambda=\rho$ of them. Mixed
L\"owenheim--Skolem supplies the requested level-$\lambda$ pairs.
Lemma~\ref{calc:approximations} supplies copies of each top list in the
current base, at the test sizes below $\lambda$ and with the displayed
exception estimate. Their total number of coordinates is at most
$\rho$. Close the sets under these operations for $\lambda^+$ steps;
the size is still $\rho$. If new elements are added later, repeat these
successor closures. At a limit $i$ of cofinality greater than $\lambda$,
every requested list was contained at an earlier stage. Local character
applied to that list, whose length is at most $\lambda<\cf(i)$, says
that its actual type over $X_i$ is free from some earlier stage.
Approximations placed in a later intervening successor base still
compute it over $X_i$ by the free-extension theorem. Their copies lie
in $R_i$. The same cofinality argument places every small-hull request
in an earlier closure. This proves both requirements at the indicated
limits.

At any such stage, if some list $d$ of length at most $\lambda$ from
$S_i$ makes $\tp(b,d/X_i)$ nonisolated relative to $b$, apply
Proposition~\ref{iso:alternative}. It gives a same-level extension of
$X_i$ in which this joint type has a nonfree extension while the
$b$-marginal remains free. By type-identifying amalgamation, extend
$Y_i$ into a common $Y_{i+1}$, identifying the old $(b,d)$ with that
realization. The new base is the extension just chosen. Transitivity
preserves~\eqref{iso:matrix-marginal}. At other stages use compatible
extensions and the bookkeeping closures. At limits use the working
scheme's unions; Definition~\ref{iso:marginal-continuity} preserves
the marginal invariant. All these unions have size $\kappa$, since
$\rho^+<\kappa$.

This process must reach an indicated stage at which every list in the
second closure requirement is isolated jointly with $b$. Suppose not,
and choose a failing list $d_i$ at every stage with $\cf(i)>\lambda$.
The set of these stages is stationary in the regular cardinal
$\rho^+$. Indeed, in any closed unbounded subset of $\rho^+$ take a
continuous increasing sequence of length $\lambda^+$ and its
supremum; the supremum is still below $\rho^+$, is in the closed
set, and has cofinality $\lambda^+$.

Because $S_i$ is continuous and $|d_i|\leq\lambda<\cf(i)$, there is
$j(i)\nu$ and lift the type to a level-$\lambda$ base by a
presentation arrow. Apply Proposition~\ref{iso:finite-existence} at
level $\lambda$ with $\theta=\nu$. We obtain a pair $A\leq U$ of
level $\lambda$ such that every tuple of length at most $\nu$ in $U$,
jointly with $b$, has isolation relative to $b$ over $A$. The original
anchors may be retained in $A$ throughout that construction.

Choose $\nu$ distinct indices from the family in
Corollary~\ref{calc:retractions}, and write the corresponding
approximate retractions as
\[
 r_j:U\longrightarrow A\qquad(j<\nu)
\]
such that each $a\in A$ is fixed by all but finitely many of them.
Use mixed L\"owenheim--Skolem to choose level-$\nu$ subobjects
$A'\leq U'$ of $A\leq U$ which contain $I_p,b$ in their indicated
places and satisfy
\begin{equation}\label{iso:retraction-closure}
 r_j[U']\subseteq A'\qquad(j<\nu).
\end{equation}
Here is the closure construction. Start with level-$\nu$ sections
containing the desired entries. From the current top of size $\nu$,
adjoin to the next base all its images under the $\nu$ selected maps;
there are at most $\nu\cdot\nu=\nu$ coordinates. Enlarge the next
top to contain that base and the old top. Iterate countably many
times and take unions. Same-level chain closure and the common upper
bound clause into $A,U$ give the pair and
\eqref{iso:retraction-closure}.

Fix any bounded tuple $d$ in $U'$. The tuple $(b,d)$ is still bounded
at $\nu$. The maps in~\eqref{iso:retraction-closure} place all its
images in $A'$. For a test $Z\subseteq A$, all but at most
$|Z|+\aleph_0$ of the maps fix $Z$ pointwise, and hence for all those
indices
\[
 D(r_j(b,d),Z)=D(b,d,Z).
\]
At a fixed testing arity below $\nu$, choose a bounded subsequence of
indices longer than the exception bound. Lemma~\ref{calc:retraction-descent}
gives
\[
 \tp(b,d/A)=\tp(b,d/A')^{\mathrm{fr}}_A.
\]
The type on the left is isolated, by the length-$\nu$ assertion at
level $\lambda$. Its uniform fragment bound for the actual arity
$|b,d|<\nu$ is below $\nu$. Downward transfer gives isolation of
$\tp(b,d/A')$ relative to $b$.

This argument applies separately to every bounded $d\subseteq U'$;
it makes no assumption that $d$ lies in one stage of the countable
construction. Thus $U'$ is all-dominated over $A'+b$. The retained
anchors and bounded diagram homogeneity identify its marginal with
the original $p$ by an isomorphism $A'\simeq X$. Transport gives the
required object over $X$. Its embedding into an actual ambient is
Proposition~\ref{iso:prime}.
\end{proof}

\subsection{Independent lists and coherent witnesses}

Finite marks already have all-dominated extensions.  To obtain the same
conclusion for a bounded independent list of finite marks, we must first
show that its finite product data determine one whole type and that this
type persists along the actual coupled chains used above.

\begin{definition}\label{iso:independent-definition}
A list $(b_i)_{i<\delta}$ of finite tuples is
\emph{product-independent over $A$} if each finite sublist has the
product of its marginal types over $A$.
A \emph{witnessing chain} is a continuous chain $(M_i)_{i\leq\delta}$
of objects, with $M_0=A$, such that $b_i$ lies in $M_{i+1}$ and
\[
 \tp(b_i/M_i)=\tp(b_i/A)^{\mathrm{fr}}_{M_i}.
\]
It is an \emph{all-dominated-increment chain} if, in addition,
$M_{i+1}$ is all-dominated over $M_i+b_i$. In uses at level $\mu$,
the chain has total size $\mu$, in particular $|\delta|\leq\mu$.
\end{definition}

\begin{lemma}\label{iso:finite-domination}
Suppose $(M_i)_{i\leq\delta}$ is an all-dominated-increment chain over
$A$ for finite tuples $(b_i)_{i<\delta}$. If a finite tuple $x$ in an
actual coupling has product over $A$ with every finite selection of
the accumulated $b_i$, then $\tp(x/M_\delta)$ is free from $A$.
\end{lemma}

\begin{proof}
Induct on the stage. At a successor $i+1$, the finite tuple $(x,b_i)$
has product with every finite selection of earlier marks, by the
finite product rules. The induction hypothesis applied to this tuple
says that its joint type over $M_i$ is free from $A$. Products lift
freely by Proposition~\ref{calc:products}; hence $x$ and $b_i$ still have
product over $M_i$. Proposition~\ref{iso:prime}, applied to the
all-dominated increment $M_{i+1}$, makes $x/M_{i+1}$ free from $M_i$.
Transitivity makes it free from $A$.

At a limit $j$, local character for the finite tuple $x$ gives a
proper stage $i\chi$. Cantor's Theorem gives
$\epsilon\le\chi$, and minimality gives $2^{|i|}\le\chi$
for every $i<\epsilon$. Consequently
\[
 \left|{}^{<\epsilon}2\right|\le\chi,
 \qquad 2^\epsilon\le 2^\chi<\mu,
\]
where $\mu$ is the common level. Every accumulator and branch
world below will have size $\mu$, and the total number of
amalgamations remains below $\mu$.

We construct branch worlds $W_s\in\mathcal C_m$ for
$s\in{}^{\le\epsilon}2$, carrying tuples $f_s$, with
coherent full arrows along each branch. Their proper
boundaries have compatible arrows
\[
 q_s:\partial W_s\longrightarrow\partial A
\]
into an increasing common accumulator $A\in\mathcal C_m$.
The accumulator may be enlarged at each operation; existing
boundary arrows are always composed with its enlargement
arrow. The invariant requires coherence of these boundary
arrows with the branch arrows. It does not require full maps
of all the branch worlds into the accumulator to be retained.

Start with $W_\varnothing=X^-$, its tuple $f$, and the
identity boundary map into $A=X^-$. At a node $s$, diagram
preservation along the branch shows that
$D(f_s)=D(f)$. Bounded homogeneity supplies an isomorphism
\[
 k_s:X^-\overset{\cong}{\longrightarrow}W_s,
 \qquad k_s(f)=f_s.
\]
There is no coherence requirement on the choices of $k_s$.
Choose the minus child to be a copy of $Y^-$ attached over
$W_s$ by $k_s^{-1}$, and the plus child to be a copy of
$Y^+$ attached by $e k_s^{-1}$. These choices give the full
branch arrows. In each child, $f$ denotes the image of $f_s$;
the corresponding upper boundary lists have diagrams
$\delta_0$ and $\delta_1$ with it. Transporting $h$ gives
a boundary arrow
\[
 h_s:\partial W_{s0}\longrightarrow\partial W_{s1}
\]
over $\partial W_s$, matching the two copies of $v$.

Apply the already proved completion theorem in dimension $m$
to $q_s$. After enlarging the accumulator, this gives a full
map $W_s\to A_0$ extending $q_s$. Ordinary amalgamation in
$\mathcal C_m$ then puts the plus child in an enlargement
$A_1$ over this full map. Let $G_1:W_{s1}\to A_1$ be the
resulting arrow. Retain its boundary restriction as $q_{s1}$,
and define
\[
 q_{s0}=q_{s1}h_s.
\]
Both restrict to the preceding $q_s$, after enlargement, and
the two boundary copies of $v$ have one common image $v_s$
in $A_1$. The temporary full maps to $A_0$ and $A_1$ are
no longer part of the invariant. In particular the minus
child has not been required to send its copy of $f$ to the
temporary image of $f_s$ in the accumulator.

\begin{figure}[htbp]
\centering
\begin{tikzpicture}[>=Latex, every node/.style={font=\small},
  world/.style={draw,rounded corners,inner sep=5pt},
  boundary/.style={draw,inner sep=4pt}]
 \node[world] (w) at (0,2.4) {$W_s,f_s$};
 \node[world] (w0) at (-2,1.1) {$W_{s0},f_{s0}$};
 \node[world] (w1) at (2,1.1) {$W_{s1},f_{s1}$};
 \node[boundary] (b0) at (-2,-.1) {$\partial W_{s0}$};
 \node[boundary] (b1) at (2,-.1) {$\partial W_{s1}$};
 \node[world] (a) at (0,-1.7) {$A_1\ni v_s$};
 \draw[->] (w) -- (w0);
 \draw[->] (w) -- (w1);
 \draw (w0) -- node[left] {boundary} (b0);
 \draw (w1) -- node[right] {boundary} (b1);
 \draw[->] (b0) -- node[above] {$h_s$} (b1);
 \draw[->,dashed] (b0) -- node[left] {$q_{s0}$} (a);
 \draw[->,dashed] (b1) -- node[right] {$q_{s1}$} (a);
 \draw[->,dotted,rounded corners=6pt] (w1.east) -- (4.2,1.1)
   -- node[right] {$G_1$} (4.2,-1.7) -- (a.east);
\end{tikzpicture}
\caption{A return-tree split. Solid arrows between worlds are
retained along their separate branches. Dashed boundary maps
persist in the common accumulator and agree on the test $v_s$.
Each dashed arrow denotes a compatible family of maps into the
proper projections of $A_1$.
The dotted full map is used to choose the plus boundary map
and need not be retained at later splits. Full maps of all
leaf worlds are installed only after the splitting tests have
been fixed.}
\label{iter:fig-return-tree}
\end{figure}

Process the nodes of each level successively. At a limit
height take the union of the worlds along each branch and
the union of the accumulators constructed so far. Their
sizes are still $\mu$. The boundary arrows into the union
accumulator exist by the chain and common-upper-bound clauses
in every proper projection. Full branch arrows and the
carried tuples also pass to the unions. This establishes
the invariant through height $\epsilon$.

At that height, apply lower-dimensional completion to each
leaf boundary map, successively enlarging the accumulator.
This supplies a full map of each $W_\eta$, for
$\eta\in{}^\epsilon2$, extending its retained boundary
map. There are fewer than $\mu$ leaves, so the final union
is still at level $\mu$. If two leaves first differ after
a node $s$, their images of $f$ have diagrams $\delta_0$
and $\delta_1$ over the common tuple $v_s$. Indeed the
corresponding copy of $v$ was in that child's boundary,
remained there along that branch, and its boundary image was never
changed except by composition with an accumulator arrow.
Thus the final images of $f$ occupy more than $\chi$
orbits over the entries of $(v_s:s\in{}^{<\epsilon}2)$.
This parameter list has size at most $\chi$. The orbit
bound of Lemma~\ref{calc:parameter-orbits} gives the
contradiction. The claimed equality of types of $v$ follows.

To pass from this type equality to the full pair diagrams, retain
an arbitrary bounded tuple $a$ from the lower face $X^-$.
The marginal of $b^+$ over
$X^+$ is the prescribed free lift from $e(X^-)$.
Relative isolation of the source type of $(b^-,v)$ and
Lemma~\ref{iso:free-isolation} therefore identify the actual type
of $(b^+,h(v))$ over $X^+$ with the free lift of that source type.

Choose sufficiently long bounded approximation lists in $X^-$
computing the source type.  Their images under $e$ compute its
free lift over $X^+$ by Theorem~\ref{calc:free-extension}.
Base homogeneity gives an isomorphism $X^-\cong X^+$ matching
$a$ and these lists with their images under $e$, since $e$
preserves their joint bounded diagram.  The transport assertion
for the approximation lists says that this isomorphism carries
the whole source type to the type of $(b^+,h(v))$.
Lemma~\ref{mark:pair-isomorphism} now extends it to an isomorphism
of the marked pairs matching $(a,v)$ with $(e(a),h(v))$.
Every bounded boundary list is of this form.  Thus its full
$\mathcal C_n$-diagram is preserved, including cross-face equalities.

We finish the induction by deriving completion from this
diagram equality. Present the source $J$ on a well-order.
Its boundary union is a natural collection of the
designated term sorts in that presentation. Choose nested
bounded lists $d_i$ exhausting $J$, including increasing
strong submodel enumerations in every vertex. We construct
extensions $K_i$ of $K$ and compatible assignments of
$d_i$ into $K_i$ satisfying
\[
 D_J(d_i,u)=D_{K_i}(d_i',h(u))
 \quad\text{for every bounded boundary list }u.
 \tag{C}
\]
Here and subsequently $h$ is composed with the current
extension arrow. At the start the assertion for the empty
list is exactly the boundary diagram equality just proved.

For the next list prescribe the source joint diagrams on
the parameter set consisting of the boundary images and
the previous assignment. Each bounded local request,
including the whole previous assigned list, is possible
by saturation: the parameter diagram agrees by $(\mathrm C)$.
This also checks repetitions and equalities between old
entries and boundary entries, so the requests define one
coherent prescription. Apply compact placement in a
well-ordered chart of $K_i$, keeping these previous
entries fixed. Work at one bounded cardinal large enough
for the profile count, the new tuple, and the testing
bound for the source boundary layout with the previous
tuple included. The resulting placement lies in a
level-$\mu$ extension $K_{i+1}$.

To check $(\mathrm C)$ beyond that initial testing cardinal,
pull the candidate diagrams back along $h$ to the natural
boundary layout of $J$. Their local possibility there
follows from the boundary diagram equality and saturation.
Lemma~\ref{calc:compact-placement} compactifies these
requests over this source layout, and
Proposition~\ref{calc:testing} says that agreement at the chosen
testing bound determines all bounded comparisons.
The actual images of the boundary inside $K_i$ have not
been assumed to form a natural layout. All uses of that
hypothesis are on the source layout after pullback.

Continue through $\omega$ steps and take the union of the
$K_i$. The working-package criterion, with the included
strong submodel enumerations, makes the union assignment
an arrow $J\to K^*$. Whenever a boundary entry is first
included in $d_i$, its equality test against that boundary
entry forces its assigned image to be $h$ of that entry.
The union arrow therefore extends the entire boundary
map. The map from $K$ is the chain inclusion. This proves
completion and closes the induction.
\end{proof}

\subsection{A bounded support for boundary tests}

We have extended boundary maps into common extensions.  Exact lifting
must instead land onto the given target.  The next lemma supplies bounded
data that control a tuple's boundary comparisons at a fixed bounded test
arity.  Together with uniform testing, this permits back-and-forth to
remain inside the two given systems.

\begin{lemma}[Fixed parameters for a boundary test function]
\label{iter:boundary-fixed-parameters}
Fix $n<\omega$. At further sufficiently closed levels,
let $J\in\mathcal C_n$, let $z$ be a bounded tuple of
$J$, and let $\sigma$ be a bounded infinite test arity.
There is a bounded list $a$ in $\partial J$ such that
every boundary automorphism $\alpha$ fixing $a$ pointwise
satisfies
\[
 D_J(z,u)=D_J(z,\alpha(u))
 \quad\text{for every boundary tuple }u
 \text{ of length at most }\sigma.
 \tag{F}
\]
A boundary automorphism means a compatible family of
isomorphisms of all proper projections; a full
automorphism of $J$ is not assumed.
\end{lemma}

\begin{proof}
The assertion is immediate for the empty boundary.
Suppose it fails otherwise. Choose a bounded infinite
$\chi$ with $\chi^{|z|+\aleph_0}=\chi$, bounding
$\sigma$ and the orbit-counting and label costs. Let
$\epsilon$ be the least cardinal with $2^\epsilon>\chi$.
Choose a smaller eligible level $\nu$ such that
\[
 |z|+\sigma+2^\chi<\nu<\mu,
\]
where $\mu$ is the level of $J$, with all required testing bounds
below $\nu$ and with
Theorem~\ref{iter:boundary-completion} available at $\nu$.
The further closure requirement on the level of $J$
ensures this choice. It is a finite refinement for this
fixed $n$.

Fix a well-ordered presentation $J=F_n(I)$. Construct
continuous subpresentations $J_i$ of size $\nu$ for
$i\le\epsilon$, beginning with $z$ in $J_0$.
At step $i$, the boundary of $J_i$ is a bounded parameter
set in $J$. By the assumed failure, a boundary
automorphism $\alpha_i$ of $J$ fixes it pointwise and
changes the value of the function at some tuple $u_i$
of length at most $\sigma$. Thus
\[
 D_J(z,u_i)\ne D_J(z,\alpha_i(u_i)).
 \tag{S}
\]
We choose $J_{i+1}$ containing both tests so that
$\alpha_i$ restricts to an automorphism of its boundary.

Here is the support closure for this choice. Begin with
the positions for $J_i$, $z$, $u_i$, and
$\alpha_i(u_i)$, padding to size $\nu$. For every element
of every proper projected subpresentation currently
generated, add positions for its image and its inverse
image under the corresponding face map of $\alpha_i$.
There are finitely many faces and $\nu$ elements in their
union, and each representation uses finitely many
positions. Repeat this operation countably many times.
The resulting position set still has size $\nu$.
Every element generated at its union appeared at a
finite stage, so both its image and inverse image are
generated in the union. Hence all restricted face maps
are onto and remain compatible with the specified
inclusions. They give the asserted boundary
automorphism of $J_{i+1}$. At a limit use the union of
the position sets. Mixed diagram preservation transfers
$(\mathrm S)$ to $J_{i+1}$, since $|z|+\sigma<\nu$.

Now build a binary tree of boundary embeddings
\[
 q_s:\partial J_i\longrightarrow\partial A,
 \qquad s\in{}^i2,
\]
where $A$ is an increasing accumulator of size $\nu$.
Start with $A=J_0$ and the identity map on $\partial J_0$.
At a successor node first apply completion to $q_s$
on $J_i$ and then amalgamate $J_{i+1}$ over that full
copy of $J_i$. This yields an arrow
$G_s:J_{i+1}\to A'$ whose boundary extends $q_s$.
Define the two next boundary embeddings by
\[
 q_{s0}=\partial G_s,
 \qquad
 q_{s1}=(\partial G_s)\alpha_i^{-1}.
\]
They restrict to the same old $q_s$, because
$\alpha_i$ fixes $\partial J_i$ pointwise. The common
parameter test $G_s(u_i)$ is the image of $u_i$ on
branch $s0$ and of $\alpha_i(u_i)$ on branch $s1$.
Only these boundary embeddings are retained for later
steps; the full map $G_s$ is temporary.

At limits the continuity of the $J_i$ and the
common-upper-bound clauses give the boundary maps into
the union accumulator. At height $\epsilon$, complete
the boundary maps to full maps of $J_\epsilon$, one
leaf at a time. The full maps at the leaves carry $z$.
If two leaves first separate at $s\in{}^i2$, their
images of $z$ have the two distinct diagrams from
$(\mathrm S)$ over the one retained test $G_s(u_i)$.
This follows from preservation by their final full maps
and from coherence of their boundary maps with the
chosen maps at the split.

There are at most $\chi$ nonterminal nodes, hence at
most $\chi$ parameters in all the splitting tests.
There are $2^\epsilon>\chi$ distinguishable leaf
images of $z$. All leaf completions and all unions
remain at level $\nu$, since $2^\chi<\nu$.
Lemma~\ref{calc:parameter-orbits} again contradicts
this number of orbits over the tests. Thus the bounded
fixing list $a$ exists.
\end{proof}

\begin{theorem}[Exact boundary lifting]
\label{iter:exact-boundary}
For each finite $n$, at further sufficiently closed
levels every boundary isomorphism
$h:\partial J\overset{\cong}{\longrightarrow}\partial K$
between $\mathcal C_n$-objects at the same level
extends to an isomorphism $J\cong K$ onto the given
target. All the prescribed marks and bounded named
data are preserved.
\end{theorem}

\begin{proof}
We build a back-and-forth sequence of matches
$a\mapsto a'$ of bounded tuples, maintaining
\[
 D_J(a,u)=D_K(a',h(u))
 \quad\text{for every bounded boundary tuple }u.
 \tag{BF}
\]
For the empty tuple this is
Lemma~\ref{iter:boundary-diagrams}. Suppose that a
match satisfying $(\mathrm{BF})$ has been chosen, and let $z$
be any bounded enlargement of $a$ in $J$.

Take a bounded infinite $\sigma$ at least the uniform
testing bound for a tuple of length $|z|$ over the
natural boundary layout of a $\mathcal C_n$-object.
Choose fixing data $c$ for $z,\sigma$ in $\partial J$
by Lemma~\ref{iter:boundary-fixed-parameters}.
The maintained equality with the particular boundary
list $c$ gives
\[
 D_J(a,c)=D_K(a',h(c)).
\]
Working-package homogeneity supplies a full
isomorphism $H:J\cong K$ carrying $a$ to $a'$ and
$c$ to $h(c)$. Put
$\alpha=(\partial H)^{-1}h$. This is a boundary
automorphism of $J$ fixing $c$ pointwise. Therefore,
for every boundary tuple $u$ of length at most
$\sigma$,
\[
 \begin{split}
 D_K(H(z),h(u))
 &=D_J(z,\alpha(u))\\
 &=D_J(z,u).
 \end{split}
 \tag{BT}
\]

We justify explicitly the passage from these tests
to all bounded boundary tests. By
Theorem~\ref{iter:boundary-completion}, embed $J$
into a same-level extension $K^*$ of $K$ by an arrow
$j$ extending $h$. Both $j(z)$ and $H(z)$ are now
tuples in $K^*$, and $(\mathrm{BT})$ says that their diagrams
agree over boundary tests from $K$ of size at most
$\sigma$. The boundary of $K$, in a well-ordered
chart of $K$, is a natural collection of term sorts.
The types of these two tuples over $K$ have order
placements by the one-dimensional calculus.
Proposition~\ref{calc:testing} restricted to this natural
boundary layout therefore gives equality over every
bounded boundary test. Preservation by $j$ then
shows
\[
 D_K(H(z),h(u))=D_J(z,u)
\]
for all bounded $u$. Thus $z\mapsto H(z)$ extends
the previous match and satisfies $(\mathrm{BF})$.

Apply this extension step alternately to $J,K$ with
$h$, and to $K,J$ with $h^{-1}$. Their level has
countable cofinality, so countably many bounded
enlargements can exhaust both systems. In each
vertex choose increasing smaller strong submodels
whose enumerations are included in these tuples.
The union assignment is onto in every component
and is an arrow by the working-package map
criterion; the reverse construction gives its
inverse arrow. If an entry lies on the boundary,
its equality test with that boundary entry in
$(\mathrm{BF})$ forces its image to be exactly the image
under $h$. The resulting isomorphism therefore
extends all of $h$, as required.
\end{proof}
==== END Eventual-Categoricity-for-Abstract-Elementary-Classes//09-marked-boundaries.tex ====

==== BEGIN Eventual-Categoricity-for-Abstract-Elementary-Classes//10-geometry.tex ====
\section{A minimal type and its geometry}
\label{geom:section-geometry}

We continue with the fixed AEC $\K$ that is categorical in unboundedly
many cardinals.  Throughout this Section, a level is eligible for the
single-model working scheme and for the refinements of the calculus
that are explicitly invoked.  The first level chosen below is denoted
by $\lambda_0$.  The level used for all finite marked constructions will
be a later cardinal $\lambda$; these two choices serve different purposes.

\begin{lemma}[Preservation of nonalgebraicity]
\label{geom:nonalgebraic}
Let $p$ be a nonalgebraic singleton type over an object $A$ of a working
scheme.  Its free lift over an extension $B$ is nonalgebraic.  The same
assertion holds for a mixed arrow whenever the input arity and the
testing bounds lie below the smaller level.
\end{lemma}

\begin{proof}
Suppose that the free lift were realized by $c\in B$.  Include equality
with $c$ among its tests.  To evaluate that test, the free-extension
construction moves $c$ into $A$, over enough of the chosen
approximations for $p$.  Its value is then the value of equality with an
element of $A$.  Every such equality has value false for $p$, whereas
equality with its alleged realization $c$ has value true.  This
contradicts the evaluation rule in Theorem~\ref{calc:free-extension}.
The mixed-level construction uses the same rule with the bounds taken
below the input level.
\end{proof}

\begin{proposition}[A minimal type]
\label{geom:minimal-type}
There is a sufficiently closed single-model level $\lambda_0$, a model
$M_0\in\K$ of size $\lambda_0$, and a nonalgebraic singleton type
$p_0$ over $M_0$ such that, over every $M_0\leq_\K A\in\K$ of size
$\lambda_0$, there is exactly one nonalgebraic extension of $p_0$.
This extension is its free lift.
\end{proposition}

\begin{proof}
Choose $\lambda_0$ with the single-model working package, the
stationary calculus, the all-dominated hull construction, and the
singleton type bound of Theorem~\ref{lev:amalgamation}(3).
Thus there are at most $\lambda_0$ singleton
types over a model of that size.  We may require at the outset strict
closure under all the fixed bounds used below for finite tuples and
their bounded tests.

There is a nonalgebraic singleton type at this level.  For example,
extend an order presentation by a fresh skeleton point.  That point is
outside the old model: if it were a labeled term on finitely many old
indices, adding a second distinct skeleton point with the same order
pattern over those indices would make both equal that term, contrary
to the distinctness of the skeleton.

Suppose that no nonalgebraic singleton type at this level is minimal in
the stated sense.  A nonalgebraic type always has a nonalgebraic free
extension by Lemma~\ref{geom:nonalgebraic}.  Consequently every such
type has two distinct nonalgebraic extensions over some model of size
$\lambda_0$.

Let $\epsilon$ be the least infinite cardinal with
$2^\epsilon>\lambda_0$.  Then $\epsilon\leq\lambda_0$ and
$2^{|i|}\leq\lambda_0$ for $i<\epsilon$.  Construct a continuous chain
$(A_i:i\leq\epsilon)$ of models of size $\lambda_0$ and types
$p_\eta$ over $A_i$, for $\eta\in{}^i2$, as follows.  At a successor
step, split every current $p_\eta$ over a model extending $A_i$.
There are at most $\lambda_0$ such models.  Successive amalgamation
over $A_i$, followed by unions, puts all of them into one next base
$A_{i+1}$ of size $\lambda_0$.  Freely extend each of the two split
types to that base.  Their restrictions to the splitting model are
different, so they remain different, and
Lemma~\ref{geom:nonalgebraic} keeps them nonalgebraic.

Along each branch retain a witness model and the same distinguished
realization.  The required successor map exists by amalgamation with
identification of realizations having the same type over the preceding
base.  At a limit take the unions of the common bases and, separately
on each branch, of its coherent witness models.  The realization is
outside every base stage, so it is outside the union base.  All these
unions have size $\lambda_0$ because the construction has length at
most $\lambda_0$.  At the final stage distinct branches have different
types over $A_\epsilon$, witnessed at their first splitting stage.
This gives more than $\lambda_0$ singleton types over $A_\epsilon$,
contrary to the type bound.  A minimal $p_0$ therefore exists.  Its
unique nonalgebraic extensions are free by existence of free lifts.
\end{proof}

The passage from a minimal type to closure and dimension follows the
geometric pattern of first-order categoricity developed through strongly
minimal sets; see Baldwin and Lachlan \cite[Sections~1--2]{BaldwinLachlan1971}.
Here the required containment, exchange, and change-of-base properties
are established directly for the AEC and its locally constructed types.

\subsection{Finite configurations over the chosen model}

\begin{definition}
\label{geom:points}
For $M_0\leq_\K M$ with $\|M\|\geq\lambda_0$, let $P(M)$ be the
set of realizations of $p_0$ in $M$.  More explicitly, $a\in P(M)$
means that in a strong section $N\leq_\K M$ of size $\lambda_0$
containing $M_0\cup\{a\}$, the type $\tp(a/M_0)$ is $p_0$.
A finite ordered list of distinct points in $P(M)$ is independent if
its type over $M_0$, computed in such a section, is the product of the
corresponding copies of $p_0$.
\end{definition}

These definitions do not depend on the section.  Two sections lie in
a third section of size $\lambda_0$, by the L\"owenheim--Skolem axiom
and coherence.  The embeddings into that section preserve their types
over $M_0$.  Products are permutation invariant, so independence is a
property of the underlying finite set.  Strong embeddings over $M_0$
preserve and reflect both membership in $P$ and finite independence.

We give a precise meaning to the containment test used in constructing
closure.  Fix a finite configuration $F\cup\{x\}\subseteq P(M)$ and
a size-$\lambda_0$ section $N$ containing it and $M_0$.  Say that $F$
\emph{forces} $x$ if, whenever $f:N\to W$ is a strong embedding fixing
$M_0$, with $W$ of size $\lambda_0$, and
$M_0\leq_\K D\leq_\K W$ has size $\lambda_0$ and contains $f[F]$,
one has $f(x)\in D$.  Thus the test permits a common extension of the
finite configuration and the proposed model; it does not presume that
intersections of strong models are strong models.

The test is invariant under the type of the entire finite
configuration over $M_0$.  Indeed, an identification of two copies of
that type is witnessed in an amalgam.  Any further configuration
witnessing failure of forced containment can be amalgamated with that
identification over the first witness model.  Its avoiding submodel
and the omitted point remain disjoint at that point because the maps
are injective.  This transports the failure to the second copy.  The
reverse transport is identical with the copies interchanged.

\begin{lemma}[The containment test]
\label{geom:containment-test}
For a finite independent set $S\subseteq P(M)$ and $x\in P(M)$,
$S$ fails to force $x$ if and only if $S\cup\{x\}$ is independent
with $x\notin S$.
\end{lemma}

\begin{proof}
First suppose that a coupling contains a model $D$ over $M_0$ and $S$
but omits $x$.  The type of $x$ over $D$ is a nonalgebraic extension of
$p_0$.  By Proposition~\ref{geom:minimal-type} it is the free lift of
$p_0$.  Restricting its parameters to $S$ shows, by
Proposition~\ref{calc:products}, that $x$ has product type with $S$ over
$M_0$.

Conversely suppose that $S,x$ has product type.  Use
Theorem~\ref{iso:all-lengths} to obtain a model all-dominated over
$M_0+S$, and amalgamate it with the actual finite configuration,
identifying the copy of $S$.  The domination conclusion of
Proposition~\ref{iso:prime} makes $x$ free over this model from $M_0$.
It is outside the model by Lemma~\ref{geom:nonalgebraic}.  The same
amalgamation can retain any further specified finite entries of the
original configuration.  This is a coupling witnessing that $S$ does
not force $x$.
\end{proof}

\begin{theorem}[The geometry of the minimal type]
\label{geom:pregeometry}
On $P(M)$, for every $M_0\leq_\K M$ of size at least $\lambda_0$,
the preceding finite independence is the independence relation of a
finitary pregeometry.  Its closure, denoted by $\cl_M$, has the
following properties.
\begin{enumerate}
\item For finite $F\subseteq P(M)$ and any maximal independent
      $S\subseteq F$, the set $\cl_M(F)$ consists exactly of those
      points that do not independently extend $S$.  Equivalently,
      $\cl_M(F)$ is the set of points forced by $F$.
\item Strong embeddings over $M_0$ preserve and reflect finite
      closure.  If $M_0\leq_\K A\leq_\K M$, then
      $P(A)$ is relatively closed in $P(M)$.
\item For finite $F$, $|\cl_M(F)|\leq\lambda_0$.  For every infinite
      $F\subseteq P(M)$,
      \[
      |\cl_M(F)|\leq |F|+\lambda_0.
      \]
\end{enumerate}
In particular bases exist, all bases have the same cardinality, and
each point of the span of a basis has finite basis support.
\end{theorem}

\begin{proof}
Choose a maximal independent subset $S$ of a finite $F$.  Every
$y\in F\setminus S$ fails to independently extend $S$, so
Lemma~\ref{geom:containment-test} says that every model containing $S$
in the actual configuration must contain all of $F$.  A point that
fails to independently extend $S$ is therefore forced by $F$.
If $x$ independently extends $S$, the avoiding dominated model from
Lemma~\ref{geom:containment-test} can be adjoined while retaining
$F,x$.  It contains $F$ by the preceding observation and omits $x$.
Thus $F$ does not force $x$.  This proves the first assertion and its
independence of the choice of $S$.

Define closure on arbitrary subsets by taking the union of closures
of finite subsets.  Extensivity and monotonicity hold directly from
the containment test.  To verify idempotence on finite configurations,
suppose that finitely many $y_j$ are in $\cl_M(F)$ and that $x$
independently extends a maximal independent $S\subseteq F$.  The
avoiding model over $S$ can be coupled with the whole finite
configuration $F,(y_j),x$.  It contains $F$ and every $y_j$, because
all these points are forced by $S$, and it omits $x$.  Hence the
$y_j$ cannot force $x$.  Finite character now yields idempotence for
all subsets.

For exchange, it suffices by finite character to take finite $F$ and
points $x,y$ with
\[
y\in\cl_M(F\cup\{x\})\setminus\cl_M(F).
\]
If $x\in\cl_M(F)$, idempotence would imply $y\in\cl_M(F)$, so
$x\notin\cl_M(F)$.  Let $S$ be a maximal independent subset of $F$.
Then $S,x$ and $S,y$ are independent.  Since every member of $F$ is
already forced by $S$, the set $S\cup\{x\}$ is maximal independent
in $F\cup\{x\}$.  The displayed membership says that $S,x,y$ is
dependent.  Permutation invariance of products makes $S,y,x$
dependent as well.  Applying the first assertion with $S\cup\{y\}$
gives $x\in\cl_M(F\cup\{y\})$.  This is exchange.

Preservation and reflection follow from the invariant finite-type
definition and the containment test.  For relative closedness, take
finite $F\subseteq P(A)$ and $x\in\cl_M(F)$.  Choose
$D\leq_\K A$ of size $\lambda_0$ containing $M_0\cup F$, and then
choose a section of $M$ containing $D\cup\{x\}$.  Forced containment
gives $x\in D\subseteq A$.  The finite closure of $F$ lies in this
same $D$, proving the finite cardinal bound.  There are $|F|$ finite
subsets of an infinite $F$, so finite character proves the displayed
bound.

For completeness, a maximal independent subset of a set can be
constructed by well-ordering it and retaining a point precisely when
it is outside the span of the points retained earlier.  Finite
character makes the resulting set independent, and maximality makes
it spanning.  If an independent set is spanned by a finite set of
$n$ points, it has at most $n$ points: successively insert its points
into a spanning list, using exchange to remove one of the original
points whenever a new independent point is inserted.  After $n$
insertions no further independent point is in the span.  This also
proves equality of finite basis sizes.

For infinite bases $H,J$ of the same closed set, choose for each
$j\in J$ a finite support $S_j\subseteq H$.  Then
$\cl(J)\subseteq\cl(\bigcup_{j\in J}S_j)$.  Independence of $H$
implies $H\subseteq\bigcup_{j\in J}S_j$, because a member of $H$
cannot belong to the span of the other members.  Hence
$|H|\leq|J|$; interchanging the bases gives the reverse inequality.
The finite argument excludes the possibility of one basis finite
and the other infinite.  Finally, for a closed $C$, the operator
$U\mapsto\cl(C\cup U)\setminus C$ on $P(M)\setminus C$ satisfies
the same closure and exchange axioms.  Finite character follows by
discarding all but the finitely many entries of $U$ in a dependence
witness.  Applying the preceding constructions to this operator
gives relative bases and their finite supports.
\end{proof}

\subsection{Pointed levels and change of base}

Choose an enumeration $\bar m_0$ of $M_0$ and place it as a strong
model in a sufficiently large well-ordered presentation of $\K$.
Such a placement exists by the order construction and categoricity at
$\lambda_0$.  Fix the stabilized diagram $\Delta$ of this entire
enumeration.  The initial supporting positions of this placement will
be held fixed in later order presentations.

\begin{proposition}[Pointed working levels]
\label{geom:pointed-levels}
At all sufficiently closed levels $\mu$ above the bounds for
$|\bar m_0|=\lambda_0$, models with a distinguished strong copy of
$M_0$ whose enumeration has diagram $\Delta$ form a categorical
working scheme.  Arrows preserve the indicated copy pointwise.
For a pointed model $B$ at such a level, $p_0$ has a unique
nonalgebraic extension $p^B$ over $B$; it is its free lift.  This family
lifts freely along pointed arrows, including the permitted mixed
arrows.  Naming further bounded data of a fixed diagram within the
base does not change type computation over the whole base.
\end{proposition}

\begin{proof}
The enumeration is a bounded tuple at $\mu$.  Bounded-diagram
homogeneity in Proposition~\ref{lev:closure-categoricity} carries it
between any two instances of $\Delta$ by an isomorphism of the entire
models.  The pointed version of the working package follows by
reserving its supporting positions and including the enumeration in
every relevant diagram, as in
Proposition~\ref{lev:named-package}.

Existence of $p^B$ is mixed free extension of $p_0$, and
Lemma~\ref{geom:nonalgebraic} gives nonalgebraicity.  To prove
uniqueness, take two nonalgebraic extensions over $B$.  A distinguishing
test for singleton types may be chosen with a fixed bound below
$\lambda_0$.  For any such parameter set $Z\subseteq B$, choose
$M_0\leq_\K A\leq_\K B$ of size $\lambda_0$ containing $Z$.
Both types restrict to nonalgebraic extensions of $p_0$ over $A$ and
are equal there by Proposition~\ref{geom:minimal-type}.  Their
diagrams on $Z$ are consequently equal.  The bounded testing theorem
gives equality over $B$.  Uniqueness and transitivity of free
extension prove the assertion for pointed arrows.

All distinguished data here already belong to the parameter model.
An amalgam over that model fixes them, and an identification of types
over that model respects them.  Thus adding them as constants does
not change this type computation.
\end{proof}

\begin{proposition}[Change of base for the geometry]
\label{geom:base-change}
Let $B$ be a pointed model at a sufficiently closed level much larger
than $\lambda_0$.  A finite list of points in an extension of $B$ is
independent over the closed set $P(B)$ in the geometry of
Theorem~\ref{geom:pregeometry} if and only if its type over $B$ is the
product of the corresponding copies of $p^B$.
\end{proposition}

\begin{proof}
A product can be witnessed by successive free realizations in models
containing all preceding entries.  Each realization is outside that
model by Lemma~\ref{geom:nonalgebraic}.  Its point set is relatively
closed, so the realization is outside the geometric span of $P(B)$
and the earlier entries.  This proves one implication.

For the converse let $x$ be a finite list independent over $P(B)$.
Fix a parameter test $Z\subseteq B$ large enough to be used in the
uniform comparison of the type of $x$ over $B$, but with
$|Z|<\lambda_0$.  Choose a regular infinite $\theta<\lambda_0$
with $|Z|<\theta$.  We may and do choose $\lambda_0$ closed enough
that the comparisons and local-character bounds used here fit below
it.

Inside $B$ choose lists $x_i$, $i<\theta$, so that every
$D^\K(x_i,Z)$ equals $D^\K(x,Z)$ and all the $x_i$ together are
independent over $M_0$.  To make the successor choice, include in the
bounded match the entire enumeration of $M_0$, $Z$, and all earlier
copies.  The original $x$, being independent over $P(B)$, is independent
from those earlier copies.  Saturation realizes its joint diagram
inside $B$.  Diagram equality is witnessed by an isomorphism, so it
preserves every finite independence comparison over $M_0$.  The total
parameters at every choice are bounded at the level of $B$.

Take a strong section $N\leq_\K B$ of size $\lambda_0$ containing
$M_0$, $Z$, and all the copies.  Their finite sublists have product
type over $M_0$.  The independent-list and finite-domination
conclusions of Theorem~\ref{iso:independent-lists} give a continuous
witness chain $(A_i:i\leq\theta)$ inside $N$, starting at $M_0$, in
which $x_i$ is free over $A_i$ from $M_0$ and is included in
$A_{i+1}$.  One may keep the chain inside $N$: at each step primeness
embeds the required all-dominated increment into $N$ over its already
placed base and the specified next list.  At limits finite domination
keeps the next finite list free, and unions remain strong in $N$.

Since $\cf(\theta)>|Z|$, local character applies to $\tp(Z/A_\theta)$.
It is free from some $A_i$.  For a later $j<\theta$, its restriction
to $A_{j+1}$ is free over $A_j$, so $Z$ and $x_j$ have product over
$A_j$.  The type of $x_j$ over $A_j$ is free from $M_0$.
The base-change identity in Proposition~\ref{calc:products} therefore
says that $x_j$ has product with $Z$ over $M_0$.  In particular
$D^\K(x_j,Z)$ is determined by $p_0$ and $\tp(Z/M_0)$.

A known product of the $p^B$ has this same joint diagram with $Z$:
products of free lifts are free lifts of products, and one may
restrict the resulting type to $M_0$ together with $Z$.  Since
$D^\K(x,Z)=D^\K(x_j,Z)$, the two candidate types over $B$ agree on
every test of the uniform comparison size.  Bounded testing makes
their full types equal.  This proves the converse.
\end{proof}

\subsection{Eliminating proper extensions with unchanged geometry}

The obstruction considered here is related to Vaughtian pairs: proper
extensions of the same cardinality with no new realizations of a fixed
nonalgebraic type; compare \cite{GrossbergVanDieren2006}, where the type
is based on a limit model.  Here finite marked systems and exact boundary
lifting eliminate the obstruction in the pointed setting.

The next use of the marked construction requires a type prescription
that can be chosen from a fixed set before choosing the common level.
We record the uniformity explicitly.

\begin{lemma}[Anchoring a singleton type]
\label{geom:anchored-type}
\label{geom:root-prescription}
There is a fixed cardinal $\beta$, depending on the single-model
template, its singleton comparison bound, and the fixed point, with
the following property.  If $A$ is a sufficiently closed pointed
model and $r$ is a nonalgebraic singleton type over $A$, a list
$c\subseteq A$ of length at most $\beta$ can be named so that:
\begin{enumerate}
\item the joint stabilized diagram of $c,\bar m_0$, together with a
      fixed majority prescription, defines a unique nonalgebraic
      singleton type $r^B$ over every sufficiently closed model $B$
      having that named diagram;
\item the prescription at $A$ is $r$, and the family $r^B$ lifts
      freely along arrows preserving the names, including across
      eligible levels;
\item the prescription occurs at arbitrarily large eligible
      single-model levels.
\end{enumerate}
The possible descriptors obtained this way form a set, with their
length bound independent of $\|A\|$.
\end{lemma}

\begin{proof}
Fix a sufficiently large uniform testing arity $\tau$ for singleton
types, including the bound needed to apply compact placement to those
tests.  The approximation construction for
Theorem~\ref{calc:free-extension} gives a list $c=(c_i:i<\beta')$ of
approximations in $A$ that computes $r$ by majority on all these
tests.  Its length and all ancillary approximation data can be bounded
by one cardinal $\beta$, independently of the level.  Choose the
length larger than the exception bound for the tests; increase
$\beta$ also to include the fixed point data.  The prescription is
the value attained by all but the permitted number of entries in
$D^\K(c_i,z)$, for each test $z$ of arity at most $\tau$.

Freely lift the actual $r$ to arbitrarily large eligible models
containing $A$.  Query matching over the fixed approximation list
shows that these lifts compute exactly the same majority
prescription.  They are nonalgebraic by
Lemma~\ref{geom:nonalgebraic}.  For another sufficiently closed
pointed $B$ with the same named diagram, embed $B$ into such a larger
instance, respecting the names.  This is possible by bounded-diagram
homogeneity and mixed placement.  Restrict the lifted type to that
copy of $B$.  It is nonalgebraic, since its realization is outside the
larger parameter model, and query matching makes its bounded answers
the prescribed ones.

Any two types having these answers are equal by the singleton
comparison bound.  Thus the construction is independent of the
larger instance and the chosen embedding.  A free lift along an arrow
preserving the names has the same prescribed answers: the
approximation evaluation is transported by matching each query over
the named list inside the old base.  Uniqueness therefore identifies
it with the prescribed receiving type.  At $A$ the answers are those
of $r$ by the choice of $c$.

The list lengths have a fixed set bound.  Their stabilized diagrams,
the fixed testing arity, and the majority rule range over a set of
descriptors.  Only descriptors realized at arbitrarily high eligible
single-model levels are needed; the preceding construction proves
that the descriptor extracted from an actual $r$ has this property.
The named diagram itself can be witnessed at one fixed eligible
level large enough for arity $\beta$, by saturation for diagrams from
larger levels.  Proposition~\ref{lev:named-package} therefore applies
with a lower threshold depending on $\beta$ and the original working
scheme, rather than on $\|A\|$.  In particular, extracting the names
from a model of size $\lambda$ does not require moving above
$\lambda$ in order to use the pointed working scheme at that level.
\end{proof}

\begin{theorem}[No proper pair with unchanged points at one level]
\label{geom:no-growth}
There is a sufficiently large cardinal $\lambda>\lambda_0$ such that
there is no proper strong inclusion $A<_\K B$ of pointed models of
size $\lambda$ with $P(A)=P(B)$.
\end{theorem}

\begin{proof}
Take the set of anchored descriptors from
Lemma~\ref{geom:anchored-type}.  Choose $\lambda$ at a common level
for all finite marked constructions for these descriptors, using
Theorem~\ref{close:common-levels}.  Require also all the relevant
single-model and pointed bounds, and $\lambda>\lambda_0+\beta$.
This is a choice uniform in the possible descriptor.  In particular
the choice does not depend on a pair that might later be assumed to
exist.

Suppose toward a contradiction that $A<_\K B$ is such a pair, and
choose $a\in B\setminus A$.  Apply
Lemma~\ref{geom:anchored-type} to $r=\tp(a/A)$ and name its list
$c$.  We work in the pointed scheme also naming this list, with its
fixed joint diagram.  Write $\mathcal C_n$ for its $n$-fold marked
iteration with the root prescription $r$, as in
Theorem~\ref{iter:finite-systems}.

Every one-step all-dominated increment of this scheme has no new
$P$-points.  Indeed, pointed categoricity carries its base, including
the named list $c$, onto $A$.  Transporting the witness $A<_\K B$
back gives an extension with a realization of the required $r$ and
unchanged $P$.  Primeness embeds the all-dominated increment into
that extension over its base and mark.  Since strong maps preserve
and reflect $P$ and fix the base, the increment has exactly the base
points.

It follows by induction that the $P$-points in the top of every
$\mathcal C_n$ object are precisely those in its root.  For the
induction step, its lower and upper layers are $\mathcal C_{n-1}$
objects and hence each has the points of its own root.  Projection
onto the new axis is a valid one-step marked increment by
Theorem~\ref{iter:finite-systems}.  The two roots therefore have the
same points, proving the assertion for the entire object.

We next construct coherent finite systems.  For each $n<\omega$
choose an object $J_n\in\mathcal C_n$.  For every
$s\subseteq\{1,\dots,n\}$ choose an isomorphism
\[
e_{n,s}:J_{|s|}\longrightarrow P_sJ_n
\]
such that these maps commute with all further face projections, using
the increasing identifications of finite index sets.  Here the full
face map is the identity.  To make these choices, induct first on
$n$ and then on the size of a proper subset $s$.  For a proper subset
$u$ of the axes of $J_{|s|}$, let $t$ be the corresponding subset of
$s$.  The boundary map for $e_{n,s}$ on this face is
$e_{n,t}e_{|s|,u}^{-1}$, with the indicated index identifications.
The already chosen maps make these boundary prescriptions compatible.
Theorem~\ref{iter:exact-boundary} extends them to the desired
isomorphism.  At dimension zero it is simply pointed categoricity.
This constructs every $e_{n,s}$ with the asserted commutation.

For the finite subsets $s$ of any ordinal $I$, take a tagged copy of
the top vertex of $J_{|s|}$.  If $s\subseteq t$, use the top component
of $e_{|t|,u}$ followed by the inclusion of that face into the top,
where $u$ records the positions of $s$ in the increasing list of $t$.
The preceding commutation gives a directed system of strong maps.
All its roots are copies of the same actual $J_0$, and no vertex has
more $P$-points than that root.

The marks corresponding to different indices of $I$ are distinct in
this directed system.  It suffices to inspect a two-axis object.  Its
new mark lies in the root of its upper one-axis layer, whereas the
old mark is the nonalgebraic mark of that layer and is outside its
root.  Face isomorphisms preserve the marks, so the distinction
persists under all transition maps.

Take $I$ of cardinality $\mu>\lambda$, where $\mu$ is a sufficiently
closed single-model pointed level.  The ordinary directed colimit in
the AEC exists: a coherent diagram of injective maps is realized as
a diagram of inclusions in its direct limit, and the directed-union
axioms apply.  There are $\mu$ finite subsets of $I$, each contributing
at most $\lambda$ elements, and there are $\mu$ distinct marks.  Thus
the colimit $N$ has size exactly $\mu$.  Every element of $N$ comes
from one finite vertex.  Preservation and reflection of $P$ give
\[
P(N)=P(J_0),\qquad |P(N)|\leq\lambda.
\]
The enumeration of its distinguished $M_0$ retains the fixed
stabilized diagram $\Delta$ under the strong colimit embeddings.

On the other hand, there is a pointed model of size $\mu$ with more
than $\lambda$ points.  Start with any pointed model of that size.
Successively realize a nonalgebraic free extension of $p_0$ outside
the current model, for $\lambda^+$ steps.  The receiving models and
their unions may all be kept of size $\mu$.  The new realizations
are distinct and belong to $P$, so the union has at least
$\lambda^+$ points.  Pointed categoricity at $\mu$ would make this
model isomorphic to $N$ over $M_0$, a contradiction.

Only the stationary prescription $r$ was lifted to higher levels.
The assumed witness with unchanged $P$ was used solely at
$\lambda$.  The large colimit used the full AEC directed-union
axioms, rather than a same-level closure assertion for a marked
scheme.
\end{proof}

\begin{corollary}[No-growth and rank on the entire tail]
\label{geom:tail-no-growth}
Increase the threshold $\lambda$ if necessary to include the bounds
for the fixed point diagram.  In arbitrary cardinalities, if
$A\leq_\K B$ are pointed models with $\|A\|\geq\lambda$ and
$P(A)=P(B)$, then $A=B$.
Moreover, for every pointed model $M$ with $\|M\|>\lambda$,
\[
|P(M)|=\rk(P(M))=\|M\|.
\]
The point sets of strong submodels are relatively closed, and
relative bases and finite basis supports are available as in
Theorem~\ref{geom:pregeometry}; no eligibility condition is imposed
on these arbitrary cardinalities.
\end{corollary}

\begin{proof}
Suppose that $a\in B\setminus A$ and $P(A)=P(B)$.  Construct
increasing strong submodels $A_i\leq_\K A$ and $B_i\leq_\K B$ of
size $\lambda$, for $i<\omega$, all containing the distinguished
copy of $M_0$, so that
\[
A_i\leq_\K B_i,\qquad a\in B_i,\qquad
P(B_i)\subseteq A_{i+1}.
\]
For the successor choice, $P(B_i)$ has size at most $\lambda$ and
is contained in $A$, so the L\"owenheim--Skolem axiom places it,
together with $A_i$, in the next $A_{i+1}$.  Choose $B_{i+1}$ to
contain $A_{i+1}\cup B_i\cup\{a\}$.  Coherence makes all the
required inclusions strong.  The two unions $A_\omega\leq_\K
B_\omega$ have size $\lambda$.  The point diagram restricts
correctly to them, and
\[
P(B_\omega)=\bigcup_{i<\omega}P(B_i)
             \subseteq A_\omega.
\]
Thus their point sets are equal, while $a\in B_\omega\setminus
A_\omega$.  This contradicts Theorem~\ref{geom:no-growth}.

Now let $\|M\|=\kappa>\lambda$.  If $|P(M)|<\kappa$, choose a
strong submodel containing $M_0\cup P(M)$ of size at most
$|P(M)|+\lambda_0$.  Enlarge it inside $M$, if necessary, to a
strong submodel of size at least $\lambda$ and still less than
$\kappa$.  It has the same $P$ as $M$, contrary to the assertion
just proved.  Hence $|P(M)|=\kappa$.  If $H$ is a basis of $P(M)$,
the closure bound gives
\[
\kappa=|P(M)|=|\cl_M(H)|\leq |H|+\lambda_0.
\]
Since $\kappa>\lambda\geq\lambda_0$, it follows that
$|H|=\kappa$.  The final assertions were established in
Theorem~\ref{geom:pregeometry} independently of eligibility.
\end{proof}
==== END Eventual-Categoricity-for-Abstract-Elementary-Classes//10-geometry.tex ====

==== BEGIN Eventual-Categoricity-for-Abstract-Elementary-Classes//11-geometric-systems.tex ====
\section{Geometric systems and classification by bases}
\label{sys:section-geometric-systems}

Throughout this section the distinguished model $M_0$, its fixed pointed
pattern, and the pregeometry $P$ are those of
Proposition~\ref{geom:pointed-levels} and
Theorem~\ref{geom:pregeometry}.
All model sizes exceed the threshold of
Corollary~\ref{geom:tail-no-growth}.  Thus a strong inclusion of pointed
models with equal $P$-sets is equality.  At an eligible uniform level
$\mu$, all vertices have size $\mu$.  A statement about unions of
objects at that level concerns chains whose total size is $\mu$, as in
the working conditions of Definition~\ref{lev:working-package}.

We first prove structural and presentation assertions without assuming
categoricity of systems.  The classification argument then proceeds by
the number of axes.  Its first assertion extends a root isomorphism and
prescribed bijections of the other basis pieces; this gives categoricity
for the current shape.  That categoricity supplies the working package
used to prove the second assertion: prescribed bijections of the basis
pieces added to a fixed system extend to an isomorphism over that system.
By splitting off the last axis, the second assertion gives the first at
the next dimension.  We establish the conditional package before carrying
out this paired induction.

\subsection{Shapes, relative bases, and arrows}

\begin{definition}[Admissible shapes and geometric systems]
\label{sys:shapes}
Let $A$ be a finite linearly ordered set of axes.  An admissible family
$L\subseteq\mathcal P(A)$ of \emph{active labels} is defined recursively.
On no axes the family is $\{\varnothing\}$.  If $k$ is a new last axis,
choose an upward closed subset $Q$ of the previously constructed family
$L$, and put
\[
 L'=L\cup\{s\cup\{k\}:s\in Q\}.
\]
Here upward closed means that $s\in Q$, $s\subseteq t$, and $t\in L$
imply $t\in Q$.

A geometric system of shape $L$ is a family
$(X_t:t\subseteq A)$ of pointed models in a common top model, with
$X_t\leq_\K X_u$ when $t\subseteq u$, satisfying the following condition.
There is a partition $(H_s:s\in L)$ of a basis of $P(X_A)$ such that
$H_s\subseteq P(X_s)$ and
\begin{equation}
\label{sys:vertex-span}
 P(X_t)=\cl_{P(X_A)}\left(\bigcup_{s\in L,\ s\subseteq t}H_s\right)
 \qquad(t\subseteq A).
\end{equation}
At uniform level $\mu$ we require $|H_s|=\mu$ for every $s\in L$.
The resulting scheme is denoted $\mathcal G_L$.
The basis partition witnesses the definition; it is not named in the
system structure.

For a vertex $t$, write
\[
 D_t(X)=\cl_{P(X_A)}\left(\bigcup_{r\subsetneq t}P(X_r)\right).
\]
For $t=\varnothing$ this is the closure of the empty set in the
pregeometry.  An arrow $X\to Y$ is a commuting family of pointed strong
embeddings for which a witnessing partition for $X$ extends to a
witnessing partition for $Y$.  Equivalently, after identifying $X$ with
its image, each finite tuple from $P(X_t)$ independent over $D_t(X)$
remains independent over $D_t(Y)$.
\end{definition}

The equivalence in the last sentence, including its independence from
the initially chosen partition, will be proved below.  All closures and
independence assertions are computed in a common containing pointed
model.  Theorem~\ref{geom:pregeometry} makes this convention
independent of the chosen common strong extension.
The notation $\cl_{P(X_A)}$ means the closure $\cl_{X_A}$ defined
there; its subscript emphasizes the pregeometry in which it is
computed.  We omit that subscript when the ambient model is clear.

\begin{lemma}[Combinatorics of shapes]
\label{sys:shape-combinatorics}
An admissible family contains $\varnothing$ and is closed under unions.
Its restriction to any subset of the axes is admissible, with the
inherited order.  Consequently every $t\subseteq A$ has a largest
active subset
\[
 a_L(t)=\bigcup\{s\in L:s\subseteq t\}.
\]
In a geometric system, $X_t=X_{a_L(t)}$ whenever $t$ is inactive.
\end{lemma}

\begin{proof}
The union assertion follows by induction on the axes.  Unions of old
labels are old.  If a union involves $s\cup\{k\}$ with $s\in Q$, its
old part is an active label containing $s$, and therefore belongs to
$Q$.  This also handles the union of two labels containing $k$.
Restriction to a set of axes replaces $L$ and $Q$, at every retained
step, by their restrictions.  The restricted $Q$ is upward closed in
the restricted $L$.  Steps on discarded axes make no contribution.
This proves the restriction assertion.

The displayed union is an active label, since the family is finite and
contains $\varnothing$.  The collections of active labels below $t$
and below $a_L(t)$ agree.  Equation~\eqref{sys:vertex-span} therefore
gives equality of their $P$-sets.  The inclusion
$X_{a_L(t)}\leq_\K X_t$ and
Corollary~\ref{geom:tail-no-growth} give equality of the models.
\end{proof}

\begin{remark}
Union closure alone would not imply the recursive last-axis
description.  For example, $\{\varnothing,\{1,2\}\}$ is union closed,
but its two layers on splitting off axis $2$ have different active
families.  We use the recursive definition, including the upward
closed set $Q$, when identifying a system with an arrow between
systems on fewer axes.
\end{remark}

\begin{lemma}[Replacement and extension of relative bases]
\label{sys:relative-bases}
Suppose $X$ is a geometric system.  For each active $s$, choose any
basis $B_s$ of $P(X_s)$ over $D_s(X)$.  Then the $B_s$ form a
witnessing partition for $X$.

A componentwise strong system embedding is an arrow precisely when
it preserves the relative independence in
Definition~\ref{sys:shapes}.  For an arrow, every witnessing partition
of its domain extends to one of its codomain.
\end{lemma}

\begin{proof}
Fix a witnessing partition $(H_s:s\in L)$, and enumerate $L$ in an
order extending inclusion.  For active $s$,
\[
 D_s(X)=\cl\left(\bigcup_{u\in L,\ u\subsetneq s}H_u\right).
\]
When the piece at $s$ is replaced, previously processed labels not
below $s$ are independent, together with the original piece at $s$,
over this lower span: they are parts of a single independent set.
Replacing $H_s$ by any basis of the same flat over its lower span
preserves both independence and the span of the union.  Explicitly,
let $C$ be the current pieces below $s$.  Then
$\cl(C\cup B_s)=\cl(C\cup H_s)=P(X_s)$, and $C\cup B_s$ is
independent.  The remaining current pieces were independent over
$\cl(C\cup H_s)$, since the full current partition was independent.
They remain independent over the equal flat $\cl(C\cup B_s)$.
Thus the new full partition is independent and has the same span.
Applying this replacement at the finitely many active labels gives the
first assertion and Equation~\eqref{sys:vertex-span} for the new
partition.

If pieces extend along an embedding, any finite independence
calculation in a vertex over its lower span is the same calculation
using the corresponding pieces in the larger independent set.
Relative independence is therefore preserved.

Conversely, let $(B_s)$ be an arbitrary witnessing partition of the
domain, viewed as a subsystem of $Y$.  Preservation implies that
$B_s$ is independent over $D_s(Y)$.  Extend it to a relative basis
$B_s\cup C_s$ of $P(Y_s)$ over $D_s(Y)$.  The first assertion, applied
to $Y$, says that these choices assemble into a witnessing partition
of $Y$.  This proves both the equivalence and the final assertion.
\end{proof}

\begin{lemma}[Structural properties and the last-axis description]
\label{sys:structural}
Arrows compose and satisfy coherence.  Same-level chains of total
size the level have unions in $\mathcal G_L$, with the common-upper-
bound clause also for arrows into a larger eligible level.

Restriction to any subset of axes preserves systems and arrows.
If $L'=L\cup\{s\cup\{k\}:s\in Q\}$, splitting off the last axis
identifies a system of shape $L'$ with an arrow $X\to Y$ in
$\mathcal G_L$ such that the complementary piece at $s$ has size
$\mu$ for $s\in Q$ and is empty for $s\notin Q$.
\end{lemma}

\begin{proof}
Composition follows from the relative independence criterion.
For coherence, suppose $X\subseteq Y$, and both embed by arrows in
$Z$.  Independence over $D_t(X)$ implies independence over $D_t(Z)$,
and hence over its subset $D_t(Y)$.  Componentwise coherence is the
AEC coherence axiom.

For a continuous chain, extend witnessing pieces successively using
Lemma~\ref{sys:relative-bases}, and take their unions at limit stages.
Every finite independent sublist and every finite dependence witness
occurs at a stage.  The resulting union pieces are independent and
span every vertex of the componentwise union.  Each contains $\mu$
elements from the first stage and has size at most $\mu$, so all
pieces still have size $\mu$.  For a chain which is not initially
continuous, insert its earlier unions: the preceding construction
applies recursively, and the common-upper-bound argument in the next
paragraph supplies its connecting arrows.

If each stage maps by an arrow into $Z$, a finite tuple independent
over the lower span of the union is independent over the lower span
at any stage containing it.  Its image is independent over $D_t(Z)$.
The componentwise AEC common-upper-bound axiom supplies the strong
maps, so the union map is an arrow.  This argument also permits a
larger level for $Z$.

On restricting to axes $B\subseteq A$, retain the pieces whose labels
are contained in $B$.  They are a basis of $P(X_B)$ and satisfy the
required span identities.  For a retained vertex all its proper
subsets are still retained; its relative independence test is
therefore exactly the old test.

Finally let $Z$ have shape $L'$, and put $X_s=Z_s$ and
$Y_s=Z_{s\cup\{k\}}$.  A partition for $Y$ is obtained by combining
$H_s$ with $H_{s\cup\{k\}}$ when $s\in Q$, and using $H_s$ alone
otherwise.  These choices extend the pieces of $X$, and their
complements have the asserted sizes.  Conversely, extend pieces of
$X$ to pieces of $Y$ along such an arrow, give the old pieces labels
$s$ and their complements labels $s\cup\{k\}$, and use $X$ and $Y$
as the two layers.  The span identities give a system of shape $L'$.
Inactive vertices cause no exception, by
Lemma~\ref{sys:shape-combinatorics}.
\end{proof}

For later use, preservation of relative independence also preserves
finite rank calculations modulo the lower span.  For finite tuples
$a,c$ in a vertex, the condition that $a$ be independent over
$D_t(X)\cup c$ is determined by the ranks, modulo $D_t(X)$, of
sublists of $a,c$.  These ranks are determined by which sublists are
independent.  Thus arrows preserve this condition as well.

\subsection{Order presentations and their rank}

\begin{proposition}[Tiled presentations]
\label{sys:tiling}
Let $L$ be admissible and let $\mu$ be sufficiently large for the
pointed pregeometry and the no-proper-pair conclusion.  The order
template $E$ gives a presentation in $\mathcal G_L$ as follows.
Choose a fixed initial order carrying the whole enumeration of $M_0$.
For each active label $t$, choose a tile $T_t$, preceded by a buffer
$B_t$, and concatenate these finitely many pairs after the initial
order, in any fixed order.  Every tile and buffer is a dense linear
order without endpoints of size $\mu$.  In vertex $s$ retain the
initial order, all buffers, and just the tiles with labels $t\subseteq
s$.

These presentations have the following properties.
\begin{enumerate}
\item Each active relative piece has rank $\mu$.
\item Order embeddings of the corresponding tiles and buffers,
fixing the initial pointed data, induce arrows, including between
different eligible levels.
\item A presentation has an extension by an arrow gaining $\mu$
independent complementary coordinates at every active label
simultaneously.
\item Tiles may be chosen with $\mu$ pairwise disjoint convex
substrips, each of size $\mu$.  Further insertions of such substrips
preserve the preceding assertions and the naturalness of the
underlying $\K$-diagrams.
\end{enumerate}
No categoricity assumption about $\mathcal G_L$ is used here.
\end{proposition}

\begin{proof}
Let $I_s$ be the indicated suborder and set $X_s=E(I_s)$, using the
literal embeddings supplied by Theorem~\ref{found:order-template}.
All $I_s$ have size $\mu$, since they contain all buffers.  The
models have size $\mu$ and are strongly included according to their
labels.  The initial order was chosen to contain the supports of the
fixed enumeration of $M_0$.  Its unchanged term pattern carries the
same pointed model in every vertex, and coherence gives the required
strong inclusion of $M_0$.

Choose a relative basis $H_s$ of $P(X_s)$ over the union of its
proper lower $P$-sets for every active $s$.  We first prove that the
indexed family of these choices is independent; this also proves
that the pieces are disjoint.  Suppose there is a finite circuit
of labeled entries, allowing a two-entry equality dependence when
two differently labeled entries coincide.  Choose a maximal label $s$ represented among its
entries.  Retain the finite term supports of all entries with label
$s$, and indeed retain every support position in a tile available
at $s$.  In each unavailable tile replace all support positions by
distinct positions in its preceding buffer, beyond all the finitely
many retained positions in that buffer.  Such positions exist because
the buffer has no greatest point and is dense.  No retained position
lies in that unavailable tile.  Consequently this replacement
preserves the order and equality pattern of all circuit supports and
fixes the whole initial pointed order.

The labels and this order pattern preserve the pointed finite
geometry comparisons.  One can formulate this either using the
natural $\K$-diagrams or by taking the term model on the fixed initial
order and the finite supports and applying its two pointed strong
embeddings into the original presentation.  In the latter formulation
Theorem~\ref{geom:pregeometry} preserves and reflects the
independence relation.

An entry with label $t\ne s$ in the circuit has no label properly
containing $s$, by maximality.  Thus $s\nsubseteq t$.  After the
replacement its term uses only common buffers, initial data, and
tiles with labels contained in $s\cap t$.  Its image belongs to
$P(X_{s\cap t})\subseteq D_s(X)$.  The entries with label $s$ have
not moved.  The preserved circuit makes a sublist of $H_s$ dependent
over $D_s(X)$, a contradiction.  The union is therefore independent.
It spans every vertex by induction on the labels: its relative basis
spans that vertex over lower vertices, which have already been
spanned.  If a vertex is inactive, the order retained there is exactly
the order retained at its largest active subset.  This proves the
decomposition without first assuming the system axioms.

We give the fresh-skeleton observation needed for the rank assertion.
If $J\subseteq I$ and $i\in I\setminus J$, the skeleton entry at $i$
does not belong to $E(J)$.  Otherwise it equals a labeled term on a
finite tuple of positions from $J$.  Enlarge the order by a second
position $i'$ having the same order pattern as $i$ relative to that
finite tuple.  Literal pattern preservation would make both
distinguished skeleton entries equal to that term.  This contradicts
their required distinctness.  The enlargement need only duplicate
the cut relative to the finite tuple, not the cut relative to all of
$J$.

For an active $t$, omit $T_t$ from $I_t$.  The resulting order still
has size $\mu$, contains the pointed data and all proper lower
vertices, and presents a strong submodel.  Enumerate $\mu$ points of
$T_t$ and adjoin them one at a time.  The fresh-skeleton observation
makes each successor inclusion proper.  All these models have size
$\mu$, because the buffers were retained.  By
Corollary~\ref{geom:tail-no-growth}, each successor adds a point of
$P$.  Choose one such point at each successor.  Relative closedness
of $P$ in strong submodels makes these choices independent over the
initial omitted-tile model.  There are $\mu$ choices, so the rank over
the proper lower vertices is at least $\mu$.  It is at most $\mu$
by the size of $X_t$.  This proves the first assertion, including the
root case $t=\varnothing$.

Next consider componentwise order embeddings into enlarged tiles and
buffers, identifying the source with its image.  Suppose a finite
tuple $a$ in $P(X_s)$, independent over $D_s(X)$, becomes dependent
over $D_s(Y)$.  Dependence has a finite witness consisting of points
from proper lower vertices of $Y$.  Fix the finitely many old
positions supporting $a$.  Move every other position needed for the
witness into its corresponding old tile or buffer, preserving its
order relative to the fixed positions.  Density and absence of
endpoints of the old order suffice for each finite pattern; it is
not necessary that the old order be dense in the enlarged order.
The initial pointed order remains fixed.  Each witness remains in
its designated proper lower vertex, now in $X$, and its finite
dependence diagram is preserved.  This contradicts independence of
$a$ over $D_s(X)$.  Lemma~\ref{sys:relative-bases} therefore gives an
arrow.  The proof did not require equal source and target sizes.

To obtain simultaneous gains, enlarge all tiles with $\mu$ fresh
points and, if desired, enlarge the buffers.  For a particular active
$t$, begin the strict-growth argument over the order containing the
old $t$-tile, all enlarged proper-lower tiles, all enlarged buffers,
and the initial data.  This base contains $X_t$ and all proper lower
vertices of $Y$.  Adjoining the fresh points of the $t$-tile yields
$\mu$ independent points over that larger base.  Hence the
complementary rank at $t$ is $\mu$.  The preceding arrow assertion
allows any old pieces to extend, and
Lemma~\ref{sys:relative-bases} combines the relative choices into
one partition.  This proves the simultaneous assertion.

Finally a lexicographic sum, indexed by a linear order of size
$\mu$, of dense endpoint-free orders of size $\mu$ is still dense
and endpoint-free and has size $\mu$.  Its summands are the desired
convex substrips.  In particular, for a presentation indexed by a
well-order $H$, one can use $H\times\Q$ and reserve intervals of
$H$ of order type and cardinality $\mu$.  Taking $H$ of order type
$\mu\cdot\mu$ supplies $\mu$ disjoint such intervals.  Additional
summands or strips do not change any of the preceding arguments.
Underlying $\K$-diagrams remain natural because the entire system
was obtained by designated term subcollections of the single
template $E$.
\end{proof}

\subsection{Obtaining the working package from categoricity}

\begin{proposition}[Conditional working package]
\label{sys:working-package}
Fix an admissible shape $L$.  Suppose that $\mathcal G_L$ is
categorical at every level in an unbounded class of eligible levels
closed sufficiently for the preceding constructions.  Assume also
the eligible-subclass hypothesis of Convention~\ref{lev:eligible-subclass}.
On an unbounded further class of sufficiently closed levels, it satisfies the full working
package of Definition~\ref{lev:working-package}, with its actual
system isomorphisms and its arrows from Definition~\ref{sys:shapes}.
The resulting diagrams, saturation, and calculus include mixed
arrows between eligible levels, and the output class retains the
eligible-subclass hypothesis.

The closure requirements are uniform in the finite shape and the
fixed pointed template.  They use only the smaller and larger input
levels specified by the general working-package construction.
\end{proposition}

\begin{proof}
The structural conditions are Lemma~\ref{sys:structural}.
Proposition~\ref{sys:tiling} supplies term presentations and mixed
presentation arrows before categoricity.  By the assumed
categoricity, every object at an input level is isomorphic to its
presentation.

We check the extra relative-basis condition throughout the reversal
argument.  In each tile and buffer use the order $H(\delta)$ from
Theorem~\ref{found:order-orbits}.  For a tuple of length $\theta$, record
its term labels, the fixed initial positions it uses, and, separately
in each of the finitely many variable orders, the order and
realized-cut record of its support positions.  If
$\theta<\cf(\delta)$, equal records are carried to one another by
order automorphisms of the respective tiles and buffers.  Their
product fixes the initial data and induces an automorphism of the
whole system.  The set of possible records has a bound depending
only on $\theta$, the finite shape, and the template.  Hence the
system orbits at that arity have a uniform set bound.

Number these orbits and record the arrows between them, together
with the partial map from support records to orbit names.  This is
again a bounded palette.  If reversal fails unboundedly often,
choose repeated profiles at eligible levels $a<\mu$ exactly as in
Theorem~\ref{found:reversal}, with $a^\theta\leq\mu$ and the required
large cofinalities for the orders.  Apply the ordinal-position
shrinking of Proposition~\ref{found:alignment} simultaneously to the
finitely many tiles and buffers.  Given at most $a$ parameters in
the large system, the resulting small presentation contains them,
has size $a$ in every tile and buffer, and computes the support
records of all its $\theta$-tuples correctly.  Its inclusion is an
actual arrow by Proposition~\ref{sys:tiling}.  Thus it is an aligned
small geometric system, not merely a componentwise subsystem.

For completeness, the contradiction uses two orbit names $p,r$ with
$p\to r$ and $r\not\to p$.  Repeatedly choose aligned small copies,
each containing the previous one, and process their at most
$a^\theta$ tuples in the large level.  Whenever a tuple can still be
sent to $p$, send it onward to $r$.  From that point it cannot reach
$p$.  Coherence makes the successive small copies a chain of
arrows.  After $\theta^+$ rounds every $\theta$-tuple of their union
occurred at a proper round.  Both unions exist by
Lemma~\ref{sys:structural}: the small union has total size $a$, and
the large construction has total size $\mu$.  Alignment says that
none of the tuples of the small union can reach $p$.  Categoricity
of that union at $a$ says that its orbit $p$ is realized, a
contradiction.  This proves eventual reversal at each fixed arity.

Mixed L\"owenheim--Skolem closure also has the required form.
In a presentation, close the supports of a prescribed small set
under finitely many intermediate and exterior positions in every
tile and buffer, repeat countably many times, and pad each order
to the chosen smaller eligible size.  The resulting dense
endpoint-free suborders give a small presentation containing the
set.  The initial pointed order is retained in full.  Its inclusion
is an arrow by Proposition~\ref{sys:tiling}.  Transport through a
presentation of an arbitrary large object gives mixed containment;
coherence supplies comparisons between such subobjects.

We now apply the first route of
Proposition~\ref{lev:scheme-diagram-routes}.  Its structural
hypothesis is Lemma~\ref{sys:structural}; its presentation and mixed
downward-closure hypotheses are Proposition~\ref{sys:tiling} and
the preceding paragraph.  Categoricity is the input assumption,
and the required arity-by-arity reversal and uniform orbit bounds
were proved above.  Thus the proposition applies to the actual
system arrows, including their relative-basis condition.

In particular, the canonical comparison at a smaller input level
is computed in a small geometric subobject.  Two such sections
are contained in a common small section by mixed downward closure,
and coherence gives its arrows, so the comparison is well defined.
The projections between comparisons at two input levels are onto
because the smaller system is a tiled presentation and extends by
the mixed order arrows of Proposition~\ref{sys:tiling}.  The bounded
palette therefore stabilizes, exactly as in the first route of
Proposition~\ref{lev:scheme-diagram-routes}.

Choose receiving levels which remain eligible, are strictly closed
under the resulting arity bounds, and have sufficiently large
smaller input levels below them for every bounded request.
These are the closure refinements described in
Section~\ref{lev:refining-levels}, supplied simultaneously in
Theorem~\ref{close:common-levels}; closure under the next input
level is not being used to infer eligibility by itself.  At such a
level, countable alternating matching in smaller input-level
sections gives actual system isomorphisms on equal bounded
diagrams, and realizes possible bounded joint diagrams over their
given subtuples.  Thus diagrams, homogeneity, and saturation have
the system interpretation required here, rather than merely their
componentwise $\K$ interpretation.  Order embeddings and order
amalgamation make the diagrams natural on term tuples, so
Proposition~\ref{lev:diagram-coding} also applies.

It remains to check the additional exhaustion condition, which
Proposition~\ref{lev:scheme-diagram-routes} explicitly leaves as a
separate obligation.  A finite tuple independent modulo the
proper lower vertices stays so when its target diagram agrees with
a tuple placed along an actual presentation arrow: the comparison
is realized by a system isomorphism, and such an isomorphism
preserves relative independence.  Every tuple in an exhaustive
sequence is handled at a stage containing it.  The finite
relative-independence criterion in Lemma~\ref{sys:relative-bases}
then supplies the additional arrow condition.  Componentwise
strongness is the conclusion of the same proposition's exhaustion
argument.  This completes the working-package verification.

All refinements used here are the bounds for the original reversal,
alignment, diagram stabilization, and saturation arguments, applied
to finitely many orders and the fixed initial data.  None introduces
an amalgamation assumption on the original AEC; the amalgamation
used below is the conclusion of the working package and
Theorem~\ref{calc:scheme-amalgamation}.
\end{proof}

\subsection{Fresh coordinates and the two induction assertions}

Fix pieces $(H_s^X:s\in L)$ in a system $X$.
For an arrow $X\to Y$, extend them to pieces
\[
 H_s^Y=H_s^X\mathbin{\dot\cup}C_s^Y.
\]
The sets $C_s^Y$ are its \emph{complementary pieces}.  Their sizes
may be any cardinals at most $\mu$, including zero, even though all
the total pieces have size $\mu$.

\begin{definition}[Joint freshness]
\label{sys:fresh}
A list of coordinates in an extension $Y$ of $X$, with individual
active labels, is jointly fresh over $X$ if it is a sublist of the
complementary pieces for some such extension of the pieces of $X$.
At a single label $s$, the corresponding condition is independence
over
\[
 \cl\bigl(P(X_s)\cup D_s(Y)\bigr).
\]
For several labels these relative conditions assemble into joint
freshness by Lemma~\ref{sys:relative-bases}.  Coordinates are
regarded as occurrences in their designated vertex sorts.
\end{definition}

Freshness is preserved by arrows of extensions.  Indeed every
failure or success of finite independence over the displayed flat
is determined by finite rank calculations using parameters from
$P(X_s)$ and the lower span.  The observation following
Lemma~\ref{sys:structural} preserves those calculations.  This also
shows that freshness is an invariant of the type over $X$ once the
working package is available.

\begin{theorem}[Classification with prescribed basis maps]
\label{sys:basis-classification}
For each finite admissible shape $L$, at all sufficiently closed
uniform levels $\mu$, the following assertions hold.
\begin{enumerate}
\item If $X,Y\in\mathcal G_L$, an isomorphism
$e_\varnothing:X_\varnothing\simeq Y_\varnothing$ and arbitrary
bijections between the chosen nonroot pieces of $X$ and $Y$ extend
to a system isomorphism $X\simeq Y$.
In particular $\mathcal G_L$ is categorical at these levels.
\item Suppose $X\to Y$ and $X\to Z$ are arrows in
$\mathcal G_L$.  Choose pieces of $X$, extend them to pieces of
$Y$ and $Z$, and prescribe a bijection
$C_s^Y\simeq C_s^Z$ for every active label $s$.
Then there is a system isomorphism $Y\simeq_X Z$ realizing every
prescribed bijection.  The complementary cardinalities may be
less than $\mu$, and zero is allowed.
\end{enumerate}
The level requirements are uniform over the finitely many shapes
at any fixed number of axes.
\end{theorem}

\begin{proof}
We prove the two assertions in order, by the number of axes.
On no axes, the first assertion is exactly the assertion that a
prescribed isomorphism of the root models is an isomorphism of the
systems.  Existence of such a root isomorphism, hence categoricity
of the zero-axis scheme, is
Proposition~\ref{geom:pointed-levels}.

Suppose the second assertion is known for all shapes on fewer
axes.  For a shape with last-axis description $L'$, apply the first
assertion for $L$ to its lower layers and then the second assertion
for $L$ to its upper layers.  The pieces added at labels in $Q$
are exactly the pieces bearing labels $s\cup\{k\}$ in $L'$.
Prescribe their given bijections, and prescribe the empty maps at
the other labels.  This produces the desired isomorphism of the
two-layer systems by Lemma~\ref{sys:structural}.
If an auxiliary root basis has been chosen, replace the target
root basis by its image under the prescribed root isomorphism;
Lemma~\ref{sys:relative-bases} permits that replacement without
changing any prescribed nonroot piece.  Thus the first assertion
at the next number of axes follows from the preceding second
assertion.

It remains to prove the second assertion for a fixed shape $L$
whose first assertion has now been established.  Refine the
levels using Proposition~\ref{sys:working-package}.  All the
one-dimensional calculus and dominated-hull results are then
available for $\mathcal G_L$.  The rest of the proof is given in
four claims.

\begin{claim}[Uniqueness of finite fresh types]
\label{sys:finite-fresh-types}
For a fixed base $X$ and a finite ordered list of active labels,
all jointly fresh tuples with those labels have the same type
over $X$.
\end{claim}

\begin{proof}
At zero axes this is the base-change calculation of
Proposition~\ref{geom:base-change}.  Types in the pointed scheme
over a whole pointed base are the underlying $\K$-types: an
amalgam or type identification over that base already fixes the
point.  All objects at the level have full $P$-rank by
Corollary~\ref{geom:tail-no-growth}.

At a positive number of axes suppose two finite jointly fresh
tuples $b^0,b^1$ have different types over $X$.  Bounded testing
gives a bounded tuple $f$ from $X$ such that
\[
 D(f,b^0)\ne D(f,b^1).
\]
Choose a cardinal $\chi<\mu$ large enough for the orbit bound at
arity $|f|$, for the finite tuple lengths, and for the template
labels, with $\chi^{|f|+\aleph_0}=\chi$.  Let $\epsilon$ be the
least cardinal for which $2^\epsilon>\chi$.  Then
$\epsilon\leq\chi$, there are at most $\chi$ nodes at all proper
levels of the binary tree of height $\epsilon$, and
$2^\epsilon\leq2^\chi<\mu$.

Build a tree of extensions of $X$ at level $\mu$.  At a node $V$,
the arrow from $X$ preserves the diagram of $f$.  Bounded-tuple
homogeneity therefore supplies an isomorphism $X\simeq V$
fixing $f$.  Transport the two witness extensions along this
isomorphism to form the children of $V$.  Their marked tuples
are fresh over $V$, and their diagrams with $f$ have the two
specified different values.  At limit nodes take unions along
the branch.  Extend chosen basis pieces at every step.  Hence
along every branch all marked coordinates, at their respective
labels, lie in complementary pieces over the initial $X$.
The total size along a branch is $\mu$, so all unions are
allowed.  Notice that the return isomorphism fixing $f$ uses
diagram homogeneity, not categoricity alone.

At every leaf make a further rich extension by
Proposition~\ref{sys:tiling}, so that the root has complementary
rank $\mu$ over the original $X_\varnothing$.  There is a common
system $U$ with the same property: present any system and make a
rich extension, transporting it over $X$ using categoricity.
For each level $\eta<\epsilon$ reserve in $U$ a finite tuple
$c_\eta$ of coordinates with the same labels as the marked
tuple at that level.  Choose all of these coordinates from
complementary pieces over $X$.  Their total number is at most
$\chi$.

For a leaf $W$, its root marked coordinates and those in $U$
are independent over $P(X_\varnothing)$.  Both full root
complements have size $\mu$, and the prescribed match uses
fewer than $\mu$ coordinates.  Extend that match to a bijection
of root complements.  The already proved second assertion for
zero axes gives
\[
 W_\varnothing\simeq_{X_\varnothing}U_\varnothing
\]
carrying all root marked coordinates correctly.  At nonroot
labels extend the prescribed matches of marked coordinates to
bijections of the full pieces, whose sizes are $\mu$.  The
first assertion for the present shape extends these maps and
the root isomorphism to an isomorphism $W\simeq U$.
The old nonroot pieces of $X$ need not be fixed in this step.

Let $f_W$ be the image of $f$ in $U$.  Two different branches
first separate at a level $\eta$; preservation of diagrams
along their arrows gives different values of
$D(f_W,c_\eta)$ after the two leaf isomorphisms.  Thus the
$2^\epsilon$ images of $f$ lie in different orbits over the
fixed set of at most $\chi$ reserved coordinates.  The
parameter-orbit bound of Lemma~\ref{calc:parameter-orbits},
applied to the working scheme, is $\chi$ at
these arities, a contradiction.
\end{proof}

For each active $s$, let $p_s^X$ denote the unique fresh singleton
type given by the claim.  Such types exist by the rich extensions
of Proposition~\ref{sys:tiling} and categoricity.  Their realizations
lie outside the base vertex, so they are nonalgebraic.

\begin{claim}[Free lifts preserve freshness]
\label{sys:free-fresh}
The free lift of $p_s^X$ along an arrow $X\to V$ is fresh over $V$.
Finite jointly fresh tuples have the product of their singleton
types.  Bounded jointly fresh lists have a unique whole type
specified by their labels and admit all-dominated hulls.
\end{claim}

\begin{proof}
Let $a$ realize the free lift in an extension $Y$ of $V$.
If $a$ is not fresh, finite character gives a finite tuple
$c\subseteq P(V_s)$ with
\[
 a\in\cl\bigl(c\cup D_s(Y)\bigr).
\]
This condition is invariant under system isomorphisms and is
therefore determined by the bounded diagram of $(a,c)$ in $Y$.
Its witnesses in lower vertices need not lie in $V$; the
isomorphism-invariant condition itself is what the diagram
records.

Put $m=|c|+1$, and choose an $m$-tuple $b$ jointly fresh over
$X$, all at label $s$.  Every singleton marginal is $p_s^X$ by
Claim~\ref{sys:finite-fresh-types}.  Take a sufficiently long
bounded family of approximations, inside $X$, for
$\tp(b/X)$, as in Lemma~\ref{calc:approximations}.
By the support-copy construction in that Lemma, every
approximating tuple has the same diagram as
$b$ without parameters, and is consequently independent
modulo $D_s(X)$.  In the free lift to $V$, each coordinate has
the same marginal as $a$.  For each coordinate, the majority
estimate gives the diagram of $(a,c)$ outside a uniformly
bounded set of approximation indices.  Choose the family
longer than the union of these finitely many exceptional sets.
One approximating tuple $(a_1,\ldots,a_m)$ is independent
modulo $D_s(X)$ and has, coordinate by coordinate, the required
diagram with $c$ in $V$.

Since $X\to V$ is an arrow, this tuple remains independent
modulo $D_s(V)$.  The comparison just obtained is an equality of
$\mathcal G_L$-diagrams,
\[
 D_{\mathcal G_L}(a,c;Y)=D_{\mathcal G_L}(a_i,c;V).
\]
The established working package therefore gives a system isomorphism
$F_i:Y\cong V$ taking $a$ to $a_i$ and fixing the displayed tuple $c$.
It carries every lower vertex onto its counterpart and preserves the
pointed closure, so $F_i[D_s(Y)]=D_s(V)$.  Transporting the dependence
witness gives $a_i\in\cl(c\cup D_s(V))$ for every $i$.  The latter
flat has relative rank at most $|c|$, whereas the tuple has
relative rank $m>|c|$.  This contradiction proves that the
free lift is fresh.

Realize a finite product successively by free lifts along a
chain of extensions.  The assertion just proved puts each
new coordinate in a complementary piece over the preceding
system.  Extending pieces along the chain makes the whole
tuple jointly fresh over $X$.  Claim~\ref{sys:finite-fresh-types}
then says that every jointly fresh finite tuple has this
product type.  A bounded jointly fresh list is consequently
product-independent in the sense of
Theorem~\ref{iso:independent-lists}.  That theorem gives
its unique whole type and its witnessing free chains; its
all-dominated-hull conclusion gives existence over the list.
\end{proof}

We now know the types of fresh coordinate lists and have all-dominated
hulls over them.  To extend a partially prescribed basis map, we also
need to cover an arbitrary bounded tuple using only boundedly many
new coordinates.  The next claim provides this size control, including
when the target basis has already been chosen.

\begin{claim}[Bounded rank cost and chosen coordinates]
\label{sys:rank-cost}
Let $X\to Y$ be an arrow.  A finite tuple $d$ of $Y$ is
contained in a subextension $X\to U\to Y$ whose complementary
pieces have finite sizes.  For an arbitrary bounded tuple
$d$, their sizes can be bounded by
$\max(|d|,\aleph_0)$.

If specified pieces of $Y$ extend those of $X$, the subextension
containing a bounded $d$ can be chosen with all its
complementary pieces subsets of the specified complementary
pieces of $Y$, still of bounded total size.
\end{claim}

\begin{proof}
For finite $d$, take an all-dominated object over $X+d$ and
embed it into $Y$ by Proposition~\ref{iso:prime}.  Call its
image $U$.  Suppose one complementary piece of $U$ is
infinite.  Choose a sequence $(a_i:i<\omega)$ from that piece.
It is jointly fresh and hence product-independent over $X$.
The witnessing-chain assertion of
Theorem~\ref{iso:independent-lists} retains this
configuration in a chain
\[
 X=V_0\longrightarrow V_1\longrightarrow\cdots
 \longrightarrow V_\omega,
\]
where $a_i$ is free over $V_i$ from $X$ and belongs to
$V_{i+1}$.  We may construct this chain inside the actual $U$.  At each stage,
finite domination makes the actual next coordinate $a_i$ free over
$V_i$ from $X$, since its products with the preceding coordinates
remain those of the original list.  Choose an all-dominated increment
over $V_i+a_i$ and use primeness to embed it into $U$, fixing this
base and this coordinate.  At limits take unions inside $U$, using
the common-upper-bound clause.  Thus $V_\omega\leq U$, and the tuple
$d$ and every $a_i$ retain their actual positions in $U$.  Equivalently,
the witnessing-chain amalgamation may retain all of these data in a
common extension.

The tuple $d$ is finite, so Proposition~\ref{calc:local-character}
at the limit of
cofinality $\omega$ makes the actual type $\tp(d/V_\omega;U)$ free from
some $V_n$.  Hence $d$ and $a_n$ have product over $V_n$.
The base-change rule of Proposition~\ref{calc:products},
together with the freeness
of $a_n$ over $V_n$ from $X$, gives that $a_n$ and $d$ have
product over $X$.  Domination of $U$ over $X+d$ now makes
$\tp(a_n/U)$ free from $X$.  This is impossible by
Claim~\ref{sys:free-fresh}: the free lift of its fresh
singleton marginal must be fresh over $U$, whereas
$a_n\in P(U_s)$.  Therefore every complementary piece of
$U$ is finite.

For a bounded list of cardinality $\tau$, include its entries
successively by this finite construction, with the preceding
subextension as base, and take unions at limit stages.
There are finitely many labels.  At most $\tau$ finite
increments therefore add at most
$\kappa=\max(\tau,\aleph_0)<\mu$ coordinates in total.
All objects continue to have size $\mu$, and their unions have
total size $\mu$.  This proves the bounded version.

For the final assertion fix the target partition
$H_s^X\mathbin{\dot\cup}C_s^Y$.  Starting with a bounded-rank
subextension containing $d$, repeat the following construction
countably many times.  Choose relative bases for the current
subextension over $X$.  Each gained basis element in vertex
$t$ has a finite support in the fixed target basis, consisting
of old coordinates and coordinates of $C_s^Y$ with
$s\subseteq t$.  Request all the latter supporting
coordinates in their own vertices, and include them in the
next subextension using the bounded construction just proved.
At every step at most $\kappa$ coordinates are requested and
the total new rank remains at most $\kappa$.

In the union let $C_s$ consist of the requested coordinates
of label $s$.  These sets are independent, together with the
pieces of $X$, because they are subsets of the target
partition.  They span every union vertex over its old pieces:
an element occurs at a stage, is spanned there by the gained
pieces and the old pieces, and the finite target supports of
those gained pieces were requested at the next stage.
Conversely the closed $P$-set of each union vertex contains
all the indicated coordinates below its label.  Thus the
span identities hold in both directions.  The $C_s$ are
precisely complementary pieces of the union, have total
size at most $\kappa$, and are subsets of the prescribed
$C_s^Y$.
\end{proof}

\begin{claim}[Primeness over bounded complementary pieces]
\label{sys:bounded-prime}
If $X\to U$ has a bounded list $b$ enumerating all its
complementary pieces, then $U$ is all-dominated over $X+b$.
It embeds over $X$ into any extension realizing a prescribed
matching of these coordinates.
\end{claim}

\begin{proof}
The list $b$ is product-independent by
Claim~\ref{sys:free-fresh}.  Take an all-dominated object over
$X+b$ and embed it into $U$ over these data.  Its image $V$
contains in each vertex the old $P$-set and all the
complementary coordinates with labels below that vertex.
Relative closedness and the span identity imply
$P(V_t)=P(U_t)$ for every $t$.  The no-proper-pair conclusion
then gives $V_t=U_t$ for every vertex.  Thus $V=U$, proving
the domination assertion.

A prescribed matching of $b$ into another extension gives
the same whole type over $X$, by
Claim~\ref{sys:free-fresh}.  Primeness of the all-dominated
object therefore gives the desired arrow fixing $X$ and
realizing that matching.
\end{proof}

We finish the second assertion of the theorem.  Identify the two
bases with $X$, and keep the prescribed bijections of all
complementary pieces.  Choose countable exhaustions of the two
targets by bounded lists; these exist because the eligible level
$\mu$ has cofinality $\omega$ and there are only finitely many
vertex sorts.  Construct alternating isomorphisms between
subextensions of the two targets.  Initially use $\id_X$.
Maintain the invariant that the complementary pieces in each
current subextension are subsets of the specified target pieces,
and that the current isomorphism agrees with their prescribed
bijections.

At a forth step, apply Claim~\ref{sys:rank-cost} over the current
subextension on the first side to include the next bounded list
and to use only remaining specified coordinates.  Its new
complementary list is bounded.  The corresponding coordinates
on the second side are jointly fresh over its current
subextension.  Claim~\ref{sys:bounded-prime}, transported by the
current isomorphism, embeds the enlarged subextension into the
second target over that isomorphism and realizes their
prescribed matching.  Its image is the next subextension there.
The span identities show that its complementary pieces are
exactly the specified images of the new pieces, so the invariant
is preserved.  A back step applies the same construction with
the roles interchanged.

The union of these countably many coherent isomorphisms covers
both targets, since every list in both exhaustions is eventually
included.  It is therefore a system isomorphism over $X$.
It realizes all prescribed basis bijections: every basis element
is eventually in the domain, and the invariant determines its
image.  This proves the second assertion, with no lower bound
on complementary cardinalities.

The induction is complete.  At each fixed finite number of axes
there are only finitely many active-label families.  Taking the
maximum of their finitely many bounds gives the stated
uniformity.  Simultaneous closure through all finite numbers of
axes is addressed separately in
Theorem~\ref{close:common-levels}.
\end{proof}
==== END Eventual-Categoricity-for-Abstract-Elementary-Classes//11-geometric-systems.tex ====

==== BEGIN Eventual-Categoricity-for-Abstract-Elementary-Classes//12-geometric-boundaries.tex ====
\section{Exact isomorphisms of geometric systems}
\label{exact:section-boundaries}

We continue with the pointed pregeometry of
Theorem~\ref{geom:pregeometry}, above the threshold of
Corollary~\ref{geom:tail-no-growth}.  A shape and its active labels have the
meaning of Definition~\ref{sys:shapes}.  Unless otherwise stated, every
active basis piece in this section has cardinality equal to the uniform
level~$\mu$.  The bases remain auxiliary choices.

\begin{definition}[A prescribed boundary isomorphism]
\label{exact:boundary-data}
Let $a$ be a finite ordered set of axes, and let
$\mathcal X^-=(X_s^-:s\subseteq a)$ and
$\mathcal X^+=(X_s^+:s\subseteq a)$ be systems of the same shape.
A prescribed boundary isomorphism is a family
\[
 h_s:X_s^-\longrightarrow X_s^+\qquad(s\subsetneq a)
\]
of pointed isomorphisms such that
$h_t\mathbin{\upharpoonright}X_s^-=h_s$ whenever
$s\subseteq t\subsetneq a$.  This condition refers to the displayed
inclusions.  It does not add an assumption about intersections of two
incomparable vertices inside the top.
\end{definition}

A list on the boundary can consequently be specified by assigning a
proper face to each of its occurrences.  Before consistency on actual
intersections has been proved, its prescribed image means the list
obtained by applying the corresponding $h_s$ to each occurrence.
In particular, the assertion that two occurrences name the same element
is one of the atomic comparisons that must be preserved.

\begin{theorem}[Exact geometric boundary lifting]
\label{exact:geometric-boundary}
For every finite allowed shape, at all sufficiently closed uniform
levels, every prescribed boundary isomorphism between two systems of
that shape extends to a pointed isomorphism of their tops.  The top
isomorphism, together with its prescribed restrictions, is an
isomorphism of the systems.

The refinements of the eligible levels needed for a fixed shape use
only the one-dimensional bounds for its working scheme, the bounds
for its tiling layouts, and the corresponding assertions for shapes
on fewer axes.  In particular these refinements have the uniformity
specified in Section~\ref{close:section-uniform}.
\end{theorem}

We prove the theorem by induction on the number of axes.  At zero axes
it is pointed categoricity.  The induction at a positive number of
axes has two parts: preserving the joint diagrams of the entire
boundary, and realizing successive extensions of a partial match
inside the given target.  The first part supplies, among other
things, the missing compatibility on actual intersections.

\begin{lemma}[Joint boundary comparisons]
\label{exact:joint-boundary}
Assume exact geometric boundary lifting for all allowed shapes on
fewer than $n$ axes.  At a sufficiently closed uniform level, a
prescribed boundary isomorphism between two $n$-axis systems preserves
the bounded $\K$-diagram of every occurrence-tagged boundary list,
computed in the respective top models.
\end{lemma}

\begin{proof}
If the top label is inactive, let $u$ be the largest active label.
It is a proper subset of the axis set, and the top vertex is $X_u$.
Every vertex is the vertex at its largest active lower label, which
is contained in $u$.  Thus the map at $u$ already gives all the
comparisons in question.  We may assume the top label is active.

Write the axis set as $a\cup\{k\}$, with $k$ last and $|a|=n-1$.
Splitting off $k$ writes the two systems as
\[
 X^-\longrightarrow Y^- ,\qquad X^+\longrightarrow Y^+
\]
in the scheme $\mathcal G_L$ on $a$.
Its categoricity is supplied by
Theorem~\ref{sys:basis-classification}; after refining the levels,
Proposition~\ref{sys:working-package} supplies its working package.
The arrows add rank $\mu$ at the labels in a fixed upward closed
$Q\subseteq L$ and add no rank at the other labels.  Call such a
step a step of shape~$Q$.  The boundary prescription gives a full
system isomorphism $e:X^-\simeq X^+$ and compatible isomorphisms
\[
 h_s:Y_s^-\simeq Y_s^+\qquad(s\subsetneq a)
\]
whose restrictions to $X_s^-$ agree with~$e$.

If joint comparison fails, choose bounded lists $f$ from $X^-$ and
$d^-$ from the proper vertices of $Y^-$ witnessing failure, and put
$d^+=h(d^-)$.  All occurrences from the lower layer may be included
in $f$; all the remaining occurrences lie in these upper proper
vertices.  The comparisons of
\begin{equation}
 (f,d^-)\text{ in }Y^-
 \quad\text{and}\quad
 (e(f),d^+)\text{ in }Y^+
 \label{exact:opposite-comparisons}
\end{equation}
differ.  The notation in \eqref{exact:opposite-comparisons} includes
the indicated vertex occurrences.  If there is no upper test $d^-$,
the base isomorphism and the strong arrows already give equality,
so this case cannot witness failure.

A system isomorphism matching these lists would in particular be a
$\K$-isomorphism of the tops matching them.  Hence the working
$\mathcal G_L$-diagrams of the lists in
\eqref{exact:opposite-comparisons} also differ.  Choose an infinite
cardinal $\sigma<\mu$ bounding the lengths of the lists.  Enlarge a
cardinal $\chi<\mu$ so that $\chi^\sigma=\chi$, it bounds the
relevant labels and parameter-orbit constants, so that
Lemma~\ref{calc:parameter-orbits} gives at most $\chi$ orbits of
$\sigma$-lists over $\chi$ parameters.  Choose $\mu$ closed far enough that all
the following tree costs are below it.  Let $\epsilon$ be the least
infinite cardinal with $2^\epsilon>\chi$.  There are at most $\chi$
nodes below height $\epsilon$, and $2^\epsilon<\mu$ leaves.

We construct a binary tree of branch worlds $C_\eta$ in
$\mathcal G_L$, for $\eta\in{}^{\le\epsilon}2$, and a single
increasing reference chain $(R_i:i\le\epsilon)$ in that scheme.
All these objects have level~$\mu$.  A branch world carries a copy
$f_\eta$ of~$f$.  For every node $\eta$ of length $i$ the invariant
also includes a prescribed isomorphism
\begin{equation}
 b_\eta:\partial C_\eta\simeq\partial R_i.
 \label{exact:reference-invariant}
\end{equation}
Along a branch, these boundary maps commute with the inclusions into
later branch and reference worlds.  At each splitting node, the two
new copies of its upper test $d$ have the same image in the next
reference boundary.  Those images will be retained at all later
stages.

Start with $C_\varnothing=R_0=X^-$ and the identity boundary map.
Suppose the objects at level $i$ have been constructed.  Choose a
reference step $R_i\to R_{i+1}$ of shape~$Q$.  Such a step exists:
categoricity of $\mathcal G_L$ identifies $R_i$ with $X^-$, and we
transport the given extension $X^-\to Y^-$ along that
identification.

For each $\eta\in{}^i2$, an isomorphism $X^-\simeq C_\eta$ can
be chosen to take $f$ to $f_\eta$.  Indeed arrows along the branch
preserve its bounded diagram, and equality of bounded diagrams in
the working scheme is implemented by an isomorphism.  Transport
the minus and plus extensions along this return isomorphism, using
$e$ on the plus base.  They give children $C_{\eta^\frown 0}$ and
$C_{\eta^\frown 1}$ over $C_\eta$, with opposite comparisons to
$f_\eta$ and with the given identification between their proper
upper vertices.  On their lower proper vertices that identification
is the identity of the current branch world.

It remains to extend \eqref{exact:reference-invariant} to the
children; merely choosing arbitrary isomorphisms of the new worlds
would not suffice.  First do this for the plus child.  Process all
proper subsets $s\subsetneq a$ in increasing cardinality.  Consider
the restriction of the plus step to the axes $s\cup\{k\}$ and the
corresponding restriction of $R_i\to R_{i+1}$.  On the base
vertex, the prescribed map is $(b_\eta)_s$.  On every other proper
vertex it is either a restriction of that map or one of the upper
maps already constructed at a proper subset of~$s$.  These maps
commute on all indicated subfaces by construction.  The restriction
has at most $n-1$ axes, so the induction hypothesis lifts this
boundary prescription onto its upper vertex.  This supplies the
map at $s$, whether that vertex is active or repeated from a
smaller active one.  The resulting family is the required plus
boundary map.  Compose it with the given minus-to-plus boundary
identification to obtain the minus boundary map.  Both extend
$b_\eta$, and the two copies of the test have equal reference
images.

At a limit $i\le\epsilon$, take unions along each branch and in
the reference chain.  The lower-dimensional working scheme has
the chain and common-upper-bound properties, and these unions have
size $\mu$.  The coherent boundary maps have unions which are
onto the reference boundary: each previous reference vertex was
already the image of the corresponding branch vertex.  Thus the
invariant persists.  No assertion that a limit inclusion is itself
a step of shape~$Q$ is needed.  At its next successor stage a fresh
step of that shape is available over the union by categoricity.

At a leaf, apply the induction hypothesis once more, this time to
the $(n-1)$-axis worlds $C_\eta$ and $R_\epsilon$, with the
boundary prescription $b_\eta$.  Obtain a full isomorphism
$j_\eta:C_\eta\simeq R_\epsilon$.  Let $A$ be the list of all
reference images of the splitting tests.  Its length is at most
$\chi$, since there were at most $\chi$ splitting nodes and each
test had length at most~$\sigma$.

For two different leaves, use their first splitting node.  The
associated test has the same image in $A$ on both branches, whereas
its comparison with the images of $f$ is opposite.  Arrow
preservation of diagrams carries this distinction to the leaves,
and $j_\eta$ preserves it in $R_\epsilon$.  Consequently the
$2^\epsilon$ lists $j_\eta(f_\eta)$ lie in different orbits over
$A$.  This contradicts the bound~$\chi$.  Joint boundary
comparison follows.
\end{proof}

\begin{remark}
The proof just given applies to equalities between occurrences from
incomparable faces.  It therefore proves that the prescribed maps
have a well-defined injective union on the actual union of the
boundary vertices.  Applying the same observation to the inverse
family proves that this union is a bijection between the two
boundary unions.  Equality of actual intersections was not an
input to the argument.
\end{remark}

The boundary prescription now respects actual intersections and all
bounded joint diagrams.  The remaining task is to extend a bounded match
inside the prescribed target.  We first establish testing for its tiled
boundary layout, then use a strip avoided by all boundary supports to
realize the resulting comparison without enlarging that target.

\begin{lemma}[Testing on rationally tiled parameter orders]
\label{exact:tiled-testing}
Fix the finite-support order template $E$ and its natural stabilized
$\K$-diagrams.  Fix a nonempty set-sized initial order $J_0$, finitely many tile
labels $i\chi$.  These operations cover
the chain lengths and cardinal costs in the domination and return-tree
arguments.

\paragraph{Placed comparison and syntax tests.}
For a specified permitted layout and tuple arity, the comparison request
asks for a bound on the size of a parameter test witnessing inequality
between two placed comparisons.  More explicitly, quantify over an
eligible level, its indicated order layout, the two candidate term lists
in order enlargements, and the parameters generated by the designated
parts.  If their comparisons differ on some bounded parameter list,
require that they differ on one of size at most the proposed bound.
Inequality is evaluated in a larger eligible padded presentation,
using isomorphism to a well-ordered chart, or equivalently by its $D_F$
comparison where the chart clause has been obtained.  All the objects
and positions involved in a particular test are sets.  Universal
quantification over the level cardinal is an ordinary first-order
quantifier.

The permitted layouts are the whole-model layout, designated vertex
parts, and finitely segmented or tiled layouts with the prescribed
order and colors.  Their codes belong to the descriptor set.  The
ordinary and rationally tiled ordinal-vector arguments of
\Cref{calc:testing,exact:tiled-testing} prove that this request has a
uniform witness.  The syntax request asks for a test size at which the fixed
$D_F$ comparison on patterns of a specified size is already determined.
The set of such patterns and the set-structure back-and-forth
construction in \Cref{lev:diagram-coding} prove existence.  Neither
request mentions a truth predicate for $\mathcal C_n$.

For the rationally tiled layouts $\sum_i(H_i\times\mathbb Q)$ used
in the geometric application, the comparison request includes the
bounded frozen data of Lemma~\ref{exact:tiled-testing}.
That lemma supplies its witness also for candidates in arbitrary
enlargements of the underlying $E$-order.  The exceptional fibers,
their frozen positions, and the set of cut coordinates have bounds
in the input arities and fixed descriptor; no new dependence on the
level or the finite depth is introduced.

\paragraph{Approximation, compactification, and isolation bounds.}
The approximation and compactification constructions take a comparison
bound and a profile bound at the specified arity, increase the lengths
to dominate the exception counts, and perform the bounded power-set
iteration just described.  Thus their sizes are fixed compositions of
the first two requests and cardinal operations.  The isolating-fragment
bound is the size of the initial supports, the bounded initial parts of
the candidate blocks, and the terms on those supports in the proof of
\Cref{iso:alternative}.  These again use the same comparison and
cardinal requests.  The construction of all-dominated objects uses
larger input ordinals in these requests, mixed LS, and the indicated
successor-length recursions; it introduces no new form of predicate
depending on the marked depth.  The existence assertions used here are
\Cref{iso:finite-existence,iso:all-lengths,iso:independent-lists}, with the mixed interface just verified.

\paragraph{Eventual orbit thresholds.}
The remaining request asks for the first threshold above which a
specified reversal, orbit-preservation, or stabilization assertion holds
at the eligible levels and the indicated arity.  The assertion itself
uses the standardized object sets, arrows, and orbit relation defined
above.  Thus the threshold test has the form
\[
 \forall\mu\bigl(S(\mu)\land\mu>\beta
           \ \Longrightarrow\ R(d,\alpha,\mu)\bigr),
\]
or its two-level version, with $R$ one of these fixed orbit assertions.
The reversal and stabilization arguments prove the existence of the
threshold when the current categoricity and the previous required
conditions hold on the unbounded eligible class.  The use for geometric
shapes has exactly those hypotheses by
\Cref{sys:working-package}.  Passing from these thresholds to
diagram homogeneity also requires smaller eligible levels cofinal
below the final level; that requirement is recorded separately as a
limit-point refinement.

We check that this list accounts for a whole generic step.  In a marked
step, extraction uses partition bounds, the underlying comparison and
isolation bounds, and arbitrarily large samples.  It chooses a template
from the set established in
Proposition~\ref{close:uniform-definitions}; see
\Cref{mark:template}.  After that choice, the two-part comparison of
\Cref{mark:two-part-testing}, used in \Cref{mark:chain-closure},
is the placed comparison request with
this template as parameter.  The downward isolation argument requires
the same bounds and sufficiently closed smaller levels.  Orbit
comparison and saturation use the transport argument; the passage to
the unary chart clause uses the syntax request.  Projection, completion,
and exact boundary lifting then use the ordinary comparison requests,
the prior unary conditions, and the tree costs; exact lifting may require
one further supply of cofinal smaller levels.  These are respectively
the constructions of \Cref{iter:projection-types,iter:boundary-completion,iter:exact-boundary}.

For geometry, first use the current categoricity condition and prior
basis conditions as unary inputs to the eventual orbit request, then
require smaller eligible levels and the chart syntax bounds.  Basis
lifting and exact boundary lifting use the same one-dimensional and
tiled-layout requests and tree costs, by
\Cref{sys:basis-classification,exact:geometric-boundary}.  A simultaneous projection calculation
or a maximum over finitely many lower descriptors is expressed by
bounded quantification over that finite descriptor.  It does not require
successively inserting their formulas into one another.

Within each of these generic proofs there are finitely many successive
uses of closure and of cofinal smaller levels.  Label those positions
in the proof in their order.  The predicate for a position is the initial
adequacy predicate conjoined with the earlier stated threshold,
closure, and limit-point conditions.  Substituting these descriptions
at the finitely many positions gives a fixed formula for each request.
The number of positions is attached to the generic proof, not to the
finite axis count; finite lower-scheme lists are handled by the bounded
quantification just described.  This produces the asserted finite
register with $S$ eliminated in favor of its uniform defining formula.

\paragraph{The eligible predicates in a marked step.}
The following substitution order also previews the common-level induction
at the end of this section.  References here to retaining $G_j$ use the
\hyperref[lev:closure-preview]{advance notation in Section~\ref*{lev:section-working-schemes}};
the actual classes and
their absorption property are constructed below, after the register is
fixed.  They supply levels for that induction, not parameters for the
requests being defined here.

Let $S_0$ be the
unary conjunction of the full individual working conditions for the
input scheme and the projection and stationary-prescription conditions
already established for the finitely many lower descriptors.  The mixed
interface supplies their mixed working conditions.  First refine $S_0$
by the testing, approximation, isolation, and domination bounds of
Sections~\ref{calc:section-calculus} and~\ref{iso:section-isolation};
call this class $S_1$.  On its sufficiently closed members the actual
constructions give the samples used in Lemma~\ref{mark:template}.
The induction maintains that $S_1$ is unbounded by retaining a $G_j$;
unboundedness of an arbitrary class alone would not justify this step.

After selecting $F^b$, let $R(\mu)$ be the conjunction of $S_1(\mu)$,
the individual presentation flag for $F^b$, and the natural-interpretation
flags for its base and upper values in the old scheme.  Evaluate the
testing request for the layout $U_H\cup A_{H'}$ on this preliminary
class $R$, using the old scheme's $D_F$.  Lemma~\ref{mark:template}
supplies the individual validity and natural interpretations;
Lemma~\ref{mark:two-part-testing} reduces the comparison to the old
working scheme, where the ordinal-vector argument of
Proposition~\ref{calc:testing} supplies its uniform bound.

Now refine $R$ by that testing bound and its placement and arity costs;
call the resulting class $S_2$.  Thus $S_2$ is the output of this
refinement, not the eligible predicate in its own defining request.
The preliminary predicate $R$ uses only the earlier costs and the two
specified kinds of flags.  Neither the request nor its witness uses
a $D_{F^b}$ chart clause or chain closure for the pair scheme.

At members of $S_2\cap\Lim(S_2)$ closed under the same arity costs,
Lemma~\ref{mark:chain-closure} proves pair-chain closure, including
bounded tuples spanning the chain.  The actual pre-closure orbit
argument and this chain assertion then give
Theorem~\ref{mark:package}; only now impose the syntax bound for
$D_{F^b}$ and request its chart clause.  Projection correspondence and
amalgamated boundary completion follow after the fixed comparison and
tree-cost refinements in Section~\ref{iter:section-boundaries}.
The fixed-parameter boundary argument and exact lifting may add one
further limit-point refinement to obtain smaller levels where
completion already holds.  Each displayed eligible predicate is thus
a finite conjunction of unary flags, previously listed bound closures,
and limit-point conditions.  Substitution follows this displayed order;
no predicate for a previously chosen $G_j$ or closure function is
inserted into a bound request.  More generally the auxiliary subclass
$T$ in the eligible-level convention is used only to ensure an
unbounded supply of levels through these finite refinements.  It is
not an additional parameter of any request.  In the present induction
$T=G_j$ supplies this existence assertion, while each request still
uses the unary adequacy predicate and the finitely expanded refinements
just displayed.

\paragraph{The eligible predicates in a geometric step.}
The first assertion of Theorem~\ref{sys:basis-classification} for the
current shape follows from the previously proved assertions for its
finitely many lower shapes.  Start with the unary conjunction of this
current categoricity assertion and the needed lower-shape assertions.
The structural and tiled-presentation proofs give the actual arrows,
coherence, union conditions, and mixed containment used by
Proposition~\ref{sys:working-package}.  Its finite-tile alignment and
orbit calculation prove eventual reversal on this class.  The first
route in Proposition~\ref{lev:scheme-diagram-routes} then proves
stabilization; impose those arity bounds and a limit-point refinement
within the current eligible class.  Actual diagram homogeneity is
proved at the retained members before the $D_F$ syntax bound is imposed.

The four subsequent claims in the proof of
Theorem~\ref{sys:basis-classification} use this established package,
the preceding one-dimensional bounds, and finite tree costs.  They
prove the relative-basis assertion at the retained levels.
For exact boundary lifting, include the already proved exact assertions
for all proper restricted shapes in the initial unary conjunction.
The tree and unoccupied-strip proofs of
Theorem~\ref{exact:geometric-boundary} add only the indicated layout,
support-closure, and tree-cost refinements.  Increasing the number of
axes changes the finite list of lower descriptors and the ordinal
size inputs; it does not add a new kind of eligible predicate or a new
position in this generic substitution order.

Finally, the witness assertions are precisely the uniform bounds proved
in the cited constructions with their stated hypotheses.  An irrelevant
descriptor, or a stage whose hypotheses fail, may give a request with
no witness.  Its value $0$ makes a total definable ordinal function and
has no mathematical force.  At a used stage we invoke the preceding
construction to establish existence before applying the bound.  In
particular, totalization supplies neither an adequate template nor a
missing lifting or testing witness.
\end{proof}

\subsection{The common majorant and its limit refinements}

We now construct the hierarchy used in the preceding previews.  The
register and its finite substitutions have been fixed independently of
this construction; the common majorant bounds their values, while the
limit refinements supply smaller eligible levels cofinally below a new
level.

Choose a cardinal $\vartheta$ above the hereditary sizes of the normalized
descriptor set and all fixed parameters.  This is one cutoff, chosen
before any finite-depth induction; it includes all candidate templates,
not just those already selected.  For $\alpha\in\Ord$, take the supremum
of the values of all the functions in the expanded finite register,
for every descriptor and for all ordinal inputs at most $\alpha$.
Finite lists of size inputs are included by taking all their coordinates
at most $\alpha$.  Each such collection is a set, and each request has
been totalized, so Replacement bounds its values.  We may therefore
choose a fixed, monotone definable ordinal function $\Phi$ such that
\[
 \Phi(\alpha)>\vartheta,\qquad \Phi(\alpha)>\alpha,
 \qquad B_q(d,\vec\beta)<\Phi(\alpha)
 \quad(\max\vec\beta\le\alpha).
\]
Include the initial single-model requirements in this finite register.
The formulas defining its members have already been fixed.  No partial
truth construction, and no bound on a variable formula's complexity,
is being used here.

For a definable class $A$ of ordinals write
\[
 \Lim(A)=\{\lambda:\sup(A\cap\lambda)=\lambda>0\},
 \qquad
 \operatorname{Cl}(f)=
 \{\lambda:\forall\alpha<\lambda\ f(\alpha)<\lambda\}.
\]
Multiple ordinal inputs can be replaced by their maximum in the closure
condition.  Define
\[
\begin{split}
G_0&=\{\mu:\mu\text{ is a strong limit cardinal},
                    \cf(\mu)=\omega,\ \mu\in\operatorname{Cl}(\Phi)\},\\
G_{j+1}&=G_j\cap\Lim(G_j)\qquad(j<\omega),\qquad
G_\omega=\bigcap_{j<\omega}G_j.
\end{split}
\]
Because $\Phi(0)>\vartheta$, every member of every $G_j$ exceeds the
common parameter cutoff.  This detail cannot be replaced by discarding
an arbitrary initial segment after each new template choice.

The hierarchy itself has a uniform definition.  For an ordinal $\lambda$,
form $A_0=G_0\cap(\lambda+1)$ by Separation and then, by finite recursion
on subsets of $\lambda+1$, put
\[
 A_{i+1}=\{\beta\in A_i:\beta>0\text{ and }
                                  \sup(A_i\cap\beta)=\beta\}.
\]
The assertion $\lambda\in A_j$ is one formula with $j,\lambda$ as inputs,
and is equivalent to $\lambda\in G_j$.  Quantifying over $j\in\omega$
defines $G_\omega$.  In particular the countable constructions below
can choose least witnesses using this formula and Replacement.

\begin{lemma}[Closure and absorption]
\label{close:absorption}
Each $G_j$ is unbounded and closed under suprema of strictly increasing
countable sequences of its members.  The class $G_\omega$ is unbounded.
If a current eligible class $S$ contains $G_j$, and a finite sequence of
refinements consists of the bound closures and thresholds in the fixed
register and restrictions to limit points of earlier eligible classes,
then the resulting class contains $G_{j+m}$ for some finite $m$.
Here every used bound must have a witness under its stated hypotheses.
\end{lemma}

\begin{proof}
Given any starting ordinal, choose strictly increasing infinite cardinals
$(\kappa_n)_{n<\omega}$ above it with
\[
 \kappa_{n+1}>
 \max\bigl(2^{\kappa_n},
                \sup\{\Phi(\alpha):\alpha<\kappa_n\}\bigr).
\]
The supremum $\kappa$ of this sequence is a cardinal of cofinality
$\omega$.  For every cardinal $\lambda<\kappa$, some $\kappa_n$ exceeds
$\lambda$, and then $2^\lambda\le2^{\kappa_n}<\kappa$.  For every
$\alpha<\kappa$, the same choice gives
$\Phi(\alpha)<\kappa_{n+1}<\kappa$.  Thus $\kappa\in G_0$.
If instead the $\kappa_n$ are an increasing sequence in $G_0$, their
supremum is again a countable-cofinality strong limit cardinal and is
strictly $\Phi$-closed by these same two tests.  This proves the two
assertions for $G_0$.

Suppose they hold for $G_j$.  Above any starting ordinal choose a strictly
increasing countable sequence in $G_j$.  Its supremum belongs to $G_j$
by closure and to $\Lim(G_j)$ because the sequence is cofinal there.
This proves unboundedness of $G_{j+1}$.  A countable increasing sequence
in $G_{j+1}$ has its supremum in $G_j$, and its own members witness that
this supremum belongs to $\Lim(G_j)$.  Hence $G_{j+1}$ has the asserted
closure as well.

Choose $\lambda_n\in G_n$, strictly increasing and above an arbitrary
prescribed ordinal.  For each fixed $j$, its tail lies in $G_j$ because
the classes are nested.  The supremum belongs to $G_j$ by its countable
closure.  It consequently belongs to $G_\omega$, proving unboundedness.

For absorption, maintain that the current eligible class contains a
particular $G_k$.  A request value on inputs below a member $\mu\in G_k$
is less than $\Phi(\alpha)$ for a suitable $\alpha<\mu$, and hence less
than $\mu$.  Thus a bound-closure refinement retains all of $G_k$.
A constant threshold is included as a request with input $0$ and has
the same property.  If the next refinement demands cofinally many
members of the current class below the new level, retain $G_{k+1}$:
its members are limit points of $G_k$ and thus of the current class.
If several earlier eligible classes are mentioned, the maintained
index can first be increased to the maximum of their finitely many
indices.  Induction through the finite refinement list proves the
claim, with $m$ bounded by its number of limit-point refinements.
\end{proof}

\begin{theorem}[Common levels for all finite depths]
\label{close:common-levels}
With the fixed data of either application and the constructions proved
in the preceding sections, there is an unbounded class of
countable-cofinality strong limit cardinals at which all its finite-depth
conclusions hold simultaneously.  In the marked application this
includes the working packages, projection and type correspondences,
amalgamated completion, and exact boundary lifting for every
$\mathcal C_n$, uniformly over the root prescription codes realized
at arbitrarily large eligible single-model levels.
In the geometric application it includes categoricity, the working
packages, basis lifting, and exact boundary lifting for every finite
shape.  One such common level may be chosen above any specified set of
fixed cardinal thresholds.
\end{theorem}

\begin{proof}
Use the fixed register and $\Phi$ just constructed.  The initial
single-model results hold on $G_0$ after the initial requirements have
been included.  Suppose the assertions required as input to a finite
induction step hold throughout $G_j$.  Take $S$ to be the class defined
by their unary adequacy formula, with the current descriptor.  It
contains $G_j$.  Lemma~\ref{close:mixed-interface} supplies the mixed
conditions for that step.  Lemma~\ref{close:recipe-register} identifies
its bound requests and gives the existence of each relevant witness
at its place in the proof.  Lemma~\ref{close:absorption} then retains
some $G_{j'}$, with $j'<\omega$, through all its refinements.

When a marked step extracts a new template, its code lies in the fixed
descriptor set by Proposition~\ref{close:uniform-definitions}.  The
remaining requests with that code as parameter were already majorized
by $\Phi$.  Thus making the choice introduces no new closure function
or cutoff.  For a given finite shape, the finitely many previously
required lower shapes can first be brought to one $G_j$ by taking the
largest of their indices.  The same observation applies to the finite
projection lists in the marked argument.  The two ordinary finite
inductions therefore give, for each finite descriptor, all its required
conclusions on $G_j$ for some finite $j$.

In the marked application only root codes consistent at arbitrarily
large eligible single-model levels are used.  A code obtained from an
actual pair at a sufficiently closed starting cardinal has that property:
freely lift its type with the named approximation data to arbitrarily
large single-model levels.  The majority rule is preserved there, and
restriction from such a level gives the same stationary prescription
at every sufficiently closed smaller single-model level with that
named pattern.  This is the prescription argument in
Lemma~\ref{geom:root-prescription}, prior to the use of the finite marked
systems.  It requires no persistence of a no-growth statement about
$P$ at larger levels.  The fixed code set and majorant include every
such possible input code, so the common-level construction can precede
the choice of the actual pair.

Every member of $G_\omega$ belongs to $G_j$ for every finite $j$.  It consequently
satisfies the conclusion for every finite descriptor used in the
application, although the index $j$ and the selected template may depend
on that descriptor.  Lemma~\ref{close:absorption} makes $G_\omega$
unbounded, so choose a member above the desired thresholds.  All
constructions in this argument are ordinary set recursions, Separation,
Replacement, and finite induction with uniform formulas.  This completes
the simultaneous closure justification in ZFC.
\end{proof}
==== END Eventual-Categoricity-for-Abstract-Elementary-Classes//13-uniform-closure.tex ====

==== BEGIN Eventual-Categoricity-for-Abstract-Elementary-Classes//14-cardinal-transfer.tex ====
\section{Transfer to all larger cardinals}
\label{tail:section-transfer}

The common levels of Theorem~\ref{close:common-levels} provide one
cardinal at which all finite geometric shapes have exact boundary
lifting.  This section uses that single cardinal as the base of an
induction through the cardinals.  The levels supplied by the closure
construction themselves need not contain a tail.

The trade between one extra dimension and an increase in cardinality
goes back to Shelah's multidimensional existence and uniqueness methods
\cite[Theorems~5.1--5.2]{Shelah1983B}; compare their later formulation in
\cite[Lemma~11.6]{ShelahVasey2024}. The argument below
is given for the exact boundary maps and cardinal assignments used here.

Fix a common uniform level $\gamma$ from
Theorem~\ref{close:common-levels}, for all the geometric shapes and
their exact boundary assertions.  Choose it strictly above the
no-growth threshold $\lambda$ of
Corollary~\ref{geom:tail-no-growth}, and above all fixed point and
single-model thresholds.  In particular $\gamma>\lambda_0$, the
cardinality of the distinguished model~$M_0$.  In every pointed
model of cardinality at least $\gamma$, model cardinality equals
the cardinality of a basis of its point geometry.

\begin{definition}[Prescribed piece cardinalities]
\label{tail:piece-cardinalities}
Let $L$ be an allowed family on a finite axis set $a$.  A cardinal
assignment on $L$ is a family of cardinals
\[
 (\kappa_s:s\in L),\qquad
 \gamma\leq\kappa_s\leq\kappa_t\quad(s\subseteq t\text{ in }L).
\]
A system with this assignment satisfies the span and inclusion
conditions of Definition~\ref{sys:shapes}, with a witnessing basis
partition $(H_s:s\in L)$ such that $|H_s|=\kappa_s$.
The bases are not named.  A prescribed boundary isomorphism has
the meaning of Definition~\ref{exact:boundary-data}.
\end{definition}

For $t\subseteq a$ let $a_L(t)$ be its largest active subset.
The span identities and monotonicity imply
\begin{equation}
 \rk P(X_t)=\max\{\kappa_s:s\in L,\ s\subseteq t\}
           =\kappa_{a_L(t)}.
 \label{tail:vertex-size}
\end{equation}
All these ranks are at least $\gamma$, so
Corollary~\ref{geom:tail-no-growth} shows that the same formula
gives $\|X_t\|$.  It also shows that an inactive vertex equals
$X_{a_L(t)}$.  Lemma~\ref{sys:relative-bases} applies without a
uniform-cardinality requirement: its proof only uses the finite
shape and the basis axioms of the pregeometry.

\begin{lemma}[Choosing subcubes with prescribed supports]
\label{tail:support-subcubes}
Suppose two systems $\mathcal X^-$ and $\mathcal X^+$ have the
same cardinal assignment, and prescribed isomorphisms $h_t$ on
their proper faces.  Suppose their top is active and put
\[
 \kappa=\max_{s\in L}\kappa_s,\qquad
 Q=\{s\in L:\kappa_s=\kappa\}.
\]
One can choose witnessing global basis partitions
$(H_s^-)$ and $(H_s^+)$ such that
\begin{equation}
 h_s[H_s^-]=H_s^+\qquad(s\in L,\ s\subsetneq a).
 \label{tail:proper-basis-choice}
\end{equation}
Fix such partitions.  Let $\chi$ be a cardinal with
$\gamma\leq\chi<\kappa$ which bounds all $\kappa_s<\kappa$.
Given at most $\chi$ requested elements in the finitely many
vertices on both sides, there are subsystems $\mathcal U^\pm$
inside $\mathcal X^\pm$ with the following properties:
\begin{enumerate}
\item Each requested element belongs to its indicated vertex.
      Every vertex whose size is strictly below $\kappa$ is
      retained in full.
\item Their witnessing pieces are subsets
      $I_s^\pm\subseteq H_s^\pm$.  They equal $H_s^\pm$ when
      $s\notin Q$, and have cardinality $\chi$ when $s\in Q$.
\item On every proper face,
      $h_t[U_t^-]=U_t^+$.
\end{enumerate}
If compatible subsystems have already been chosen whose witnessing
pieces are subsets of these fixed partitions $(H_s^\pm)$, and whose
total vertex sizes are at most $\chi$, their entire vertices can be
included among the requests.  Moreover, at every $s\in Q$ one can
require exactly $\chi$ additional basis coordinates beyond those
old selected pieces, on both sides.  All resulting inclusions
preserve the relative independence condition for system arrows.
\end{lemma}

\begin{proof}
Choose the pieces on the minus side.  For each proper active $s$,
the isomorphism $h_s$ takes its lower span onto the corresponding
lower span on the plus side, since it agrees with the prescribed
maps on every lower vertex.  Thus $h_s[H_s^-]$ is a relative basis
at~$s$.  By Lemma~\ref{sys:relative-bases}, these relative bases
assemble in the plus system.  Complete them by a relative basis
at its top.  Their cardinalities have the required values because
relative rank is invariant under isomorphism.  This gives the
claimed partitions.

We construct the desired subsystems by a countable closure
process, on both sides and at all the finitely many vertices.
Begin with the requested sets, the fixed point, and any specified
old subsystems.  At every growing active label $s\in Q$, also
request $\chi$ basis coordinates.  In the extension version
choose these outside the old selected piece.  There are enough
coordinates since $|H_s^\pm|=\kappa$ and the old piece has size
at most $\chi<\kappa$.  At a proper label the choices may first
be made on the minus side and transported by $h_s$; these are
still fresh on the plus side.  At the top make the choices on
both sides separately.  Retain all nongrowing vertices in full.

At each finite stage choose, by the L\"owenheim--Skolem axiom,
strong submodels of the ambient vertices containing all requests
so far.  Their sizes are at most $\chi$: the LS bound, point,
retained smaller vertices, and requested data all fit within that
cardinal.  At the next stage make the following further requests.
\begin{enumerate}
\item For each inclusion of labels $s\subseteq t$, put all
      elements of the currently chosen model at $s$ into the
      requests at~$t$.
\item For every point obtained in a chosen vertex, choose a finite
      support for it from the union of the global basis pieces
      below that vertex.  Request each supporting coordinate in
      the vertex of its own active label.
\item At each proper face, request the image under $h_t$ of every
      element currently included on the minus side, and the
      inverse image of every element currently included on the
      plus side.
\end{enumerate}
Also retain all previous requests and chosen models.  These
operations make at most $\chi$ requests at each stage.  Each
ambient point set has the given basis partition, so the supports
in the second operation exist and lie in the indicated vertices.
For a retained smaller vertex all supporting labels are retained
as well: if $s\subseteq t$ and $\kappa_t<\kappa$, monotonicity
gives $\kappa_s<\kappa$.  Thus no operation requires enlarging a
retained vertex beyond its given ambient model.

Take the unions of the chosen models through the countable
process.  Coherence makes all successive and vertex inclusions
strong, and the AEC chain axioms give strong limit models
$U_t^\pm\leq_\K X_t^\pm$.  On a proper face the image and
inverse-image requests give exactly $h_t[U_t^-]=U_t^+$.
This construction used the maps one face at a time; it did not
assume that their union on possible extra intersections was
already a function.

Put $I_s^\pm=H_s^\pm\cap P(U_s^\pm)$.  Every point of
$P(U_t^\pm)$ occurs in a finite-stage model, and its supporting
coordinates were subsequently placed at their own labels.
Conversely, the point set of $U_t^\pm$ is relatively closed in
the ambient model and contains all selected coordinates below
$t$.  Therefore
\[
 P(U_t^\pm)=\cl\left(\bigcup_{s\in L,\ s\subseteq t}
                                      I_s^\pm\right).
\]
The selected pieces are subsets of the single global independent
basis and hence are independent together.  They supply precisely
the required decomposition.  Nongrowing pieces and vertices were
retained in full.  At a growing label at least $\chi$ coordinates
were requested and its model has size at most $\chi$, so its
piece has size exactly $\chi$.  In the extension version, at
least $\chi$ fresh coordinates were requested; at most $\chi$
coordinates altogether were added.  The additional piece
therefore has cardinality exactly~$\chi$.

Finally, the selected subsets increase when old subsystems are
included.  Being subsets of the same global basis proves the
relative independence requirement for their inclusions, using
the criterion of Lemma~\ref{sys:relative-bases}.
\end{proof}

The subcube lemma makes compatible smaller systems available, but an
arbitrary isomorphism between the next two subcubes need not extend the
previous one.  The cardinal induction resolves this by adding an axis:
the old full isomorphism becomes part of a boundary prescription at a
strictly smaller maximum cardinal.  This is why the induction must cover
all finite shapes simultaneously.

\begin{theorem}[Exact lifting at every larger cardinal]
\label{tail:all-cardinals}
For every finite allowed shape and every monotone assignment
$(\kappa_s:s\in L)$ of cardinals at least $\gamma$, any prescribed
boundary isomorphism between two systems with that assignment
extends to an isomorphism of their tops.
\end{theorem}

\begin{proof}
We induct on the cardinal
$\kappa=\max_{s\in L}\kappa_s$, proving the assertion
simultaneously for all finite shapes and all assignments with
that maximum.  For $\kappa=\gamma$ all pieces have size
$\gamma$, so Theorem~\ref{exact:geometric-boundary} applies at
the chosen common level.  Suppose $\kappa>\gamma$ and the
assertion is known at every smaller maximum.

As before, an inactive top equals a proper active vertex and its
prescribed map already gives the conclusion.  Assume the top is
active.  Keep all smaller pieces and their vertices in full.
There are only finitely many of them, so their cardinalities
have a common bound below~$\kappa$.  Choose the global basis
partitions of Lemma~\ref{tail:support-subcubes}.

Let $\delta=\cf(\kappa)$.  Choose an increasing sequence
$(\alpha_i:i<\delta)$ of ordinals below $\kappa$, cofinal in
$\kappa$, and fix enumerations of every growing vertex on each
side by~$\kappa$.  We construct continuous chains of subsystems
\[
 (\mathcal U_i^-:i<\delta),\qquad
 (\mathcal U_i^+:i<\delta),
\]
and compatible full system isomorphisms
$f_i:\mathcal U_i^-\simeq\mathcal U_i^+$.
Every proper-face restriction of $f_i$ is the given $h_t$ on
that subface.  Their pieces are increasing subsets of the
chosen global partitions.  Nongrowing vertices are retained
in full; all growing pieces at stage $i$ have the same
cardinality $\rho_i<\kappa$, at least~$\gamma$.

For the initial stage, choose $\chi<\kappa$ bounding $\gamma$,
the retained pieces, and the sizes of the requested initial
enumeration segments.  Apply Lemma~\ref{tail:support-subcubes}
on both sides.  This gives systems with the same piece sizes
and maximum below $\kappa$, whose proper-face maps are the
restrictions of the given prescription.  The induction
hypothesis at that maximum supplies~$f_0$.

Suppose $\mathcal U_i^\pm$ and $f_i$ are given.  Choose a
cardinal $\chi<\kappa$ which bounds $\gamma$, all retained
piece sizes, all old vertex sizes, and the next requested
enumeration segments.  The size checks justifying this choice
at every proper stage are given below.  Apply the extension
part of Lemma~\ref{tail:support-subcubes}.  It produces
$\mathcal U_{i+1}^\pm$ containing the old systems and the
requested segments, with exactly $\chi$ new independent
coordinates at every label in
\[
 Q=\{s\in L:\kappa_s=\kappa\},
\]
and none at the other labels.  The set $Q$ is upward closed:
if $s\in Q$ and $s\subseteq t\in L$, then
$\kappa\leq\kappa_t\leq\kappa$, so $t\in Q$.

Add a new last axis $k$.  Regard
$\mathcal U_i^\pm\to\mathcal U_{i+1}^\pm$ as the two layers
of systems with active labels
\[
 L'=L\cup\{s\cup\{k\}:s\in Q\}.
\]
The old pieces have their previous cardinalities and the
additional pieces all have cardinality~$\chi$.  These are
valid decompositions: the old and added coordinate sets are
disjoint subsets of the fixed global basis, and their unions
span the new vertices.  The cardinal assignment on $L'$ is
monotone.  Comparisons among old labels use the old
monotonicity, comparisons among new labels use equality to
$\chi$, and an old label below a new one has size at most
$\chi$ by its choice.  No new label is contained in an old
one.  All assigned cardinals are at least $\gamma$ and the
maximum is still strictly below~$\kappa$.

Prescribe the boundary maps of these enlarged shapes by $f_i$
on the entire old cube and by the given $h_t$ on every enlarged
proper face of the new cube.  They commute on all indicated
subfaces: on an old proper face the two prescriptions already
agree by the invariant for~$f_i$.  The cardinal induction
hypothesis applies to this shape as well, since it is
simultaneous in the number of axes and its maximum decreased.
It yields an isomorphism of the new tops extending $f_i$ and
all the enlarged proper-face maps.  This is the required
$f_{i+1}$.

At a nonzero limit $i<\delta$, take componentwise unions and
put $f_i=\bigcup_{j