\documentclass[12pt]{article}

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

\hypersetup{
  colorlinks=true,
  linkcolor=blue!45!black,
  citecolor=green!35!black,
  urlcolor=blue!55!black,
  pdftitle={Incremental Semantic Materialization: Maintaining Integrated Views under Schema and Data Change},
  pdfauthor={Matthew Long; The YonedaAI Collaboration}
}

\newtheorem{definition}{Definition}[section]
\newtheorem{obligation}[definition]{Obligation}
\theoremstyle{remark}
\newtheorem{example}[definition]{Example}
\newtheorem{remark}[definition]{Remark}

\newcommand{\CatDB}{{\normalfont\textsc{CatDB}}}
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\ev}[1]{{\normalfont\textsc{#1}}}
\newcommand{\prior}{\ev{SUPPORTED BY PRIOR LITERATURE}}
\newcommand{\enghyp}{\ev{ENGINEERING HYPOTHESIS}}
\newcommand{\openconj}{\ev{OPEN CONJECTURE}}
\newcommand{\openstatus}{\ev{OPEN}}
\newcommand{\obstructed}{\ev{OBSTRUCTED}}
\newcommand{\status}[1]{\par\noindent{\normalfont\textit{Evidence status.} #1.}\par}
\newcommand{\Full}{\mathsf{Full}}
\newcommand{\Norm}{\mathsf{Normalize}}
\newcommand{\DataEval}{\mathsf{DataEval}}
\newcommand{\ProvEval}{\mathsf{ProvEval}}
\newcommand{\Observe}{\mathsf{Observe}}
\newcommand{\Impact}{\mathsf{Impact}}
\newcommand{\Affected}{\mathsf{SemanticAffected}}
\newcommand{\DefId}{\mathsf{DefId}}
\newcommand{\PlanId}{\mathsf{PlanId}}
\newcommand{\RelJoin}{\mathbin{\bowtie}}
\newcommand{\Bag}{\mathsf{Bag}}
\newcolumntype{L}[1]{>{\RaggedRight\arraybackslash}p{#1}}
\newcolumntype{Y}{>{\RaggedRight\arraybackslash}X}

\setlength{\emergencystretch}{4em}
\setlist{itemsep=0.25em,topsep=0.4em}
\raggedbottom
\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-incremental-materialization\quad
       [\,cs.DB\,]\quad
       23 Jul 2026};
    \end{tikzpicture}
  \fi
}

\title{Incremental Semantic Materialization:\\
Maintaining Integrated Views under Schema and Data Change}
\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}
An integrated view can change even when no new source row arrives.  A source
schema can change, a source-to-domain mapping can gain a new conversion, an
identity decision can be reversed, or a provenance policy can require evidence
that an old materialization did not retain.  Conventional incremental view
maintenance provides mature techniques for data deltas.  Those techniques
alone do not decide whether old state still has the same meaning after a
semantic change.

We give a provisional semantics and systems contract for incremental
materialization in \CatDB{}.  Its authoritative object is an immutable
materialization definition that binds schema, mapping, query, reconciliation,
provenance, scalar-semantics, coverage, and consistency revisions.  A physical
realization also records a plan, per-source frontiers, auxiliary state, a
dependency graph, and a checkpoint.  For a deliberately small positive bag
algebra, we state the established first-order delta laws.  We then state the
stronger \CatDB{} obligation: normalized data and provenance after incremental
maintenance must equal independent full recomputation at the same semantic
definition and declared source frontier.  Some data changes may admit deltas.
Schema, mapping, reconciliation, provenance-policy, and capability changes
instead pass through a typed dependency and invalidation decision.  Reuse is
permitted only by a named adaptation rule; otherwise the exact treatment is
rebuild or rejection.

This version contributes a falsifiable design, not an implemented result.
Classical incremental maintenance, self-maintainable views, lazy
refresh, view adaptation, DBToaster, differential dataflow, DBSP, Noria,
change-data capture, transactional streaming, distributed snapshots, and
provenance semirings are established prior art.  The current repository has no
\code{catdb-materialization} crate, full or incremental evaluator, P6 fixture
family, source-change connector, crash failpoint harness, Haskell oracle, Lean
P6 declaration, or benchmark run.  All CatDB equivalence, cursor safety,
recovery, provenance, and performance claims therefore remain \openstatus{} or
\obstructed{}.  In particular, this paper reports no exactly-once guarantee,
no transactional cursor result, no crash-recovery result, no formal proof of a
CatDB maintenance algorithm, and no performance result.
\end{abstract}

\tableofcontents

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

\subsection{A corrected order is the easy case}

Consider two source systems that contribute orders to a canonical
\code{CustomerRevenue} view.  The PostgreSQL source reports amounts in cents.
A periodic CSV snapshot stores decimal text.  Versioned mappings convert both
representations, while a reconciliation policy connects source-local customer
identifiers to canonical customers.  The view groups accepted orders by
canonical identity.

A correction changes one PostgreSQL order from 2,500 to 3,000 cents.  A local
delta is straightforward: subtract the old contribution and add the new one.
That rule no longer settles the matter if the correction is replayed after a
crash, the mapping changes from gross to net revenue, the reconciliation
policy splits a customer that had been merged, or the provenance profile
begins requiring the origin of a newly used refund field.  Each event changes
the maintenance problem differently.  A row-level merge statement cannot
tell the system which old state remains valid.

There is also no single obvious meaning of ``now.''  PostgreSQL may be applied
through one log sequence number while the CSV source remains at
\code{snapshot-8}.  Together they form a vector of observations, not evidence
for a simultaneous distributed snapshot.  A display that says only
``refreshed at 14:03'' hides whether a source is missing, a log gap exists, a
new definition is rebuilding, or the data is current while required
provenance is not.

This leaves a narrow question:

\begin{quote}
How should a mapped view respond to data, schema, mapping, identity,
provenance-policy, coverage, and execution-capability changes without letting
its physical cache become the authoritative definition of meaning?
\end{quote}

\subsection{Thesis and boundary}

The candidate thesis is:

\begin{quote}
For an explicitly supported operator fragment, a versioned semantic
definition, a declared source-capture profile, and a recoverable checkpoint
protocol, \CatDB{} can compile a materialization strategy that updates
affected state after admitted data changes and conservatively invalidates or
rebuilds state after semantic changes.  Correctness requires agreement with
independent full recomputation for normalized data and provenance at the same
declared source frontier.
\end{quote}

This thesis is an \enghyp{}, not evidence of an implementation.  Incremental
view maintenance is established and covers a broad range of cases
\cite{GuptaMumickSubrahmanian1993,GuptaMumick1995,GriffinLibkin1995}.
Higher-order and automatically derived deltas, partially ordered
incrementality, and shared partial state are also established
\cite{AhmadEtAl2012,McSherryEtAl2013,BudiuEtAl2023,GjengsetEtAl2018}.
The possible \CatDB{} delta lies in binding those execution techniques to
typed, immutable semantic revisions and using explicit dependencies to decide
when a data-delta plan remains applicable.

\subsection{Research questions}

The paper organizes the program around five questions:

\begin{enumerate}
  \item Which finite query and change fragment admits an independent
  full-recomputation oracle and exact delta maintenance?
  \item How should dependency information connect source schemas, mappings,
  queries, reconciliation, provenance, coverage, capabilities, and physical
  state?
  \item Which source, sink, cursor, and checkpoint contracts prevent a
  published position from outrunning durable effects?
  \item Which semantic changes admit validated adaptation, and which must
  invalidate, rebuild, or block?
  \item Under which workload regions, if any, does incremental maintenance
  reduce work or latency after auxiliary state, provenance, recovery, and
  source-history costs are included?
\end{enumerate}

\subsection{Contributions of this author pass}

This manuscript contributes:

\begin{enumerate}
  \item an immutable materialization-definition model that separates
  denotation from a replaceable physical realization;
  \item a source-change envelope, per-source frontier model, and explicit
  status vocabulary;
  \item a bounded positive bag-algebra fragment with stated delta and
  auxiliary-state obligations;
  \item a typed dependency graph and a conservative decision lattice for data
  and semantic changes;
  \item a cursor/checkpoint safety condition, a crash matrix, and
  snapshot-to-stream cutover contract;
  \item a multidimensional freshness envelope;
  \item a prior-art and novelty boundary; and
  \item implementation, formalization, and experimental plans with named
  falsifiers.
\end{enumerate}

These are specification artifacts.  No item is presented as a working P6
system result.

\subsection{Exact nonclaims}

\CatDB{} does not currently claim that it eliminates ETL, data movement, full
recomputation, staleness, source coordination, or distributed-systems
tradeoffs.  It does not claim to incrementalize every query or arbitrary
schema and mapping change.  It does not infer missing before-images or treat
independent source positions as a global snapshot.  It does not claim generic
exactly-once delivery or an atomic transaction across unrelated sources and
sinks.  It does not claim that materialization is free, that provenance is
free, that retained state always admits reuse, or that category theory proves
an execution protocol correct.

\section{Evidence vocabulary and prerequisite boundary}
\label{sec:evidence}

\subsection{Labels}

\Cref{tab:evidence-labels} fixes how claims are read.  A result supported in a
different system remains prior literature, not a \CatDB{} result.  A decoded
record is not evidence that its intended state transition works.

\begin{table}[ht]
\centering
\small
\caption{Evidence labels used by this manuscript.}
\label{tab:evidence-labels}
\begin{tabularx}{\textwidth}{L{0.25\textwidth}Y}
\toprule
Label & Meaning \\
\midrule
\prior & A primary paper, standard, or official system document establishes
the stated result or capability within its own assumptions. \\
\enghyp & A proposed \CatDB{} behavior that still needs implementation and
experiment. \\
\openconj & A mathematical statement without a completed proof for the
declared fragment. \\
\openstatus & Required definitions, code, fixtures, experiments, or review
are incomplete. \\
\obstructed & A prerequisite semantic boundary is missing, so a claim cannot
yet be implemented or tested honestly. \\
\bottomrule
\end{tabularx}
\end{table}

No P6 claim in this manuscript is labelled proved, machine-checked,
computational, or experimentally supported.  DBSP's mechanized core does not
verify a future \CatDB{} compiler \cite{BudiuEtAl2023}.  PostgreSQL logical
decoding does not make a future \CatDB{} checkpoint atomic
\cite{PostgresLogicalDecoding2026}.  Equality of materialized rows would not
by itself establish equality of provenance.

\subsection{Blocking paper contracts}

P6 depends on four other CatDB papers:

\begin{itemize}
  \item P2 must define logical-query denotation, normalization, capabilities,
  and the semantic-to-physical plan boundary.
  \item P4 must define read-direction mapping semantics, coverage,
  partiality, information loss, conversion, and composition.
  \item P5 must define source observations, connector capabilities, source
  coverage, snapshot policy, partial availability, and result reconciliation.
  \item P13 must define normalized data provenance, retention, completeness,
  and equality for full and incremental paths.
\end{itemize}

Those contracts are not frozen.  Consequently, data and provenance
equivalence, safe mapping adaptation, and strategy interchangeability are
\obstructed{}.  A P6 implementation can begin around isolated source and
checkpoint types, but it cannot close the central claim until these
dependencies are explicit.

\subsection{Current repository audit}

The repository contains typed schema, path, mapping, and a small migration
slice across Rust, Haskell, Lean, and shared fixtures.  Those are prerequisites
only.  At the time of this author pass, the repository does not contain:

\begin{itemize}
  \item a \code{catdb-materialization} crate;
  \item a logical query evaluator or P6 full-recomputation oracle;
  \item a change envelope, dependency extractor, delta compiler, invalidator,
  or auxiliary aggregate store;
  \item PostgreSQL logical-slot or SQLite session-extension integration;
  \item checkpoint publication, applied-effect state, or process-kill
  failpoints;
  \item initial snapshot and change-stream cutover;
  \item freshness responses or a materialization API;
  \item incremental provenance semantics;
  \item P6 Haskell modules or Lean declarations;
  \item P6 fixtures, raw runs, or benchmarks; or
  \item terminal P6 paper review.
\end{itemize}

The current system gate \code{SYS-MAT-01} and claim \code{CR-063} therefore
remain \openstatus{} and unresolved respectively.

\section{Semantic model}
\label{sec:model}

\subsection{Authoritative definition}

\begin{definition}[Materialization definition]
A materialization definition is the immutable tuple
\[
\mathcal D=(S,M,Q,R,P,\Lambda,A),
\]
where \(S\) is a vector of source-schema revisions, \(M\) is a versioned
read-mapping bundle, \(Q\) is a typed canonical query, \(R\) is a
reconciliation and authority policy, \(P\) is a provenance and retention
profile, \(\Lambda\) fixes scalar and error semantics, and \(A\) fixes source
coverage, availability, and consistency policy.
\end{definition}

The definition identifier is a deterministic content digest:
\[
\DefId=H(S,M,Q,R,P,\Lambda,A).
\]
The future repository must specify the serialization and hash domain.  The
equation is a design requirement, not evidence that content addressing is
implemented.

Connector capability manifest \(C\) and physical plan \(L\) are versioned
execution inputs.  They may change how \(\mathcal D\) is evaluated.  They may
not silently change what \(Q\) means.  Every result binds both the semantic
definition and the execution revisions used to compute it.

\subsection{Source observation and full semantics}

\begin{definition}[Source frontier]
A source frontier \(f_s\) identifies one stream, a source-specific position,
its completeness class, and the time at which \CatDB{} observed it.  A
multi-source frontier is the vector \(f=\{s\mapsto f_s\}\).
\end{definition}

Positions can be PostgreSQL log sequence numbers, Kafka partition offsets,
SQLite changeset identities, API delta tokens, file-snapshot digests, or other
declared values.  Comparison is valid only within the same source, stream, and
ordering profile.  The vector does not imply a distributed transaction or
simultaneous snapshot.  Distributed snapshot algorithms require explicit
channel and process assumptions \cite{ChandyLamport1985}.

For definition \(\mathcal D\) and the actual input observation \(I_f\), the
authoritative reference is
\[
\Full(\mathcal D,I_f)
=
\Norm\left(
  \DataEval(\mathcal D,I_f),
  \ProvEval(\mathcal D,I_f)
\right).
\]
Normalization must fix bag or set semantics, duplicates, null and missing
values, decimals, time zones, collation, errors, row identity, source-token
identity, provenance normalization, completeness, and any relevant ordering.
The independent full evaluator may not call the same delta compiler as the
incremental path.

\subsection{Replaceable realization}

\begin{definition}[Materialization realization]
A physical realization is
\[
\mathcal X=(\DefId,\PlanId,f,V,U,G,K,\sigma),
\]
where \(V\) is materialized output, \(U\) is auxiliary incremental state,
\(G\) is a dependency-graph revision, \(K\) is the latest durable checkpoint,
and \(\sigma\) is the status.
\end{definition}

The realization may be deleted, rebuilt, or replaced if retained sources and
the immutable definition permit reproduction.  Generated SQL, task logs,
indexes, cached batches, and physical tables are execution artifacts.  If a
manual patch adds semantic logic only to generated SQL, the realization has
left the managed correctness boundary.

\subsection{Incremental correctness obligation}

Let \(J\) be a candidate incremental strategy, \(X\) its old state, and
\(\Delta\) an admitted change.  The post-change definition and frontier are
\(\mathcal D'\) and \(f'\).  Exact incremental mode requires:
\[
\Norm\!\left(\Observe(J(X,\Delta))\right)
=
\Full(\mathcal D',I_{f'}).
\]
The equality includes normalized data, provenance, definition identity,
frontier, completeness, and status.

\begin{obligation}[Data equivalence]
Every admitted incremental history must produce the same normalized bag
result as independent full recomputation at the same definition and frontier.
\end{obligation}

\begin{obligation}[Provenance equivalence]
Every admitted incremental history must produce the same normalized P13
provenance as full recomputation.  Matching row values alone is insufficient.
\end{obligation}

\begin{obligation}[Strategy separability]
Federation, full recomputation, eager delta maintenance, lazy maintenance,
partition rebuild, and validated reuse may implement one semantic definition
only where their normalized result envelopes agree.
\end{obligation}

All three obligations are \obstructed{}.  There is no current evaluator,
provenance profile, fixture corpus, or cross-strategy comparison.

\subsection{Status vocabulary}

\begin{table}[ht]
\centering
\small
\caption{Candidate realization statuses.}
\label{tab:statuses}
\begin{tabularx}{\textwidth}{L{0.18\textwidth}Y}
\toprule
Status & Meaning \\
\midrule
\code{building} & Initial snapshot or full recomputation is incomplete. \\
\code{fresh} & All required declared frontiers are applied under the active
definition. \\
\code{stale} & Known source or semantic changes are not applied. \\
\code{partial} & Only a declared subset of required sources or evidence is
present. \\
\code{invalid} & The realization cannot answer under its bound definition. \\
\code{rebuilding} & A replacement realization is being computed. \\
\code{recovering} & Replay or checkpoint repair is in progress. \\
\code{blocked} & Missing history, capability, schema, or policy prevents
repair. \\
\code{unknown} & Progress or completeness cannot be established. \\
\bottomrule
\end{tabularx}
\end{table}

``Fresh'' is relative to a definition and frontier.  It does not mean merely
that a worker ran recently.

\section{Change model}
\label{sec:changes}

\subsection{Change envelopes}

An admitted source event needs more structure than an operation name and row
body.  The candidate record is:

\begin{lstlisting}
ChangeEnvelopeV1 {
  source_id
  source_schema_revision
  capture_profile_revision
  stream_or_snapshot_id
  source_transaction_id?
  source_position
  event_ordinal?
  event_id?
  operation
  relation_id
  key_before?
  key_after?
  row_before?
  row_after?
  source_commit_time?
  observed_time
  provenance_token
}
\end{lstlisting}

Optional fields determine which computations are possible.  A delete without
an old key cannot reliably retract a keyed join contribution.  An update that
changes a key is not equivalent to an update of a non-key attribute.  An event
identifier can support deduplication, but it does not make the output update,
auxiliary state, provenance, and cursor publication atomic.

The initial operation vocabulary includes snapshot boundaries and reads,
insert, delete, update, truncate, source transaction boundaries, heartbeat,
schema marker, and gap.  A heartbeat establishes liveness only within its
connector profile.  A gap states that required incremental history is no
longer available.  Exact mode then stops and reboots from a new declared
snapshot or returns a blocked state.

\subsection{Capture profile}

Each connector supplies an immutable capture profile:

\begin{lstlisting}
CaptureProfileV1 {
  source
  position_kind
  ordering
  delivery
  transaction_boundaries
  row_images
  ddl_capture
  gap_detection
}
\end{lstlisting}

The conservative v1 profile is at-least-once delivery, complete source
transaction order, permitted duplicates, no transaction fragmentation, and
fatal gaps.  Out-of-order and late events require an explicit buffer, repair,
rejection, or logical-time policy.  Arrival order is not a semantic ordering
rule.

PostgreSQL makes old-row availability depend on replica identity and can
replay recent changes after a crash because slot position persistence is
checkpointed \cite{PostgresLogicalDecoding2026,PostgresPublication2026}.
SQLite changesets preserve keyed old and new values under documented
conditions, while patchsets retain less information
\cite{SQLiteSession2026}.  The ordinary SQLite update hook omits important
cases and has no suitable general CDC contract \cite{SQLiteUpdateHook2026}.
These facts justify connector-specific profiles.  They do not establish that
\CatDB{} has implemented either profile.

\subsection{Data changes and semantic changes}

\Cref{tab:change-taxonomy} separates data events from changes that alter the
view's meaning or the evidence required to justify it.

\begin{landscape}
\begin{longtable}{L{0.16\linewidth}L{0.21\linewidth}L{0.25\linewidth}L{0.27\linewidth}}
\caption{Candidate change classification and conservative treatment.}
\label{tab:change-taxonomy}\\
\toprule
Class & Example & Default treatment & Condition for reuse \\
\midrule
\endfirsthead
\toprule
Class & Example & Default treatment & Condition for reuse \\
\midrule
\endhead
data insert & new order & delta & admitted operator and complete keyed event \\
data delete & removed order & delta or rebuild & old key and every required old
value available \\
data update & amount or key changes & old retraction plus new insertion, or
declared direct delta & before/after and key semantics fixed \\
truncate & relation cleared & bulk invalidation or explicit truncate delta &
exact source coverage and dependency scope \\
duplicate & replayed transaction & deduplicate or idempotently reapply &
stable effect identity and one sink transaction \\
out of order & earlier source position arrives late & reorder, repair, reject,
or use an admitted time domain & source ordering profile supports the choice \\
source schema & field add, drop, type, key, or equation change & revalidate,
usually invalidate & dependency proof and conversion rule \\
mapping & gross-to-net conversion & invalidate affected dependency slice &
named adaptation rule and full oracle \\
query & new filter or grouping & adapt or rebuild & retained state is
sufficient and equality passes \\
reconciliation & identity merge or split & affected-identity recomputation &
complete reverse dependency index \\
provenance policy & require field origin & provenance rebuild, possibly data
rebuild & retained evidence derives the stricter profile \\
coverage or authority & source becomes optional or nonauthoritative & new
definition and invalidation & exact subtraction of old contribution \\
capability & before-images disappear or pushdown changes & stop/replan/reboot &
logical semantics and in-flight boundary preserved \\
runtime & new delta compiler & shadow verify before promotion & deterministic
fixture and oracle equivalence \\
\bottomrule
\end{longtable}
\end{landscape}

The size of a text diff is not a safe impact estimate.  A one-character unit
change can alter every output value.  Conversely, an added nullable source
field may be irrelevant if the capture, wildcard, provenance, mapping, and
query dependencies all exclude it.

\section{A bounded differential fragment}
\label{sec:deltas}

\subsection{Signed bags}

Classical IVM already handles inserts, deletes, updates, duplicates, joins,
aggregation, and broad SQL or Datalog fragments
\cite{GuptaMumickSubrahmanian1993,GuptaMumick1995,GriffinLibkin1995}.  This
paper chooses a smaller initial profile so that a separate full evaluator and
cross-language fixtures remain feasible.

Represent a bag relation by a finitely supported integer-valued function:
\[
R:\mathrm{Tuple}\to\mathbb Z.
\]
A signed change \(\Delta R\) updates it by
\[
R'=R+\Delta R.
\]
Intermediate deltas may contain negative multiplicities.  Every published
database state must have nonnegative final multiplicities.  A negative
published count is a diagnostic for an invalid history, a source gap, or an
implementation defect.

For query \(Q\), state \(I\), and admitted change \(\Delta I\), the established
data-level target is
\[
Q(I+\Delta I)=Q(I)+\Delta Q(I,\Delta I).
\]
This identity is \prior{} for classical incremental maintenance.  It is not a
proof that a future \CatDB{} compiler derives the right \(\Delta Q\).

\subsection{Selection, projection, and union}

For deterministic predicate \(p\),
\[
\Delta(\sigma_p R)=\sigma_p(\Delta R).
\]
The predicate is excluded if it depends on a volatile clock, unversioned
model, remote mutable lookup, locale not fixed by \(\Lambda\), or opaque code.

For bag projection,
\[
\Delta(\pi_A R)=\pi_A(\Delta R).
\]
Projection must preserve multiplicity.  A set-valued result instead needs
support counts so that removing one derivation does not remove an output still
supported by another derivation.

For bag union,
\[
\Delta(R\uplus S)=\Delta R\uplus\Delta S.
\]
Set union again needs counts of alternative support.  Counting is established
practice, not a \CatDB{} novelty
\cite{GuptaMumickSubrahmanian1993,GriffinLibkin1995}.

\subsection{Inner equijoin}

For a simultaneous batch against a declared pre-state convention:
\[
\Delta(R\RelJoin S)
=
(\Delta R\RelJoin S)
\uplus(R\RelJoin\Delta S)
\uplus(\Delta R\RelJoin\Delta S).
\]
The cross term matters when both sides change in the same logical batch.
Applying source events one at a time without a fixed pre-state, post-state, or
staging convention can omit or double-count that term.

At the provenance level, a positive-algebra join multiplies joint derivations
and union adds alternatives in semiring-style models
\cite{GreenEtAl2007}.  Retractions and canonical provenance normalization need
the exact P13 profile.  The preceding data identity therefore does not close
the provenance obligation.

\subsection{Initial aggregate boundary}

\begin{table}[ht]
\centering
\small
\caption{Auxiliary state and retraction concerns for candidate aggregates.}
\label{tab:aggregates}
\begin{tabularx}{\textwidth}{L{0.18\textwidth}L{0.30\textwidth}Y}
\toprule
Aggregate & Auxiliary state & Retraction concern \\
\midrule
\code{COUNT} & count per group & subtract multiplicity and remove empty group
under the declared zero policy \\
\code{SUM} & sum per group & subtract old contribution under a fixed numeric
and overflow profile \\
\code{AVG} & sum and count & define zero-count result and maintain both
components \\
\code{MIN}/\code{MAX} & ordered support multiset & deleting the extremum needs
the next candidate \\
\code{COUNT DISTINCT} & support count per distinct value & state can approach
or exceed the input projection \\
\bottomrule
\end{tabularx}
\end{table}

The proposed v1 admits \code{COUNT}, \code{SUM}, and \code{AVG}.  It excludes
\code{MIN}, \code{MAX}, and \code{COUNT DISTINCT} until memory, provenance,
numeric, and deletion semantics are specified.  An implementation may later
support them, but this manuscript does not rely on that possibility.

\subsection{Unsupported exact mode}

The first exact profile rejects arbitrary difference and negation, outer
joins, recursive queries, correlated subqueries, volatile functions, opaque
user code, external side effects, approximate vector search, unstable top-k,
floating-point rewrites without an equivalence profile, and any operator whose
provenance delta is undefined.

Richer fragments are possible and already appear in the literature.
DBToaster recursively materializes higher-order delta queries and uses costed
materialization \cite{AhmadEtAl2012}.  Differential dataflow maintains indexed
differences across partially ordered versions
\cite{McSherryEtAl2013}.  DBSP provides algebraic automatic
incrementalization for a rich language with mechanized core results
\cite{BudiuEtAl2023}.  A smaller CatDB fragment is an engineering choice that
makes its own oracle and failure boundary auditable.

\subsection{Auxiliary state is part of the cost}

An incremental plan must declare every required base lookup, index, support
count, aggregate component, retained input, provenance circuit, applied-effect
record, and pending batch.  Self-maintainable-view results show that avoiding
base access depends on the view and retained information
\cite{GuptaJagadishMumick1996}.  Incrementality may therefore trade update
latency for memory, write amplification, source-log retention, and recovery
work.  Those resources belong in the evaluation, not in an implementation
footnote.

\section{Dependency, invalidation, and adaptation}
\label{sec:dependency}

\subsection{Typed dependency graph}

The candidate graph contains more than relations and columns.  Its nodes
include source and canonical schema revisions, fields, paths, capture
profiles, mapping revisions and clauses, query revisions and logical
operators, reconciliation and identity decisions, authority and coverage
policies, provenance and retention profiles, capability manifests, physical
plans, auxiliary state, checkpoints, result partitions, and both definition
and realization identities.

Edges state roles such as:

\begin{lstlisting}
reads              types_against
maps_through       depends_on_clause
uses_identity      uses_authority
requires_coverage  requires_provenance
requires_capability
compiled_to        maintains
derived_from       checkpointed_at
invalidates        can_adapt_from
\end{lstlisting}

One untyped \code{depends-on} edge is too weak for selective invalidation.  The
system needs to distinguish whether a field contributes a displayed value, a
filter, a join key, a group key, an identity rule, a coverage decision,
provenance only, capture, or physical pushdown only.  Dependencies must be
extracted from typed IR.  SQL text search cannot reliably find stable semantic
identity, composed mapping clauses, or an opaque dependency.  An opaque
operator yields a wildcard edge or rejection.

\subsection{Soundness before minimality}

For change \(c\) and graph \(G\), the first obligation is:
\[
\Affected(c)\subseteq\Impact(c,G).
\]
The impact set may initially over-approximate.  Extra recomputation is a cost;
a missed dependency is an incorrect result.  Minimality is a later
optimization objective:
\[
\Impact(c,G)\approx\Affected(c).
\]

\begin{obligation}[Impact soundness]
For the frozen finite IR, every output whose normalized data, provenance,
status, or definition binding can change must be reachable from the change
through the dependency graph.
\end{obligation}

This obligation is an \openconj{} for a future formal fragment and an
\enghyp{} for a runtime.  It is \openstatus{} because no P6 graph or
invalidation algorithm exists.  A single mutation-generated false negative
would falsify it.

\subsection{Decision lattice}

A refresh decision selects one of:

\begin{lstlisting}
retain
replan_only
delta_update
adapt_from_old_state
invalidate_partition
invalidate_all
rebootstrap_source
blocked
\end{lstlisting}

The record stores the old and new definition identities, change identity,
affected graph slice, rule or proof identifier, needed source history,
freshness and provenance effects, fallback, and a reviewer-readable rationale.
Correctness filters candidate actions before a cost model ranks them.

\subsection{Reuse obligation}

Old state \(X_{\mathcal D}\) may be transformed for a new definition
\(\mathcal D'\) only if a named transformer \(T\) satisfies:
\[
\Norm\!\left(\Observe(T(X_{\mathcal D}))\right)
=
\Full(\mathcal D',I_f).
\]
Selected SQL view redefinitions can reuse old materializations and retained
extra information \cite{GuptaEtAl2001Adapt}.  That result does not authorize
universal reuse across categorical mappings, identity splits, authority
changes, or provenance profiles.

When no validated rule applies, exact mode marks the realization stale or
invalid, computes a replacement under \(\mathcal D'\), checks it against the
oracle, atomically publishes the new reference, and retains or removes the old
artifact according to policy.  Full recomputation is a safe strategy, not a
failure of the semantic model.

\subsection{Partition recomputation}

Partition-level repair needs a conservative affected-key function:
\[
\mathsf{KeysWhoseOutputChanges}(c,\mathcal D)
\subseteq
\mathsf{AffectedKeys}(c,\mathcal D).
\]
Candidate keys include canonical entity, tenant, source, time range,
provenance domain, and workspace.  Identity merges and splits can fan out
across joins and aggregates, so a customer-local source update does not imply
a customer-local semantic impact.  If reverse reachability is incomplete,
the correct treatment is a larger rebuild.

\section{Checkpoint and recovery contract}
\label{sec:recovery}

\subsection{Checkpoint state}

A candidate checkpoint is:

\begin{lstlisting}
MaterializationCheckpointV1 {
  checkpoint_id
  definition_id
  dependency_graph_id
  plan_id
  compiler_runtime_id
  parent_checkpoint_id?
  input_frontiers
  applied_batch_ids
  data_artifact_id
  auxiliary_state_artifact_ids
  provenance_artifact_id
  state_digest
  status
  staged_at
  committed_at?
}
\end{lstlisting}

It is valid only when output, auxiliary state, provenance, and applied source
positions name one durable boundary.  Async snapshots and stateful streaming
systems provide important precedents
\cite{CarboneEtAl2015,AkidauEtAl2013}.  A future \CatDB{} protocol must still
state its own source and sink assumptions.

\subsection{Cursor safety}

For every published position \(p\):
\[
\mathsf{Published}(p)
\Rightarrow
\mathsf{Durable}(\mathsf{EffectsThrough}(p)).
\]
The converse need not hold at every crash point.  Durable effects may exist
while the published cursor lags.  Recovery can then detect a staged effect or
replay idempotently.

The candidate external-source sequence is:

\begin{enumerate}
  \item durably ingest the event or retain a replayable source position;
  \item derive a stable batch and effect identity;
  \item stage output, auxiliary, and provenance updates;
  \item validate local invariants;
  \item commit effects and the local applied-position record together;
  \item publish the new realization reference;
  \item acknowledge upstream under the connector contract; and
  \item tolerate replay from the last acknowledged position.
\end{enumerate}

This is a proposed protocol.  No transactional cursor test has run.  When
source, sink, provenance, and cursor share one transactional database, one
implementation may commit them atomically.  Across PostgreSQL, Kafka, SQLite,
files, and APIs there is no generic transaction.  Kafka can atomically combine
Kafka output writes and consumer offsets inside its own transaction model, but
external sinks require participation or a separate protocol
\cite{KafkaDesign2026}.  This paper makes no exactly-once claim.

\subsection{Effect identity and replay}

A candidate stable effect identity is:
\[
\mathsf{EffectId}
=H(\DefId,\mathsf{SourceId},\mathsf{StreamId},
   \mathsf{TxId},\mathsf{Position},\mathsf{Ordinal}).
\]
At the observable checkpoint boundary, replay should satisfy:
\[
\mathsf{Apply}(e,\mathsf{Apply}(e,X))
=\mathsf{Apply}(e,X).
\]
Signed deltas themselves are additive and would normally double-apply.  The
runtime therefore needs an applied-effect guard in the same sink transaction
as the effects it protects.  The Debezium outbox pattern places source state
and an event record in one source transaction, and its event identity helps
deduplication; it does not solve downstream semantic maintenance
\cite{DebeziumOutbox2026}.

\subsection{Crash matrix}

\begin{longtable}{L{0.32\textwidth}L{0.24\textwidth}L{0.36\textwidth}}
\caption{Required crash observations and recovery behavior.}
\label{tab:crash}\\
\toprule
Failure point & Potential durable state & Required safe recovery \\
\midrule
\endfirsthead
\toprule
Failure point & Potential durable state & Required safe recovery \\
\midrule
\endhead
before ingest & no new local record & reread from source \\
after durable ingest & input log only & resume the batch \\
during staged delta & partial invisible stage & rollback or discard stage \\
after validation, before commit & complete invisible stage & commit once or
discard and replay \\
between data and provenance updates & forbidden published state & use one
transaction or invisible artifacts \\
after effects commit, before cursor publication & effects present, cursor
lags & detect effect or replay harmlessly \\
after cursor publication, before source acknowledgement & complete local
state & upstream replay is harmless \\
after acknowledgement, before durability & forbidden ordering & protocol
must prevent it \\
during full rebuild & old realization visible & publish replacement only
after validation \\
during definition change & old and new artifacts coexist & every read binds
one immutable definition \\
\bottomrule
\end{longtable}

The future failpoint harness must terminate the process, reopen durable stores,
recover, and compare with full recomputation.  Throwing and catching an
exception in one process is not a durability test.  No row in
\cref{tab:crash} is a reported CatDB result.

\section{Bootstrap, source gaps, and freshness}
\label{sec:freshness}

\subsection{Initial snapshot and stream cutover}

Let \(p_0\) be the source position associated with an initial snapshot.  A
correct bootstrap represents
\[
I_{p_0}\quad\text{followed by}\quad\Delta I_{(p_0,p_1]}.
\]
No change between snapshot and stream may disappear, and a row visible through
both paths may not be counted twice.

A candidate protocol binds a replayable stream, records a cut position, reads
a snapshot under a declared isolation mode, persists completion, replays
committed changes after the cut, resolves collisions by key and position, and
validates at a later frontier before publication.  PostgreSQL's initial copy
and ordered catch-up are a concrete precedent
\cite{PostgresArchitecture2026}.  Debezium documents consistent snapshots,
log-sequence streaming, offsets, transaction metadata, and duplicate cases
\cite{DebeziumPostgres2026}.  Neither is evidence that \CatDB{} has a working
cutover.

PostgreSQL logical replication does not carry DDL as row replication
\cite{PostgresRestrictions2026}.  A P6 connector therefore needs a separate
schema-observation channel and a safe response to a mismatch between observed
DDL and the capture stream.  If WAL, offsets, delta tokens, or required
snapshots expire, the materialization records the gap, stops exact incremental
repair, and reboots or blocks.  It must not advance a freshness marker across
missing history.

\subsection{Freshness envelope}

The candidate response is:

\begin{lstlisting}
FreshnessEnvelopeV1 {
  definition_id
  status
  required_sources
  per_source_observed_frontier
  per_source_applied_frontier
  source_commit_time_range?
  last_successful_checkpoint
  known_pending_batches
  known_gap?
  completeness
  measured_at
}
\end{lstlisting}

The envelope reports position lag where positions are comparable, source-time
lag where source commit time exists, processing lag, definition lag,
provenance lag, source completeness, and whether each quantity is known,
bounded, partial, or unknown.  A single wall-clock refresh time cannot replace
these fields.

\subsection{Consistency profiles}

\begin{table}[ht]
\centering
\small
\caption{Candidate materialization consistency profiles.}
\label{tab:consistency}
\begin{tabularx}{\textwidth}{L{0.26\textwidth}Y}
\toprule
Profile & Promise \\
\midrule
\code{local-atomic} & One local checkpoint exposes output, auxiliary state,
provenance, and applied positions together. \\
\code{source-prefix} & Output reflects a complete prefix of each declared
source stream. \\
\code{single-source-}\newline\code{snapshot} & Output matches one source snapshot or
position. \\
\code{vector-frontier} & Output names an independently observed position for
each source. \\
\code{coordinated-snapshot} & Output is cross-source consistent only under an
external protocol with recorded evidence. \\
\code{eventual-repair} & Known changes converge if sources and definitions
eventually stop changing and retained history remains available. \\
\code{bounded-staleness} & A measured bound is enforced or its violation is
surfaced. \\
\bottomrule
\end{tabularx}
\end{table}

\code{vector-frontier} is the realistic heterogeneous default.  A read policy
then decides whether stale, partial, invalid, or recovering states are
rejected, returned with metadata, waited on, recomputed, federated, or answered
from an earlier valid definition.  A cost optimizer cannot override a strict
consistency or completeness policy.

Stale-view cleaning studies incorrect, missing, and superfluous records and
can provide approximate repair \cite{KrishnanEtAl2015}.  P6 exact mode must
keep approximation separate from freshness and must never return an
approximate or partial result as complete.

\section{Semantic changes}
\label{sec:semantic-changes}

\subsection{Source schema changes}

The invalidator compares typed old and new schema revisions.  An unused
nullable field may permit retention after capture, wildcard, mapping, query,
identity, and provenance dependencies are checked.  A used field, dropped
field, nullability change, key change, type narrowing, table split, or path
equation change generally requires revalidation and rebuild.  A rename is
reusable only when a stable semantic identity or explicit rename artifact
establishes what remained the same.

A replica-identity change affects future delete and update evidence even if
the query text is unchanged.  The connector must stop at a safe checkpoint,
reconfigure or reboot, and record the stream and profile change.

\subsection{Mapping and query changes}

A mapping edit can alter conversion, object construction, path meaning, enum
normalization, identity keys, coverage, information loss, or provenance.
Default treatment is reachability-based invalidation from the changed mapping
clause.  The paper does not claim that mapping composition always localizes
repair.

Selected query changes may admit adaptation.  An added filter may be computed
from an old broader view.  A projected column may be available in retained
auxiliary state.  A coarser grouping may be derivable from finer aggregates.
A new union branch may be computed independently.  Each rule has assumptions,
retained-state requirements, and an oracle comparison.  View-adaptation prior
art supplies algorithms for selected SQL cases
\cite{GuptaEtAl2001Adapt}; the \CatDB{} program must identify rather than
assume its applicable subset.

\subsection{Identity and authority changes}

An identity merge, split, reversal, contradiction, supersession, or authority
change may move many facts between canonical groups.  The dependency graph
needs reverse indexes from reconciliation decisions to canonical entities,
joined facts, aggregates, provenance evidence, and consumer materializations.
If the index is incomplete, the system rebuilds the larger affected view.
Vector similarity or a small textual edit does not bound this impact.

\subsection{Provenance and retention changes}

A weaker provenance policy may allow audited redaction or compaction.  A
stricter policy can reuse data only when retained raw evidence can derive and
validate the required provenance.  Without that evidence, old row values may
still be usable while the exact provenance profile is partial or invalid.
Changing the derivation semantics may require rebuilding both.

This distinction is why P6 requires data and provenance equivalence.  Semiring
provenance gives a compositional basis for positive algebra
\cite{GreenEtAl2007}, but retention, redaction, source-token identity,
definition revisions, and retractions still need the P13 profile.

\subsection{Capabilities and physical replans}

A capability change may remove predicate pushdown, supply transaction
metadata, remove before-images, weaken ordering, or change numeric behavior.
If logical equivalence remains established, a physical replan can retain
output.  If capture evidence becomes insufficient for future deltas, the
system stops at a safe boundary and switches to full recomputation or
rebootstrap.

An in-flight batch binds the capability and plan revisions under which it was
compiled.  Recovery may not reinterpret that batch under a new plan without
validation.  Physical plan caching is subordinate to semantic definition and
checkpoint identity.

\section{Materialization as an execution strategy}
\label{sec:strategy}

The intended compilation chain is:
\[
\begin{gathered}
\text{immutable semantic definition}\\
\Downarrow\\
\text{logical maintenance specification}\\
\Downarrow\\
\text{physical refresh strategy}\\
\Downarrow\\
\text{replaceable materialized realization}.
\end{gathered}
\]
Every arrow records compiler, input, output, and revision identities.  The
last artifact is not the definition of the first.

These layers allow a planner to choose live federation, full local
recomputation, eager or lazy delta maintenance, partition invalidation,
partial or complete materialization, cached execution, or validated state
reuse.  Lazy view maintenance has established task-log, row-version,
on-demand catch-up, ordering, and recovery precedents
\cite{ZhouEtAl2007}.  Oracle's materialized-view documentation likewise
illustrates mature refresh and freshness choices
\cite{OracleMaterializedViews2026}.  \CatDB{} does not invent those choices.

Any strategy that copies or materializes data still moves data.  Generated ETL
still needs credentials, scheduling, retries, monitoring, storage, and
remediation.  The proposed change is narrower: integration meaning stays in
versioned mappings and semantic definitions, while the transfer program
becomes a generated, inspectable realization.

Materialization selection is also established as a cost and dependency
problem, including aggregate-view lattices
\cite{HarinarayanEtAl1996}.  P14 will own a broader cost model.  P6 supplies
correctness-filtered alternatives and the measurements needed to price update,
checkpoint, source, state, and provenance costs.

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

\subsection{Classical incremental view maintenance}

Gupta, Mumick, and Subrahmanian describe incremental algorithms for inserts,
deletes, and updates over SQL and Datalog features, including counting
treatments for set and duplicate semantics
\cite{GuptaMumickSubrahmanian1993}.  Gupta and Mumick organize materialized-view
maintenance by view class, available resources, modification type, and
applicability \cite{GuptaMumick1995}.  Griffin and Libkin provide an algebraic
treatment of duplicates \cite{GriffinLibkin1995}.  These sources establish
that deltas, bag changes, counts, and broad operator support are prior art.

Self-maintainable views characterize when selected integration views can be
maintained from old state and change information without source access
\cite{GuptaJagadishMumick1996}.  Materialized-view adaptation shows that
selected SQL redefinitions can reuse old state
\cite{GuptaEtAl2001Adapt}.  P6 therefore cannot presume either
self-maintainability or adaptation.  It must derive required state and reject
reuse outside a named rule.

Lazy maintenance defers work while retaining ordered tasks and row versions
\cite{ZhouEtAl2007}.  Stale-view cleaning studies repair and approximation
\cite{KrishnanEtAl2015}.  The \CatDB{} terminology distinguishes eager, lazy,
stale, partial, approximate, invalid, and blocked states so that execution
policy does not silently weaken semantics.

\subsection{Compiled and differential systems}

DBToaster derives higher-order deltas, recursively materializes delta queries,
and uses a costed choice between materialization and lazy evaluation
\cite{AhmadEtAl2012}.  Differential dataflow retains indexed differences over
partially ordered logical times and supports iterative computations
\cite{McSherryEtAl2013}.  Naiad provides the timely dataflow substrate and
low-latency iterative execution precedent \cite{MurrayEtAl2013}.  DBSP gives a
general algebraic incrementalization framework, a compiler/runtime direction,
and a machine-checked theoretical core \cite{BudiuEtAl2023}.  Noria studies
shared partial state, on-demand reconstruction, and online dataflow-graph
changes \cite{GjengsetEtAl2018}.

A fair P6 evaluation must compare equivalent fragments, disclose unsupported
features, record compile time and retained state, and avoid attributing an
established delta method to \CatDB{}.  DBSP is the strongest direct baseline
for generic automatic IVM.  Differential dataflow is the logical-time and
retained-trace baseline.  DBToaster is the higher-order compiler baseline.
Noria is the partial-state and graph-change baseline.

The proposed P6 question is different: when does a data-delta strategy remain
valid after a versioned schema, mapping, reconciliation, provenance, coverage,
or capability change?  A differential timestamp does not by itself answer
that question, and adding a version label would not constitute a contribution
without a validated dependency and recovery property.

\subsection{Snapshots, streams, and capture}

Distributed snapshots require explicit process and channel assumptions
\cite{ChandyLamport1985}.  Lightweight asynchronous snapshots apply barrier
techniques to stateful dataflows \cite{CarboneEtAl2015}.  MillWheel combines
persistent per-key state, logical time, low watermarks, and framework-scoped
fault tolerance \cite{AkidauEtAl2013}.  Kafka transactions can atomically
couple Kafka offsets and Kafka outputs under their documented model
\cite{KafkaDesign2026}.  These results reject any vague claim that a cursor,
checkpoint, or ``exactly once'' label is new or universal.

PostgreSQL logical decoding, replica identity, initial copy, and replication
restrictions define one source profile
\cite{PostgresLogicalDecoding2026,PostgresPublication2026,
PostgresArchitecture2026,PostgresRestrictions2026}.  SQLite sessions and
update-hook limits define different embedded boundaries
\cite{SQLiteSession2026,SQLiteUpdateHook2026}.  Debezium documents a practical
snapshot and streaming connector plus outbox support
\cite{DebeziumPostgres2026,DebeziumOutbox2026}.  P6 must implement and test its
own integration with these mechanisms.

\subsection{Plausible CatDB contribution}

The publication-safe candidate is the combination of:

\begin{enumerate}
  \item one immutable definition binding schema, mapping, query,
  reconciliation, provenance, scalar, coverage, and consistency revisions;
  \item one typed dependency model spanning semantic definitions, source
  observations, capabilities, plans, auxiliary state, checkpoints, and
  realizations;
  \item a change classifier that separates admitted data deltas from semantic
  invalidation and adaptation;
  \item normalized full-versus-incremental equality for both data and
  provenance;
  \item a cursor/effect protocol verified by process-kill recovery; and
  \item a freshness envelope that exposes heterogeneous frontiers,
  completeness, definition lag, and provenance lag.
\end{enumerate}

Every item is currently \openstatus{} or \obstructed{}.  The combination is
only plausibly novel.  If it reduces to conventional IVM with version columns,
if the graph misses dependencies, or if no validated cross-layer rule exists,
the novelty thesis fails.

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

\subsection{Profile freeze}

The first gate is joint ownership, not code generation.  P2, P4, P5, and P13
must freeze:

\begin{itemize}
  \item the finite logical query and normalization profile;
  \item read-direction mapping and conversion semantics;
  \item source observation, coverage, snapshot, and failure semantics; and
  \item normalized provenance, retention, and completeness semantics.
\end{itemize}

The resulting schemas cover materialization definition, capture profile,
change envelope, checkpoint, and freshness envelope.  Deterministic
serialization, normative examples, rejection cases, and terminology review
are required before an implementation can claim conformance.

\subsection{Hand-worked fixtures and Haskell oracle}

The first fixture contains two keyed relations, one read mapping, one inner
equijoin, one grouped sum, one positive provenance circuit, insert/update/
delete/duplicate events, one mapping change that forces rebuild, one source
frontier, and one crash after effects but before cursor publication.  Two
independent human derivations must agree before either program uses the
expected output.

An independent Haskell oracle then evaluates full semantics, interprets the
small delta fragment, normalizes bags and P13 provenance, classifies
invalidation, and emits JSON observations.  It must not share Rust
implementation logic or read golden expected values as computed results.
Haskell agreement would be bounded computational evidence, not a proof.

\subsection{Rust runtime boundary}

The proposed Rust crate owns definition references, change and frontier
handling, dependency and invalidation mechanics, maintenance state,
checkpoint/recovery, freshness, and realization lifecycle.  It does not own
schema truth, mapping truth, query denotation, connector capability truth,
identity authority, or provenance meaning.

An initial module split is:

\begin{lstlisting}
definition.rs  change.rs      frontier.rs
dependency.rs  delta.rs       state.rs
invalidation.rs checkpoint.rs recovery.rs
freshness.rs   error.rs
\end{lstlisting}

SQLite is the first local durable store for checkpoints, applied-effect IDs,
output, auxiliary state, and provenance references.  The session extension can
be evaluated as a local source profile.  PostgreSQL work adds publication and
replica-identity preflight, slot lifecycle, snapshot/stream cutover, LSN and
transaction metadata, schema polling, gap detection, backpressure, and
connector-specific recovery.  Dropping or advancing a source slot is a
consequential operation and must be logged.

\subsection{Recovery and observability}

Named failpoints terminate the process before ingest, after ingest, during
state and provenance staging, before and after sink commit, around cursor
publication, around upstream acknowledgement, during rebuild, and during old
artifact cleanup.  Recovery reopens every store and compares with the
independent oracle.

The API exposes definition and realization identities, status, per-source
frontiers, pending batches, last checkpoint, invalidation reason, selected
strategy, recovery history, data and provenance completeness, and wait,
rebuild, or federated-fallback operations.  A later MDReader view can inspect
these fields, but UI display is not a substitute for the underlying
invariants.

\subsection{Formalization roadmap}

Lean work begins with finite bags and signed changes, followed by selection,
projection, union, join, and basic aggregate delta laws.  It should identify
and reuse the precise theoretical delta already available from DBSP where
appropriate rather than restating existing formal work as a CatDB result.

The high-value new targets are:

\begin{enumerate}
  \item impact soundness for one frozen finite semantic IR;
  \item checkpoint-state safety,
  \(\Box(\mathsf{cursorPublished}(p)\Rightarrow
  \mathsf{effectsDurable}(p))\);
  \item provenance equivalence for one P13 positive-algebra profile; and
  \item selected adaptation laws, such as an unused-field addition, a rename
  with stable semantic identity, a stronger selection over retained rows, a
  coarser grouping over finer state, and an equivalent physical replan.
\end{enumerate}

No such P6 declaration exists.  These are \openconj{} or \obstructed{} targets,
not formal results.

\section{Experimental and reproducibility contract}
\label{sec:evaluation}

\subsection{Evaluation order}

Correctness precedes performance.  For each generated history, the harness:

\begin{enumerate}
  \item creates a source state and records the initial frontier;
  \item runs independent full recomputation;
  \item initializes full, invalidate-on-read, eager-delta, lazy, and selected
  external baseline treatments;
  \item applies the same source transactions and semantic changes;
  \item checkpoints after every batch;
  \item kills selected runs at declared failpoints;
  \item recovers and completes;
  \item independently recomputes at comparison frontiers;
  \item normalizes data, provenance, definitions, and status;
  \item compares exact values, multiplicities, tokens, and envelopes; and
  \item preserves the first mismatch and a minimized reproducer.
\end{enumerate}

Any correctness mismatch stops performance interpretation for that treatment.
Failed histories and raw store snapshots remain part of the artifact.

\subsection{Baselines}

\begin{table}[ht]
\centering
\small
\caption{Preregistered baseline roles.}
\label{tab:baselines}
\begin{tabularx}{\textwidth}{L{0.24\textwidth}Y}
\toprule
Baseline & Role \\
\midrule
full recomputation & correctness oracle and reference cost \\
invalidate on read & conservative cache treatment \\
classical first-order IVM & simplest delta compiler baseline \\
DBToaster & higher-order delta and costed materialization baseline \\
differential dataflow & partially ordered incremental computation baseline \\
DBSP & automatic rich-query incrementalization baseline \\
Noria lineage & partial-state and reuse baseline where reproducibly buildable \\
PostgreSQL treatment & native backend reference \\
lazy task log & update/read latency and staleness tradeoff \\
CatDB candidate & dependency-aware strategy under the same admitted semantics \\
\bottomrule
\end{tabularx}
\end{table}

Every external baseline needs an exact revision, build, configuration,
capability statement, and validation fixture.  A published number from another
machine is context, not a co-measured result.  Unsupported features are
reported rather than silently translated.

\subsection{Correctness and change workloads}

Data histories vary cardinality, selectivity, join fanout, duplicates, groups,
batch size, insert/delete/update mix, key changes, source count, skew,
duplicate and out-of-order rates, and retained-history window.  Semantic
mutations add, drop, rename, and change fields; alter keys and equations; edit
mapping clauses; change filters, projections, groups, and joins; merge and
split identities; change authority or coverage; tighten provenance and
retention; remove a connector capability; and change consistency policy.

For invalidation, the oracle computes the true affected output.  The experiment
records predicted nodes, false negatives, false positives, retained and
rebuilt state, decision time, and time to validated freshness.  One false
negative fails impact soundness.

\subsection{Crash and bootstrap workloads}

Each crash run records source positions, sends an actual termination signal,
reopens durable state, inspects checkpoint and applied-effect records, resumes
the source, and compares with full recomputation.  It counts replayed and
deduplicated events and verifies that no published cursor leads durable
effects.  Filesystem, database durability, isolation, and acknowledgement
settings are part of the result.

Bootstrap tests run concurrent writes around the snapshot cut.  They vary
source isolation, snapshot chunk count, row-key collisions, restarts, DDL
during copy, log retention, and source failover.  The final bag must have no
missing or duplicate multiplicity, and every observed and applied frontier is
retained.

\subsection{Freshness and recovery truthfulness}

The harness injects source delay, source outage, connector pause, backlog,
failed checkpoint, definition change, provenance rebuild, lost history, and
partial availability.  It checks that status matches ground truth and strict
reads do not consume inadmissible state.  A stale or partial response returned
as exact fresh output is a correctness failure.

\subsection{Performance measurements}

Only correct treatments enter performance analysis.  Measurements include:

\begin{itemize}
  \item compilation, delta-plan generation, and dependency-impact time;
  \item refresh CPU, wall time, and p50/p95/p99 update-to-visible latency;
  \item source rows and bytes read, output rows and bytes changed;
  \item auxiliary, provenance, deduplication, and retained-history bytes;
  \item checkpoint size and duration, recovery time, and full-recompute time;
  \item source load, stale duration, and lazy read delay; and
  \item cost-estimate error and crossover curves by update fraction and batch
  size.
\end{itemize}

The central performance claim succeeds only if a declared workload region
shows lower work or latency without unacceptable storage, source, provenance,
or recovery cost.  It fails if no such region exists.  No measurements are
reported in this paper.

\subsection{Artifact retention}

Each run records the Git commit and dirty-tree digest, operating system,
hardware, storage, filesystem, Rust/Haskell/Lean/database/connector versions,
topology, durability and isolation settings, random seeds, fixture and source
digests, definition and plan IDs, exact commands, timestamps, raw output,
crash signal and failpoint, correctness verdict, and exclusion reason.

Confirmatory workloads and metrics are preregistered.  Runs repeat after
warm-up and report distributions and intervals, not means alone.  Timeouts,
out-of-memory runs, and correctness failures remain visible.  Exact and
approximate treatments are never pooled.

\section{Claim register and present results}
\label{sec:results}

\subsection{Claim anchors}

\begin{landscape}
\footnotesize
\begin{longtable}{L{0.08\linewidth}L{0.25\linewidth}L{0.22\linewidth}L{0.14\linewidth}L{0.14\linewidth}}
\caption{P6 claim anchors and current evidence state.}
\label{tab:claims}\\
\toprule
ID & Claim & Required witness & Falsifier & Status \\
\midrule
\endfirsthead
\toprule
ID & Claim & Required witness & Falsifier & Status \\
\midrule
\endhead
P6-C01 & incremental data equals normalized full recomputation & independent
oracle, fixtures, randomized histories, backend comparison & one admitted
mismatch & \obstructed \\
P6-C02 & incremental provenance equals P13-normalized full provenance &
provenance oracle and adversarial derivations & missing, extra, stale, or
mis-versioned contributor & \obstructed \\
P6-C03 & published cursor never leads durable data, state, and provenance &
state model and process-kill matrix & one crash skips an unapplied change &
\openstatus \\
P6-C04 & replaying a committed batch leaves normalized checkpoint unchanged &
duplicate/crash histories per connector & duplicate row, count, token, or
effect & \openstatus \\
P6-C05 & dependency impact contains every semantically affected output &
formal fragment, mutations, wildcard behavior & one missed output &
\openstatus \\
P6-C06 & named semantic changes can adapt old state exactly & rules,
oracle checks, cost comparison & one admitted adapted mismatch & \obstructed \\
P6-C07 & users can distinguish freshness and failure states & API, fixtures,
failure tests, UI review & stale or partial returned as exact & \openstatus \\
P6-C08 & execution strategies preserve one immutable definition &
cross-strategy data/provenance equality & strategy changes denotation &
\obstructed \\
P6-C09 & incremental mode benefits a declared workload region & preregistered
baselines, raw runs, crossover curves & no measured beneficial region &
\openstatus \\
P6-C10 & realization is disposable and reproducible & delete/rebuild exercise
with equal output and provenance & logic exists only in mutable execution
state & \openstatus \\
\bottomrule
\end{longtable}
\end{landscape}

\subsection{What this paper establishes}

This author pass establishes only artifact facts.  It provides a LaTeX
manuscript, source bibliography, paper-local ledgers, candidate definitions,
the supported-fragment boundary, falsification conditions, implementation and
formalization roadmaps, and an experimental contract.  Its algebraic delta
identities and cited source behaviors are \prior{}.

\subsection{What remains absent}

No P6 source event has been applied by CatDB.  No full and incremental outputs
have been compared.  No provenance circuit has been maintained.  No
dependency-impact set has been computed.  No materialization has been
invalidated or adapted.  No cursor has been published by a P6 runtime.  No
process-kill recovery, initial cutover, source-gap repair, freshness response,
formal check, baseline run, or performance measurement exists.

The paper therefore reports no runtime, crash-safety, formal, provenance, or
performance result.  The overall P6 state is \obstructed{} because central
semantic prerequisites and executable evidence are missing.

\section{Limitations and threats to validity}
\label{sec:limitations}

\subsection{Semantic limitations}

The proposed operator fragment omits negation, outer join, recursion,
volatility, approximate search, and several common aggregates.  It assumes a
normalization profile that has not yet been frozen.  SQL nulls, missing values,
collation, time zones, decimal overflow, floating point, and error behavior can
break equivalence if left implicit.

The dependency model is presently prose.  Dynamic SQL, unregistered source
logic, opaque functions, external models, and human decisions can escape a
graph unless the system rejects them or uses conservative wildcard edges.
Impact minimality may be unattainable for practical policies; sound
over-approximation remains the first requirement.

\subsection{Connector and recovery limitations}

At-least-once capture, old row images, transaction boundaries, DDL
observation, order, gap detection, and retention differ by source.  A protocol
valid for one PostgreSQL/sink topology may not apply to Kafka, SQLite, files,
or APIs.  A local atomic checkpoint does not imply upstream acknowledgement or
downstream side effects are atomic.

Process-kill tests cover chosen failpoints and durability settings.  They do
not prove behavior under every hardware, kernel, filesystem, database,
network, or operator failure.  Liveness needs assumptions about source
availability, retry, retention, and eventual quiescence.

\subsection{Provenance limitations}

Positive semiring provenance is not a complete operational provenance model.
Retractions, duplicate derivations, identity revisions, plan history,
checkpoint recovery, redaction, retention, and trust policy all need explicit
normalization.  Data may remain correct after evidence needed for a stricter
profile has expired.  The system must report that separation rather than
reconstruct an explanation it cannot justify.

\subsection{Experimental limitations}

A finite fixture corpus and two initial backends do not represent all
workloads, schemas, update distributions, organizational policies, or failure
modes.  Property-based tests can expose counterexamples but do not prove an
unbounded implementation.  A positive workload region does not imply that
incremental maintenance is generally faster.  A negative result may show that
full recomputation is the better strategy for the measured region.

External baseline builds can differ in language coverage, tuning, state
retention, and durability.  Comparisons must disclose those differences.  A
translation that weakens a baseline or silently excludes unsupported input is
not fair.

\subsection{Novelty limitations}

Almost every component has direct prior art.  The candidate contribution is a
cross-layer contract.  Combination alone is weak novelty.  The program needs
evidence that typed semantic versions change invalidation correctness,
recovery accountability, or planner behavior in a way not provided by a
conventional IVM system plus ordinary metadata.

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

\begin{enumerate}
  \item What is the smallest P2 logical language that supports useful joins
  and aggregates plus an independent evaluator?
  \item Which P4 mapping clauses expose exact reverse dependencies and affected
  keys?
  \item Should v1 admit only one totally ordered cursor per source?
  \item How should cross-source transactions be represented when no global
  transaction exists?
  \item Which PostgreSQL logical-decoding plugin and version should be pinned?
  \item Is the SQLite session extension sufficient, or does embedded capture
  need an application-owned outbox?
  \item How should truncate, key changes, partition movement, and source
  failover appear in a portable change envelope?
  \item How long must source history be retained for lazy repair and recovery?
  \item Which aggregates enter v1 without unbounded auxiliary state?
  \item Can the P13 representation retract provenance support without
  exponential expansion?
  \item Which evidence survives retention and redaction, and how is
  incompleteness reported?
  \item Which schema and mapping changes deserve proved adaptation rules?
  \item How are versioned opaque functions and learned models invalidated?
  \item Can a capability-only replan preserve an in-flight checkpoint?
  \item How can materializations be shared across workspaces with different
  identity, authority, or provenance policies?
  \item Which read policy applies while a new definition rebuilds?
  \item How is bounded staleness expressed when a source exposes no commit
  timestamp?
  \item What prevents a slow consumer from retaining unbounded source logs?
  \item How is stream reset distinguished from duplicate or failover replay?
  \item What measured benefit justifies auxiliary and provenance state?
\end{enumerate}

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

In \CatDB{}, incremental materialization is one physical realization of an
immutable semantic definition.  Admitted data changes may use established
delta techniques.  Before old state can be reused, changes to schemas,
mappings, reconciliation, provenance, coverage, or capabilities need a typed
dependency decision.  Exact mode compares normalized data and provenance with
independent full recomputation at the same declared source frontier.  If the
evidence is insufficient, the system must invalidate, rebuild, block, or label
the result.

This remains a research target.  The current repository has no P6 runtime,
oracle, formalization, connector, crash harness, or benchmark.  The manuscript
therefore makes no exactly-once, transactional cursor, recovery, equivalence,
proof, or performance claim.  Its next evidence gate is a joint P2/P4/P5/P13
profile freeze, followed by one small full-versus-delta fixture computed
independently in Haskell and Rust.  The paper should report a CatDB
incremental result only after that gate passes.

\begingroup
\sloppy
\bibliographystyle{plainnat}
\bibliography{references}
\endgroup

\end{document}
