\documentclass[12pt,letterpaper]{article}

\usepackage[margin=1in]{geometry}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage{amsmath,amssymb,amsthm,mathtools,stmaryrd}
\usepackage{booktabs,longtable,tabularx,array}
\usepackage{enumitem}
\usepackage{xcolor}
\usepackage{xspace}
\usepackage{listings}
\usepackage{tikz}
\usetikzlibrary{arrows.meta,positioning,fit}
\usepackage{pdflscape}
\usepackage{caption}
\usepackage{natbib}
\usepackage{fancyhdr}
\usepackage{hyperref}
\usepackage[nameinlink,noabbrev]{cleveref}

\definecolor{catblue}{HTML}{193B67}
\definecolor{catgreen}{HTML}{1F6A55}
\definecolor{catred}{HTML}{8B2E2E}
\definecolor{catgray}{HTML}{4B5563}
\definecolor{catlight}{HTML}{F3F6F8}

\hypersetup{
  colorlinks=true,
  linkcolor=catblue,
  citecolor=catgreen,
  urlcolor=catblue,
  pdftitle={CatDB: Toward a Compositional Semantic Data Layer},
  pdfauthor={Matthew Long; The YonedaAI Collaboration}
}

\pagestyle{fancy}
\fancyhf{}
\lhead{\small CatDB provisional synthesis}
\rhead{\small Evidence cut: 23 July 2026}
\cfoot{\thepage}
\setlength{\headheight}{15pt}

