\documentclass[12pt]{article}

\usepackage[T1]{fontenc}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{tikz}
\usepackage{tikz-cd}
\usetikzlibrary{positioning}
\usepackage[margin=1in]{geometry}
\usepackage{xcolor}
\usepackage{graphicx}
\usepackage{hyperref}
\usepackage[capitalise,noabbrev]{cleveref}
\usepackage[numbers,sort&compress]{natbib}
\usepackage{booktabs}
\usepackage{longtable}
\usepackage{tabularx}
\usepackage{array}
\usepackage{ragged2e}
\usepackage{enumitem}
\usepackage{microtype}
\usepackage{listings}
\usepackage{pdflscape}
\usepackage{url}
\usepackage{float}

\hypersetup{
  colorlinks=true,
  hypertexnames=false,
  linkcolor=blue!45!black,
  citecolor=green!35!black,
  urlcolor=blue!55!black,
  pdftitle={Versioned Semantic Workspaces: Branching, Diffing, and Merging Schemas with Data},
  pdfauthor={Matthew Long; The YonedaAI Collaboration}
}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{requirement}[theorem]{Requirement}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{conjecture}[theorem]{Open conjecture}

\newcommand{\CatDB}{\textsc{CatDB}}
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\ev}[1]{\textsc{#1}}
\newcommand{\prior}{\ev{SUPPORTED BY PRIOR LITERATURE}}
\newcommand{\enghyp}{\ev{ENGINEERING HYPOTHESIS}}
\newcommand{\openstatus}{\ev{OPEN}}
\newcommand{\obstructed}{\ev{OBSTRUCTED}}
\newcommand{\openconj}{\ev{OPEN CONJECTURE}}
\newcommand{\speculative}{\ev{SPECULATIVE}}
\newcommand{\proposed}{\ev{PROPOSED}}
\newcommand{\status}[1]{\par\noindent{\normalfont\textit{Evidence status.} #1}\par}
\newcommand{\State}{\mathsf{State}}
\newcommand{\Commit}{\mathsf{Commit}}
\newcommand{\Artifact}{\mathsf{Artifact}}
\newcommand{\Workspace}{\mathsf{Workspace}}
\newcommand{\Operation}{\mathsf{Operation}}
\newcommand{\Diff}{\mathsf{Diff}}
\newcommand{\Merge}{\mathsf{Merge}}
\newcommand{\Validate}{\mathsf{Validate}}
\newcommand{\Apply}{\mathsf{Apply}}
\newcommand{\Normalize}{\mathsf{Normalize}}
\newcommand{\Impact}{\mathsf{Impact}}
\newcommand{\Query}{\mathsf{Query}}
\newcommand{\Provenance}{\mathsf{Provenance}}
\newcommand{\Materialization}{\mathsf{Materialization}}
\newcommand{\Identity}{\mathsf{Identity}}
\newcommand{\Digest}{\mathsf{Digest}}
\newcommand{\Profile}{\mathsf{Profile}}
\newcommand{\Outcome}{\mathsf{Outcome}}
\newcolumntype{L}[1]{>{\RaggedRight\arraybackslash}p{#1}}
\newcolumntype{Y}{>{\RaggedRight\arraybackslash}X}

\setlength{\emergencystretch}{4em}
\setlist{itemsep=0.25em,topsep=0.4em}
\allowdisplaybreaks
\lstset{
  basicstyle=\ttfamily\footnotesize,
  breaklines=true,
  breakatwhitespace=false,
  columns=fullflexible,
  frame=single,
  rulecolor=\color{black!20},
  showstringspaces=false
}

\definecolor{grokgray}{RGB}{110,110,110}
\AddToHook{shipout/background}{%
  \ifnum\value{page}=1
    \begin{tikzpicture}[remember picture,overlay]
      \node[
        rotate=90,
        anchor=south,
        font=\Large\sffamily\bfseries\color{grokgray},
        inner sep=0pt
      ] at ([xshift=38pt,yshift=0.52\paperheight]current page.south west)
      {GrokRxiv:2026.07.catdb-versioned-workspaces\quad
       [\,cs.DB\,]\quad
       23 Jul 2026};
    \end{tikzpicture}
  \fi
}

\title{Versioned Semantic Workspaces:\\
Branching, Diffing, and Merging Schemas with Data}
\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{abstract}
Database branches are easy to describe until a branch changes what the data
means.  Two analysts can begin with the same customer records, then choose
different schema revisions, mapping paths, identity decisions, provenance
requirements, and materialized views.  A line-oriented merge reports which
files changed.  It cannot decide whether an address split preserves a mapping,
whether an identity decision invalidates an aggregate, or whether an old query
can still be reproduced after source evidence expires.

This paper specifies versioned semantic workspaces for \CatDB{}.  A workspace
is an isolated overlay over an immutable semantic commit.  The commit jointly
references compatible revisions of schemas, mappings, migrations, data
observations, identity decisions, provenance profiles, policies, queries, and
materialization definitions.  Diff has five layers: structural, operational,
impact, validation, and realization.  Three-way merge is partial.  It
automatically combines only operation pairs admitted by a reviewed
noninterference or commutativity rule, then validates the complete candidate
state before atomically publishing a branch reference.  Every other case
becomes a typed conflict, a reconciliation request, a rejection, or an
unsupported result.

The proposal is an \enghyp{}, not an implemented result.  Dataset branching,
relational difference and merge, schema histories, mapping adaptation,
coexisting schema versions, temporal query, persistent data structures,
provenance, dynamic data citation, and materialized-view adaptation are
established prior work.  The current repository has no workspace crate,
semantic commit profile, overlay evaluator, merge classifier, atomic reference
store, workspace fixtures, Haskell oracle, Lean workspace theorem, or
workspace benchmark.  Claims about overlay equivalence, isolation, atomic
publication, historical reproduction, and safe coexistence therefore remain
\openstatus{} or \obstructed{}.  The paper's contribution is a falsifiable
contract, a conflict taxonomy, a formalization boundary, and an evaluation
plan for testing whether cross-object versioning adds practical value beyond
relational dataset version control.
\end{abstract}

\tableofcontents

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

\subsection{One source snapshot, two interpretations}

Consider a company that integrates customer records from an ERP system and a
CRM database.  At commit \(C_0\), the canonical customer schema stores an
address as a string, the revenue mapping reads gross revenue, and two source
records remain separate because their identity evidence is inconclusive.  A
materialized report uses row-level provenance from both source snapshots.

Team A creates a workspace from \(C_0\).  It splits the address into an
\code{Address} object, rewrites the ERP mapping to follow the new path, and
approves the two source records as one canonical customer.  Team B starts from
the same commit.  It keeps the old address shape, changes the revenue mapping
from gross to net, rejects the identity match, and requires field-level
provenance for the report.

Both workspaces can be internally useful.  Team A wants to measure the effect
of deduplication; Team B wants a conservative financial view.  Trouble begins
when someone asks to merge them.  The address edit and revenue edit touch
different files, but that fact says little.  The address split changes a typed
mapping path.  The identity decisions contradict each other.  The stricter
provenance policy may make the old materialization inadmissible.  The two
revenue definitions may produce different totals even when the source rows
are unchanged.

A source-control tool can preserve both text histories.  A database
versioning system can preserve and compare record versions.  Neither fact
supplies the missing semantic decisions.  The merge needs stable identities
for schema and mapping elements, explicit dependencies, branch-local
constraints, authority for reconciliation, provenance completeness, and a
publication protocol that cannot expose half of a merged state.

\subsection{Research question}

The paper asks:

\begin{quote}
What is a semantic branch, diff, and merge when schemas, mappings, data,
provenance, materializations, and reconciliation decisions evolve together?
\end{quote}

The proposed answer is deliberately conservative.  A branch is a mutable
reference to an immutable semantic commit plus, while work is in progress, an
isolated typed overlay.  A diff reports semantic operations and dependency
effects rather than serialized changes alone.  A merge is a partial procedure
with closed outcomes.  It may return a validated commit, typed conflicts,
reconciliation requirements, or an unsupported result.  Unknown does not mean
safe.

\subsection{Scope and claimed contribution}

The database-versioning literature already provides nonlinear dataset
branches, working copies, version-aware queries, relational difference and
three-way merge, and multiple physical layouts
\cite{MaddoxEtAl2016Decibel,HuangEtAl2017OrpheusDB,
BhardwajEtAl2014DataHub,BhattacherjeeEtAl2015DatasetVersioning}.
Schema-evolution systems record schema-modification operators, derive
mappings, support legacy access, and rewrite queries or updates across schema
versions \cite{MoonEtAl2008PRIMA,CurinoEtAl2008PRISM,
CurinoEtAl2010PRISMPlus,CurinoEtAl2013Automation}.  Mapping adaptation and
model-management operators also precede \CatDB{}
\cite{VelegrakisEtAl2003MappingAdaptation,
VelegrakisEtAl2004MappingConsistency,YuPopa2005SemanticAdaptation,
BernsteinMelnik2007Model,SchultzEtAl2017ModelManagement}.

The candidate \CatDB{} contribution is one executable compatibility boundary
across artifacts that these systems often treat separately:

\begin{enumerate}
  \item distinguish logical identity, immutable revision identity, content
  digest, physical location, and mutable branch reference;
  \item bind every query and merge to one semantic commit or explicit overlay;
  \item co-version schema, mapping, migration, data observation, identity,
  provenance, authority, query, and materialization definitions;
  \item compute typed structural, operational, impact, validation, and
  realization diffs;
  \item restrict automatic merge to reviewed operation pairs and validate the
  whole candidate after local pair processing;
  \item publish a merge atomically through a compare-and-swap reference; and
  \item distinguish state reconstruction, query replay, and exact result
  reproduction.
\end{enumerate}

Every item in this list is an \enghyp{}.  The paper gives no CatDB performance
number and no successful workspace execution.  Its strongest present result
is a prior-art boundary: the constituent ideas are established, while the
cross-object contract remains to be built and tested.

\subsection{Contributions of this manuscript}

This provisional manuscript contributes:

\begin{itemize}
  \item a finite semantic model for commit bundles, workspace overlays,
  operations, dependencies, typed diffs, and merge outcomes;
  \item a taxonomy of direct and cross-object conflicts, with exact
  unsupported and reconciliation boundaries;
  \item contracts for branch-local constraints, provenance,
  materialization state, rollback, and historical query contexts;
  \item thirteen falsifiable claim anchors linked to fixtures,
  implementation stages, formal obligations, and experiments;
  \item a fair comparison plan with Decibel and ORPHEUSDB on mutually
  supported relational operations; and
  \item explicit limitations, nonclaims, open questions, and current
  repository status.
\end{itemize}

\subsection{Paper organization}

\Cref{sec:evidence} records evidence labels and the repository audit.
\Cref{sec:prior} establishes the prior-art boundary.  \Cref{sec:framework}
defines identities, artifacts, commits, workspaces, and operations.
\Cref{sec:diff} defines semantic diff and impact.  \Cref{sec:merge} gives the
three-way merge procedure and conflict taxonomy.
\Cref{sec:coversioning,sec:history} treat co-versioning, provenance,
materializations, historical queries, and rollback.
\Cref{sec:formal} states candidate laws without presenting them as proved.
\Cref{sec:implementation,sec:evaluation} give the implementation and
falsification programs.  \Cref{sec:related} returns to related work, followed
by limitations, open questions, and a status-preserving conclusion.

\section{Evidence vocabulary and present status}
\label{sec:evidence}

\subsection{Evidence labels}

\Cref{tab:evidence-labels} applies to every result-like sentence in this
paper.  A label belongs to one claim under stated assumptions.  It does not
transfer from one layer to another.

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.25\textwidth}Y}
\toprule
Label & Meaning in this paper \\
\midrule
\prior{} &
A primary paper, standard, or official system artifact establishes the
stated result within its assumptions. \\
\enghyp{} &
A proposed CatDB behavior requires implementation and experiment. \\
\openconj{} &
A mathematical statement has no accepted proof for the frozen formal
fragment. \\
\openstatus{} &
Definitions, code, fixtures, experiments, or review are incomplete. \\
\obstructed{} &
A prerequisite semantic boundary is missing, so the claim cannot yet be
implemented or tested honestly. \\
\speculative{} &
The claim is too underspecified for a stronger label. \\
\bottomrule
\end{tabularx}
\caption{Evidence labels used throughout the manuscript.  No P9 claim is
currently labelled proved, machine-checked, computational, or experimentally
supported.}
\label{tab:evidence-labels}
\end{table}

An accepted path-composition theorem does not establish workspace isolation.
A relational merge result does not establish a CatDB cross-object merge.  A
content digest does not prove semantic equivalence.  A successful historical
query would not, by itself, establish scientific reproducibility.

\subsection{Current repository audit}

The current Rust workspace contains \code{catdb-core}, \code{catdb-ir},
\code{catdb-schema}, \code{catdb-mapping}, \code{catdb-migration}, and
\code{catdb-cli}.  Fixture schema v1 covers eight categories: schema parsing,
path typing, path composition, identity mapping, mapping composition,
migration validation, information-loss detection, and a deterministic
stable-identifier schema declaration diff.  Haskell covers that admitted
schema/path/mapping/migration slice.  Lean coverage lists path identity and
associativity plus selected lawful-mapping identity and composition
declarations.

That evidence is useful, but it stops before P9.  The repository contains no:

\begin{itemize}
  \item \code{catdb-workspace} crate or semantic commit profile;
  \item immutable artifact/commit store or atomic mutable-reference store;
  \item workspace state machine, overlay evaluator, or branch-aware query
  context;
  \item dependency-aware diff, conflict classifier, or merge validator;
  \item identity, provenance, and materialization workspace integration;
  \item historical-query reproduction or rollback implementation;
  \item workspace fixture family, Haskell workspace oracle, Lean workspace
  representation, or D7 benchmark run.
\end{itemize}

The existing schema diff reports declaration changes between two finite
schemas.  It does not record operation history, infer rename continuity,
compute mapping or data impacts, merge commits, or preserve branch context.
Calling it a complete semantic diff would be an overclaim.

\subsection{Program status}

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.24\textwidth}L{0.20\textwidth}Y}
\toprule
Item & Status & Reason \\
\midrule
CR-069, overlay workspaces & \proposed{} & no workspace implementation or
experiment \\
CR-045, reproducible histories & \proposed{} and disputed & no replay,
merge, or convergence witness \\
\code{SYS-WS-01} & \openstatus{} & no overlay/materialized equivalence test \\
\code{SYS-WS-02} & \openstatus{} & no workspace isolation test \\
\code{SYS-WS-03} & \openstatus{} & no commit/ref store or crash test \\
P9 formal fragment & \openstatus{} & no Haskell or Lean workspace model \\
P9 systems evaluation & \openstatus{} & no harness, baseline, or raw run \\
Slice 12 & \obstructed{} & prerequisite contracts and merge rules are not
frozen \\
\bottomrule
\end{tabularx}
\caption{Present status of the principal P9 artifacts and claims.}
\label{tab:status}
\end{table}

\subsection{Dependency boundary}

P9 depends on five other paper contracts:

\begin{description}[style=nextline]
  \item[P3, migration.]
  Immutable schema revisions, typed migration packages, information loss,
  synthesis, ambiguity, and the boundary among eager, lazy, and virtual
  execution.
  \item[P4, mapping and integration.]
  Mapping direction, domain, coverage, path images, loss, synthesis,
  ambiguity, composition, and obligations.
  \item[P6, materialization.]
  The split between authoritative semantic definitions and replaceable
  realizations, together with invalidation, reuse, freshness, and recovery.
  \item[P7, identity and reconciliation.]
  Source-local identity, candidate evidence, authority-bearing decisions,
  contradiction, supersession, and reversal.
  \item[P13, provenance.]
  Immutable provenance references, completeness, retention, redaction, and
  survival across schema change.
\end{description}

These dependencies are not editorial conveniences.  A workspace cannot merge
a migration whose meaning is unspecified, silently choose among ambiguous
mapping adaptations, or treat a stale cache as authoritative state.  This
boundary keeps the present P9 profile \obstructed{}.

\section{Prior-art boundary}
\label{sec:prior}

\subsection{Database branching and version-aware query}

DataHub proposed collaborative dataset branch, merge, difference, search, and
access \cite{BhardwajEtAl2014DataHub}.  Decibel implemented nonlinear
relational dataset branches, working copies, version-aware scan and
difference, field-level three-way merge, and alternative physical layouts
\cite{MaddoxEtAl2016Decibel}.  ORPHEUSDB added version control to a
conventional RDBMS and evaluated version representation, retrieval,
partitioning, and migration \cite{HuangEtAl2017OrpheusDB}.  Principles of
Dataset Versioning formalized the tradeoff between storing versions and
recreating them from deltas \cite{BhattacherjeeEtAl2015DatasetVersioning}.

P9 therefore cannot claim database branches, immutable dataset commits,
checkout, relational difference, record merge, historical dataset query, or
compact multi-version storage as new.  Decibel and ORPHEUSDB are direct
systems baselines on the relational subset.

\subsection{Schema histories and coexisting schemas}

Schema versioning for multitemporal databases predates the CatDB proposal
\cite{DeCastroEtAl1997SchemaVersioning}.  PRISM records
schema-modification operators, derives mappings, supports legacy access, and
generates migration or views \cite{CurinoEtAl2008PRISM}.  PRISM++ extends
this line with update rewriting and integrity-constraint maintenance
\cite{CurinoEtAl2010PRISMPlus}.  PRIMA represents evolving schemas with
transaction-time data and rewrites historical queries across versions
\cite{MoonEtAl2008PRIMA}.  Later work systematizes automation of the
schema-evolution process \cite{CurinoEtAl2013Automation}.

InVerDa and BiDEL let multiple schema versions access one dataset through
generated bidirectional delta code
\cite{HerrmannEtAl2017BiDEL}.  P9 cannot claim that multiple schema
interpretations over shared data are new.  It must show a wider compatibility
bundle and a cross-object merge contract.

\subsection{Mapping adaptation and model management}

Schema evolution can invalidate mappings.  Velegrakis, Miller, and Popa
developed methods to preserve mapping consistency and adapt mappings while
retaining earlier user choices where possible
\cite{VelegrakisEtAl2003MappingAdaptation,
VelegrakisEtAl2004MappingConsistency}.  Yu and Popa used mapping composition
and pruning to adapt mappings under evolution
\cite{YuPopa2005SemanticAdaptation}.  Composition itself requires a precise
mapping language: ordinary source-to-target dependencies are not generally
closed under composition \cite{FaginEtAl2005Composition}.

Model Management 2.0 names match, compose, diff, merge, translation, and
generation of executable transformations as first-class concerns
\cite{BernsteinMelnik2007Model}.  Algebraic model management connects these
operators to algebraic and categorical structure
\cite{SchultzEtAl2017ModelManagement}.  Functorial data migration provides
foundational categorical semantics for schema mappings and instance migration
\cite{Spivak2012Functorial}.  A P9 paper cannot obtain novelty merely by using
the words ``semantic diff'', ``mapping-aware merge'', or ``categorical
merge''.

\subsection{Time, persistence, provenance, and reproduction}

Transaction-time and application-time databases answer questions along
declared temporal dimensions.  SQL:2011 standardizes system-versioned and
application-time periods \cite{KulkarniMichels2012Temporal}.  Multiversion
concurrency control retains versions to enforce transactional correctness
\cite{BernsteinGoodman1983MVCC}; persistent data structures retain access to
old states \cite{DriscollEtAl1989Persistent}.  Neither an MVCC row version nor
a persistent node is automatically a semantic commit.

Scientific archives preserve historical data and element continuity so later
readers can check earlier results \cite{BunemanEtAl2004Archiving}.  The RDA
dynamic-data-citation recommendations use versioned data, timestamps,
normalized stored queries, and persistent identifiers to recover precise
subsets \cite{RauberEtAl2016RDA,RauberEtAl2016Subsets}.  VQuel proposed
unified queries over versions and provenance
\cite{ChavanEtAl2015VQuel}.  W3C PROV provides an interchange vocabulary for
entities, activities, agents, revisions, derivations, and invalidations
\cite{PROVO2013}; provenance semirings give an algebraic account for positive
query provenance \cite{GreenEtAl2007Provenance}.  PROV-IDEA explicitly
connects schema and data provenance during database evolution
\cite{PerezEtAl2025PROVIDEA}.

A commit identifier is therefore not a novelty claim and not a reproducibility
certificate.  Exact replay also needs the query, source observations,
semantic profiles, external dependencies, backend semantics, and declared
nondeterminism.

\subsection{Change explanation and materialization adaptation}

Explain-Da-V infers transformations that explain changes between dataset
versions \cite{ShragaMiller2023ExplainDaV}.  Such an explanation can be useful
evidence, but it is not necessarily the operation that happened or the
author's intent.  P9 keeps recorded operation, reconstructed state diff,
inferred explanation, and approved intent as separate evidence kinds.

Materialized-view adaptation reuses prior materializations after selected
view-definition changes when retained information makes it safe
\cite{GuptaEtAl2001Adapt}.  P9 must classify reuse, staleness, invalidation,
and rebuild.  It cannot merge cached bytes as semantic truth.

\section{Mathematical framework}
\label{sec:framework}

\subsection{Five identities}

\begin{definition}[Logical identity]
A logical identity names the continuing semantic role of an artifact or
schema element.  Examples include \code{schema/customer},
\code{attribute/customer/legal-name}, and \code{mapping/sap-customer}.
Continuity is declared by an admitted operation; it is not inferred from
similar spelling.
\end{definition}

\begin{definition}[Revision identity]
A revision reference is a triple
\[
  r=(k,\ell,v)
  \in \mathsf{Kind}\times\mathsf{LogicalId}\times\mathsf{RevisionId},
\]
where \(k\) is an artifact kind, \(\ell\) is a logical identity, and \(v\)
names one immutable revision.  Two revisions of one logical artifact remain
distinct even when their display names match.
\end{definition}

\begin{definition}[Content digest]
For profile \(p\) and canonical body \(b\), the content digest is
\[
  d=H(\mathsf{domain}\parallel p\parallel b).
\]
The domain and profile separate otherwise identical byte strings used for
different purposes.
\end{definition}

\begin{definition}[Physical locator]
A physical locator records where bytes or rows currently reside.  It may
change without changing logical or revision identity.  It belongs to
execution metadata and provenance, not semantic equivalence.
\end{definition}

\begin{definition}[Mutable reference]
A branch or tag reference is
\[
  \rho=(n,c,g),
\]
where \(n\) is a name, \(c\) is a commit identifier, and \(g\) is a
generation.  Updating \(\rho\) requires the caller to present the expected
generation or target.
\end{definition}

These layers prevent three common errors.  Equal content does not collapse
independently declared logical artifacts.  A display rename does not create a
new logical artifact when an authorized rename operation preserves its
identity.  A branch name does not identify an immutable commit.

\subsection{Artifact revisions and dependencies}

\begin{definition}[Artifact revision]
An artifact revision is the tuple
\[
\begin{aligned}
A = (&k,\ell,v,p,d,P,D,\pi,\alpha,e),\\
k&:\mathsf{Kind},\quad
\ell:\mathsf{LogicalId},\quad
v:\mathsf{RevisionId},\\
p&:\Profile,\quad
d:\Digest,\quad
P:\mathsf{RevisionRef}^{*},\\
D&:\mathsf{DependencyRef}^{*},\quad
\pi:\Provenance,\quad
\alpha:\mathsf{AuthorityRef},\\
e&:\mathsf{EventRef}.
\end{aligned}
\]
The digest covers the canonical semantic body.  Display names, timestamps,
and physical locations enter metadata or provenance unless the profile makes
them semantically relevant.
\end{definition}

The first profile admits the artifact classes in
\cref{tab:artifact-classes}.

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.16\textwidth}Y Y}
\toprule
Class & Authoritative versioned content & Replaceable or excluded content \\
\midrule
schema & objects, arrows, paths, equations, domains, constraints, stable IDs &
backend DDL cache \\
mapping & direction, path images, coverage, loss, synthesis, ambiguity,
obligations & generated SQL text \\
migration & source/target revisions, semantic transformation, mode, validation
& one run's lock schedule \\
data observation & source-local references, snapshot/cursor, normalized
operations & unversioned live source \\
identity & profile, evidence, decisions, contradictions, supersession,
reversal & similarity score alone \\
provenance & source tokens, activities, completeness, retention, redaction &
opaque log strings \\
query & normalized logical query and semantics & cached backend plan \\
materialization & definition, coverage, frontier policy, provenance profile &
stored rows, index files, cache entries \\
policy & principals, authority scope, obligations, approvals & ambient
administrator assumptions \\
\bottomrule
\end{tabularx}
\caption{Artifact classes in the proposed first workspace profile.}
\label{tab:artifact-classes}
\end{table}

\begin{definition}[Typed dependency]
A dependency edge is
\[
  (r_f,r_t,k,s,q,i,e),
\]
where \(r_f\) and \(r_t\) are revision references, \(k\) is a dependency kind,
\(s\) is a selector or scope, \(q\) is strength, \(i\) is an invalidation
rule, and \(e\) is evidence.  Kinds include \code{typed-against},
\code{maps-from}, \code{maps-to}, \code{queries}, \code{reconciles},
\code{derived-from}, \code{materializes}, \code{requires-policy}, and
\code{observes-source}.
\end{definition}

Compiler-emitted, user-declared, and inferred dependencies are separate
evidence classes.  An inferred edge may prompt review.  It does not silently
become authoritative.

\subsection{Semantic commits}

\begin{definition}[Semantic commit]
A semantic commit body is
\[
\begin{aligned}
C = (&p,\,\vec{c},\,m,\,o,\,v,\,a,\,\pi,\,x,\,r,\,z),\\
p&:\Profile,\quad
\vec{c}:\mathsf{CommitId}^{*},\\
m&:\mathsf{ArtifactManifestRef},\quad
o:\mathsf{OperationBatchRef},\\
v&:\mathsf{ValidationReportRef},\quad
a:\mathsf{ApprovalSetRef},\\
\pi&:\Provenance,\quad
x:\mathsf{SourceSnapshotSetRef},\\
r&:\mathsf{MaterializationStatusSetRef},\quad
z:\mathsf{ConflictResolutionSetRef}.
\end{aligned}
\]
Its identifier is the domain-separated digest of its canonical body.
\end{definition}