\newcommand{\CatDB}{\textsc{CatDB}\xspace}
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\status}[1]{\par\noindent\textit{Evidence status.} #1\par}
\newcommand{\paperreasoning}{\textnormal{\textsc{Paper Reasoning}}}
\newcommand{\computational}{\textnormal{\textsc{Computational}}}
\newcommand{\machinechecked}{\textnormal{\textsc{Machine-Checked}}}
\newcommand{\obstructed}{\textnormal{\textsc{Obstructed}}}
\newcommand{\openstatus}{\textnormal{\textsc{Open}}}
\newcommand{\rejected}{\textnormal{\textsc{Rejected}}}
\newcommand{\conditional}{\textnormal{\textsc{Conditional}}}
\newcommand{\acceptedmodel}{\textnormal{\textsc{Accepted Paper Model}}}
\newcommand{\provisional}{\textnormal{\textsc{Provisional}}}
\newcommand{\partref}[1]{\textsc{#1}}

\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]
\newtheorem{proposition}[definition]{Proposition}
\newtheorem{obligation}[definition]{Obligation}
\newtheorem{counterexample}[definition]{Counterexample}
\newtheorem{remark}[definition]{Remark}

\newcolumntype{Y}{>{\raggedright\arraybackslash}X}
\newcolumntype{L}[1]{>{\raggedright\arraybackslash}p{#1}}
\newcolumntype{C}[1]{>{\centering\arraybackslash}p{#1}}

\lstset{
  basicstyle=\ttfamily\small,
  backgroundcolor=\color{catlight},
  frame=single,
  rulecolor=\color{catgray},
  breaklines=true,
  columns=fullflexible,
  keepspaces=true,
  showstringspaces=false
}

\title{\CatDB: Toward a Compositional Semantic Data Layer\\
\large A conservative synthesis of model results, bounded computation, and open systems work}
\author{Matthew Long \\
\textit{The YonedaAI Collaboration} \\
\textit{YonedaAI Research Collective} \\
Chicago, IL \\
\texttt{matthew@yonedaai.com} $\cdot$ \url{https://yonedaai.com}}
\date{23 July 2026}

\begin{document}
\maketitle

\begin{center}
\fcolorbox{catred}{catlight}{
  \begin{minipage}{0.88\textwidth}
  \small
  \textbf{Provisional status.}
  This synthesis is not an accepted paper and is not a systems result.
  Internally accepted companion manuscripts establish paper models, not
  implementations.  The only current executable evidence used here is a
  closed shared-fixture surface for a finite semantic kernel.  No distributed
  runtime, optimizer, connector suite, federation engine, materialization
  engine, MDReader application, or scale benchmark is established.
  \end{minipage}
}
\end{center}

\begin{abstract}
Integration work fails in a familiar way.  A customer identifier means one
thing in an application database, another in a billing service, and something
less precise in an analytical export.  The joins still run, but their meaning
lives in migration scripts, transformation jobs, naming conventions, and the
memory of the people who wrote them.  When a schema or policy changes, the
team must reconstruct which decisions were copied into which pipeline.

This paper synthesizes a research program around a narrower response.  We
define \CatDB as a semantic multimodel data platform in which schemas,
mappings, migrations, identities, and provenance are first-class, versioned,
executable objects.  ``Executable'' means that an artifact has a typed
interpretation, validation obligations, and a route to compilation or
evaluation.  It does not mean that the current repository implements every
such route.

The synthesis answers five questions.  First, \CatDB's candidate distinction
is not a new physical data model.  It is one versioned contract connecting
several models while retaining each model's residual semantics.  Second,
typed mappings can make migration direction, coverage, loss, ambiguity,
authority, and physical intent reviewable before execution.  Third, mappings
may replace duplicated semantic logic or generate physical jobs only when the
required transformations factor through an adequate domain.  Extraction,
cleaning, transport, loading, scheduling, retries, and pair-specific rules
often remain.  Fourth, competitive physical execution is an open question.
Accepted papers specify compilation, federation, and cost contracts, but no
current compiler, connectors, optimizer, or benchmark establish their
performance.  Fifth, realistic distributed guarantees are operation
specific.  Immutable proposals and admitted monotone updates may converge;
single-valued activation, authority, membership, and noncommutative migration
transitions still require conflict preservation or coordination.

Evidence is deliberately uneven.  The accepted Slice 4 record reports that
Rust and independently implemented Haskell programs agree on 29 semantic
cases in a closed 33-fixture profile; four cases remain structural only.
Selected Lean declarations cover
named path and mapping laws, not the runtime.  Everything beyond that bounded
kernel remains a paper contract, an engineering hypothesis, or an obstruction.
The defensible thesis is therefore conditional: \CatDB moves some integration
meaning into typed, composable, versioned mappings, while federation,
materialization, ETL, and migration remain execution strategies with ordinary
systems costs and limits.
\end{abstract}

\tableofcontents
\newpage

\section{Problem, thesis, and evidence cut}
\label{sec:introduction}

\subsection{Plain-language problem}

A company has three definitions of ``active customer.''  The application
means an account that can sign in.  Billing means an account with an open
contract.  Analytics means an account with an order in the last ninety days.
The databases are not broken.  Each definition serves a real purpose.  The
failure begins when a pipeline treats the three definitions as interchangeable
and records the choice only in code.

A semantic layer cannot make the disagreement disappear.  It can give the
disagreement a durable form.  A mapping can state which source field denotes
which domain concept, under which snapshot and authority, with which loss and
coverage.  A migration can state how a version changes.  An identity decision
can retain evidence and uncertainty.  Provenance can state which source
records and semantic artifacts justify a result.  Those objects can then be
reviewed, composed, invalidated, and compiled.

This is the research program's central thesis:

\begin{quote}
\CatDB moves integration meaning from bespoke pipelines into typed,
composable, versioned mappings, while federation and materialization remain
execution strategies.
\end{quote}

The qualification matters.  A typed mapping does not clean a malformed postal
address, move bytes across a network partition, or decide who may merge two
customer records.  It can describe and constrain those operations.  The
physical work still has to run.

\subsection{Five synthesis questions}

The manuscript answers the five questions fixed by the accepted synthesis
outline:

\begin{enumerate}[label=\textbf{Q\arabic*.},leftmargin=2.4em]
  \item What does \CatDB model that relational, graph, document, and vector
  databases do not model together?
  \item How do typed mappings improve the description and execution of schema
  evolution?
  \item Which integration workloads can mappings replace, generate, or leave
  unchanged?
  \item Can semantic compilation preserve competitive physical execution?
  \item Which distributed consistency and convergence guarantees are
  realistic?
\end{enumerate}

\Cref{tab:five-answers} gives the short answers.  Later sections state the
assumptions and evidence behind them.

\begin{table}[htbp]
\centering
\small
\caption{Five answers at the current evidence cut.}
\label{tab:five-answers}
\begin{tabularx}{\textwidth}{C{0.09\textwidth}Y L{0.16\textwidth}}
\toprule
Question & Conservative answer & Current status \\
\midrule
Q1 & A versioned semantic contract can connect heterogeneous models while
recording mappings, migrations, identity, and provenance as objects.  It does
not subsume every source model. & Accepted paper models;
bounded kernel computation \\
Q2 & Typed mappings expose direction, coverage, loss, ambiguity, authority,
and obligations before a migration mode is selected. & Paper reasoning;
finite \(\Delta\) computation only \\
Q3 & Reusable semantic logic may factor through a domain; physical and
pair-specific work often remains. & Conditional counting result;
maintenance effect open \\
Q4 & Native compilation is plausible only if result equivalence and overhead
gates pass.  No current artifact establishes that. & \obstructed \\
Q5 & Guarantees must be selected per operation.  Some monotone or immutable
updates may converge; other transitions require coordination. & Accepted
paper model; runtime \obstructed \\
\bottomrule
\end{tabularx}
\end{table}

\subsection{What ``accepted'' means here}

All eighteen companion manuscripts are internally accepted as paper artifacts:
\partref{P1} through \partref{P18}
\citep{CatDBP01,CatDBP02,CatDBP03,CatDBP04,CatDBP05,CatDBP06,CatDBP07,
CatDBP08,CatDBP09,CatDBP10,CatDBP11,CatDBP12,CatDBP13,CatDBP14,
CatDBP15,CatDBP16,CatDBP17,CatDBP18}.  Acceptance means that each manuscript's
definitions, citations, nonclaims, build, and review gate closed at its
recorded source.  It does not turn a paper proposition into runtime evidence.

This synthesis remains unreviewed and provisional.  Companion-paper acceptance
closes one dependency gate but does not review or accept the synthesis.

\section{Evidence discipline and central definition}
\label{sec:evidence}

\subsection{Two status axes}

The research program separates the kind of evidence from the current workflow
outcome.  A claim may be supported by prior literature, paper reasoning,
machine checking, bounded computation, or an experiment.  Independently, its
operational status may be \textsc{Proved}, \textsc{Conditional},
\textsc{Computational}, \textsc{Open}, or \textsc{Obstructed}.  This prevents a
well-reviewed design from being reported as an implementation.

\begin{table}[htbp]
\centering
\small
\caption{Evidence classes used in this synthesis.}
\label{tab:evidence-classes}
\begin{tabularx}{\textwidth}{L{0.22\textwidth}Y Y}
\toprule
Class & What it establishes & What it does not establish \\
\midrule
Primary prior literature & A result or capability under the cited source's
model and assumptions & A \CatDB-specific result or implementation \\
\acceptedmodel & A reviewed mathematical or systems contract in a companion
manuscript & Executable behavior, performance, or scale \\
\paperreasoning & A definition, derivation, or proof under stated assumptions
in this source & Kernel checking or implementation conformance \\
\machinechecked & An exact named declaration under its audited assumptions &
The Rust source, SQL backends, connectors, networks, or the full engine \\
\computational & Observed output of named programs on a closed input surface &
General proof, unseen cases, production readiness, or performance \\
Experiment & Measured behavior with baselines, controls, raw data, and
failures retained & Universal behavior outside the tested workload \\
\bottomrule
\end{tabularx}
\end{table}

\subsection{Central definition}

\begin{definition}[CatDB]
\label{def:catdb}
\CatDB is a semantic multimodel data platform in which schemas, mappings,
migrations, identities, and provenance are first-class, versioned, executable
objects.
\end{definition}

Each word imposes a boundary.

\begin{itemize}
  \item \emph{Semantic} means that declared relationships, equations,
  coverage, loss, authority, and evidence are part of the contract rather than
  only comments around a physical job.
  \item \emph{Multimodel} means that several source models can participate
  without claiming that one finite category subsumes all relational, graph,
  RDF/OWL, document, vector, or full-text semantics.
  \item \emph{First-class} means that an artifact has identity, a typed
  representation, references, validation, and provenance.
  \item \emph{Versioned} means that every decision is bound to immutable
  revisions and can be compared, replayed, superseded, or rejected.
  \item \emph{Executable} means that an artifact names an interpretation and
  the obligations required for validation, compilation, or evaluation.  It is
  a design property.  Current execution exists only for the bounded kernel
  described in \Cref{sec:runtime-evidence}.
\end{itemize}

\begin{definition}[Semantic commit]
\label{def:semantic-commit}
A semantic commit is a content-addressed tuple
\[
K=(\mathcal S,\mathcal M,\mathcal U,\mathcal I,\mathcal P,
   \mathcal Q,\mathcal W,\mathcal X),
\]
where \(\mathcal S\) contains schema revisions, \(\mathcal M\) typed mapping
revisions, \(\mathcal U\) migration declarations, \(\mathcal I\) identity and
reconciliation decisions, \(\mathcal P\) provenance and policy profiles,
\(\mathcal Q\) query definitions, \(\mathcal W\) workspace references, and
\(\mathcal X\) physical execution profiles.  A commit is admissible only when
all referenced revisions exist and the selected cross-object obligations are
discharged or explicitly unresolved.
\end{definition}

This tuple is a synthesis contract, not an implemented catalog type.  The
internally accepted workspace paper gives a more detailed proposed commit
model \citep{CatDBP09}; no current workspace runtime constructs or publishes
such a value.

\subsection{Schemas, mappings, and physical realizations}

For the finite profile used by the current kernel, a schema presentation is
written
\[
S=(E,G,A,R),
\]
with entities \(E\), generating functional arrows \(G\), typed attributes
\(A\), and equations \(R\) between parallel paths.  Categories as schemas,
instances as functors, and functorial migration are established prior work
\citep{SpivakKent2012Ologs,Spivak2012Functorial,
SpivakWisnesky2015Relational,SchultzWisnesky2017AlgebraicIntegration,
SchultzEtAl2017AlgebraicDatabases}.  Executable categorical integration also
predates \CatDB \citep{CQL2026}.  The candidate delta is the versioned
operational contract and evidence boundary, not the categorical foundation.

\begin{definition}[Typed semantic mapping]
\label{def:mapping}
A typed semantic mapping revision is a tuple
\[
m=(s,t,F,\omega,\gamma,\lambda,\alpha,\pi),
\]
where \(s\) and \(t\) identify source and target schema revisions; \(F\)
assigns admitted entities, paths, and attribute expressions; \(\omega\)
selects a data operator or read interpretation; \(\gamma\) records coverage
and completeness; \(\lambda\) records loss, partiality, and ambiguity;
\(\alpha\) records authority and write policy; and \(\pi\) records provenance
and validation evidence.
\end{definition}

Schema-arrow direction does not determine data-flow direction.  For a schema
mapping \(F:S\to T\), the established pullback operator is contravariant,
\[
\Delta_F:\operatorname{Inst}(T)\longrightarrow\operatorname{Inst}(S),
\]
while \(\Sigma_F\) and \(\Pi_F\) are covariant under their own assumptions
\citep{Spivak2012Functorial}.  A forward ETL or data-exchange claim must name
the selected operator, query rewrite, target construction, or materialization
semantics.  It cannot be inferred from \(F\) alone.

\begin{definition}[Realization]
\label{def:realization}
For a semantic request \(q\) at commit \(K\), a physical realization
\(r\in\mathcal R(q,K)\) is a backend plan, federated plan, materialization,
incremental refresh, or generated transfer job that carries a certificate of
its semantic dependencies and residual obligations.
\end{definition}

Every realization is subordinate to a declared result contract.  If
\(\llbracket q\rrbracket_K\) is the abstract answer and \(N_K\) is the
profile-specific normalization, an exact realization must eventually satisfy
\[
N_K\!\left(\operatorname{run}(r)\right)
=\llbracket q\rrbracket_K.
\tag{1}
\]
Equation (1) is an evaluation obligation.  No current compiler, federation
engine, connector, or materialization engine discharges it.

\section{Running example: customer, order, and policy evidence}
\label{sec:example}

\subsection{Four sources and two consumers}

The example uses four heterogeneous sources:

\begin{enumerate}
  \item a SQLite application database with \code{customer},
  \code{organization}, and \code{order\_row};
  \item a PostgreSQL operational database with \code{account},
  \code{purchase}, regional residency tags, and billing status;
  \item a JSON product API with string SKUs, prices in minor currency units,
  and source-specific availability codes; and
  \item Markdown policy and evidence records that name approval, retention,
  and exception decisions.
\end{enumerate}

The proposed domain contains customers, organizations, orders, products, local
references, identity assertions, and provenance links.  One consumer is an
analytical model.  The other is a proposed MDReader view over evidence and
policy records.  MDReader is used only as a motivating consumer.  The
repository has no current MDReader application result.

\subsection{One order through the semantic objects}

SQLite records customer \code{c-17} with email
\code{alex@example.test}.  PostgreSQL records billing account
\code{acct-944} with the same normalized email and an open contract.  The JSON
API describes product \code{SKU-9}.  A Markdown decision says that billing
records may contribute to a revenue report but may not reveal the raw email.

A \CatDB-style account of the example would retain:

\begin{itemize}
  \item a mapping from the SQLite customer and order schema into the domain;
  \item a distinct mapping from PostgreSQL accounts and purchases;
  \item a conversion from integer minor units to the domain's money value,
  with currency and rounding assumptions;
  \item a candidate identity link between \code{c-17} and \code{acct-944},
  followed by an authority-bearing decision if they are confirmed to denote
  the same customer;
  \item provenance connecting the revenue row to source records, snapshots,
  mappings, the identity decision, and the policy revision; and
  \item a physical plan that either queries both live databases or reads a
  materialized integration result.
\end{itemize}

The shared email is evidence, not identity.  Record linkage and entity
resolution have long treated matching as an uncertain inference problem
\citep{FellegiSunter1969,BenjellounEtAl2009}.  A vector index could rank the
pair as a candidate.  It could not authorize the merge.

\subsection{A schema change}

Suppose the SQLite application splits \code{customer.name} into
\code{given\_name} and \code{family\_name}.  A migration artifact can say:

\begin{itemize}
  \item which immutable schema revisions it connects;
  \item whether the old-to-new transformation is total;
  \item whether reconstructing the old display name is ambiguous;
  \item which consumers require the old formatting;
  \item whether execution is eager, lazy, virtual, or hybrid;
  \item which materializations and identity features become stale; and
  \item which provenance record explains the choice.
\end{itemize}

The declaration does not split every name correctly.  It makes the unresolved
cases and selected policy visible before a physical rewrite or compatibility
view runs.

\subsection{Federation, materialization, and replay}

The analytical query can be realized in at least two ways.  A federated plan
pushes exact filters to SQLite and PostgreSQL, transfers selected rows, applies
local reconciliation, and joins them.  A materialized plan reads a maintained
domain view.  Both strategies depend on the same mapping and identity
revisions, but their freshness, availability, provenance, and resource costs
differ.

Now place the semantic catalog at two sites.  Adding an immutable proposal may
be replay-safe.  Activating the new mapping as the single current mapping is a
different operation.  Two sites cannot each publish a different active
mapping and then recover one value by set union.  The system must retain a
conflict or coordinate the transition.  The example therefore reaches the
same boundary as the distributed paper models: typed structure can expose the
conflict, but it cannot remove the network and authority problem.

\section{Q1: What is modeled together?}
\label{sec:q1}

\subsection{The answer}

\CatDB's candidate contribution is a shared version and obligation boundary
across schema structure, mappings, migrations, identity decisions, provenance,
queries, workspaces, and physical realizations.  Existing systems model many
of these pieces well.  The claim is about their joint treatment as referenced
objects, not first invention of any individual piece.

The relational model separates logical relations from physical access
paths \citep{Codd1970RelationalModel}.  Entity-relationship modeling supplies
a conceptual layer \citep{Chen1976EntityRelationship}.  RDF and OWL define
graph and ontology semantics \citep{W3CRDF11Concepts,W3COWL2Overview};
GQL standardizes a property-graph language \citep{ISOIEC39075_2024};
AsterixDB provides a typed semistructured model
\citep{AlsubaieeEtAl2014AsterixDB}.  None of those facts licenses the claim
that a finite category subsumes the others.

\subsection{Preservation rather than subsumption}

For each source model \(D_i\), a mapping into a shared domain must produce a
preservation report:
\[
\operatorname{Preserve}(D_i,m_i)
=(P_i,L_i,U_i),
\]
where \(P_i\) lists represented semantics, \(L_i\) lists declared loss or
approximation, and \(U_i\) lists unsupported or unknown semantics.  A property
graph may retain edge identity and multiplicity that the finite functional
profile cannot express.  RDF blank nodes and open-world entailment need their
own boundary.  A document may preserve order and mixed content.  A vector
index has approximate retrieval behavior rather than an identity theorem.

\begin{obligation}[No silent residual]
\label{obl:residual}
A mapping may be admitted as exact only if every source feature required by
the target request is represented or discharged by a named residual.  An
unrepresented required feature yields a conditional, partial, unsupported, or
unknown result.
\end{obligation}

This obligation is proposed.  The current finite kernel validates a much
smaller schema, path, mapping, instance, and pullback profile.  It does not
compute general multimodel preservation reports.

\subsection{Identity and provenance complete the account}

Mappings relate schemas and data interpretations.  They do not decide that two
records denote the same entity.  The internally accepted identity paper therefore
separates local references, evidence, method outputs, and authorized
reconciliation decisions \citep{CatDBP07}.  The accepted provenance paper
separates source identity, relational derivation, semantic artifact versions,
execution evidence, and authority decisions \citep{CatDBP13}.  Why- and
where-provenance, provenance semirings, and PROV interchange are established
foundations \citep{buneman2001whywhere,green2007semirings,lebo2013provo}.

Together, those objects let a result identify the source snapshot, mapping
revision, identity decision, policy, and plan behind a row.  The paper model is
accepted.  No current provenance runtime, completeness checker, exporter, or
overhead measurement establishes that behavior.

\section{Q2: How typed mappings change schema evolution}
\label{sec:q2}

\subsection{Description before execution}

A migration script lists commands.  A typed migration package can also record
the old and new schema identities, the mapping direction, the selected data
operator, coverage, loss, ambiguity, authority, dependencies, provenance, and
physical intent.  This is useful even when a conventional engine executes the
actual change.

The distinction is familiar in adjacent work.  Data exchange gives mappings,
solutions, and certain-answer semantics \citep{FaginEtAl2005DataExchange};
schema-mapping composition has language-dependent closure limits
\citep{FaginEtAl2005Composition}; model management treats mappings as values
\citep{BernsteinMelnik2007Model}.  \CatDB's internally accepted migration paper
packages those concerns into one immutable versioned artifact
\citep{CatDBP03}.  That package is a candidate operational synthesis, not a
new general migration theory.

\begin{definition}[Migration declaration]
\label{def:migration}
A migration declaration between schema revisions \(S_v\) and \(S_w\) is
\[
\mu_{v,w}=(m_{v,w},o,c,\ell,a,d,p),
\]
where \(m_{v,w}\) is a typed schema relation, \(o\) selects an admitted data
operator, \(c\) states coverage, \(\ell\) states loss and ambiguity, \(a\)
states authority, \(d\) lists dependent artifacts, and \(p\) records
provenance.  A physical mode is a separate value in
\[
\{\text{eager},\text{lazy},\text{virtual},\text{hybrid},
\text{mixed-version}\}.
\]
\end{definition}

Changing the physical mode must not silently change the declared meaning.
An eager rewrite and a virtual compatibility view can still differ in
snapshot, collation, null, multiplicity, and failure behavior.  They are
equivalent only after a normalized comparison under one frozen profile.

\subsection{Composition is partial}

For mappings \(m_1:S\to T\) and \(m_2:T\to U\), write
\[
m_2\odot m_1\downarrow
\]
when the endpoint revisions match, the selected mapping language is closed
under the composition, required equations are preserved in the admitted
equality fragment, and coverage, loss, authority, and provenance compose
without an unresolved contradiction.  Otherwise the composition returns a
typed partial, ambiguous, unsupported, or unknown outcome.

\begin{counterexample}[Type correctness is not business correctness]
A mapping sends a source \code{customer\_id} string to a target
\code{customer\_id} string.  The types align.  The source value is local to one
tenant while the target value is global.  A type checker accepts the scalar
assignment, but the mapping is semantically wrong unless tenant scope enters
the identity contract.
\end{counterexample}

\subsection{What current computation establishes}

The accepted Slice 4 release and terminal code review record validation of 33
closed fixtures.  Rust and an independently implemented Haskell process
compared 29 semantic cases, retained four structural-only cases, and reported
zero disagreements.  The semantic surface includes finite instance validation
and two finite pullback \(\Delta\) successes, several negative validation
cases, and exact unsupported outcomes for \(\Sigma\) and \(\Pi\) outside the
profile.

\status{\computational{} for the 29 admitted semantic cases at the accepted
Slice 4 cut.  General migration, physical execution, online cutover, rollback,
information-loss computation, and schema-diff execution are not established.}

The result is useful because it proves less than the slogan ``migration is
implemented.''  It shows exact agreement over one closed fixture surface.
The independent Slice 4 review records possible diagnostic-order divergences
on unfixtured inputs.  Agreement is not a theorem of program equivalence.

\section{Q3: What mappings replace, generate, or leave unchanged}
\label{sec:q3}

\subsection{A conditional factorization}

Let \(I\) be a finite set of sources, \(J\) a finite set of consumers, and
\(A\subseteq I\times J\) the connection relation that the workload actually
requires.  A direct design supplies a transformation \(T_{ij}\) for each
\((i,j)\in A\).  A mediated design supplies source mappings
\[
a_i:S_i\longrightarrow D
\]
and consumer mappings
\[
b_j:D\longrightarrow C_j.
\]
The pair \((i,j)\) factors exactly when the selected integration semantics
satisfy
\[
T_{ij}\equiv b_j\odot a_i.
\tag{2}
\]
An exception \(E_{ij}\) remains when the domain omits required pair-specific
meaning or the mapping language cannot express the transformation.

\begin{proposition}[Conditional base-mapping count]
\label{prop:nplusm}
If \(A=I\times J\), every required \(T_{ij}\) factors as in (2), the admitted
mapping language is closed under those compositions, and no pair-specific
exception is required, then the mediated description needs
\(|I|+|J|\) base mappings rather than \(|I||J|\) pair mappings.
\end{proposition}

\begin{proof}
Choose one \(a_i\) for each \(i\in I\) and one \(b_j\) for each \(j\in J\).
There are \(|I|+|J|\) such mappings.  By assumption, every required pair is
the admitted composition \(b_j\odot a_i\), so no additional pair mapping is
needed.
\end{proof}

The proposition is elementary accounting.  It does not show lower maintenance
time.  If \(A\) is sparse, \(|A|\) may already be smaller than
\(|I|+|J|\).  If the domain collapses a distinction, the factorization fails.
If an exception remains, it still has to be authored and repaired.

\subsection{The complete cost ledger}

A fair comparison includes more than mapping count.  One conservative
accounting is
\[
\begin{split}
C_{\mathrm{med}}={}&
\sum_{i\in I_A}C(a_i)
+\sum_{j\in J_A}C(b_j)
+C_D+C_R\\
&+\sum_{(i,j)\in A}C(E_{ij})+C_X,
\end{split}
\tag{3}
\]
where \(C_D\) is domain governance, \(C_R\) is identity and reconciliation
work, and \(C_X\) is physical and operational work.  The direct cost is
\[
C_{\mathrm{direct}}
=\sum_{(i,j)\in A}C(T_{ij})+C_X^{\mathrm{direct}}.
\tag{4}
\]
Only a controlled repair-surface study can compare (3) and (4) after source,
consumer, and domain changes.  No current experiment does so.

\subsection{Replace}

Mappings can replace duplicated semantic logic only inside a declared
fragment.  Examples include:

\begin{itemize}
  \item repeated renaming and typed path navigation that factors through one
  adequate domain;
  \item shared unit or value-domain conversions with one authority and
  explicit loss behavior;
  \item query rewrites whose source coverage and scalar semantics are known;
  \item repeated provenance attachment to a versioned semantic artifact; and
  \item validation rules that the admitted mapping language can express and
  check.
\end{itemize}

Mediators, federated databases, GAV/LAV integration, data exchange, Clio, and
ontology-based data access already establish much of this territory
\citep{ShethLarson1990Federated,Wiederhold1992Mediators,
Lenzerini2002DataIntegration,FaginEtAl2009Clio,CalvaneseEtAl2017Ontop}.
The \CatDB question is whether one versioned contract can reduce correct
repair work after its own governance and exception costs are counted.

\subsection{Generate}

A semantic mapping may generate a physical artifact without becoming that
artifact.  Possible outputs include SQL views, ETL or ELT transformations,
federated subqueries, validation queries, compatibility layers, cache keys,
materialization definitions, and provenance hooks.  Clio already demonstrated
mapping-driven generation of data-exchange transformations
\citep{FaginEtAl2009Clio}.  ARKTOS treated ETL modeling and execution as an
operational workflow \citep{VassiliadisEtAl2001Arktos}.  Generation itself is
not novel.

The mapping and its evidence remain the semantic authority when a generated
job is rebuilt.  The job is one physical realization.  Federation and
materialization can therefore change without silently redefining the
integration contract.

\subsection{Leave unchanged}

Many tasks remain physical or source specific:

\begin{itemize}
  \item extraction from proprietary APIs and unreliable files;
  \item cleaning text, addresses, units, and malformed values whose policy is
  not captured by the mapping language;
  \item bulk transfer, loading, scheduling, retries, checkpoints, and
  recovery;
  \item source-side triggers, external side effects, and operational cutover;
  \item human decisions about identity, policy, legal authority, and
  exceptions;
  \item pair-specific transformations that do not factor through the domain;
  \item schema changes with unavoidable information loss or downtime; and
  \item distributed coordination where operations do not commute.
\end{itemize}

\status{The mapping-count proposition is \paperreasoning{}.  Reduced
maintenance, fewer regressions, and lower integration cost remain
\openstatus{}.  ``CatDB replaces ETL'' is \rejected{}.}

\section{Q4: Can semantic compilation remain competitive?}
\label{sec:q4}

\subsection{The intended boundary}

The accepted physical-compilation paper places semantic work before native
row processing \citep{CatDBP02}.  A canonical request is validated and
rewritten into a logical plan.  Backend capabilities classify each operation
as exact, residual, approximate, or unsupported.  A physical lowerer then
emits a parameterized native realization.  The backend retains access-path
selection, join ordering, and row execution.

That boundary follows established optimizer architecture.  System R separated
access-path selection from query semantics \citep{SelingerEtAl1979AccessPath}.
Volcano provided extensible physical operators \citep{Graefe1994Volcano}.
Calcite supports query processing across heterogeneous sources
\citep{BegoliEtAl2018Calcite}.  Semantic compilation and heterogeneous
planning are not new by themselves.

\begin{definition}[Compilation certificate]
\label{def:certificate}
A compilation certificate for plan \(p\) at semantic commit \(K\) records:
\[
\chi(p,K)=
(\text{query},\text{mapping},\text{capabilities},\text{snapshot},
\text{residuals},\text{normalization},\text{provenance}).
\]
It is reusable only when every declared dependency remains compatible and the
selected backend operation retains the claimed exactness.
\end{definition}

The certificate would make approximations and residual work explicit.  It
does not make the cost estimate correct or the generated query fast.

\subsection{Federation}

The accepted federation paper specifies mapping-aware read profiles,
coverage, source authority, exact and repaired pushdown, join placement,
partial availability, reconciliation, and typed result quality
\citep{CatDBP05}.  A required source failure must not become an empty complete
answer.  The concrete customer-order example in that paper is hand worked.
There is no current source selector, planner, connector executor, result
envelope, or heterogeneous differential run.

This distinction constrains the synthesis.  A federation paper does not
establish a federation engine.  It also does not establish that semantic
metadata improves pushdown, network traffic, or plan quality.

\subsection{Materialization and incremental maintenance}

The internally accepted materialization paper treats a materialized state as a
realization of a versioned definition, not the semantic authority
\citep{CatDBP06}.  Classical materialized-view maintenance, differential
dataflow, and DBSP already provide mature delta techniques
\citep{GuptaMumick1995,McSherryEtAl2013,BudiuEtAl2023}.  \CatDB adds a proposed
invalidation question: does a schema, mapping, identity, provenance-policy, or
capability change preserve the old meaning?

For a materialization \(V\) at source frontier \(f\) and semantic revision
\(K\), the proposed correctness gate is
\[
N_K\!\left(V_{\mathrm{incremental}}(K,f)\right)
=N_K\!\left(V_{\mathrm{recompute}}(K,f)\right).
\tag{5}
\]
Equation (5) is not a result.  The repository has no P6 evaluator, source
change connector, recovery harness, or benchmark.

\subsection{Cost-based choice}

The accepted planning paper makes feasibility precede cost
\citep{CatDBP14}.  A plan that violates coverage, freshness, consistency,
provenance, policy, or approximation requirements is inadmissible even if its
predicted latency is low.  Among feasible plans, a versioned objective may
consider latency, network and storage traffic, local and remote work, memory,
source load, freshness, coordination, provenance overhead, approximation
quality, and failure behavior.

Traditional and adaptive optimization provide strong baselines
\citep{LeisEtAl2015,AvnurHellerstein2000,MarcusEtAl2021Bao}.  The current
repository has no P14 candidate enumerator, calibrator, connector statistics
contract, adaptive executor, or benchmark.  There is no evidence for global
optimality or scale.

\subsection{Answer and promotion gate}

Semantic compilation can be called competitive only if all of the following
are observed on preregistered workloads:

\begin{enumerate}
  \item normalized results and declared provenance match an independent
  oracle;
  \item generated plans preserve required source semantics or declare a
  residual;
  \item cold compilation and cached-plan overhead are measured separately;
  \item native plan shape, bytes, calls, source load, latency, throughput, and
  memory are retained;
  \item failures, timeouts, approximations, stale reads, and no-plan outcomes
  remain in the dataset; and
  \item physical-only, conventional federated, and materialization baselines
  are strong enough to falsify the treatment.
\end{enumerate}

\status{\obstructed{}.  No current query compiler, SQLite/PostgreSQL
connector suite, federation planner, materialization engine, optimizer, native
plan comparison, or scale benchmark establishes competitive execution.}

\section{Q5: Realistic consistency and convergence}
\label{sec:q5}

\subsection{One adjective is not enough}

A local transaction can be serializable while a remote materialization is
stale.  An immutable provenance assertion may merge by set union while an
active mapping reference requires one authorized value.  Replaying a pure
validation event may be harmless while replaying an external payment side
effect is not.  The accepted consistency paper therefore defines a profile per
operation rather than one platform-wide adjective \citep{CatDBP11}.

\begin{definition}[Operation consistency profile]
\label{def:consistency-profile}
For operation \(u\), a consistency profile is
\[
\kappa_u=(L,V,S,C,R,F,A,H),
\]
where \(L\) is local isolation, \(V\) replica visibility, \(S\) session
guarantees, \(C\) convergence, \(R\) replay behavior, \(F\) freshness,
\(A\) validation and authority, and \(H\) historical retention.
\end{definition}

Linearizability, CAP, CRDTs, monotone coordination analysis, and
invariant-confluence are established foundations
\citep{HerlihyWing1990Linearizability,GilbertLynch2002CAP,
ShapiroEtAl2011CRDT,AmelootEtAl2013Transducers,
BailisEtAl2014Coordination}.  They apply under their own models.  Categorical
typing does not bypass them.

\subsection{Operations that may converge without a single global order}

The distributed paper model identifies candidates for available convergence
under frozen admissibility rules \citep{CatDBP10}:

\begin{itemize}
  \item addition of immutable content-addressed schema or mapping proposals;
  \item monotone accumulation of evidence whose authority does not imply
  activation;
  \item idempotent delivery of a pure validation result bound to the same
  inputs;
  \item explicit multi-value retention of concurrent alternatives; and
  \item join-based metadata components with proved or tested merge laws.
\end{itemize}

Even these cases need causal dependencies, stable identities, duplicate
handling, and a frozen component contract.  ``Immutable'' does not guarantee
that a dependent artifact arrived first.

\subsection{Operations that require coordination or explicit conflict}

Single-valued activation is different from proposal creation.  The following
operations generally require coordination, escrow, serialized authority, or a
retained conflict state:

\begin{itemize}
  \item replacing the active schema or mapping for one workspace;
  \item confirming one canonical identity when competing decisions exist;
  \item publishing a branch head under noncommuting semantic changes;
  \item changing membership, authority, or retention policy;
  \item performing a migration cutover that cannot run twice safely;
  \item advancing a checkpoint past unobserved dependencies; and
  \item preserving uniqueness or other cross-object invariants.
\end{itemize}

\begin{counterexample}[Delivery is not semantic convergence]
Site A activates mapping \(m_1\).  During a partition, site B activates
mapping \(m_2\) for the same single-valued reference.  Both operations are
eventually delivered everywhere.  A set union converges to
\(\{m_1,m_2\}\), but the required state has one active mapping.  The replicas
have converged on an explicit conflict, not on a valid single-valued answer.
\end{counterexample}

\subsection{Answer}

The realistic guarantee is an operation-by-operation matrix.  Some immutable
and admitted monotone operations may remain available and converge.  Some
updates can preserve concurrent alternatives as first-class conflicts.
Noncommutative activation, authority, membership, retention, and migration
transitions need coordination or cannot promise one valid value.

\status{\acceptedmodel{} for the P10/P11 specifications.
\obstructed{} for runtime, convergence histories, recovery, availability, and
performance.  The repository has no distributed transport, replicated log,
consensus-backed reference store, fault harness, or distributed benchmark.}

\section{Cross-cutting semantics}
\label{sec:cross-cutting}

\subsection{Identity}

The internally accepted identity model uses at least four separate artifacts:
source-local references, observed evidence, versioned method output, and an
authority-bearing decision.  Only an effective confirmed-same decision may
enter a canonical equivalence projection.  Possible, probable, contradicted,
superseded, and retracted relationships remain visible.

This avoids a dangerous shortcut in the running example.  The shared email
between SQLite and PostgreSQL may be a strong feature.  It may also be a
reused family address, a recycled account, or a tenant-local identifier.
Similarity can propose the pair.  It cannot establish identity or write
authority.

\subsection{Provenance}

Provenance must compose across the semantic and physical layers.  A useful
answer record may need:

\[
\operatorname{Prov}(x)=
(\text{sources},\text{derivation},\text{semantic revisions},
\text{execution},\text{decisions},\text{completeness}).
\]

The completeness field matters.  Retention may have removed source evidence.
A connector may report only file-level origin.  A transformation may preserve
why-provenance but not exact value origin.  A result should report that limit
rather than present every provenance graph as complete.

\subsection{Versioned workspaces}

A semantic workspace is proposed as an isolated overlay over an immutable
semantic commit.  Diff has structural, operational, impact, validation, and
realization layers.  Merge is partial: it automatically combines only
operation pairs admitted by a reviewed commutativity or noninterference rule,
then validates the whole candidate state before publishing a branch
reference.  Dataset branching systems such as Decibel show established
relational versioning capabilities \citep{MaddoxEtAl2016Decibel}.  \CatDB's
candidate delta is cross-object versioning over semantic artifacts.

No current workspace crate, overlay evaluator, merge classifier, atomic
reference store, or workspace fixture establishes this behavior.

\subsection{Bidirectional updates}

A readable canonical view is not automatically a safe write surface.  Lenses
and relational lenses provide precise prior foundations for well-behaved
bidirectional transformations \citep{foster2007combinators}.  The accepted
bidirectional-mapping paper proposes a write profile that classifies a mapping
as fully writable, partially writable, read-only, or
reconciliation-dependent relative to a declared update language
\citep{CatDBP08}.

Universal safe writeback is rejected.  Loss, ambiguity, ownership, target
constraints, stale source versions, multi-source atomicity, and external side
effects can all force rejection or reconciliation.

\section{Dependency graph and manuscript status}
\label{sec:dependencies}

\subsection{Why the graph matters}

The accepted research manifest defines a 19-node acyclic blocking graph:
papers \partref{P1} through \partref{P18}, followed by this synthesis.  Its
exact projection has 70 edges, including one edge from every paper into the
synthesis.  The graph prevents an accepted model in one paper from quietly
supplying absent evidence to a dependent paper.

\begin{figure}[htbp]
\centering
\begin{tikzpicture}[
  node distance=5mm and 6mm,
  box/.style={draw=catblue,rounded corners,fill=catlight,
    align=center,font=\scriptsize,minimum height=7mm},
  blocked/.style={draw=catred,rounded corners,fill=red!4,
    align=center,font=\scriptsize,minimum height=7mm},
  arr/.style={-{Latex[length=2mm]},thin,draw=catgray}
]
\node[box] (p134) {P1/P3/P4\\semantic/mapping};
\node[box,right=of p134] (p1379)
  {P13/P7/P9\\provenance\\identity/workspace};
\node[box,right=of p1379] (p101214)
  {P10/P11/P12/P14\\distribution\\routing/planning};
\node[blocked,right=of p101214] (s) {S provisional\\synthesis};
\node[box,below=of p1379] (p15) {P15\\runtime};
\node[box,right=of p15] (p18) {P18\\MDReader contract};
\node[box,below=of p15] (p16) {P16\\semantics};
\node[box,right=of p16] (p17) {P17\\formal};

\draw[arr] (p134) -- (p1379);
\draw[arr] (p1379) -- (p101214);
\draw[arr] (p101214) -- (s);
\draw[arr] (p134) |- (p15);
\draw[arr] (p15) -- (p18);
\draw[arr] (p18) -| (s);
\draw[arr] (p134) |- (p16);
\draw[arr] (p16) -- (p17);
\draw[arr] (p17) -| (s);
\end{tikzpicture}
\caption{Three critical evidence chains, compressed from the exact 70-edge
manifest graph.  Blue boxes include internally accepted paper artifacts;
the red box is the unreviewed synthesis.}
\label{fig:dependencies}
\end{figure}

The longest blocking path is
\[
\partref{P1}\to\partref{P3}\to\partref{P4}\to\partref{P13}
\to\partref{P7}\to\partref{P9}\to\partref{P10}\to\partref{P11}
\to\partref{P12}\to\partref{P14}\to\partref{S}.
\]
The runtime and application path is
\[
\partref{P1}\to\partref{P3}\to\partref{P4}\to\partref{P13}
\to\partref{P15}\to\partref{P18}\to\partref{S},
\]
and the formal path is
\[
\partref{P1}\to\partref{P3}\to\partref{P4}\to\partref{P16}
\to\partref{P17}\to\partref{S}.
\]
All companion-paper dependencies on the three displayed paths are now
internally accepted.  The formal paper \partref{P17} is accepted, but its
machine-checked scope remains limited to the declarations reported below.
The accepted \partref{P15} paper still describes a bounded research kernel,
not a production runtime.  The synthesis itself has not entered independent
review and cannot be accepted.

\subsection{Paper-by-paper status}

\begin{landscape}
\small
\begin{longtable}{L{0.07\linewidth}L{0.22\linewidth}L{0.20\linewidth}L{0.42\linewidth}}
\caption{Current paper and implementation boundary.}
\label{tab:paper-status}\\
\toprule
Paper & Topic & Manuscript status & Strongest current evidence and exact limit \\
\midrule
\endfirsthead
\toprule
Paper & Topic & Manuscript status & Strongest current evidence and exact limit \\
\midrule
\endhead
\partref{P1} & Semantic model & Internally accepted &
Paper proofs, bounded kernel computation, and selected Lean declarations;
does not subsume all data models or prove a backend. \\
\partref{P2} & Physical compilation & Internally accepted &
Compilation contract only; no query compiler, connectors, native-plan
capture, or performance result. \\
\partref{P3} & Migration & Internally accepted &
Paper proofs plus Slice 4 finite \(\Delta\) prerequisite; no physical
migration, cutover, rollback, or general loss analysis. \\
\partref{P4} & Composable integration & Internally accepted &
Conditional mapping-count result; no factorization checker, connector,
identity resolver, or repair-surface experiment. \\
\partref{P5} & Federation & Internally accepted &
Federation contract only; no planner, executor, heterogeneous result
comparison, or benchmark. \\
\partref{P6} & Materialization & Internally accepted &
Delta and invalidation contract only; no evaluator, recovery harness,
freshness result, or benchmark. \\
\partref{P7} & Identity & Internally accepted &
Typed decision model only; no profile, matcher, state machine, fixtures, or
experiment. \\
\partref{P8} & Bidirectional mappings & Internally accepted &
Write-profile model only; no safe-write runtime, proof, or database
experiment. \\
\partref{P9} & Workspaces & Internally accepted &
Workspace and partial-merge model only; no overlay, merge, publication, or
historical-query runtime. \\
\partref{P10} & Distributed CatDB & Internally accepted &
Typed operation algebra and paper classification; no transport, replicated
log, resolver, fault history, or benchmark. \\
\partref{P11} & Consistency & Internally accepted &
Operation-level consistency model; no consistency-profile runtime,
consensus store, recovery, or convergence evidence. \\
\partref{P12} & Semantic sharding & Internally accepted &
Placement, routing, pruning, join, exchange, index, and materialization
contracts; no distributed planner or locality/performance result. \\
\partref{P13} & Provenance & Internally accepted &
Profile-relative provenance algebra; no runtime, completeness checker,
security result, exporter, theorem, or benchmark. \\
\partref{P14} & Cost planning & Internally accepted &
Feasibility and cost contract; no optimizer, calibration, adaptive executor,
global-optimality result, or scale benchmark. \\
\partref{P15} & Rust runtime & Internally accepted &
Six-crate finite semantic kernel and accepted Slice 4 computation; no query,
storage, connector, transaction, server, replay, or performance layer. \\
\partref{P16} & Haskell semantics & Internally accepted &
Its audited paper snapshot reports the accepted Slice 2 boundary; Slice 4 is
a separate accepted release, and current Slice 5 work is excluded.  No proof,
backend, distributed, or performance authority follows. \\
\partref{P17} & Lean formalization & Internally accepted &
Selected path and mapping declarations are machine checked; the accepted
paper does not verify instances, migration, queries, runtimes, backends, or
distributed behavior. \\
\partref{P18} & MDReader & Internally accepted &
The accepted paper supplies an application contract, but no application
artifact establishes projections, UI behavior, provenance,
SQLite/PostgreSQL synchronization, or user value. \\
\bottomrule
\end{longtable}
\end{landscape}

\section{Current runtime and formal evidence}
\label{sec:runtime-evidence}

\subsection{Slice 4 is the executable boundary}

The repository contains a real semantic kernel, but it is small.  The current
Rust workspace has six crates for closed values, schemas, paths, mappings,
finite instances, bounded migration, and fixture verification
\citep{CatDBP15}.  The Haskell package independently evaluates the same closed
profile \citep{CatDBP16}.  The accepted Slice 4 release record reports:

\begin{lstlisting}
fixture cases=33
validation ok=12 error=19 unsupported=2
slice-4 semantic-compared=29 structural-compared=4
slice-4 disagreements=0
\end{lstlisting}

The 29 semantic cases cover schema parsing, path typing and composition,
mapping identity and composition, finite-instance validation, two finite
pullback migrations, negative migration cases, and exact unsupported
\(\Sigma/\Pi\) outcomes.  Information-loss and schema-diff cases remain
structural only.

Slice 5 implementation work is present in the shared worktree, but it has no
release record or accepted independent review.  This synthesis excludes it
until release.  The accepted executable boundary therefore remains Slice 4,
including the structural-only status of information-loss and schema-diff
cases.

The accepted \partref{P16} and \partref{P18} manuscripts each record a
42-case author-audit snapshot in which a Slice 4 selection produced 29
semantic and 13 structural comparisons.  \partref{P16} separately labels all
42 as semantic only under its unreviewed Slice 5 candidate.  Those counts are
snapshot-relative observations, not accepted Slice 5 evidence.  The live
Slice 5 worktree has continued to change, so this synthesis reports no live
Slice 5 count.

\begin{obligation}[Fixture boundary]
\label{obl:fixture}
A statement derived from Slice 4 must name the capability set, corpus size,
semantic count, structural count, disagreement count, repository revision,
and known unfixtured divergences.  It must not be generalized to a runtime,
compiler, backend, distributed system, or theorem.
\end{obligation}

\subsection{What Lean establishes}

The accepted Lean Slice 3 checks exact path and mapping declarations in the
\code{PATH-02} through \code{PATH-04} and \code{MAP-03} through
\code{MAP-05} boundary \citep{CatDBP17}.  Machine-checked database
semantics and query rewrite
proofs already have strong prior art, including HoTTSQL
\citep{ChuEtAl2017HoTTSQL}.  The current Lean result neither verifies Rust nor
proves query, connector, migration-runtime, cost, distributed, or MDReader
claims.

\subsection{What does not exist}

The following artifacts are absent from the current evidence cut:

\begin{itemize}
  \item a query IR implementation, compiler, physical planner, or plan cache;
  \item SQLite, PostgreSQL, JSON, Markdown, warehouse, vector, or full-text
  connector execution;
  \item a federation engine, distributed join executor, exchange layer, or
  semantic pruning oracle;
  \item a materialization or incremental-maintenance engine;
  \item identity, reconciliation, provenance, workspace, or policy runtimes;
  \item a replicated operation log, causal transport, consensus-backed
  reference store, or fault harness;
  \item a calibrated optimizer or adaptive execution loop;
  \item an MDReader application;
  \item a complete benchmark, cross-shard measurement, scale result, or
  production readiness assessment.
\end{itemize}

The presence of empty or scaffolded directories would not establish these
capabilities.  This synthesis uses observed behavior only where a current
command and closed artifact support it.

\section{Evaluation contract and falsifiers}
\label{sec:evaluation}

\subsection{No results are reported here}

The evaluation program below is a promotion contract.  It is not a benchmark
section disguised in future tense.  No numerical performance, repair,
federation, materialization, provenance, distributed, or MDReader result is
reported.

\begin{table}[htbp]
\centering
\small
\caption{Required evaluation groups and present status.}
\label{tab:evaluation}
\begin{tabularx}{\textwidth}{L{0.22\textwidth}Y L{0.18\textwidth}}
\toprule
Group & Minimum comparison & Status \\
\midrule
Semantic compilation & Native query versus compiled query with normalized
bags, scalar semantics, provenance, plan capture, and cold/cache separation &
\obstructed \\
Federation & Native per-source oracle, R*-style or Calcite baseline, bytes,
calls, partial availability, and exactness labels & \obstructed \\
Materialization & Full recomputation versus incremental treatment across data
and semantic changes, with crash and cursor faults & \obstructed \\
Integration repair & Pairwise, mediated, GAV, LAV, and generated-plan
conditions after source, consumer, and domain changes & \obstructed \\
Provenance & Derivation correctness, completeness class, query cost, storage
cost, privacy, and retention failure & \obstructed \\
Distribution & Partition, reorder, duplicate, replay, healing, checkpoint,
authority, and invariant histories & \obstructed \\
Routing and planning & Physical-only and communication-aware baselines,
semantic ablations, prediction error, cross-shard bytes, and failure behavior &
\obstructed \\
MDReader & End-to-end typed projections, violations, provenance, history,
responsive UI, and task outcomes & \obstructed \\
\bottomrule
\end{tabularx}
\end{table}

\subsection{Falsifiers}

The synthesis thesis must be rejected or narrowed if any of the following is
observed:

\begin{enumerate}
  \item a required source or consumer meaning cannot be represented without
  hidden pair-specific code that the mapping contract reports as exact;
  \item a supposedly exact composition has a counterexample under the admitted
  equality, coverage, loss, or authority profile;
  \item a virtual and materialized realization under the same declared
  snapshot and scalar profile return different normalized results;
  \item the mediated treatment does not reduce correct-repair work after
  domain governance, reconciliation, exceptions, failures, and operations are
  counted;
  \item compilation overhead or generated-plan quality is unacceptable
  against strong native and conventional-planner baselines;
  \item a required unavailable source is reported as an empty complete
  federated answer;
  \item incremental state differs from full recomputation at the same semantic
  revision and source frontier;
  \item provenance omits a declared contributing source, mapping, identity
  decision, or execution revision while claiming completeness;
  \item a replay, reorder, duplicate, or partition history violates the
  guarantee named by its operation profile;
  \item semantic routing prunes a shard containing a qualifying occurrence,
  changes bag multiplicity, or bypasses policy;
  \item current Rust and Haskell programs disagree on an admitted fixture or
  replay an expected value instead of computing it;
  \item a claimed Lean theorem contains an unreported axiom, assumption, or
  scope mismatch;
  \item the MDReader application cannot expose the mapping, provenance,
  violation, or history that motivates it; or
  \item measured semantic-metadata maintenance cost exceeds its benefit on the
  intended workload.
\end{enumerate}

\subsection{Staged adoption}

A conservative adoption path starts with artifacts that can be inspected
without replacing an existing database:

\begin{enumerate}
  \item validate and version finite schemas, paths, and mappings;
  \item compare generated validation or read plans with existing hand-written
  behavior;
  \item attach mapping and source-version provenance to selected reports;
  \item add one read-only federated or materialized path behind a differential
  oracle;
  \item measure repair work after controlled source and consumer changes;
  \item add writeback only for a declared update language with authority and
  transaction checks; and
  \item attempt distributed replication only after operation profiles and
  fault histories close.
\end{enumerate}

This order permits \CatDB to fail cheaply.  A team can reject the semantic
layer if it cannot represent its integration decisions or if the maintenance
cost is not justified.

\section{Related work and candidate novelty}
\label{sec:related}

\subsection{Established foundations}

The synthesis sits at the intersection of mature areas.  Categories, functors,
data migration, algebraic databases, and categorical integration are
established \citep{Spivak2012Functorial,SpivakWisnesky2015Relational,
SchultzWisnesky2017AlgebraicIntegration,
SchultzEtAl2017AlgebraicDatabases}.  Model management, schema mapping, data
exchange, mediation, federation, and ontology-based access already treat
integration knowledge as explicit structure
\citep{BernsteinMelnik2007Model,FaginEtAl2005DataExchange,
FaginEtAl2005Composition,ShethLarson1990Federated,
Wiederhold1992Mediators,Lenzerini2002DataIntegration,
CalvaneseEtAl2017Ontop}.  Lenses address bidirectional updates
\citep{foster2007combinators}.  Materialized-view maintenance and differential
systems address incremental computation
\citep{GuptaMumick1995,McSherryEtAl2013,BudiuEtAl2023}.  Distributed
consistency and convergence have their own formal limits
\citep{GilbertLynch2002CAP,ShapiroEtAl2011CRDT,
BailisEtAl2014Coordination}.

The paper-local related-work and primary-source ledgers give the exact
source-to-claim map.  No companion manuscript or external source is used as
evidence that the unimplemented \CatDB components work.

\subsection{Narrow candidate delta}

The research claim is a systems synthesis:

\begin{quote}
One versioned artifact graph could connect typed schema mappings, migration
intent, identity authority, provenance, workspace history, and physical
realizations, while independent computation and selected theorem checking
make each promotion boundary visible.
\end{quote}

That combination may be useful.  It is not yet a demonstrated systems result.
Novelty would require both a completed artifact and direct comparison with
categorical integration, model management, mediated data integration,
ontology-based access, conventional planners, provenance systems, dataset
versioning, and distributed databases.  A vocabulary that simply places
known ideas beside each other is not enough.

\section{Limitations and open questions}
\label{sec:limitations}

\subsection{Limitations}

\begin{enumerate}
  \item The current semantic profile is finite, total, and narrow.  It omits
  nulls, optional attributes, partial functions, general constraints, richer
  typesides, bags in the kernel, and general path equality.
  \item Multimodel preservation is proposed, not implemented.  Native
  relational, graph, RDF/OWL, document, vector, and full-text semantics may
  require residual engines.
  \item Typed mappings do not establish intended business meaning.  Human
  governance and source authority remain necessary.
  \item Composition can be partial, ambiguous, lossy, unsupported, or unknown.
  \item The conditional \(|I|+|J|\) mapping count does not imply lower repair
  time, fewer incidents, or lower total cost.
  \item Generated plans can be semantically wrong or physically slow.
  \item Federation inherits source capability, availability, privacy,
  snapshot, and network limits.
  \item Materializations become stale and require dependency, checkpoint, and
  recovery semantics.
  \item Identity decisions remain uncertain and may require reversal.
  \item Provenance can be incomplete, expensive, sensitive, or removed by
  retention.
  \item Workspace merge is partial and cannot automatically resolve every
  semantic conflict.
  \item CAP, PACELC, consensus, and noncommutativity remain physical limits.
  \item Slice 4 fixtures are a bounded acceptance surface, not proof,
  performance evidence, or production readiness.
  \item Selected Lean declarations do not verify the runtime.
  \item MDReader is an accepted reference-application contract, not product
  evidence.
\end{enumerate}

\subsection{Open questions}

\begin{enumerate}
  \item Which mapping language is expressive enough for real integration
  while retaining decidable and explainable validation?
  \item Can loss, ambiguity, and coverage analyses remain conservative without
  returning unknown too often?
  \item What semantic domain granularity avoids both pairwise duplication and
  an ungovernable enterprise-wide model?
  \item Which provenance granularity is sufficient for debugging, compliance,
  and replay at acceptable cost?
  \item Can compiled plans preserve native optimizer quality while the
  semantic layer stays outside row execution?
  \item Which schema and mapping changes admit safe incremental adaptation
  rather than rebuild?
  \item How should uncertain identity affect query completeness,
  materialization, and writeback?
  \item Which operation components are monotone or invariant-confluent under a
  frozen semantic profile?
  \item Can semantic partition metadata improve routing after its collection,
  validation, and maintenance cost is counted?
  \item Does MDReader provide a sufficiently demanding vertical slice, or does
  it hide the hardest transactional and scale requirements?
\end{enumerate}

\section{Conclusion}
\label{sec:conclusion}

\CatDB is best understood as a proposal about where integration meaning lives.
Instead of treating a schema mapping, migration choice, identity decision, and
provenance rule as unrelated configuration around a pipeline, the proposal
gives each one a typed identity, version, interpretation, and evidence
boundary.  Federation, ETL, and materialization then become physical
realizations of that contract.

The current evidence supports only part of this picture.  Internally accepted
papers provide careful models for the semantic core, compilation, migration,
composable integration, federation, materialization, identity, bidirectional
updates, workspaces, distribution, consistency, provenance, planning, and
formalization, together with sharding, the bounded Rust kernel, Haskell
semantics, and the MDReader application contract.  The accepted Slice 4 record
shows exact Rust/Haskell agreement on 29 semantic cases inside a closed
33-fixture profile, with four structural-only cases.  Selected Lean
declarations check named path and mapping laws.

No current evidence establishes a distributed runtime, query compiler,
connector suite, federation engine, materialization engine, optimizer,
MDReader application, or benchmark.  The synthesis therefore cannot claim
that \CatDB replaces ETL, removes migration cost, preserves native
performance, enables universal writeback, or escapes distributed-systems
tradeoffs.

The narrower thesis survives: typed, composable, versioned mappings may move
some integration meaning out of bespoke pipelines and into inspectable
objects.  Whether that shift improves repair work while preserving competitive
execution remains the central experiment.

\appendix

\section{Synthesis claim ledger}
\label{app:claims}

\begin{landscape}
\scriptsize
\begin{longtable}{L{0.075\linewidth}L{0.36\linewidth}L{0.17\linewidth}L{0.30\linewidth}}
\caption{Claim anchors and promotion gates.}
\label{tab:claims}\\
\toprule
ID & Claim & Current status & Required promotion evidence \\
\midrule
\endfirsthead
\toprule
ID & Claim & Current status & Required promotion evidence \\
\midrule
\endhead
\code{S-C01} & \CatDB is defined as a semantic multimodel platform whose
schemas, mappings, migrations, identities, and provenance are first-class,
versioned, executable objects. & \paperreasoning{} definition & Accepted
cross-object IR and validators \\
\code{S-C02} & The finite semantic kernel represents and validates the exact
Slice 4 profile. & \computational{} & Current commands, closed manifest, and
reviewed source boundary; unreleased Slice 5 work is excluded \\
\code{S-C03} & Rust and independent Haskell implementations agree on 29
semantic cases in the accepted 33-fixture Slice 4 corpus. & \computational{} &
Recorded revision, exact reports, and zero disagreements \\
\code{S-C04} & Typed migration artifacts can make direction, coverage, loss,
ambiguity, authority, dependencies, and execution intent reviewable. &
Engineering hypothesis; \openstatus{} & Implemented artifact, negative
fixtures, and user/reviewer study \\
\code{S-C05} & Under complete factorization assumptions, a full
\(|I|\times|J|\) topology can use \(|I|+|J|\) base mappings. &
\paperreasoning{} conditional count & Assumptions retained; no maintenance
promotion inferred \\
\code{S-C06} & Mediated mappings reduce total correct-repair work. &
Engineering hypothesis; \obstructed{} & Preregistered repair-surface
experiment with full cost ledger \\
\code{S-C07} & Federation and materialization can realize one mapping contract
without changing declared meaning. & Engineering hypothesis; \obstructed{} &
Two implementations and normalized equivalence under one profile \\
\code{S-C08} & Semantic compilation preserves competitive native execution. &
Engineering hypothesis; \obstructed{} & Compiler, connectors, native plans,
correctness oracle, and benchmark \\
\code{S-C09} & Semantic metadata improves federation, pruning, routing, or plan
selection. & Engineering hypothesis; \obstructed{} & Physical-only baselines,
ablations, overhead, and cross-shard measurements \\
\code{S-C10} & Incremental maintenance preserves full recomputation across
data and semantic changes. & Engineering hypothesis; \obstructed{} & P6
evaluator, fault harness, independent oracle, and recovery evidence \\
\code{S-C11} & Identity evidence can be preserved without silently collapsing
uncertainty. & Engineering hypothesis; \obstructed{} & Identity profile,
state machine, fixtures, reversal, and authority tests \\
\code{S-C12} & Provenance can compose source, derivation, semantic-version,
execution, and decision evidence with an explicit completeness class. &
\acceptedmodel{}; runtime \obstructed{} & Runtime, completeness tests,
retention/privacy gates, and overhead \\
\code{S-C13} & Some immutable or monotone operations may converge without a
single global order, while noncommutative activation requires conflict or
coordination. & \acceptedmodel{} & Executable histories and invariant-specific
proof or computation \\
\code{S-C14} & A versioned workspace can support safe semantic diff and partial
merge across related artifacts. & \acceptedmodel{}; runtime \obstructed{} &
Workspace state machine, overlay oracle, merge fixtures, and atomic publish \\
\code{S-C15} & MDReader demonstrates end-to-end \CatDB value. & \rejected{} at
current cut & Implemented application, scenarios, UI checks, and user evidence \\
\code{S-C16} & \CatDB eliminates ETL, migration cost, CAP tradeoffs, or the need
for human authority. & \rejected{} & No positive promotion path; claim
contradicts scope \\
\code{S-C17} & The overall systems thesis is established. & \obstructed{} &
Accepted P1--P18, current implementation evidence, independent review, and
preregistered experiments \\
\bottomrule
\end{longtable}
\end{landscape}

\section{Exact disputed statements}
\label{app:disputes}

\begin{longtable}{L{0.30\textwidth}L{0.62\textwidth}}
\caption{Statements rejected by the synthesis.}
\label{tab:disputes}\\
\toprule
Rejected statement & Required correction \\
\midrule
\endfirsthead
\toprule
Rejected statement & Required correction \\
\midrule
\endhead
CatDB replaces ETL. & Some reusable semantic logic may move into mappings;
physical ETL/ELT, cleaning, transport, loading, scheduling, and operations
remain. \\
Integration drops from \(NM\) to \(N+M\). & The count is conditional on a full
topology, exact factorization, closure, domain adequacy, and no residual pair
exceptions. \\
Fewer mappings mean less maintenance. & Mapping count is not correct-repair
time; include governance, reconciliation, exceptions, failures, and
operations. \\
Typed mappings solve schema matching. & Matching proposes correspondences;
typed acceptance still needs validation and authority. \\
Vector similarity proves identity. & Similarity may rank candidates; an
authority-bearing decision establishes a canonical relation. \\
A type-correct mapping is business-correct. & Business meaning, policy,
coverage, freshness, and authority require separate evidence. \\
Virtual and materialized results are automatically equivalent. & Compare them
under the same frozen snapshot, scalar, bag, identity, and provenance profile. \\
Semantic compilation preserves native performance. & No compiler, connector,
native-plan comparison, or benchmark currently exists. \\
The accepted federation paper proves federation works. & It establishes a
reviewed contract, not a planner, executor, or experiment. \\
The accepted distributed papers prove convergence. & They classify operations
on paper; no distributed runtime or fault history exists. \\
Category theory removes CAP or consensus. & Typing can expose obligations; it
cannot deliver messages or make noncommutative updates commute. \\
Writeback is safe whenever a read mapping exists. & Writeback needs a declared
update language, authority, constraints, snapshot checks, and transaction
policy. \\
Rust/Haskell agreement proves correctness. & It establishes exact agreement on
the admitted fixtures, subject to common-mode and coverage limits. \\
Lean verifies the runtime. & Lean checks exact named declarations under
audited assumptions, not Rust, backends, networks, or the complete engine. \\
MDReader validates the platform. & An accepted paper supplies a reference
application contract, but no MDReader application artifact exists. \\
Unreleased Slice 5 work extends the accepted kernel. & Slice 5 has no release
record or accepted independent review.  The synthesis retains Slice 4 as its
executable boundary. \\
\bottomrule
\end{longtable}

\section{Review and reproduction gate}
\label{app:gate}

A future acceptance candidate must satisfy all of the following:

\begin{enumerate}
  \item every companion paper \partref{P1} through \partref{P18} is accepted
  at a current source and evidence revision;
  \item every synthesis claim links to a paper result, primary source, exact
  computation, theorem, experiment, or explicit obstruction;
  \item the Slice 4 counts and known unfixtured limits remain current;
  \item any Slice 5 claim is excluded unless a release record and accepted
  independent review establish its exact boundary;
  \item any Lean statement names its exact declaration and assumptions;
  \item compilation, federation, materialization, distribution, planning, and
  MDReader claims use real current artifacts rather than planned interfaces;
  \item all external claims close against the paper-local primary-source and
  related-work ledgers;
  \item the disputed-claim ledger has no unresolved trigger;
  \item Humanizer touches prose only and does not alter definitions,
  equations, evidence labels, tables, citations, or falsifiers;
  \item a clean isolated build closes references and citations with no
  warnings or overfull content;
  \item every rendered page is inspected;
  \item a separately authorized independent paper review reaches a
  publishable verdict; and
  \item any later source or relied-on evidence change reopens the candidate.
\end{enumerate}

This authoring pass does not invoke the independent review gate and does not
create an accepted PDF or cover.

\bibliographystyle{plainnat}
\bibliography{references}

\end{document}