A root commit has no parent.  An ordinary commit has one parent.  A merge
commit has two or more parent references plus an explicit merge-base record.
Parent order is semantic when the profile distinguishes target and source
roles; otherwise canonicalization fixes an order.

\begin{requirement}[Commit validity]
\label{req:commit-validity}
A commit is publishable only when all required artifacts resolve and verify,
dependencies target compatible revisions, profile constraints agree,
reconciliation decisions satisfy authority rules, provenance completeness is
sufficient, invalid materializations are not advertised as current, approvals
cover the exact candidate digest, and normalized operation application agrees
with the manifest state.
\end{requirement}

Commit immutability does not certify data accuracy, mapping intent, source
authority, scientific reproducibility, or long-term availability.

\subsection{Workspaces and overlays}

\begin{definition}[Workspace]
A workspace is
\[
  W=(w,c,\vec{o},u,p,s,h_v,h_a,\rho,\pi),
\]
where \(w\) is the workspace ID, \(c\) the base commit, \(\vec{o}\) an ordered
overlay of typed operation references, \(u\) the owner, \(p\) a policy
revision, \(s\) the workspace state, \(h_v\) the validation head, \(h_a\) the
approval head, \(\rho\) a proposed target reference, and \(\pi\) provenance.
\end{definition}

The workspace identifier is not a commit identifier.  A workspace can change
until it is committed or abandoned.  An edit after validation changes the
overlay digest and returns the workspace to a draft state.

\begin{definition}[Workspace materialization]
Let \(\State(C)\) denote the normalized state named by commit \(C\).  For
profile \(p\),
\[
  \mathsf{materialize}(W)
  =
  \Apply_p\bigl(\State(c),\Normalize_p(\vec{o})\bigr).
\]
Application is partial and returns a typed outcome.
\end{definition}

\begin{requirement}[Workspace validity]
\label{req:workspace-validity}
A workspace is valid only if
\[
  \Validate_p(\mathsf{materialize}(W))=\mathsf{valid}.
\]
An optimized overlay evaluator may avoid full materialization, but its
normalized data and provenance must match this canonical semantics.
\end{requirement}

\subsection{Workspace state machine}

The proposed local state machine appears in \cref{tab:workspace-states}.

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.18\textwidth}Y L{0.28\textwidth}}
\toprule
State & Meaning & Permitted next states \\
\midrule
\code{draft} & overlay accepts authorized edits & validating, abandoned \\
\code{validating} & exact overlay digest is under validation & draft,
review-ready, blocked \\
\code{review-ready} & validation passed for the named profile & draft,
approved, rejected \\
\code{approved} & approvals cover the exact candidate & draft, merge-staging \\
\code{merge-staging} & immutable candidate artifacts are staged & approved,
merged, blocked \\
\code{merged} & target ref atomically names the merge commit & terminal \\
\code{blocked} & conflict, missing evidence, or failed gate & draft,
abandoned \\
\code{rejected} & reviewer or policy rejected the candidate & draft,
abandoned \\
\code{abandoned} & no publication from this workspace & terminal \\
\bottomrule
\end{tabularx}
\caption{Candidate workspace states.  Approval never survives a changed
candidate unless policy proves that it remains applicable.}
\label{tab:workspace-states}
\end{table}

\subsection{Semantic operations}

\begin{definition}[Semantic operation]
An operation is
\[
  o=(i,k,r,e,b,R,W,P,Q,\pi,\alpha),
\]
where \(i\) is an operation ID, \(k\) its kind, \(r\) the subject,
\(e\) the expected subject revision, \(b\) a typed payload, \(R\) and \(W\)
the semantic read and write sets, \(P\) preconditions, \(Q\) postconditions,
\(\pi\) provenance, and \(\alpha\) authority.  The operation may also carry
obligations.
\end{definition}

The initial operation families cover:

\begin{itemize}
  \item schema add, remove, rename, retype, equation, constraint, domain,
  split, and merge declarations;
  \item mapping endpoint, object image, path image, direction, coverage, loss,
  synthesis, ambiguity, and obligation changes;
  \item keyed data insert, delete, field update, rekey, assertion, retraction,
  and source-frontier advance;
  \item identity evidence, confirmed same/different, contradiction,
  supersession, reversal, and owner change;
  \item provenance evidence, profile, incompleteness, redaction, expiry, and
  invalidation;
  \item materialization definition, freshness, invalidation, reuse, rebuild,
  checkpoint, and retirement; and
  \item policy proposal, approval, rejection, obligation, discharge, and
  delegated-authority revocation.
\end{itemize}

The operation's semantic footprint is
\[
  \mathsf{footprint}(o)
  =
  \bigl(\mathsf{reads}(o),\mathsf{writes}(o),
  \mathsf{invalidates}(o),\mathsf{requires}(o)\bigr).
\]
A schema retype may write one attribute but invalidate mappings, queries, and
materializations that depend on it.

\begin{definition}[Local independence]
Operations \(a\) and \(b\) are locally independent in state \(s\) only when
their direct and derived footprints do not conflict, each remains well typed
after the other, preconditions survive in either order, authority decisions
are compatible, and the combined local effects validate.
\end{definition}

\begin{definition}[Commutativity]
Admitted operations commute in state \(s\) when
\[
  \Apply(\Apply(s,a),b)
  \equiv
  \Apply(\Apply(s,b),a),
\]
including the profile's normalized audit and provenance projection.
\end{definition}

Local commutativity does not replace complete merged-state validation.  Two
operations can commute over their immediate subjects and still violate a
global equation, key, cardinality, provenance, or policy constraint.

\section{Semantic diff and dependency impact}
\label{sec:diff}

\subsection{Five diff layers}

A semantic diff is not one list.  The proposed result separates five layers:

\begin{enumerate}
  \item \emph{structural diff} reports added, removed, renamed, or changed
  artifacts and elements;
  \item \emph{operational diff} reports retained typed operations between an
  ancestor and descendant;
  \item \emph{impact diff} reports registered dependencies whose denotation or
  admissibility may change;
  \item \emph{validation diff} reports newly satisfied, violated, unknown, or
  stale obligations; and
  \item \emph{realization diff} classifies materializations, plans, indexes,
  caches, and checkpoints as reusable, stale, invalid, or rebuild-required.
\end{enumerate}

\begin{definition}[Semantic diff result]
For commits \(A\) and \(B\) under profile \(p\),
\[
\begin{aligned}
\Diff_p(A,B)=(&p,A,B,\Delta_s,\Delta_o,\Delta_i,\Delta_v,\Delta_r,\\
             &\Delta_e,\Delta_a,\Delta_u,\kappa),
\end{aligned}
\]
where \(\Delta_s\) is structural change, \(\Delta_o\) retained operations,
\(\Delta_i\) impact, \(\Delta_v\) validation change, \(\Delta_r\)
realization change, \(\Delta_e\) inferred explanations, \(\Delta_a\)
ambiguity, \(\Delta_u\) unsupported cases, and \(\kappa\) completeness.
\end{definition}

Recorded operations and inferred explanations never receive the same evidence
label.  When operations are retained along an ancestor path, the candidate
reconstruction law is
\[
  \Apply\bigl(\State(A),\mathsf{operationalDiff}(A,B)\bigr)
  \equiv
  \State(B).
\]
For a state-derived diff, the weaker target is extensional state
reconstruction.  It says nothing about the historical operation order or the
author's intent.

\subsection{Stable identities and rename}

A schema diff must distinguish:

\begin{itemize}
  \item explicit rename from remove-plus-add;
  \item object identity from display label;
  \item type widening from narrowing;
  \item equation addition from a changed equation subject;
  \item path spelling from path denotation under a stable profile;
  \item cardinality change with checked data witnesses from an unchecked
  declaration; and
  \item declared split or merge from a structural pattern inferred after the
  fact.
\end{itemize}

The default rules appear in \cref{tab:identity-operations}.

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.18\textwidth}Y Y}
\toprule
Operation & Logical identity treatment & Required evidence \\
\midrule
display rename & preserve logical ID; create new revision & explicit rename
operation and authority \\
remove plus add & distinct IDs by default & no inferred continuity \\
copy & new logical ID; possible shared ancestry/content & copy provenance \\
split & new target IDs plus mapping from prior ID & migration, loss,
synthesis, and identity policy \\
merge & new or designated surviving ID & collision policy, reconciliation,
and provenance \\
rekey & explicit identity transition & source and canonical identity policy \\
content-equal import & profile-dependent deduplication only & namespace and
ownership policy \\
\bottomrule
\end{tabularx}
\caption{Identity treatment for changes that text diff often conflates.}
\label{tab:identity-operations}
\end{table}

Text similarity may propose a rename candidate.  Only an accepted typed
operation establishes logical continuity.

\subsection{Mapping-aware diff}

A mapping revision is not adequately described by changed field names.  Its
diff includes:

\begin{itemize}
  \item source and target revision changes;
  \item object images and arrow or path substitutions;
  \item direction and total or partial domain;
  \item source and target coverage;
  \item information loss and synthesis/default rules;
  \item ambiguity alternatives and unresolved obligations;
  \item authority; and
  \item dependent migrations, queries, write policies, and materializations.
\end{itemize}

Mapping adaptation may return multiple valid alternatives
\cite{VelegrakisEtAl2003MappingAdaptation,YuPopa2005SemanticAdaptation}.
A workspace must preserve those alternatives or request a decision.  It must
not select one because its serialized representation sorts first.

\subsection{Keyed data diff and identity ambiguity}

The first data-diff profile is finite and keyed.  It reports inserted and
deleted keys, updated fields with before/after digests, rekeys, changed
source-local identity, assertions, retractions, and source snapshot changes.
If no stable key exists, the result is an ambiguity set or
\code{unsupported}.  Positional row comparison cannot establish semantic
identity.

This restriction is intentional.  P7 treats candidate generation, probable
equivalence, confirmed sameness, confirmed difference, contradiction, and
supersession as separate artifacts.  A P9 diff may report changed identity
evidence and decisions, but it cannot turn similarity into an identity merge.

\subsection{Impact closure}

Let \(G=(V,E)\) be the versioned typed dependency graph and \(X\subseteq V\)
the changed artifact set.  Define the conservative closure
\[
  \Impact_G(X)
  =
  \mu Y.\;
  X\cup
  \{v\mid \exists u\in Y.\;(u,v)\in E
    \land \mathsf{propagates}(u,v)\}.
\]
Propagation is change-specific.  An unused nullable attribute addition may
leave a projection valid.  A wildcard projection makes the same addition
relevant.  A stable-ID display rename may preserve a mapping, while a type
narrowing may invalidate the mapping and existing data.  A changed identity
decision may alter aggregate groups.  A stricter provenance profile can
invalidate a data-equivalent materialization.

Every impact edge reports whether it is direct or transitive; compiler
emitted, user declared, inferred, or wildcard; and valid, stale, or unknown.
It also names the propagation rule and source revision.

\begin{conjecture}[Impact soundness for a frozen fragment]
\label{conj:impact}
If an admitted change can alter the normalized denotation or admissibility of
a registered dependent artifact, that artifact belongs to the computed impact
set.
\end{conjecture}
\status{\openconj{}.  The dependency language and proof fragment are not
frozen.  One false negative would refute the statement for that profile.}

Impact precision is empirical.  False positives cost review and recomputation;
they cannot be dismissed as harmless.  The evaluation must report recall and
precision against a preregistered seeded oracle.

\section{Three-way semantic merge}
\label{sec:merge}

\subsection{Inputs and outcomes}

\begin{definition}[Merge request]
A merge request is
\[
\begin{aligned}
M_q = (&p,c_b,c_t,c_s,\rho,g,u,a,q,\sigma),\\
p&:\Profile,\quad
c_b,c_t,c_s:\mathsf{CommitId},\\
\rho&:\mathsf{TargetRef},\quad
g:\mathsf{ExpectedGeneration},\\
u&:\mathsf{Principal},\quad
a:\mathsf{AuthorityRevision},\\
q&:\mathsf{PolicyRevision},\quad
\sigma:\mathsf{RequestedStrategy}.
\end{aligned}
\]
\end{definition}

The merge base is explicit.  If ancestry yields several candidate bases, the
profile must select or construct one and record that choice.  The output is:
\[
\begin{aligned}
\Merge_p(B,T,S)\in{}\;&
\mathsf{Merged}(C,\Pi,\Gamma)
\;+\;\mathsf{Conflicts}(K)\\
&+\;\mathsf{Reconciliation}(R)
\;+\;\mathsf{Unsupported}(U)
\;+\;\mathsf{Rejected}(E).
\end{aligned}
\]
Here \(C\) is a candidate commit, \(\Pi\) its validation and approval record,
and \(\Gamma\) decision provenance.

\subsection{Merge stages}

The procedure has twelve ordered stages:

\begin{enumerate}
  \item resolve and verify base, target, and source commits;
  \item compute or load typed diffs from the base;
  \item expand semantic footprints and dependency impacts;
  \item classify every relevant operation pair;
  \item apply reviewed automatic rules;
  \item emit typed conflicts and reconciliation requests;
  \item apply authorized resolutions to a candidate state;
  \item validate the entire candidate state;
  \item recompute materialization validity and historical availability;
  \item stage immutable artifacts, commit, and reports;
  \item compare-and-swap the target reference; and
  \item record publication provenance.
\end{enumerate}

\begin{requirement}[Closed automatic merge]
\label{req:closed-merge}
An operation pair may auto-merge only if a rule exists in the exact profile,
the pair is well typed at the base, all rule preconditions hold,
noninterference or commutativity is checked, authority and policy agree,
dependency effects are included, and the complete resulting state validates.
An unclassified pair returns \code{unsupported-pair}.
\end{requirement}

Different files, rows, or logical subjects can support an independence
argument.  None is sufficient for every operation kind.

\subsection{Conflict records}

\begin{definition}[Conflict record]
A conflict record is
\[
  k=(i,c,B,T,S,A,W,R,V,s,z),
\]
where \(i\) is a conflict ID, \(c\) the conflict class, \(B\) base
references, \(T\) and \(S\) target/source operations, \(A\) affected
artifacts, \(W\) witnesses, \(R\) allowed resolutions, \(V\) required
validations, \(s\) status, and \(z\) an optional resolution reference.
Required authority is part of the record.
\end{definition}

\Cref{tab:conflicts-core} lists the core classes.

\begin{longtable}{L{0.24\textwidth}L{0.43\textwidth}L{0.21\textwidth}}
\caption{Core semantic conflict taxonomy.}
\label{tab:conflicts-core}\\
\toprule
Class & Example & Default outcome \\
\midrule
\endfirsthead
\toprule
Class & Example & Default outcome \\
\midrule
\endhead
same-subject divergent edit &
both branches replace one mapping path differently & conflict \\
delete/modify &
target removes an attribute that source retypes & conflict \\
rename/rename &
one stable ID receives two display names & policy or conflict \\
rename/remove-add ambiguity &
one branch renames; the other creates a lookalike & reconciliation \\
type/domain incompatibility &
one branch widens an integer while the other parses it as a date & conflict \\
equation violation &
combined paths violate a declared schema equation & invalid candidate \\
constraint/data conflict &
non-null strengthens while branch data still contain null & repair or block \\
schema/mapping conflict &
a mapping image references a removed path & adaptation or conflict \\
migration/direction conflict &
branches assume incompatible read directions & conflict \\
mapping coverage conflict &
one branch excludes newly admitted source rows & policy review \\
data same-key conflict &
both branches update one field differently & field conflict \\
data rekey conflict &
two records claim one stable key & reconciliation \\
identity merge/split conflict &
one confirms same; the other confirms different & reconciliation required \\
decision authority conflict &
the approving actor lacks scope & reject decision \\
provenance completeness conflict &
a stricter profile lacks retained evidence & block or degrade \\
retention or reproduction conflict &
a branch expires a source needed by a cited result & policy conflict \\
materialization conflict &
one branch reuses state invalidated by the other & rebuild or conflict \\
policy conflict &
branches impose incompatible obligations & governance resolution \\
physical-only conflict &
plans differ while semantic digest agrees & execution choice \\
unsupported operation pair &
opaque transform combined with a schema split & unsupported or manual \\
\bottomrule
\end{longtable}

The intended CatDB delta lies mainly in cross-object conflicts.  Decibel
already treats tuple and field conflicts
\cite{MaddoxEtAl2016Decibel}.  P9 must show value on cases such as schema
retype plus mapping edit, identity decision plus aggregate materialization,
provenance-policy change plus retention event, and migration plus branch-local
data operations.

\subsection{Resolution and preserved disagreement}

A conflict may describe two legitimate alternatives that cannot be combined
automatically.  The system preserves both branches and their evidence.
Branch-local queries can continue while the target merge remains blocked.

\begin{definition}[Conflict resolution]
A resolution contains the conflict reference, selected or synthesized effect,
rejected alternatives, reason, evidence, authority, approvals, validations,
reversibility declaration, and provenance.
\end{definition}

Resolution never deletes the conflict history.  If it is declared reversible,
the inverse or compensating procedure and its affected-artifact policy must be
explicit.

\subsection{Why merge is not a pushout by default}

Pushouts and other colimits can model selected integrations under a stated
category and class of morphisms
\cite{SchultzEtAl2017ModelManagement}.  The operational merge above may also
contain partial or lossy mappings, probabilistic identity evidence,
authority, data constraints, retention policy, materialization state, and an
atomic publication step.  The paper does not call every merge a pushout.

A concrete counterexample is a base customer object changed on one branch
into separate Person and Organization objects while another branch retains
the customer object but records two plausible, authority-dependent identity
assignments for one source record.  The merge must preserve both candidates
and synthesize a resolution artifact awaiting authority; there is no declared
unique mediating morphism that chooses one candidate.  That conflict-bearing
result is not asserted to satisfy a pushout universal property.

If a future formal result uses a categorical construction, it must state the
objects and morphisms, the diagram, existence conditions, quotient policy,
and operational interpretation.  Other merges remain partial procedures with
validation and conflict outcomes.

\subsection{Candidate merge laws}

The following are targets, not results:

\begin{conjecture}[Identity merge law]
For a valid base state \(B\), merging \(B\) with two unchanged descendants
returns a state extensionally equal to \(B\).
\end{conjecture}

\begin{conjecture}[One-sided merge law]
If \(T\) is a valid admitted descendant of \(B\) and \(S=B\), then
\(\Merge(B,T,S)\) returns a state extensionally equal to \(T\), subject to
publication authority and current policy.
\end{conjecture}

\begin{conjecture}[Conservative automatic merge]
Every pair accepted by the closed automatic rule table commutes or is
noninterfering under its stated preconditions, and complete validation
preserves the admitted global invariants.
\end{conjecture}

\status{All three statements are \openconj{}.  No P9 Lean declarations,
Haskell properties, Rust implementation, or exhaustive pair cases exist.}

\section{Co-versioned semantic state}
\label{sec:coversioning}

\subsection{The compatibility bundle}

A workspace state is not just a schema and rows.  The proposed bundle is
\[
\begin{aligned}
\mathcal{B}=(&S,M,G,I,D,Q,P,R,A,X,F),\\
S&=\text{schema revisions},\\
M&=\text{mapping and migration revisions},\\
G&=\text{typed dependency graph},\\
I&=\text{data observations and overlay operations},\\
D&=\text{identity and reconciliation decisions},\\
Q&=\text{logical query definitions},\\
P&=\text{provenance profile and retained evidence},\\
R&=\text{materialization definitions and status},\\
A&=\text{authority and approval state},\\
X&=\text{source snapshots and connector observations},\\
F&=\text{freshness and completeness envelope}.
\end{aligned}
\]
Validity means that all cross-references and profile obligations hold.

\subsection{Schema changes with data}

A schema operation classifies its data response as:

\begin{itemize}
  \item unchanged and still valid;
  \item transformed by an admitted migration;
  \item available through a compatibility view;
  \item partially valid with explicit rejected rows;
  \item requiring backfill, synthesis, or reconciliation;
  \item invalid pending repair; or
  \item unsupported.
\end{itemize}

Each branch-local data operation records the schema and identity context in
which it was typed.  A rebase or merge revalidates or migrates the operation.
Matching field names do not justify blind replay against a different schema.

\subsection{Mapping changes with data}

A mapping revision must report:

\begin{itemize}
  \item whether source and target schema revisions still match;
  \item whether the mapping is total over its declared domain;
  \item which source observations are reinterpreted;
  \item whether canonical identities or values change;
  \item which queries and materializations are affected;
  \item whether old provenance explanations remain meaningful; and
  \item whether physical rematerialization is required.
\end{itemize}

This is the practical meaning of mapping-aware merge in P9.  It does not mean
that all adapted mappings are unique or safe.

\subsection{Branch-local constraints}

Each workspace validates its own declared profile.  Two branches can both be
valid while imposing incompatible constraints.  Team A may require unique
canonical customer identity after its merge decision; Team B may require that
the same source records remain separate.  Independent validity is not merge
compatibility.

A branch-local constraint record includes its logical identity, revision,
scope, dependency footprint, authority, validation procedure, and evidence.
Promoting the branch to a shared ref requires revalidation against the
candidate commit, not reuse of a stale branch-local pass.

\subsection{Alternative interpretations}

An interpretation branch may change mapping choice, unit normalization,
identity decision, trust policy, ontology, schema constraint, query
definition, or materialization strategy while referencing the same immutable
source observations.

\begin{requirement}[Interpretation isolation]
\label{req:interpretation-isolation}
Results from interpretation \(I_A\) may enter \(I_B\) only through an explicit
import, mapping, or merge operation that records source and target contexts,
transformation, provenance, authority, loss, ambiguity, validation, and
conflict behavior.
\end{requirement}

A comparison across interpretations reports shared evidence, changed
artifacts, output differences, provenance differences, the assumptions
responsible for those differences, and unresolved ambiguity.  Promoting one
interpretation to a canonical branch is an authority-bearing reference
update.  It is not a claim that the interpretation is universally true.

\begin{conjecture}[Safe coexistence for the admitted local profile]
Alternative interpretations over retained source snapshots produce
context-labelled results without leaking branch-local operations or decisions.
\end{conjecture}
\status{\obstructed{}.  No workspace evaluator, isolation boundary, or
provenance audit exists.}

\subsection{Identity decisions and downstream effects}

P7 separates evidence, method output, and authority-bearing decision.  P9 adds
workspace context and effective decision projection.  Confirming two source
records as one canonical entity may merge aggregate groups, change uniqueness
constraints, redirect relationships, alter coverage interpretation,
invalidate caches, change explanations, and make write-back ambiguous.

If one branch confirms sameness and another confirms difference, the merge
returns a typed contradiction.  Last-writer-wins is not admitted.  Reversing a
decision creates a new event, restores or creates separate canonical
projections under P7 rules, invalidates dependents, preserves prior result
provenance, and reports any information that cannot be separated
automatically.

\section{Provenance, materialization, history, and rollback}
\label{sec:history}

\subsection{Commit and result provenance}

Commit provenance should answer:

\begin{itemize}
  \item who or what proposed each operation;
  \item which base and source snapshots were used;
  \item which schema, mapping, migration, identity, query, and policy
  revisions applied;
  \item which validations ran over which candidate digest;
  \item which approvals and obligations were effective;
  \item how conflicts were resolved;
  \item which derived artifacts became invalid; and
  \item which target reference was published.
\end{itemize}

Every workspace query result names the workspace and overlay digest or the
immutable commit, source snapshots, schema and mapping revisions, identity
projection, provenance profile, query revision, materialization or plan if
used, freshness, approximations, unsupported components, and retention or
redaction boundary.

W3C PROV can carry an interoperability projection: commits and artifacts as
\code{prov:Entity}, executions as \code{prov:Activity}, principals as
\code{prov:Agent}, and revision, use, generation, invalidation, and delegation
through the corresponding relations \cite{PROVO2013}.  The projection is not
the internal workspace semantics.  A loss audit must identify CatDB
distinctions that the projection cannot express exactly.

\subsection{Materialization definition versus realization}

The semantic commit versions the logical query or mapping definition, source
coverage and frontier policy, provenance profile, consistency and freshness
requirements, allowed execution strategies, and dependency edges.  Stored
rows, indexes, cache entries, backend plans, and temporary overlay state are
replaceable realizations.

A materialization status records:
\[
  (r_d,i_r,f_s,d_l,d_p,s,v,u),
\]
where \(r_d\) is the definition revision, \(i_r\) a realization ID, \(f_s\)
the source frontier, \(d_l\) the logical digest, \(d_p\) the provenance
digest, \(s\) status, \(v\) validation, and \(u\) an optional reuse or rebuild
rule.

After a merge, each materialization becomes one of:

\begin{itemize}
  \item unaffected and reusable;
  \item reusable after validated adaptation;
  \item stale with an explicit frontier;
  \item invalid;
  \item rebuild required;
  \item provenance re-derivation required;
  \item retired; or
  \item unsupported.
\end{itemize}

Physical row differences need no semantic merge when both realizations can be
discarded and rebuilt.  The semantic conflict lies in definitions,
dependencies, frontiers, provenance requirements, or promises made to
readers.

\subsection{Historical query context}

\begin{definition}[Historical query context]
A historical query context is
\[
\begin{aligned}
K = (&c,w,q,x,s,m,d,p,a,b,r,n),\\
c&:\mathsf{CommitId},\quad
w:\mathsf{OptionalOverlayDigest},\\
q&:\mathsf{LogicalQueryRevision},\quad
x:\mathsf{SourceSnapshotSet},\\
s&:\mathsf{SchemaRevisionSet},\quad
m:\mathsf{MappingMigrationRevisionSet},\\
d&:\mathsf{IdentityProjectionRevision},\quad
p:\mathsf{ProvenanceProfile},\\
a&:\mathsf{PolicyRevision},\quad
b:\mathsf{BackendSemanticsProfile},\\
r&:\mathsf{MaterializationPolicy},\quad
n:\mathsf{NondeterminismProfile}.
\end{aligned}
\]
\end{definition}

Commit ancestry, system time, valid time, source cursor, and materialization
frontier are distinct.  A query may request a commit state \(C\), facts valid
at domain time \(t_v\), decisions known at system time \(t_s\), source
observations through frontier \(f\), and a materialization at checkpoint
\(k\).  The response names every cut.

Re-executing a current query against an old commit is not the same as
executing the historical query revision.  Both operations can be useful, but
the caller must choose explicitly.

\subsection{Reconstruction, replay, and reproduction}

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.20\textwidth}Y Y}
\toprule
Goal & Meaning & Minimum evidence \\
\midrule
state reconstruction &
rebuild the normalized semantic bundle &
commits, artifacts, and operations or snapshots \\
query replay &
execute the same logical query under the same declared context &
reconstructed state, query revision, and execution semantics \\
result reproduction &
obtain the same normalized data and provenance and explain nondeterminism &
replay evidence plus retained external observations and dependencies \\
\bottomrule
\end{tabularx}
\caption{Three historical goals that must not share one success label.}
\label{tab:history-goals}
\end{table}

A reproduction envelope contains the result and commit IDs, canonical query,
source snapshots, artifact and semantic-profile revisions, connector and
backend versions, external-function digests, materialization and plan
references, normalized result and provenance digests, environment manifest,
retention status, and known nondeterminism.

For retained context \(K\), exact reproduction requires:
\[
  \Normalize(\mathsf{execute}(q,K))=(d,p),
\]
where both the normalized data digest \(d\) and provenance digest \(p\) match
the stored result.  Equal data with different provenance is not exact
P13-enabled reproduction.

The machine-readable status set includes:
\begin{itemize}
  \item \code{exact-reproduction};
  \item \code{exact-reconstruction-new-plan};
  \item \code{semantically-equivalent-under-profile};
  \item \code{partial-source};
  \item \code{stale-materialization};
  \item \code{provenance-incomplete};
  \item \code{redacted};
  \item \code{nondeterministic};
  \item \code{unavailable-retention};
  \item \code{unsupported-backend-semantics}; and
  \item \code{blocked}.
\end{itemize}

Immutable history does not override lawful deletion, confidentiality, access,
or retention policy.  The system may retain a tombstone, deletion event,
non-sensitive digest, redacted provenance skeleton, or only an authorized
audit record.  The reproduction status must change accordingly.

\subsection{Rollback and compensation}

P9 distinguishes four operations:

\begin{description}[style=nextline]
  \item[Reference rollback.]
  An authorized mutable ref moves from \(C_n\) to an ancestor \(C_k\).  The
  event is recorded and immutable commits remain.
  \item[Revert commit.]
  A new commit applies admitted inverse or compensating operations on top of
  the current head:
  \[
    C_{n+1}=\mathsf{commit}
      (C_n,\mathsf{compensate}(C_k\rightarrow C_n)).
  \]
  \item[Workspace discard.]
  A draft workspace becomes abandoned without changing its base commit.
  \item[Physical compensation.]
  Backend DDL, external writes, messages, and source-system effects use their
  own transaction or compensation protocol.
\end{description}

Every attempted external compensation creates an immutable
\code{CompensationReceipt} artifact linked to the triggering revert commit.
The receipt records the external-effect reference, connector and capability
revision, idempotency key, declared footprint, pre- and post-observations,
outcome \(\{\code{succeeded},\code{failed},\code{unknown}\}\), authority,
timestamps, and provenance.  A \code{succeeded} receipt supports restoration
only for the declared footprint and postcondition actually checked; it does
not prove that the whole external system equals an earlier state.  A missing
or \code{unknown} receipt blocks any exact-restoration status and remains a
visible unresolved artifact in the commit graph.

A semantic ref movement cannot claim to reverse external side effects.
Rollback reclassifies materializations, checks source-frontier compatibility,
preserves identity and provenance history, reevaluates policy, and keeps the
original context of historical results.

\section{Candidate results and formal obligations}
\label{sec:formal}

\subsection{Status of this section}

This section contains no established P9 theorem.  It defines the smallest
fragment in which selected claims could become machine checked.  Haskell is
the proposed executable semantic oracle; Lean is the kernel-checked authority
for selected pure laws; Rust is the proposed production implementation.
Agreement among them would provide valuable evidence, but the evidence types
remain different.

The first formal fragment is finite.  It includes artifact kinds and revision
references, canonical commit bodies, schemas and lawful mappings from the
accepted CatDB fragment, keyed finite instances, typed dependency graphs,
operations with decidable preconditions, base-plus-overlay workspaces, a
closed conflict enumeration, and a finite automatic-merge table.  It excludes
arbitrary SQL, opaque functions, probabilistic matching algorithms,
cryptographic hash security, access-control correctness, persistent storage,
wall-clock and distributed time, external connectors, cost optimization, and
complete scientific reproducibility.

\subsection{Haskell reference semantics}

The planned Haskell surface is:

\begin{lstlisting}
canonicalArtifact :: Profile -> ArtifactRevision
                  -> Either Error Bytes
canonicalCommit   :: Profile -> SemanticCommit
                  -> Either Error Bytes
applyOperation    :: Profile -> State -> Operation
                  -> Either Outcome State
normalizeOverlay  :: Profile -> [Operation]
                  -> Either Error [Operation]
materialize       :: Profile -> CommitState -> [Operation]
                  -> Either Outcome State
semanticDiff      :: Profile -> State -> State
                  -> Either Outcome SemanticDiff
impactClosure     :: Profile -> DependencyGraph -> Set Ref
                  -> ImpactReport
classifyPair      :: Profile -> State -> Operation -> Operation
                  -> PairResult
merge3            :: Profile -> State -> State -> State
                  -> MergeResult
\end{lstlisting}

The property suite should test:

\begin{enumerate}
  \item idempotence of canonicalization;
  \item invariance under permutation of set-like members;
  \item declared duplicate-operation replay behavior;
  \item denotational preservation by overlay normalization;
  \item operational-diff reconstruction from an ancestor;
  \item state-diff reconstruction up to extensional equality;
  \item commutativity for every pair labelled commuting;
  \item precondition preservation for every pair labelled independent;
  \item identity and one-sided merge laws;
  \item refusal of unclassified operation pairs;
  \item rejection by full validation when local pair checks are insufficient;
  \item explicit commit or workspace context in result provenance; and
  \item exact normalized equality with Rust fixtures.
\end{enumerate}

Passing these properties would be \emph{computational evidence} for the tested
inputs and generators, not proof of the production runtime or real sources.
No P9 property currently exists.

\subsection{Lean targets}

\Cref{tab:lean-targets} lists the proposed proof obligations.

\begin{longtable}{L{0.12\textwidth}L{0.30\textwidth}L{0.43\textwidth}}
\caption{Proposed Lean targets.  Every row remains \openconj{}.}
\label{tab:lean-targets}\\
\toprule
ID & Target & Exact boundary \\
\midrule
\endfirsthead
\toprule
ID & Target & Exact boundary \\
\midrule
\endhead
P9-F01 & canonicalization idempotence &
pure finite representation, not byte codec or hash security \\
P9-F02 & normalization preservation &
selected overlay rewrites preserve pure state and retained audit projection \\
P9-F03 & materialization-fold determinism &
fixed ordered operations over deterministic partial application \\
P9-F04 & ancestor diff reconstruction &
retained admitted operation sequence reconstructs the descendant \\
P9-F05 & state-diff reconstruction &
finite keyed states under one frozen diff algorithm \\
P9-F06 & independent-operation commutativity &
exact named operation pairs under explicit footprint assumptions \\
P9-F07 & merge identity and one-sided laws &
valid base and one-sided admitted changes \\
P9-F08 & local well-formedness preservation &
selected schema and mapping laws after admitted auto-merge \\
P9-F09 & conflict-table completeness &
total classification over the closed pair enumeration \\
P9-F10 & pure context noninterference &
separate state maps and explicit context, not storage isolation \\
\bottomrule
\end{longtable}

Even successful proofs would not establish SHA-256 collision resistance, JSON
codec correctness, SQLite durability, atomic publication under hardware
failure, authorization soundness, human reconciliation correctness,
provenance completeness from external sources, source retention, performance,
or distributed convergence.

\subsection{Cross-language acceptance}

Each pure fixture follows:
\[
\begin{aligned}
\text{JSON fixture}
&\longrightarrow \text{Haskell normalized result}\\
&\longleftrightarrow \text{Rust normalized result}\\
&\longrightarrow \text{Lean declaration where available}.
\end{aligned}
\]
The manifest records claim anchor, assumptions, expected status, Rust and
Haskell tests, optional Lean declaration, unsupported boundary, and source
revision.  A blank Lean field means ``not machine checked.''

\begin{conjecture}[Overlay/materialized equivalence]
\label{conj:overlay}
For every workspace, query, and operation in the frozen finite profile, the
optimized base-plus-overlay evaluator returns the same normalized data and
provenance as query evaluation over the canonical materialized workspace.
\end{conjecture}
\status{\obstructed{}.  This is P9-C02 and \code{SYS-WS-01}; no evaluator or
fixture profile exists.}

\begin{conjecture}[Pure workspace noninterference]
\label{conj:noninterference}
Given explicit disjoint workspace contexts, evaluation in \(W_A\) is
independent of unimported overlay operations and branch-local decisions in
\(W_B\).
\end{conjecture}
\status{\openconj{} for a pure evaluator and \obstructed{} for the storage and
authorization system.}

\section{Implementation roadmap}
\label{sec:implementation}

\subsection{Architecture boundary}

The implementation sequence refines the shared Slice 12 plan.  It does not
replace it.  The semantic model belongs in immutable IR and workspace
interfaces; SQLite is the first durable realization.  Storage may persist
artifacts and references, but it does not decide schema validity, mapping
lawfulness, identity authority, or provenance completeness.

\begin{figure}[ht]
\centering
\begin{tikzpicture}[
  box/.style={draw,rounded corners,align=center,minimum width=3.1cm,
              minimum height=0.8cm,fill=blue!5},
  arr/.style={->,thick}
]
\node[box] (profile) {Frozen artifact and\\operation profile};
\node[box,below=0.6cm of profile] (ir) {Canonical artifact, commit,\\and reference IR};
\node[box,below=0.6cm of ir] (store) {Immutable store and\\atomic reference store};
\node[box,below left=0.7cm and -0.1cm of store] (overlay) {Overlay evaluator\\and isolation};
\node[box,below right=0.7cm and -0.1cm of store] (diff) {Diff, dependency,\\and impact};
\node[box,below=1.9cm of store] (merge) {Conflict classification,\\validation, publication};
\node[box,below=0.6cm of merge] (cross) {Identity, provenance, and\\materialization integration};
\node[box,below=0.6cm of cross] (history) {History, rollback, CLI,\\and evaluation};
\draw[arr] (profile) -- (ir);
\draw[arr] (ir) -- (store);
\draw[arr] (store) -- (overlay);
\draw[arr] (store) -- (diff);
\draw[arr] (overlay) -- (merge);
\draw[arr] (diff) -- (merge);
\draw[arr] (merge) -- (cross);
\draw[arr] (cross) -- (history);
\end{tikzpicture}
\caption{Proposed local implementation order.  The cross-object layers enter
only after commit, overlay, diff, and publication contracts are fixed.}
\label{fig:implementation}
\end{figure}

\subsection{Stage I0: freeze prerequisites and profile}

P3, P4, P6, P7, and P13 must publish compatible finite contracts.  P9 then
freezes artifact classes, identity layers, operation kinds, conflict classes,
authority, provenance, materialization boundaries, unsupported operations,
fixture version, diagnostic codes, threat model, and crash model.

\status{\obstructed{}.}

\subsection{Stage I1: canonical artifacts, commits, and refs}

Implement logical and revision IDs, domain-separated digests, typed
dependencies, semantic commit bodies, mutable refs with generation,
canonical serialization, closed diagnostics, and profile versioning.  Rust
and Haskell must produce identical canonical bytes and identifiers under
permutation fixtures.

\status{\openstatus{}.}

\subsection{Stage I2: immutable store and atomic refs}

Implement put-if-absent artifact and commit storage, digest verification,
reachability audit, transactional SQLite reference storage,
compare-and-swap publication, recovery receipts, and a retention-aware
garbage-collection design.  The crash matrix covers every boundary before and
after artifact staging, commit persistence, reference update, and
acknowledgement.

\status{\openstatus{}.}

\subsection{Stage I3: workspace and overlay}

Create \code{catdb-workspace} with the state machine, typed operation
application, deterministic normalization, validation-head invalidation,
explicit query context, canonical materialized-state evaluator, and optimized
overlay evaluator.  Concurrency schedules must test isolation from
branch-local rows, decisions, validation state, approvals, and cache effects.

\status{\obstructed{}.}

\subsection{Stage I4: diff, dependencies, and impact}

Implement all five diff layers, exact separation of recorded and inferred
changes, typed impact closure, compiler and user edge provenance, wildcard
dependencies, and conservative unknown handling.  Mutation tests remove
dependency edges and validators to confirm that the oracle catches omissions.

\status{\obstructed{}.}

\subsection{Stage I5: merge and publication}

Implement merge-base resolution, the reviewed pair table, footprint expansion,
precondition and authority checks, typed conflicts, resolution operations,
complete candidate validation, approval coverage over the exact digest, and
atomic publication through Stage I2.

\status{\obstructed{}.}

\subsection{Stages I6 through I11}

\begin{description}[style=nextline]
  \item[I6, cross-object integration.]
  Add branch-local identity projections, contradictions, reversal, result
  provenance, completeness and retention, materialization invalidation,
  reuse, and rebuild.
  \item[I7, history and rollback.]
  Add explicit temporal cuts, reproduction envelopes, degraded outcomes, ref
  rollback, revert, and compensation.
  \item[I8, SQLite realization.]
  Persist append-only artifacts and commits, transactional refs, workspace
  operations, dependencies, conflicts, validations, approvals, and failpoint
  receipts.
  \item[I9, CLI.]
  Expose create, apply, validate, diff, query, merge, resolve, publish,
  history, reproduce, and audit through closed machine-readable envelopes.
  \item[I10, hardening.]
  Add model-based tests, fuzzing, mutation tests, concurrency schedules,
  failpoints, authorization time-of-check/time-of-use cases, digest
  confusion, profile-crossing, malicious cycles, resource limits, and
  redaction noninterference.
  \item[I11, D7 harness.]
  Implement the common relational subset and baseline adapters, preserve
  failed observations, and run correctness before performance.
\end{description}

All six stages are \openstatus{} or \obstructed{}.

\subsection{Command-line surface}

The planned deterministic commands are:

\begin{lstlisting}
catdb workspace create --base <commit>
catdb workspace apply --workspace <id> --ops <file>
catdb workspace validate --workspace <id>
catdb workspace diff <from> <to>
catdb workspace query --workspace <id> --query <file>
catdb workspace merge --base <id> --target <id> --source <id>
catdb workspace resolve --conflict <id> --resolution <file>
catdb workspace publish --workspace <id> --ref <name> --expect <generation>
catdb workspace history --ref <name>
catdb workspace reproduce --result <id>
catdb workspace audit --commit <id>
\end{lstlisting}

The CLI must not infer a default workspace for branch-local or historical
queries.  Human-readable output is a rendering of the closed envelope, not an
alternative semantics.

\section{Evaluation and falsification plan}
\label{sec:evaluation}

\subsection{Research questions}

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.12\textwidth}Y}
\toprule
ID & Question \\
\midrule
RQ1 & Does base-plus-overlay query equal canonical materialization for every
admitted operation and query case? \\
RQ2 & Are workspace reads isolated under concurrent schedules and shared
caches? \\
RQ3 & How sound and precise are semantic diff, impact closure, and conflict
classification on seeded changes? \\
RQ4 & Does automatic merge remain deterministic, conservative, and globally
valid? \\
RQ5 & Is merge publication atomic across every declared crash point and ref
race? \\
RQ6 & What storage, checkout, diff, merge, and historical-query cost does
CatDB add on the shared relational subset? \\
RQ7 & Does cross-object metadata detect faults or reduce diagnosis and repair
effort beyond data-only versioning? \\
RQ8 & Under what retained inputs can historical results be reproduced,
reconstructed, degraded, or not recovered? \\
RQ9 & Can alternative interpretations remain isolated while supporting
explicit, provenance-bearing comparison? \\
\bottomrule
\end{tabularx}
\caption{P9 evaluation questions.}
\label{tab:research-questions}
\end{table}

\subsection{Correctness gate}

Performance measurements stop if any run exhibits:

\begin{itemize}
  \item canonical commit mismatch;
  \item overlay/materialized data or provenance mismatch;
  \item workspace leakage;
  \item omitted preregistered impact;
  \item incorrect automatic merge or untyped supported conflict;
  \item incomplete merged-state validation;
  \item unauthorized identity decision;
  \item stale materialization reported as current;
  \item partial target-reference publication;
  \item historical reproduction misclassification; or
  \item raw-artifact integrity failure.
\end{itemize}

A slower correct execution remains evidence.  A faster incorrect execution is
rejected.

\subsection{Baselines and fairness}

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.24\textwidth}Y}
\toprule
Baseline & Fair comparison boundary \\
\midrule
Decibel & relational branch, checkout, difference, merge, version query, and
storage; released artifact if reproducible, otherwise labelled reconstruction
\\
ORPHEUSDB & relational version storage, retrieval, query, and version
operations under the same artifact/reconstruction rule \\
full-copy SQL & one table copy per version in SQLite or PostgreSQL \\
row-delta SQL & parent-linked keyed row deltas without CatDB semantics \\
Git files & canonical JSON storage and text workflow only; a negative
semantic baseline, not database-query equivalence \\
CatDB data-only ablation & commit engine with cross-object features disabled
to isolate their overhead and value \\
\bottomrule
\end{tabularx}
\caption{Evaluation baselines.  CatDB-only semantics cannot be used to claim
that a prior system fails requirements outside its scope.}
\label{tab:baselines}
\end{table}

Published performance numbers are not executable baselines by themselves.  If
an original artifact cannot run in the pinned environment, the evaluation
uses a reviewed reconstruction and reports the difference.

\subsection{Workload dimensions}

Generate version graphs across:

\begin{itemize}
  \item graph depth, branch width, merge density, and changed fraction;
  \item data size, row width, key skew, and hot-key concentration;
  \item schema object, path, equation, and constraint counts;
  \item mapping count, path depth, coverage, loss, and ambiguity;
  \item dependency fan-out and wildcard use;
  \item identity evidence, decision, contradiction, and reversal count;
  \item provenance density, completeness, redaction, and retention;
  \item materialization count and source-frontier skew;
  \item policy and approval count; and
  \item conflict mix: independent, commuting, direct conflict,
  reconciliation-required, globally invalid, and unsupported.
\end{itemize}

Every generated history retains its seed and canonical manifest.  Workload
families cover the relational shared subset, schema/data evolution, mapping
evolution, identity evolution, provenance and retention, materialization
evolution, alternative interpretations, crash recovery, and historical
reproduction.

\subsection{Correctness metrics}

Report:

\begin{itemize}
  \item exact normalized data and provenance agreement;
  \item workspace leakage count;
  \item diff reconstruction;
  \item changed-artifact and impact recall;
  \item impact precision;
  \item conflict-class precision, recall, and per-class confusion;
  \item automatic-merge false positives;
  \item unsupported-pair and global-validator escape rates;
  \item unauthorized-decision acceptance;
  \item stale-materialization false-current count;
  \item crash outcome membership and lost acknowledged publications;
  \item historical-status confusion; and
  \item missing interpretation context.
\end{itemize}

Deterministic correctness invariants require zero observed violations within
the reported workload bounds.  Zero failures do not prove correctness outside
those bounds.

\subsection{Performance and storage metrics}

Measure commit canonicalization and validation, artifact and commit bytes,
metadata/index amplification, version-storage amplification, branch creation,
checkout, overlay and materialized query latency, diff latency by layer,
impact closure, merge classification, full validation, publication, history
query, reproduction replay, invalidation and rebuild work, memory, CPU, and
bytes read or written.

Report medians, tail percentiles, dispersion, cold and warm cache, hardware,
database settings, and confidence intervals.  Do not collapse every operation
into one ``workspace overhead'' number.

\subsection{Seeded fault and reviewer study}

The blinded fault corpus includes true independent edits, direct conflicts,
cross-object conflicts, global-only violations, unauthorized decisions, stale
caches, missing provenance, retention failures, unknown operation pairs, and
benign physical-only differences.  Database/versioning and dependency-domain
reviewers freeze the oracle before running the classifier.

If the paper claims reduced review or repair effort, a preregistered study
compares:

\begin{enumerate}
  \item Git/file diff plus relational data diff;
  \item data-only version control;
  \item CatDB structural diff; and
  \item the complete CatDB impact, validation, and conflict explanation.
\end{enumerate}

Participants identify affected artifacts, merge safety, conflict class,
missing evidence or authority, required rebuild, and historical
reproducibility.  The study reports accuracy, time, confidence calibration,
repair steps, expertise, order effects, and inter-reviewer agreement.  A
convenience sample supports only an exploratory claim.

\subsection{Crash protocol}

For each failpoint:

\begin{enumerate}
  \item begin from a verified old head;
  \item stage a deterministic candidate;
  \item kill the process at the instrumented boundary;
  \item restart in a fresh process;
  \item verify reachable digests;
  \item read the target ref and generation;
  \item audit commit completeness, approval, validation, and provenance; and
  \item preserve the database, log, and observed outcome.
\end{enumerate}

The target ref may name the old complete commit or the new complete commit.
It may not name a partial state.  Complete but unreachable staged artifacts
are allowed and reported.

\subsection{Historical reproduction protocol}

For each sampled result, freeze the envelope, execute and store normalized
data/provenance digests, rerun in the pinned environment, rerun with a
semantically permitted different plan, remove or alter one dependency, and
require the status classifier to explain the outcome.  An independent
clean-room run preserves both successes and failures.

\subsection{Statistical and reporting plan}

Primary metrics, comparisons, thresholds, and exclusions are frozen before
confirmatory execution.  All runs, failures, and timeouts remain in the
artifact.  Paired comparisons use identical generated histories when
possible.  Skewed distributions use preregistered bootstrap intervals or a
robust alternative.  The report gives effect sizes and raw distributions,
not only \(p\)-values.  Noninferiority or usability thresholds come from pilot
data and external requirements before confirmatory outcomes are inspected.

\subsection{Claim-level falsification}

\begin{longtable}{L{0.12\textwidth}L{0.34\textwidth}L{0.39\textwidth}}
\caption{Primary claim anchors and falsifiers.}
\label{tab:claim-falsifiers}\\
\toprule
Anchor & Candidate claim & Immediate falsifier \\
\midrule
\endfirsthead
\toprule
Anchor & Candidate claim & Immediate falsifier \\
\midrule
\endhead
P9-C01 & deterministic commit identity across Rust and Haskell &
different canonical bytes or IDs for one valid body/profile \\
P9-C02 & overlay query equals canonical materialization &
any normalized data or provenance mismatch \\
P9-C03 & workspace isolation &
one leaked row, decision, validation, approval, or cache effect \\
P9-C04 & typed diff reconstructs admitted descendant &
state mismatch, omitted artifact, invented intent, or unstable order \\
P9-C05 & conservative impact closure &
one affected registered dependent is absent \\
P9-C06 & conservative automatic merge &
order dependence, authority breach, global violation, or missing rule \\
P9-C07 & atomic publication &
published dangling ref, mixed state, or lost acknowledged update \\
P9-C08 & cross-object conflict classification &
supported conflict auto-merges or unknown receives permissive default \\
P9-C09 & reconciliation-bearing merge &
decision lacks evidence/authority or reversal leaves stale dependents \\
P9-C10 & evidence-based history status &
exact reproduction reported after a required input is substituted or lost \\
P9-C11 & alternative-interpretation isolation &
context leakage or unsupported compatibility inference \\
P9-C12 & rollback preserves audit boundary &
silent history rewrite or false claim that external effects were undone \\
P9-C13 & value beyond relational versioning &
no added fault/review value or unacceptable false-positive burden \\
\bottomrule
\end{longtable}

Every anchor is \openstatus{} or \obstructed{}.  None is a result of this
manuscript.

\section{Related work revisited}
\label{sec:related}

\subsection{Relational version-control systems}

Decibel is the closest direct baseline for branch semantics and relational
three-way merge \cite{MaddoxEtAl2016Decibel}.  It makes the distinction from
line-oriented file versioning concrete: relations are unordered, primary keys
matter, versions share data, and users query across histories.  ORPHEUSDB
shows that version control can be layered over a mature relational engine and
that physical representation and partitioning dominate important performance
tradeoffs \cite{HuangEtAl2017OrpheusDB}.  DataHub and its versioning work
place those operations in collaborative analysis
\cite{BhardwajEtAl2014DataHub,BhattacherjeeEtAl2015DatasetVersioning}.

P9 adopts immutable commits, branch references, ancestry, working overlays,
and three-way comparison.  Its proposed difference is the commit atom and
conflict boundary across semantic artifacts.  That difference must be
measured.  Merely adding metadata files to a relational version graph would
not establish it.

\subsection{Schema and mapping evolution}

PRISM, PRISM++, and PRIMA demonstrate that schema evolution can be represented
through operators, mappings, query rewriting, and histories rather than
treated only as ordered DDL
\cite{CurinoEtAl2008PRISM,CurinoEtAl2010PRISMPlus,
MoonEtAl2008PRIMA}.  Mapping-adaptation work shows that an evolved mapping may
require composition, pruning, or a user decision
\cite{VelegrakisEtAl2003MappingAdaptation,
VelegrakisEtAl2004MappingConsistency,YuPopa2005SemanticAdaptation}.  InVerDa
demonstrates coexisting schema versions over one dataset
\cite{HerrmannEtAl2017BiDEL}.

P9's schema/data co-versioning and mapping-aware merge are therefore
extensions of established lines, not a new research category.  The proposed
systems contribution must be the exact compatibility bundle, conservative
cross-object impacts, and atomic publication.

\subsection{Model management and categorical structure}

Model management supplies a broad operator vocabulary for models and mappings
\cite{BernsteinMelnik2007Model}.  Algebraic model management asks when those
operators admit algebraic or categorical descriptions
\cite{SchultzEtAl2017ModelManagement}.  Functorial data migration supplies a
precise categorical foundation for selected schema mappings and instance
transformations \cite{Spivak2012Functorial}.  These works motivate typed paths
and compositional transformations in CatDB.  They also create strong novelty
pressure.

The operational workspace includes evidence, authority, partiality, source
availability, materialization state, and storage publication.  Category
theory may prove laws for a selected pure fragment; it does not discharge
those operational obligations by itself.

\subsection{Temporal data and reproducibility}

Temporal databases separate system and application time
\cite{KulkarniMichels2012Temporal}; P9 adds commit ancestry, source frontiers,
and branch context rather than replacing temporal dimensions.  Scientific
archiving and dynamic data citation show that later verification needs stable
history and the query that selected a subset
\cite{BunemanEtAl2004Archiving,RauberEtAl2016RDA,
RauberEtAl2016Subsets}.  VQuel demonstrates that provenance and versioning can
share a query language \cite{ChavanEtAl2015VQuel}.

P9's contribution, if validated, would be a more explicit reproduction
envelope for CatDB's semantic artifacts.  It cannot claim that versioned
provenance or query-based citation is new.

\subsection{Provenance and materialized state}

W3C PROV gives a standard interchange vocabulary
\cite{PROVO2013}; provenance semirings give compositional annotations for
positive relational queries \cite{GreenEtAl2007Provenance}; PROV-IDEA joins
schema and data provenance during evolution
\cite{PerezEtAl2025PROVIDEA}.  P9 relies on P13 to define the exact internal
provenance profile and any external projection.

Materialized-view adaptation establishes that selected changed definitions
can reuse earlier realizations \cite{GuptaEtAl2001Adapt}.  P9 adds branch and
cross-artifact context, but must still prove or test each reuse rule.

\section{Limitations and exact nonclaims}
\label{sec:limitations}

The current design has several hard boundaries.

\subsection{Semantic limitations}

The proposed stable IDs require governance.  They do not prove that two
revisions retain the same meaning, and they do not resolve independently
assigned IDs across administrative domains.  The initial data diff assumes
finite keyed data.  Records without stable keys remain ambiguous or
unsupported.  The first operation-pair table is closed and will classify many
real changes as manual or unsupported.

Mapping semantics can be partial, lossy, ambiguous, and direction-sensitive.
A semantic merge cannot reconstruct stakeholder intent that was never
recorded.  A state-derived diff reconstructs a state relation, not the
historical operation or the reason for it.  Inferred explanations remain
hypotheses.

Branch-local validation does not imply merge compatibility.  Pairwise
commutativity does not imply that the final state satisfies global
constraints.  The complete validator and dependency registry become part of
the trusted computing base for automatic merge.

\subsection{Systems limitations}

The local proposal does not supply distributed convergence, causal
consistency, consensus, or a CAP result.  Those questions depend on P10 and
P11 after P9 freezes the operation algebra.  SQLite failpoint evidence would
not establish PostgreSQL, object-store, or distributed durability.  A
process-kill matrix cannot simulate every filesystem, kernel, power, or
hardware failure.

Atomic reference publication does not atomically reverse or coordinate
external source effects.  Write-through and compensation require P8 and
backend-specific protocols.  Garbage collection conflicts with retention,
legal deletion, and audit requirements; the design does not solve that policy
problem.

\subsection{Formal limitations}

The proposed Lean fragment covers finite pure representations and selected
laws.  It excludes codecs, cryptographic assumptions, storage, authorization,
external provenance, probabilistic reconciliation, and performance.  Haskell
property tests would supply computational evidence, not proof.  A kernel
checked theorem would not verify the Rust implementation unless a separately
verified correspondence were established.

\subsection{Experimental limitations}

Decibel and ORPHEUSDB may require reconstructed baselines.  Generated version
histories may not reflect real organizational conflicts.  Stable keys make the
first profile easier than general entity resolution.  A richer conflict
classifier may produce too many false positives.  Human participants may
learn the classifier or differ sharply in expertise.  A dependency oracle
could repeat the implementation's assumptions.  One backend, graph shape, or
conflict mix cannot support a universal performance claim.

\subsection{Exact nonclaims}

The paper does not claim:

\begin{enumerate}
  \item that Git file diff is a semantic database merge;
  \item invention of database branching, dataset version control, schema
  versioning, mapping adaptation, temporal query, provenance, or data
  citation;
  \item that stable logical IDs prove semantic continuity;
  \item that a digest proves equivalence, truth, authorship, authority,
  completeness, or availability;
  \item recovery of unrecorded intent from a typed diff;
  \item that an inferred change explanation is authoritative history;
  \item safety of unknown operation pairs;
  \item automatic resolution of every semantic conflict;
  \item total, lossless, unambiguous, invertible, or writable mappings;
  \item that vector similarity establishes canonical identity;
  \item that provenance proves the correctness of a source, mapping, decision,
  or result;
  \item that stored materialization bytes are authoritative meaning;
  \item reproducibility from a semantic commit ID alone;
  \item equivalence of state reconstruction, query replay, and exact result
  reproduction;
  \item permanent recovery after lawful deletion or expired retention;
  \item reversal of external effects through ref rollback;
  \item compatibility or equal credibility of alternative branches;
  \item that every workspace merge is a categorical pushout;
  \item distributed convergence or elimination of coordination tradeoffs;
  \item that SQLite evidence transfers to every backend;
  \item that Haskell tests are Lean proofs;
  \item that finite Lean theorems verify the production runtime;
  \item that reconstructed baselines inherit published performance;
  \item that CatDB-only cases reveal defects in systems that never claimed
  those semantics; or
  \item any current publishable P9 implementation or performance result.
\end{enumerate}

\section{Open questions}
\label{sec:open}

\subsection{Profile and identity}

\begin{itemize}
  \item Which P3 migration operators can appear in the first overlay profile?
  \item What is P4's canonical equivalence for mappings, and how does it encode
  ambiguity?
  \item Which P6 materialization statuses and reuse rules are authoritative
  inputs?
  \item What exact P7 decision and reversal projection enters a commit?
  \item What completeness and retention structure does P13 expose?
  \item When may a logical identity cross a namespace or administrative
  domain?
  \item How are forked assignments of one logical ID reconciled?
\end{itemize}

The first five questions are \obstructed{} by prerequisite papers.  The
remaining questions are \openstatus{}.

\subsection{Diff and dependency}

\begin{itemize}
  \item Can impact soundness be proved for the selected dependency language?
  \item How are inferred dependencies shown without making them authoritative?
  \item What precision keeps impact review and recomputation usable?
  \item Which query and connector properties affect semantic identity rather
  than only reproducibility?
\end{itemize}

\subsection{Merge}

\begin{itemize}
  \item What is the complete first operation-pair table?
  \item Which rules are proved, dynamically checked, or only tested?
  \item How is a merge base selected when ancestry has several candidates?
  \item Which parent roles make merge intentionally asymmetric?
  \item How are policy changes authorized during merge?
  \item What happens when the validation procedure changes between branches?
  \item What should the result be when both branches validate independently
  but violate a global trust or retention rule when combined?
\end{itemize}

\subsection{Storage, history, and evaluation}

\begin{itemize}
  \item Should the first store use normalized relations, content-addressed
  blobs, or a hybrid?
  \item What durability assumptions are made about SQLite and the filesystem?
  \item How long are unreachable complete commits retained after failed
  publication?
  \item Which operations have inverses, compensation, or no safe reversal?
  \item How can lawful deletion coexist with content-addressed history?
  \item Which backend-version changes preserve semantic equivalence?
  \item Can original Decibel and ORPHEUSDB artifacts run in a pinned current
  environment?
  \item Which cross-object cases occur often enough to support external
  validity?
\end{itemize}

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

Database version control already has serious systems work behind it.  Schema
evolution, mapping adaptation, temporal query, provenance, and dynamic data
citation do too.  CatDB should not rename those results and call the bundle
new.

The remaining question is narrower and testable.  Can a database commit bind
schemas, mappings, migrations, data observations, identity decisions,
provenance requirements, policies, queries, and materialization definitions
closely enough to support conservative diff and merge?  The design in this
paper answers with a partial contract.  It separates five identity layers and
five diff layers.  It requires typed dependency impact, closed merge rules,
complete candidate validation, explicit reconciliation, and atomic reference
publication.  It also keeps reconstruction, replay, and reproduction apart.

None of that behavior exists in the current CatDB repository.  CR-069 remains
\proposed{}; \code{SYS-WS-01}, \code{SYS-WS-02}, and \code{SYS-WS-03} remain
\openstatus{}; the first formal and experimental slices remain
\obstructed{}.  The next useful step is not stronger prose.  It is a frozen
finite profile followed by adversarial fixtures, independent Haskell and Rust
results, selected Lean obligations, an atomic SQLite reference store, and a
fair D7 evaluation.

If those gates pass, CatDB may support a defensible systems claim: alternative
semantic interpretations can coexist under explicit context, and some
cross-object changes can be diffed and merged safely under a reviewed finite
profile.  If the gates fail, the claim must narrow.  The design is meant to
make either outcome visible.

\appendix

\section{Fixture and counterexample families}
\label{app:fixtures}

Workspace cases require a new immutable fixture-schema version.  Version 1
must remain unchanged.  Expected outcomes are closed:
\code{ok}, \code{conflict}, \code{reconciliation-required}, \code{blocked},
\code{error}, \code{unsupported}, or \code{crash-recovery}.  Free-form
exceptions and skipped cases fail the fixture.

\begin{longtable}{L{0.18\textwidth}L{0.33\textwidth}L{0.35\textwidth}}
\caption{Representative fixture families.}
\label{tab:fixtures}\\
\toprule
Family & Case & Expected result \\
\midrule
\endfirsthead
\toprule
Family & Case & Expected result \\
\midrule
\endhead
\code{WS-COMMIT} &
permuted set-like members; changed profile; missing inherited artifact;
digest mismatch &
stable canonical ID; domain separation; completeness/integrity errors \\
\code{WS-ID} &
explicit rename; remove/add lookalike; copy; split; merge; content-equal
import &
declared continuity only; new IDs otherwise; missing-policy block \\
\code{WS-OV} &
independent inserts; repeated updates; add/retract; rekey/update; identity
merge with aggregate &
overlay and materialized data/provenance equality or typed conflict \\
\code{WS-ISO} &
branch-local row, decision, validation, approval, and shared-cache schedules &
no cross-workspace observation without explicit import \\
\code{WS-DIFF} &
retained operations; state-only reconstruction; rename versus remove/add;
wildcard query; removed dependency edge &
exact reconstruction, evidence separation, and mutation-detected omission \\
\code{WS-MRG} &
disjoint additions; path/path conflict; delete/use; local commutativity with
global uniqueness failure; stale ref; unknown pair &
validated merge, typed conflict, CAS failure, or exact unsupported outcome \\
\code{WS-REC} &
confirmed same versus different; unauthorized decision; supersession;
reversal after lossy aggregate &
reconciliation, authority rejection, preserved history, partial compensation
\\
\code{WS-PROV} &
stricter profile; missing evidence; retention expiry; redaction; equal data
with different provenance &
blocked, incomplete, unavailable, redacted, or non-exact reproduction \\
\code{WS-MAT} &
unrelated change; mapping value change; schema rename; frontier skew; stale
cache advertised current &
reuse, adaptation, invalidation, stale status, or validation failure \\
\code{WS-HIST} &
retained environment; new plan; current query on old commit; missing API
response; changed collation; deleted restricted input &
exact, reconstructed, explicit mismatch, unavailable, or nondeterministic \\
\code{WS-RB} &
ref move; total inverse; lossy operation; abandoned draft; external API write
&
recorded rollback, new revert, compensation required, or external effect
preserved \\
\code{WS-CRASH} &
kill before/after staging, commit, CAS, and acknowledgement; concurrent
publishers &
old complete or new complete ref only; one concurrent winner \\
\code{WS-ALT} &
gross/net mapping; same/different identity; strict/permissive trust; explicit
comparison and promotion &
isolated context-labelled results and authority-bearing promotion \\
\bottomrule
\end{longtable}

Acceptance first validates the closed representation, then compares canonical
envelopes, Haskell, Rust, and any Lean-linked law.  Mutation tests remove
dependency, authority, validation, or provenance checks.  Crash fixtures run
in disposable databases.  Every failure is preserved under a run ID.

\section{Operation-pair policy sketch}
\label{app:pair-policy}

\Cref{tab:pair-policy} is illustrative.  It is not the frozen first profile.

\begin{longtable}{L{0.22\textwidth}L{0.22\textwidth}L{0.43\textwidth}}
\caption{Illustrative operation-pair outcomes.}
\label{tab:pair-policy}\\
\toprule
Left operation & Right operation & Required classification \\
\midrule
\endfirsthead
\toprule
Left operation & Right operation & Required classification \\
\midrule
\endhead
add object \(A\) & add object \(B\) &
candidate independent if IDs, constraints, and dependencies are disjoint;
full validation still required \\
rename object \(A\) & add unrelated object \(B\) &
candidate independent only when rename continuity is explicit and no
wildcard dependency observes labels \\
remove attribute \(f\) & replace mapping image with path using \(f\) &
schema/mapping conflict \\
retype attribute \(f\) & keyed row update to \(f\) &
revalidate value-domain conversion; conflict or migration required \\
add equation & add equation &
candidate merge, followed by global consistency and data validation \\
confirm same \(x,y\) & confirm different \(x,y\) &
reconciliation-required contradiction \\
confirm same \(x,y\) & refresh dependent aggregate &
order-dependent unless refresh is recomputed after effective decision \\
strengthen provenance profile & expire supporting source &
retention/provenance conflict \\
change query definition & reuse old materialization &
validated adaptation, rebuild, or invalid \\
physical plan change & equal semantic definition &
execution-strategy choice, not semantic conflict \\
opaque transform & any semantic structural change &
unsupported/manual unless the exact pair gains a reviewed rule \\
\bottomrule
\end{longtable}

\section{Claim-to-evidence matrix}
\label{app:claims}

\begin{longtable}{L{0.12\textwidth}L{0.22\textwidth}L{0.23\textwidth}L{0.25\textwidth}}
\caption{Claim anchors, evidence, and present status.}
\label{tab:claim-matrix}\\
\toprule
Anchor & Program link & Required evidence & Present status \\
\midrule
\endfirsthead
\toprule
Anchor & Program link & Required evidence & Present status \\
\midrule
\endhead
P9-C01 & commit identity &
cross-language canonical fixtures & \openstatus{} \\
P9-C02 & CR-069, SYS-WS-01 &
equivalence fixtures and selected proof & \obstructed{} \\
P9-C03 & CR-069, SYS-WS-02 &
concurrent isolation schedules & \openstatus{} \\
P9-C04 & semantic diff &
reconstruction and mutation tests & \openstatus{} \\
P9-C05 & dependency impact &
formal fragment and seeded faults & \obstructed{} \\
P9-C06 & automatic merge &
closed exhaustive pair table and property tests & \obstructed{} \\
P9-C07 & CR-045, SYS-WS-03 &
storage argument and failpoint recovery & \openstatus{} \\
P9-C08 & conflict taxonomy &
blinded seeded corpus and confusion matrix & \obstructed{} \\
P9-C09 & P7/P9/P13 integration &
decision, contradiction, and reversal fixtures & \obstructed{} \\
P9-C10 & historical query &
retained and missing-input replay runs & \obstructed{} \\
P9-C11 & interpretation branches &
paired scenarios and provenance audit & \obstructed{} \\
P9-C12 & rollback &
semantic, storage, and compensation tests & \openstatus{} \\
P9-C13 & systems value &
fair baselines and preregistered reviewer study & \openstatus{} \\
\bottomrule
\end{longtable}

\section{Reproducibility artifact schema}
\label{app:repro}

A confirmatory run should contain:

\begin{lstlisting}
benchmarks/runs/<run_id>/
  manifest.json
  preregistration.md
  source-lock.json
  environment.json
  baseline-status.json
  fixtures/
  raw/
  workspace-results.jsonl
  crash-results.jsonl
  reproduction-results.jsonl
  classifier-confusion.json
  statistics.json
  failures/
  checksums.sha256
\end{lstlisting}

The manifest records repository revision and dirty state, fixture and profile
versions, Rust/Haskell/Lean versions, database and operating-system versions,
baseline source or reconstruction status, hardware, seeds, execution order,
warmup and repetition policy, exclusions, failed runs, analysis digest, and
review sign-off.

Before a future manuscript promotes a claim:

\begin{itemize}
  \item dependency contracts and the workspace profile must be frozen;
  \item immutable fixtures and counterexamples must be committed;
  \item Rust and Haskell results must agree;
  \item Lean coverage must name only kernel-checked declarations;
  \item \code{SYS-WS-01} through \code{SYS-WS-03} must pass;
  \item every unknown pair must remain explicit;
  \item materialization and provenance invalidation must be audited;
  \item historical status must be tested with missing inputs;
  \item baseline artifact status must be explicit; and
  \item all failures, raw observations, statistics, and checksums must
  reproduce.
\end{itemize}

\bibliographystyle{plainnat}
\bibliography{references}

\end{document}
