\documentclass[12pt]{article}

\usepackage{amsmath,amssymb,amsthm}
\usepackage{tikz}
\usetikzlibrary{arrows.meta,positioning,shapes.geometric,fit}
\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={Provenance as First-Class Execution Semantics},
  pdfauthor={Matthew Long; The YonedaAI Collaboration}
}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{requirement}[theorem]{Requirement}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{example}[theorem]{Example}
\newtheorem{counterexample}[theorem]{Counterexample}

\newcommand{\CatDB}{\textsc{CatDB}}
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\prior}{\textsc{supported by prior literature}}
\newcommand{\paperreasoned}{\textsc{paper reasoning}}
\newcommand{\enghyp}{\textsc{engineering hypothesis}}
\newcommand{\openclaim}{\textsc{open}}
\newcommand{\obstructed}{\textsc{obstructed}}
\newcommand{\unresolved}{\textsc{unresolved}}
\newcommand{\structural}{\textsc{structural-only}}
\newcommand{\nonclaim}{\textsc{nonclaim}}
\newcommand{\status}[1]{\par\noindent{\normalfont\textit{Evidence status.} #1.}\par}
\newcommand{\Prov}{\mathsf{Prov}}
\newcommand{\Norm}{\mathsf{Norm}}
\newcommand{\Eval}{\mathsf{Eval}}
\newcommand{\Tokens}{\mathsf{Tokens}}
\newcommand{\Origin}{\mathsf{Origin}}
\newcommand{\Complete}{\mathsf{Complete}}
\newcommand{\Exact}{\mathsf{ExactForProfile}}
\newcommand{\Partial}{\mathsf{Partial}}
\newcommand{\Opaque}{\mathsf{Opaque}}
\newcommand{\Redacted}{\mathsf{Redacted}}
\newcommand{\Unknown}{\mathsf{Unknown}}
\newcommand{\Digest}{\mathsf{Digest}}
\newcommand{\Why}{\mathsf{Why}}
\newcommand{\Where}{\mathsf{Where}}
\newcommand{\How}{\mathsf{How}}
\newcommand{\llbracket}{[\![}
\newcommand{\rrbracket}{]\!]}
\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}
\definecolor{provblue}{RGB}{226,238,250}
\definecolor{provorange}{RGB}{252,237,216}
\definecolor{provgreen}{RGB}{229,243,229}
\definecolor{provred}{RGB}{250,227,227}
\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-provenance\quad
       [\,cs.DB\,]\quad
       23 Jul 2026};
    \end{tikzpicture}
  \fi
}

\title{Provenance as First-Class Execution Semantics:\\
A Profile-Relative Contract for Versioned Derivations}
\author{Matthew Long \\
\textit{The YonedaAI Collaboration} \\
\textit{YonedaAI Research Collective} \\
Chicago, IL \\
\texttt{matthew@yonedaai.com} $\cdot$ \url{https://yonedaai.com}}
\date{23 July 2026}

\begin{document}
\maketitle

\begin{center}
\fbox{\large Provisional status: \obstructed{}}
\end{center}

\begin{abstract}
A row can carry the name of its source and still conceal almost everything
needed to explain it. The name does not say which snapshot was read, which
records contributed, which mapping transformed them, why conflicting
identities were reconciled, which plan actually ran, or whether retention has
already removed part of the evidence. Calling all of these facts
``provenance'' does not make them interchangeable.

This paper proposes a profile-relative execution contract for provenance in
\CatDB{}, a research architecture for versioned semantic integration. The
contract keeps five layers distinct: source identity, relational derivation,
versioned semantic artifacts, retrospective execution, and authority or
reconciliation decisions. For a finite positive bag-relational fragment, it
reuses established semiring provenance and records derivations as shared
circuits. It then connects those circuits to immutable schema, mapping,
migration, query, plan, materialization, snapshot, and decision references.
Every explanation reports its model, granularity, retained evidence, and one
of five completeness classes. A W3C PROV projection supplies interchange
without pretending that an entity-activity graph preserves polynomial
structure or value origin.

The proposal includes normalization and identity rules, a query surface,
counterexamples, privacy and retention behavior, falsifiers, systems
baselines, and separate implementation, experiment, and formalization gates.
The possible contribution is the typed composition boundary across database,
workflow, version, and decision evidence. Why-, where-, lineage-, semiring-,
workflow-, storage-, and security-oriented provenance are prior art.

This is not a completed systems result. The repository has no frozen
provenance profile, provenance fixtures, \code{catdb-provenance} runtime,
independent provenance oracle, provenance theorem, exporter, or benchmark
run. The prerequisite query and mapping-data semantics are not frozen.
Accordingly, all \CatDB{} execution, completeness, performance, security, and
formal claims in this manuscript are \openclaim{} or \obstructed{}.
\end{abstract}

\tableofcontents

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

\subsection{One result, several different questions}

Suppose an analyst asks for active customers and their current support tiers.
The customer records came from two PostgreSQL snapshots, a CSV correction,
and a service response. A mapping renamed fields and converted units. A
reconciliation rule linked two identifiers, while a reviewer rejected a
third candidate. A materialized result was refreshed incrementally. The
planner pushed one selection to PostgreSQL and evaluated a residual
predicate locally.

The analyst may ask:

\begin{enumerate}
  \item Which source records contributed to this row?
  \item Which location supplied the displayed tier value?
  \item Which alternative derivations made the row appear?
  \item Which schema, mapping, query, and plan revisions governed the run?
  \item Which identity decision joined these records?
  \item Would a changed mapping invalidate the result?
  \item Is the answer complete, or did an opaque call, retention rule, source
  failure, or access policy hide part of it?
\end{enumerate}

These are not variants of one graph traversal. Why- and where-provenance are
different models \citep{buneman2001whywhere}. Backward lineage for a warehouse
view has requirements that depend on the view definition and retained
auxiliary data \citep{cui2000lineage}. Positive relational how-provenance has
an established semiring semantics \citep{green2007semirings}. Prospective and
retrospective workflow provenance distinguish the planned recipe from the
observed run \citep{davidson2008workflows}. W3C PROV supplies interoperable
entities, activities, agents, and relations
\citep{lebo2013provo,moreau2013provdm}. A source label, polynomial, workflow
trace, and PROV graph therefore answer overlapping but nonidentical questions.

The design error addressed here is not a lack of provenance terminology. It
is the loss of these distinctions at execution boundaries. A connector emits
a row identifier without its snapshot. A mapping records an operation name
without the immutable mapping artifact. A planner records a physical stage
without the semantic query it was meant to implement. A reconciliation score
is copied into a result as though it established truth. A retained lineage
set is described as a complete explanation even after field origin was
discarded.

\subsection{Research question and bounded answer}

The research question is:

\begin{quote}
How should provenance compose across mappings, migrations, reconciliation,
materialization, and queries while preserving explicit evidence and
completeness boundaries?
\end{quote}

The proposed answer is deliberately finite:

\begin{quote}
For a versioned, explicitly delimited transform fragment, record typed source
identity, derivation, execution, artifact, and decision evidence. Compose only
the admitted derivations. Every answer states the provenance model,
granularity, retained evidence, and completeness class.
\end{quote}

\status{\enghyp{}. The contract is specified here but is not implemented.}

\subsection{Contributions and prior-art boundary}

This paper contributes a provisional contract, not a new general provenance
algebra:

\begin{enumerate}
  \item a question-to-representation table that prevents a lineage set, value
  origin, derivation circuit, activity graph, or trust decision from
  impersonating another model;
  \item a positive bag-relational composition profile that reuses
  \(\mathbb N[X]\) annotations and makes unsupported operators explicit;
  \item a typed envelope linking derivations to immutable artifact versions,
  snapshots, plans, materializations, and decisions;
  \item normalization, completeness, retention, disclosure, and W3C PROV
  projection rules;
  \item counterexamples and falsifiers for overclaiming source tags,
  completeness, rewrite preservation, incremental equivalence, and trust;
  and
  \item executable and formal roadmaps with separate acceptance gates.
\end{enumerate}

Source tagging for heterogeneous integration is decades old
\citep{wang1990polygen}. Uncertainty and lineage were integrated in ULDBs and
Trio \citep{benjelloun2006uldb,agrawal2006trio}. Database-style and workflow
provenance have been composed \citep{amsterdamer2011lipstick}. Provenance-aware
storage, database middleware, PostgreSQL extensions, Spark dataflow tracing,
and operator-integrated lineage are established systems directions
\citep{muniswamyreddy2006pass,arab2018gprom,senellart2018provsql,
interlandi2015titian,psallidas2018smoke}. The novelty question is whether a
typed, versioned bridge across these evidence layers produces useful and
affordable explanations in the stated \CatDB{} fragment. That remains open.

\section{Evidence and dependency status}
\label{sec:status}

\subsection{What exists}

The repository contains a research manifest, claim register, prior-art map,
implementation and formalization roadmaps, benchmark artifact contract,
structural Rust instance envelopes, and smaller Rust, Haskell, and Lean work
on schemas, paths, and mappings. These artifacts constrain the proposal. They
do not execute provenance.

P13 depends on two upstream papers. P1 must define immutable schema and
mapping identities. P4 must define the instance-level mapping and
data-transformation semantics whose provenance is to compose. Logging an
underspecified operation name cannot repair either dependency.

\subsection{What is absent}

No current repository artifact supplies:

\begin{itemize}
  \item a frozen query or provenance profile;
  \item source-record and snapshot identity rules accepted by review;
  \item provenance fixtures or a fixture manifest;
  \item a \code{catdb-provenance} crate or provenance query surface;
  \item an independent Haskell oracle;
  \item a Lean provenance representation or theorem;
  \item mapping, migration, reconciliation, connector, or materialization
  capture hooks;
  \item a W3C PROV exporter with a projection-loss audit; or
  \item correctness, overhead, security, or user-study runs.
\end{itemize}

The implementation-roadmap obligation \code{SYS-PROV-01} is \openclaim{}:
every admitted result must carry the exact version, snapshot, and record
lineage required by profile v1, composing through selection, projection, and
join. The \code{SYS-MAT-01} full-versus-incremental data and provenance
equivalence obligation is also \openclaim{}. The query/provenance semantic
gate is \obstructed{} until its profiles and fixtures are reviewed.

\begin{table}[ht]
\centering
\caption{Current evidence status. ``Literature'' supports only the cited
external result within its assumptions.}
\label{tab:status}
\begin{tabularx}{\textwidth}{L{0.24\textwidth} L{0.22\textwidth} Y}
\toprule
Layer & Status & Current reason \\
\midrule
why/where/how distinctions & \prior{} & Primary sources define the models \\
typed \CatDB{} envelope & \openclaim{} & Manuscript proposal only \\
query and mapping semantics & \obstructed{} & Upstream profiles not frozen \\
Rust runtime & \openclaim{} & Owning crate absent \\
independent oracle & \openclaim{} & Haskell module absent \\
formal laws & \openclaim{} & Lean representation absent \\
materialization equivalence & \openclaim{} & Runtime and fixtures absent \\
PROV export & \openclaim{} & Exporter and loss report absent \\
security and disclosure & \openclaim{} & Policy semantics absent \\
experiments & \openclaim{} & No P13 run bundle \\
\bottomrule
\end{tabularx}
\end{table}

\section{Models before records}
\label{sec:models}

\subsection{Source tokens}

\begin{definition}[Source token]
A source token is a typed reference
\[
  x=(n,s,r,g)
\]
where \(n\) is a source namespace, \(s\) is a source snapshot or cursor
identity, \(r\) is a stable record identity within that snapshot, and \(g\)
is a declared granularity such as record, field, byte range, or text span.
\end{definition}

The token says what the capture boundary claims to have observed. It does not
authenticate the source, prove that the record is true, or guarantee that the
same external identifier denotes the same entity in a later snapshot.

\begin{definition}[Granularity subsumption]
For granularities \(g_f,g_c\), write \(g_f\preceq g_c\) only when the profile
publishes a total deterministic parent projection
\[
  \uparrow_{f\rightarrow c}:(n,s,r,g_f)\longrightarrow(n,s,r',g_c)
\]
whose fine region is wholly contained in exactly one coarse region. A
field-level or byte-range token can answer a record-level request exactly only
when this projection is available, every retained fine token maps
unambiguously, and the capture profile is complete for the requested question.
The response returns the projection rule and both granularities. Missing
coverage yields \(\Partial\); missing or ambiguous parentage yields
\(\Unknown\). Coarse evidence is never silently refined into finer evidence.
\end{definition}

\begin{requirement}[Token collision resistance]
The profile must reject two observations that normalize to the same source
token while denoting different bytes, records, fields, or spans under the
declared source-identity contract.
\end{requirement}

\status{\openclaim{}. No source-token profile or collision fixture exists.}

\subsection{Lineage, why, where, and how}

A lineage set lists contributing tokens. It is useful for backward and
forward dependency questions, but it loses alternative derivations and
multiplicity. Why-provenance identifies witnesses or contributing
subdatabases. Where-provenance identifies source locations from which output
values were copied. How-provenance distinguishes alternative and joint
derivations algebraically \citep{buneman2001whywhere,green2007semirings}.

For example, if output tuple \(t\) can be derived either from source record
\(x\) or from a join of \(y\) and \(z\), the lineage set
\(\{x,y,z\}\) does not preserve the distinction
\[
  p_t = x + yz.
\]
If two copies of \(x\) contribute under bag semantics, a set also loses the
coefficient. Conversely, the polynomial does not tell which input field was
copied into the displayed output field unless value origin is modeled.

\begin{counterexample}[A lineage set is not an explanation circuit]
Consider two databases whose output row has the same contributing token set
\(\{x,y,z\}\). In the first, the row follows \(x+yz\); in the second, it
follows \(xy+xz\). Their lineage sets agree, but removing \(x\) has different
effects. Any interface that returns the set and labels it an exact
how-explanation is unsound.
\end{counterexample}

\subsection{Prospective and retrospective provenance}

Prospective provenance records the intended recipe: immutable schema,
mapping, migration, query, logical plan, physical plan, materialization
definition, and policy artifacts. Retrospective provenance records what
happened: source observations, operator activities, retries, partial results,
decisions, outputs, failures, and publication events. Workflow research
already makes this distinction \citep{davidson2008workflows,
amsterdamer2011lipstick}.

The two must be connected but not collapsed. A plan artifact can exist
without a successful execution. An execution can depart from a plan through
fallback or retry. Recording the plan alone does not establish that a
connector executed its claimed snapshot. Recording a trace alone does not
establish that its physical operators implemented the logical query.

\subsection{Question-to-representation contract}

\begin{longtable}{L{0.24\textwidth} L{0.29\textwidth} L{0.37\textwidth}}
\caption{Each question binds to a model and an explicit insufficiency.}
\label{tab:questions}\\
\toprule
Question & Required representation & Insufficient substitute \\
\midrule
\endfirsthead
\toprule
Question & Required representation & Insufficient substitute \\
\midrule
\endhead
Which records contributed? & record tokens plus lineage edges or circuit
support & source name, workflow activity, or value origin alone \\
Why did this row appear? & declared why-model or derivation circuit & an
unordered token set presented without model \\
Where did this value come from? & field/range token and value-origin rule &
row lineage alone \\
How was the row derived? & normalized additive/multiplicative circuit &
PROV entity-activity graph alone \\
Which versions governed it? & immutable artifact references and source
frontiers & a timestamp or mutable object name \\
Which plan ran? & logical and physical plan identities plus retrospective
stage events & physical trace without logical binding \\
Why were identities joined? & decision artifact, evidence refs, authority,
outcome, and revision & similarity score alone \\
What depends on this source? & forward dependency index with completeness
metadata & a backward-only trace \\
Does it survive a schema change? & changed artifact plus revalidation of
affected semantics & old provenance graph alone \\
Is this explanation complete? & profile, evidence retention, disclosure,
source availability, and completeness class & success status alone \\
\bottomrule
\end{longtable}

\section{Positive relational derivations}
\label{sec:algebra}

\subsection{Profile boundary}

The first algebraic profile admits finite bags, scans, pure total selection,
projection, union, and inner equijoin. Required attributes are non-null.
Scalar equality and collation are fixed by the query profile. Results are
unordered canonical multisets. Outer joins, null and three-valued logic,
difference, general negation, aggregation, recursion, ordering, volatile
functions, floating-point equality, and opaque external calls are
unsupported until separately versioned.

This is intentionally smaller than SQL. Aggregation needs additional value
provenance structure \citep{amsterdamer2011aggregates}. Difference has known
limits for uniform semiring extensions \citep{amsterdamer2011difference}.
Provenance games offer a different approach to negation and why-not questions
\citep{kohler2013games}. Datalog circuits address recursion with their own
representation and complexity choices \citep{deutch2014circuits}. None may
be imported by implication.

\subsection{Annotations}

Let \(X\) be the finite set of source tokens observed for a run. Each input
tuple is annotated by a generator in \(\mathbb N[X]\). For an annotated
relation \(R\), write \(R(t)\) for the annotation of tuple \(t\), with absent
tuples mapped to \(0\). Addition records alternative derivations and
multiplication records joint use. Coefficients retain bag multiplicity.

\begin{definition}[Profile-v1 denotation]
For the admitted fragment, the annotation semantics are:
\begin{align}
\llbracket \operatorname{scan}(R)\rrbracket(t)
  &= R(t),\\
\llbracket \sigma_\phi Q\rrbracket(t)
  &=
  \begin{cases}
    \llbracket Q\rrbracket(t) & \text{if }\phi(t),\\
    0 & \text{otherwise},
  \end{cases}\\
\llbracket \pi_A Q\rrbracket(u)
  &= \sum_{\pi_A(t)=u}\llbracket Q\rrbracket(t),\\
\llbracket Q_1\cup Q_2\rrbracket(t)
  &=\llbracket Q_1\rrbracket(t)+\llbracket Q_2\rrbracket(t),\\
\llbracket Q_1\Join_\theta Q_2\rrbracket(u)
  &=\sum_{\substack{t_1,t_2\\t_1\Join t_2=u\\\theta(t_1,t_2)}}
    \llbracket Q_1\rrbracket(t_1)
    \llbracket Q_2\rrbracket(t_2).
\end{align}
\end{definition}

\status{\prior{} as an algebraic basis
\citep{green2007semirings}; \openclaim{} as a \CatDB{} profile and runtime.}

\subsection{Circuits rather than forced expansion}

Canonical expanded polynomials can grow sharply. A proposed runtime stores a
directed acyclic circuit with token, zero, one, addition, and multiplication
nodes. Commutative children are sorted by child digest. Associative nodes are
flattened where the profile permits. Neutral elements are removed and
annihilation by zero is applied. Equal subcircuits share a content-addressed
node. Expansion remains a query or test operation, not the storage default.

Circuits for provenance are established prior art
\citep{deutch2014circuits}. The open \CatDB{} issue is whether this
normalization is deterministic across Rust and an independent oracle, retains
the profile's multiplicities, and stays operationally bounded.

\begin{requirement}[Denotational normalization]
For every well-formed circuit \(c\),
\[
  \Eval(\Norm(c))=\Eval(c)
\]
in every commutative semiring admitted by the profile.
\end{requirement}

\status{\openclaim{}. It needs definitions, cross-language fixtures, and
selected machine-checked laws.}

\subsection{Typed substitution across mappings}

Suppose a mapping \(F\) produces intermediate tokens \(y\) from source
tokens \(X\), and a query \(Q\) derives outputs from \(y\). Composition
substitutes each intermediate generator with its mapping derivation:
\[
  \Prov(Q\circ F)(t)
  =
  \Prov(Q)(t)\left[y\mapsto \Prov(F)(y)\right].
\]
Substitution is allowed only when source, schema, snapshot, mapping, and
granularity types agree. A string replacement over identifiers is not
composition.

\begin{proposition}[Sequential/composed target]
For admitted positive mappings \(F,G\) and input instance \(I\), the intended
law is
\[
 \Norm\!\left(\Prov(G,F(I))\circ\Prov(F,I)\right)
 =
 \Norm\!\left(\Prov(G\circ F,I)\right).
\]
\end{proposition}

\status{\obstructed{}. The proposition is a target, not a theorem, because
P4's instance-level mapping language and composition semantics are not
frozen.}

\subsection{Rewrites}

Equal visible rows do not guarantee equal provenance. A rewrite is enabled
only if it preserves the declared result and provenance profile. For each
enabled rewrite \(Q\rightsquigarrow Q'\), the gate compares both normalized
bags and normalized derivation circuits:
\[
  \Norm(\llbracket Q\rrbracket_I)
  =
  \Norm(\llbracket Q'\rrbracket_I).
\]

\begin{counterexample}[Distinct erases evidence]
Let a bag contain two equal visible rows with source annotations \(x\) and
\(y\). Projection followed by duplicate elimination can return one visible
row. A row-only test sees agreement whether its provenance is \(x+y\),
\(\{x,y\}\), \(x\), or an opaque marker. The rewrite is not provenance
preserving until duplicate semantics and the required model are fixed.
\end{counterexample}

\section{Composition across the execution stack}
\label{sec:composition}

\subsection{Source ingestion}

A connector observation binds:

\begin{itemize}
  \item connector and capability-manifest digests;
  \item source namespace and authenticated endpoint class;
  \item transaction, snapshot, cursor, or best-effort frontier;
  \item source record and optional field or range identity;
  \item pushed and residual operations;
  \item observed bytes or a digest when retention permits;
  \item timing, retry, partial-availability, and failure facts; and
  \item an exactness class justified by the connector contract.
\end{itemize}

A source may expose only page offsets, unstable row numbers, or an opaque
service response. Such observations cannot be upgraded to stable exact
record identity. They remain \(\Opaque\), \(\Partial\), or \(\Unknown\).

\begin{counterexample}[Timestamp is not a snapshot]
Two requests begin at the same wall-clock time but read different committed
states. If the envelope identifies both by timestamp alone, later explanation
cannot distinguish them. The timestamp may remain an observation, but it
cannot serve as the snapshot identity.
\end{counterexample}

\subsection{Schema mapping and migration}

A mapping activity references immutable source and target schemas, the
mapping artifact, discharged and deferred obligations, the admitted
instance-level operator, and the input and output derivations. A migration
adds direction, unit, and materialization identity. If the transformation
synthesizes a target object, the profile must say whether the token denotes
the new object, its generating derivation, or both.

Category-theoretic structure may type mappings and compose transformations.
It does not eliminate capture, storage, identity, or query costs. A mapping
between schemas also does not uniquely determine how a particular runtime
transformed instances. Prospective artifact provenance must be paired with
retrospective execution evidence.

\begin{requirement}[No semantic event by name alone]
An event claiming a mapping or migration must carry the immutable artifact
identity and a profile-supported operator or an explicit opaque boundary. A
free-form label such as \code{"customer-map-v2"} is not sufficient.
\end{requirement}

\subsection{Reconciliation}

Reconciliation provenance records evidence and authority without turning
either into truth. A candidate decision contains:

\[
\begin{split}
  d = (&\text{decision revision},\text{candidate identities},
       \text{evidence refs},\\
      &\text{rule/model revision},\text{score with semantics},
       \text{authority},\\
      &\text{outcome},\text{approvals},\text{reversal link},
       \text{retention class}).
\end{split}
\]

Possible outcomes include accept, reject, defer, require approval, split, and
revoke. Similarity is evidence for a decision, not semantic identity.
Changing or reversing a decision invalidates downstream results according to
the dependency graph.

\begin{counterexample}[Confidence is not identity]
Two records have vector similarity \(0.99\). A rule accepts them today and is
reversed tomorrow after an authoritative identifier conflicts. If the
provenance stores only the score, it cannot explain who or what authorized
the old merge, identify affected results, or distinguish evidence from the
decision. The result envelope was incomplete for the stated question.
\end{counterexample}

\status{\obstructed{}. P7 decision and authority semantics are not available.}

\subsection{Planning and execution}

The logical query identity, normalized logical plan, physical plan, connector
capabilities, pushed operators, residual operators, and actual stages are
separate records. The planner emits a decision certificate. Connectors emit
source observations. The executor emits activities, retries, fallback,
partial results, and outputs. A later provenance query can then distinguish:

\begin{itemize}
  \item what the request meant;
  \item what the planner intended;
  \item what each connector claimed to execute;
  \item what the local engine observed; and
  \item what result artifact was published.
\end{itemize}

An execution trace does not prove semantic plan correctness. That relation
requires query-profile equivalence fixtures and backend differential tests.

\subsection{Materialization and incremental refresh}

A materialization provenance record binds its definition, dependency
frontier, refresh mode, prior checkpoint, input deltas, output changes,
derivation updates, cursor publication, and durable result identity.
Incremental view maintenance is established prior art
\citep{gupta1993ivm,budiu2023dbsp}. The \CatDB{} obligation is stronger than
equal visible rows:
\[
 \Norm(\mathrm{Data}_{\mathrm{inc}})
 =
 \Norm(\mathrm{Data}_{\mathrm{full}})
 \quad\land\quad
 \Norm(\Prov_{\mathrm{inc}})
 =
 \Norm(\Prov_{\mathrm{full}}).
\]
Cursor advancement and the corresponding durable data and provenance effects
must be atomic under the supported failure model.

Provenance sketches can support data skipping and can themselves be
incrementally maintained \citep{li2026sketches}. A sketch is an
overapproximation for its purpose, not exact derivation evidence. A result
using a sketch must declare approximate granularity and must not receive
\(\Exact\).

\status{\openclaim{}. No materialization implementation or equivalence run
exists.}

\subsection{Workspace and distribution boundaries}

Workspace operations contribute immutable base, overlay, commit, merge,
approval, and publication identities. Distribution contributes delivery,
ordering, retry, causal, replay, checkpoint, and stale-state events. Neither
layer may invent a second provenance model. They emit typed events into the
one versioned envelope owned by the provenance abstraction.

A finite execution graph can be acyclic even when the complete version
history contains revisions, reversals, and references across time. Cycle
rules are therefore profile-specific: derivation circuits may require a DAG;
version and influence graphs need separate constraints.

\begin{figure}[ht]
\centering
\begin{tikzpicture}[
  node distance=8mm and 11mm,
  box/.style={draw,rounded corners,align=center,minimum height=8mm,
    text width=31mm,font=\small},
  arr/.style={-{Latex[length=2mm]},thick}
]
\node[box,fill=provblue] (src) {source observations\\tokens and snapshots};
\node[box,fill=provblue,right=of src] (map) {mapping and migration\\artifact derivations};
\node[box,fill=provorange,right=of map] (dec) {reconciliation\\decision evidence};
\node[box,fill=provgreen,below=of map] (qry) {query and plan\\derivation circuit};
\node[box,fill=provgreen,right=of qry] (mat) {materialization\\refresh and checkpoint};
\node[box,fill=provred,below=of qry] (env) {normalized result envelope\\profile and completeness};
\node[box,fill=provred,left=of env] (api) {origin, impact, version,\\assumption queries};
\node[box,fill=provred,right=of env] (w3c) {W3C PROV projection\\plus loss report};
\draw[arr] (src) -- (map);
\draw[arr] (map) -- (dec);
\draw[arr] (map) -- (qry);
\draw[arr] (dec) -- (mat);
\draw[arr] (qry) -- (mat);
\draw[arr] (mat) -- (env);
\draw[arr] (env) -- (api);
\draw[arr] (env) -- (w3c);
\end{tikzpicture}
\caption{Proposed composition boundary. Arrows denote typed references and
substitution obligations, not implemented dataflow.}
\label{fig:layers}
\end{figure}

\section{Candidate typed profile}
\label{sec:profile}

\subsection{Stable references}

Every durable reference carries a namespace, kind, version, digest algorithm,
digest, and canonicalization profile. Mutable aliases may point to immutable
objects, but provenance stores the resolved immutable identity used by the
operation.

\begin{lstlisting}
ArtifactRef {
  namespace,
  kind,
  version,
  canonicalization_profile,
  digest_algorithm,
  digest
}
\end{lstlisting}

Digest equality establishes equality of canonical bytes under the named
algorithm and profile. It does not prove authority, authorship, semantic
equivalence, or external authenticity.

\subsection{Derivation and value origin}

\begin{lstlisting}
DerivationCircuit {
  profile_ref,
  source_token_namespace,
  root_node,
  nodes[],
  canonicalization_profile,
  completeness
}

ValueOrigin {
  output_record,
  output_field,
  rule: Copy | Constant | PureExpression | Opaque,
  input_ranges[],
  expression_ref,
  completeness
}
\end{lstlisting}

Profile v1 admits exact value origin only for declared copy, constant, and
pure total expression rules. A unit conversion may list input fields and the
versioned expression, but it is not where-provenance in the narrow copied-cell
sense unless the selected model defines it that way.

\subsection{Activity and decision records}

\begin{lstlisting}
ActivityEvidence {
  activity_id,
  prospective_artifact_refs[],
  logical_plan_ref,
  physical_plan_ref,
  used_entities[],
  generated_entities[],
  source_frontiers[],
  connector_observations[],
  started_at,
  ended_at,
  outcome,
  retry_parent,
  partiality_reasons[]
}

DecisionEvidence {
  decision_ref,
  candidates[],
  evidence_refs[],
  rule_or_model_ref,
  authority_ref,
  outcome,
  approval_refs[],
  reverses,
  uncertainty_semantics,
  completeness
}
\end{lstlisting}

Times help sequence observations. They do not replace version, transaction,
snapshot, or causal identity.

\subsection{Result envelope}

\begin{lstlisting}
ProvenanceEnvelope {
  envelope_profile_ref,
  result_artifact_ref,
  semantic_commit_ref,
  schema_refs[],
  mapping_refs[],
  migration_refs[],
  query_ref,
  logical_plan_ref,
  physical_plan_ref,
  source_frontiers[],
  derivation_circuit_ref,
  value_origin_refs[],
  activity_refs[],
  decision_refs[],
  materialization_ref,
  policy_ref,
  retention_ref,
  completeness,
  missing_evidence[],
  redaction_summary,
  created_at
}
\end{lstlisting}

This listing is a proposed field inventory. Exact types, optionality,
cardinality, serialization, and compatibility rules belong in a reviewed
profile and fixture schema.

\section{Completeness is part of the answer}
\label{sec:completeness}

\subsection{Five classes}

\begin{definition}[Completeness class]
Every provenance response has one of:
\begin{description}
  \item[\(\Exact\)] Exact for the named profile, question, granularity,
  retained interval, source frontier, and disclosure principal.
  \item[\(\Partial\)] Some known evidence is absent because capture, source
  availability, or retention was incomplete.
  \item[\(\Opaque\)] An activity is known but its internal derivation is not
  represented.
  \item[\(\Redacted\)] Evidence exists or may exist but policy withholds it.
  \item[\(\Unknown\)] The system cannot establish which of the stronger
  classes applies.
\end{description}
\end{definition}

\(\Exact\) is never an unqualified global claim. A record-lineage answer may
be exact for profile v1 and still provide no value origin. An authorized
administrator and a tenant may receive different graph projections. A
retention horizon may make an old answer partial. A failed source can make a
federated result's provenance incomplete even if the returned rows are
syntactically valid.

\begin{requirement}[Monotone honesty]
Normalization, export, redaction, and query processing may preserve or weaken
the completeness class. They may not strengthen it without new verified
evidence.
\end{requirement}

\status{\paperreasoned{} contract; runtime enforcement is \openclaim{}.}

\subsection{Evidence matrix}

The answer carries machine-readable reasons:

\begin{longtable}{L{0.22\textwidth} L{0.30\textwidth} L{0.39\textwidth}}
\caption{Examples of evidence that constrain completeness.}
\label{tab:completeness}\\
\toprule
Condition & Maximum honest class & Required response behavior \\
\midrule
\endfirsthead
\toprule
Condition & Maximum honest class & Required response behavior \\
\midrule
\endhead
stable source token, retained circuit, full admitted run & \(\Exact\) for the
named question/profile & list profile, frontier, granularity, and evidence
digests \\
source records unavailable during partial federation & \(\Partial\) & name
missing source/frontier and affected result region \\
opaque API or model call & \(\Opaque\) & list declared inputs, outputs,
activity, and unsupported internal explanation \\
policy hides a contributing record & \(\Redacted\) & avoid leaking protected
identity through graph shape, counts, or timing \\
legacy result without capture manifest & \(\Unknown\) & refuse exactness and
state which capture facts cannot be established \\
retention deleted field ranges but kept row tokens & \(\Partial\) for value
origin; possibly exact for row lineage & classify per question, not once per
result \\
sketch overapproximates contributing partitions & approximate \(\Partial\) &
report false-positive possibility and sketch revision \\
\bottomrule
\end{longtable}

\section{Normalization and identity}
\label{sec:normalization}

\subsection{Canonical form}

A shared artifact requires cross-implementation agreement on:

\begin{enumerate}
  \item Unicode, scalar, identifier, and byte canonicalization;
  \item object-field and map ordering;
  \item set, bag, and sequence distinctions;
  \item number and timestamp encodings;
  \item source-token namespace construction;
  \item associative and commutative circuit normalization;
  \item multiplicity and coefficient representation;
  \item content-addressed sharing;
  \item unknown, opaque, partial, and redacted markers; and
  \item version negotiation and unsupported-version behavior.
\end{enumerate}

Two equivalent polynomials need not have the same syntax. A practical profile
must decide whether canonical identity means syntactic normal form, circuit
isomorphism, expanded polynomial equality, or denotational equality under a
bounded evaluator. The first release should use a deterministic syntactic
normal form and separately test denotation on finite models.

\begin{counterexample}[Commutative but nondeterministic]
One runtime serializes \(x+y\); another serializes \(y+x\). They evaluate
equally but receive different digests. If artifact identity depends on raw
construction order, cache keys, differential tests, and forward indexes
diverge. Sorting by a stable child digest repairs this example but does not
by itself solve all algebraic equivalence.
\end{counterexample}

\subsection{Identity is typed}

The text \code{"42"} may be a source row key, target entity key, plan node,
execution activity, or content digest fragment. Identity comparison is
defined only within compatible namespaces and kinds. Cross-system translation
is an explicit mapping with its own evidence.

\begin{requirement}[No inferred authenticity]
Receiving a stable source identifier establishes only that the connector
reported that identifier under its contract. Authenticity requires separate
transport, credential, signature, attestation, or trusted-source evidence.
\end{requirement}

\section{Provenance query surface}
\label{sec:queries}

\subsection{Operations}

The proposed API exposes typed questions rather than a single unrestricted
graph endpoint:

\begin{lstlisting}
origin(result_ref, field?, model, depth, principal)
why(result_ref, record, model, depth, principal)
derivation(result_ref, record, representation, budget, principal)
upstream(result_ref, depth, kinds, principal)
downstream(artifact_or_token_ref, depth, kinds, principal)
versions(result_ref, kinds)
assumptions(result_ref, include_deferred)
decisions(result_ref, status, principal)
execution(result_ref, stages, attempts, principal)
schema_survival(result_ref, proposed_change_ref)
export_prov(result_ref, profile, principal)
  -> {prov_document, loss_report, completeness, ...}
\end{lstlisting}

Every response includes:

\begin{itemize}
  \item question and normalized parameters;
  \item model and granularity;
  \item provenance-profile and result-envelope revisions;
  \item completeness class and reasons;
  \item source frontiers and retained interval;
  \item policy principal and redaction summary;
  \item returned nodes, edges, circuits, or origins;
  \item truncation, depth, count, byte, and time budgets;
  \item evidence digests; and
  \item unsupported or unknown fields.
\end{itemize}

For \code{export\_prov}, \code{loss\_report} is required rather than optional.
It names each represented, summarized, extended, omitted, redacted, or opaque
internal structure. An export without that field is invalid even if its PROV
document satisfies the external syntax and constraints.

\subsection{Bounded expansion}

Provenance queries can be larger or more sensitive than the result. The API
must bound depth, nodes, edges, circuit expansion, response bytes, CPU, and
wall time. Truncation changes completeness for the requested expansion and is
returned as data, not buried in a transport warning. Continuation tokens bind
the result, profile, principal, and query parameters to prevent cross-policy
reuse.

\subsection{Schema survival}

Provenance helps identify affected artifacts, but it cannot by itself prove
that a result survives a schema change. The procedure is:

\begin{enumerate}
  \item resolve the old result envelope and proposed change;
  \item find dependencies through typed artifact and field/range references;
  \item classify obviously unaffected references where the profile supports
  such a rule;
  \item revalidate mappings, queries, constraints, decisions, and
  materializations under the changed semantics;
  \item replay or recompute where static reasoning is insufficient; and
  \item report survived, invalidated, unknown, or requires-replay with
  evidence.
\end{enumerate}

\begin{counterexample}[Reachability is not survival]
A column is renamed with an apparently preserved identifier, but its unit
changes from dollars to cents. A graph reachability check finds the same
dependency. The old result does not survive without validating the mapping
and scalar semantics. Provenance locates the risk; it does not discharge it.
\end{counterexample}

\section{W3C PROV interoperability}
\label{sec:prov}

\subsection{Projection}

W3C PROV defines a conceptual model and representations centered on entities,
activities, agents, generation, use, derivation, attribution, association,
and related qualified influences
\citep{moreau2013provdm,lebo2013provo}. \CatDB{} can project:

\begin{itemize}
  \item immutable source, semantic, plan, materialization, and result
  artifacts to \code{prov:Entity};
  \item mapping, migration, query, reconciliation, refresh, and publication
  runs to \code{prov:Activity};
  \item users, services, connectors, organizations, and policy authorities to
  \code{prov:Agent};
  \item inputs to \code{prov:used};
  \item outputs to \code{prov:wasGeneratedBy};
  \item revisions and derivations to qualified PROV relations; and
  \item planned artifacts to \code{prov:Plan} where appropriate.
\end{itemize}

The export must satisfy the applicable PROV constraints
\citep{cheney2013provconstraints}. Access and query behavior should also heed
the PROV-AQ separation between locating provenance and deciding whether it is
authoritative, correct, trustworthy, or disclosable \citep{klyne2013provaq}.

\subsection{Loss report}

The projection does not automatically preserve:

\begin{itemize}
  \item additive versus multiplicative derivation structure;
  \item coefficients and bag multiplicity;
  \item canonical circuit identity;
  \item precise field or range origin;
  \item profile-relative exactness;
  \item unsupported-operator semantics;
  \item uncertainty and reconciliation outcome distinctions;
  \item policy-redaction behavior; or
  \item source-token namespace constraints.
\end{itemize}

Every export therefore includes a machine-readable loss report naming which
internal structures were represented, summarized, extended, omitted,
redacted, or made opaque.

\begin{requirement}[No lossy round-trip claim]
An imported PROV graph is external evidence. It is not a verified internal
derivation envelope unless it carries a recognized profile, validates, has
trusted identity bindings, and contains all required structures for the
question.
\end{requirement}

\status{\prior{} for the W3C model; \openclaim{} for the \CatDB{} projection,
validation, and loss audit.}

\section{Trust, integrity, privacy, and retention}
\label{sec:security}

\subsection{Provenance is not truth}

Provenance can support an assessment of quality, reliability, or
trustworthiness. It does not produce that assessment by itself. A precise
trace of a false source remains precise. A signed false statement remains
false. A trusted agent may make a mistaken decision. An exact circuit can
correctly explain a semantically invalid query.

The envelope separates:

\begin{itemize}
  \item identity evidence;
  \item integrity evidence;
  \item authority and policy decisions;
  \item uncertainty or confidence;
  \item derivation semantics;
  \item execution observations; and
  \item completeness.
\end{itemize}

\subsection{Integrity}

Secure provenance work treats integrity and confidentiality as distinct
requirements \citep{hasan2009secure,braun2008securing,chong2009semantics}. A
hash chain may expose modification or reordering under a named serialization
and threat model. It does not establish that every event was captured, that a
compromised producer told the truth, or that the first trusted anchor was
correct.

The proposed integrity manifest records event digests, parent links,
canonicalization profile, signer or trusted anchor when used, append
semantics, gap detection, clock assumptions, and verification outcome.
Optional cryptography must be described by the exact property it supplies.

\begin{counterexample}[A complete-looking hash chain]
A malicious producer omits one source read, then hashes every remaining event
correctly. Chain verification passes. The chain proves consistency of the
retained sequence under the hash assumption, not capture completeness.
\end{counterexample}

\subsection{Confidentiality and disclosure}

Provenance can reveal protected data even when the result is public. A hidden
edge may expose participation. Node counts can reveal alternatives. Timing
can reveal whether a protected branch exists. A forward-impact query can
reveal tenants or models that depend on a source.

Policy therefore applies to provenance operations, not only to result rows.
Each response is evaluated under a principal, purpose, tenant, profile, and
retention context. Redaction must consider nodes, edges, attributes, counts,
continuation tokens, error classes, and timing. Returning an empty exact graph
when evidence was withheld is forbidden; the response is \(\Redacted\) or a
policy denial.

\subsection{Retention and deletion}

Retention can remove raw source values while preserving digests, record
tokens, circuit structure, or aggregate audit facts. Deletion policy can
conflict with reproducibility and accountability. The profile does not hide
that conflict.

A retention revision specifies:

\begin{itemize}
  \item evidence classes and retention horizons;
  \item legal or policy basis;
  \item compaction and deletion operations;
  \item tombstone or proof-of-deletion behavior;
  \item effects on backward, forward, value-origin, and export queries;
  \item downgrade rules for completeness; and
  \item revalidation of downstream materializations and caches.
\end{itemize}

Exact provenance is available only relative to retained evidence. No paper
claim should imply indefinite perfect history.

\section{Systems precedents and evaluation baselines}
\label{sec:related}

Source-tagging systems already address heterogeneous origin
\citep{wang1990polygen}. ULDBs and Trio connect lineage with uncertainty
\citep{benjelloun2006uldb,agrawal2006trio}. Panda integrates provenance and
data \citep{ikeda2010panda}. GProM uses middleware and query rewriting across
several provenance tasks \citep{arab2018gprom}. ProvSQL brings several
provenance interpretations to PostgreSQL \citep{senellart2018provsql}.

Physical capture choices matter. Titian integrates record-level lineage with
Spark \citep{interlandi2015titian}. Smoke places capture logic in physical
operators and optimizes expected lineage queries
\citep{psallidas2018smoke}. Provenance-aware storage captures system-level
history automatically, while also exposing the semantic limits of an opaque
storage boundary \citep{muniswamyreddy2006pass}. These are direct baselines,
not background decoration.

Formal explanation work also demands exact guarantees. Trace slicing for
database queries can state disclosure and recomputation properties
\citep{cheney2014explain}. P13 must likewise say what an explanation preserves
and under which calculus, rather than claiming that a graph ``explains'' an
answer.

The CQL project reports symbolic lineage and JDBC import/export behavior in
its official materials \citep{categoricaldata2026cql}. Its documentation also
warns about convenience-generated identifiers. This is external precedent,
not evidence that \CatDB{} implements categorical provenance or inherits CQL
performance.

\begin{table}[ht]
\centering
\caption{Baseline families and the mismatch that must be retained.}
\label{tab:baselines}
\begin{tabularx}{\textwidth}{L{0.25\textwidth} L{0.29\textwidth} Y}
\toprule
Baseline & Comparison & Required caveat \\
\midrule
PostgreSQL without provenance & execution and storage overhead & no
fine-grained explanation baseline \\
ProvSQL & relational annotations and where-provenance & not the full
version/workflow/decision envelope \\
GProM & query-rewrite provenance tasks & different capture and backend
architecture \\
Smoke & eager, lazy, and deferred lineage tradeoffs & operator-integrated
lineage, not semantic artifact provenance \\
Titian & distributed dataflow lineage & Spark-specific execution model \\
raw event log & prospective/retrospective activity & no exact record
derivation semantics \\
W3C PROV graph & interoperability and graph queries & does not preserve the
internal circuit by default \\
full recomputation & data and provenance result & expensive but necessary
correctness oracle for the supported fragment \\
\bottomrule
\end{tabularx}
\end{table}

\section{Evaluation protocol}
\label{sec:evaluation}

\subsection{Research questions}

\begin{enumerate}
  \item[\textbf{RQ1}] Do normalized derivations match an independent oracle
  for every admitted fixture and generated finite model?
  \item[\textbf{RQ2}] Does composed execution preserve sequential mapping and
  query provenance?
  \item[\textbf{RQ3}] Does incremental maintenance match full recomputation
  for both data and provenance?
  \item[\textbf{RQ4}] What capture, storage, and explanation-query overhead
  does each provenance mode impose?
  \item[\textbf{RQ5}] Do W3C PROV exports validate and report all declared
  projection loss?
  \item[\textbf{RQ6}] Do schema-survival answers match seeded semantic
  changes and replay outcomes?
  \item[\textbf{RQ7}] Do disclosure policies prevent unauthorized inference
  without silently returning complete-looking answers?
  \item[\textbf{RQ8}] Does the cross-layer envelope improve explanation
  accuracy over row-lineage and raw-log baselines?
\end{enumerate}

\subsection{Modes and ablations}

At minimum, compare provenance off; artifact identity only; record lineage
set; exact positive derivation circuit; circuit plus value origin; prospective
plus retrospective activities; the full admitted decision envelope; and an
explicitly approximate sketch mode. Ablate artifact versions, source
frontiers, plan identity, decision evidence, value origin, completeness
metadata, and retention/disclosure fields one at a time.

The off mode measures overhead but cannot serve as a correctness baseline for
provenance. A weaker profile cannot be used to claim the cost of a stronger
one.

\subsection{Fixtures and generated models}

Hand-worked families must cover:

\begin{itemize}
  \item token namespace collision, snapshot drift, and unstable row IDs;
  \item selection preservation and rejection;
  \item projection alternatives and bag coefficients;
  \item union alternatives, self-join multiplication, and join fan-out;
  \item sequential versus composed typed mappings;
  \item unsupported difference, aggregation, null, volatile, and opaque
  operators;
  \item accepted, rejected, deferred, and reversed reconciliation decisions;
  \item materialization refresh, duplicate delivery, out-of-order change,
  crash, and cursor atomicity;
  \item valid, invalid, lossy, redacted, and partial PROV exports;
  \item retention-induced downgrade; and
  \item graph-shape, count, timing, and continuation-token disclosure.
\end{itemize}

The independent finite evaluator may not call Rust, SQL, a backend, FFI, or
the fixture's expected field. Exhaustive small models and independently
seeded property tests compare result bags and circuits. A found
counterexample is minimized and retained. Passing finite tests do not prove
the unbounded runtime.

\subsection{Metrics}

Correctness metrics include token false positives and negatives, exact
circuit agreement, value-origin agreement, composed/sequential agreement,
full/incremental data and provenance agreement, PROV validation and loss
agreement, schema-survival precision and recall on seeded changes, and
unauthorized disclosure failures.

Performance metrics include capture CPU and wall time, execution slowdown,
bytes per source and output row, circuit nodes and edges, sharing ratio, write
amplification, forward and backward query latency, export time and size,
policy overhead, refresh overhead, and retention-compaction cost.

Operational metrics include missing observations, opaque activities, retries,
duplicate events, cursor failures, stale materialization use,
retention-induced unknown answers, disclosure-denied expansions, and
workloads exceeding resource budgets.

\subsection{Run contract}

Each immutable run records:

\begin{itemize}
  \item hypothesis and claim IDs;
  \item profile, fixture, schema, mapping, query, and plan revisions and
  digests;
  \item repository revision and dirty state;
  \item runtime, container, operating system, CPU, memory, storage, backend
  versions, and configuration;
  \item dataset generator, seed, source snapshots, and workload split;
  \item provenance mode, retention, disclosure, and completeness policy;
  \item warmup, repetitions, exclusions, failures, and timeouts;
  \item raw outputs and checksums;
  \item statistical method, intervals, and correction policy;
  \item preregistered acceptance and falsification thresholds; and
  \item every failed or rejected run.
\end{itemize}

No numerical threshold is supplied in this manuscript because no pilot run
supports one. A future preregistration must choose workload-specific
correctness requirements and practical overhead bounds before examining held
out outcomes.

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

\subsection{I0: freeze the profile}

Specify query fragment, tokens, snapshots, artifact references, circuit
syntax, value origins, activities, decisions, result envelope,
normalization, completeness, retention, disclosure, W3C projection, and
version negotiation. Independent database-provenance and security review must
find no unresolved critical or important ambiguity.

\subsection{I1: hand-worked fixtures}

Create an immutable schema-v2 extension and provenance-v1 cases. Each case
states the question, model, exact input, hand-derived output, completeness,
negative alternative, and rationale. A manifest hashes every artifact.

\subsection{I2: independent Haskell oracle}

Implement a total finite denotation for the admitted operators and record
lineage. It consumes decoded inputs and emits normalized bags and circuits.
It must not invoke Rust, SQLite, PostgreSQL, SQL parsing, FFI, or expected
fixture outputs.

\subsection{I3: owning Rust abstraction}

Create \code{catdb-provenance} as the only event and result-envelope schema.
It owns token, circuit, normalization, query, completeness, retention, and
projection types. Other crates emit typed obligations and observations. A
connector-specific lineage encoding is translated at the boundary and never
becomes a second authoritative model.

The first circuit profile uses a versioned deterministic normal-form
serialization: domain-separated node tags; canonical scalar and coefficient
bytes; ordered children for noncommutative constructors; lexicographically
sorted child digests with retained multiplicities for commutative
constructors; and a domain-separated root digest. Decoders reject duplicate
encodings of one normal form. Shared golden fixtures require Rust and Haskell
to emit identical bytes and digests; finite denotation tests remain a separate
check because byte identity alone does not prove semantic completeness.

\subsection{I4: capture hooks}

Add capture in dependency order:

\begin{enumerate}
  \item schema, mapping, migration, and query compilation;
  \item connectors and source frontiers;
  \item planner and executor;
  \item reconciliation decisions;
  \item materialization and checkpoint publication;
  \item workspaces and distribution; and
  \item policy, export, retention, and deletion.
\end{enumerate}

No hook may claim a stronger identity or completeness class than its owning
boundary can support.

\subsection{I5: queries and interoperability}

Implement bounded origin, why, derivation, upstream, downstream, versions,
assumptions, decisions, execution, survival, and PROV export operations.
Test policy on graph structure and metadata, not only on returned values.

\subsection{I6: equivalence and backend conformance}

Compare the independent oracle, Rust, SQLite, and each supported PostgreSQL
version on the portable fragment. Then test full versus incremental
recomputation, connector translation, crash recovery, and cursor atomicity.
Only passing these gates can promote \code{SYS-PROV-01} or
\code{SYS-MAT-01}.

\section{Formalization roadmap}
\label{sec:formalization}

Formalization should target the finite core, not simulate a database engine.

\subsection{F0: representation and denotation}

Define finite token namespaces, well-formed typed references, positive
derivation circuits, normalization, and evaluation into a commutative
semiring. Candidate theorems are:

\begin{align}
\operatorname{WellFormed}(c)
  &\Longrightarrow \operatorname{WellFormed}(\Norm(c)),\\
\Eval(\Norm(c)) &= \Eval(c),\\
\operatorname{share}(c) &\simeq c.
\end{align}

The last relation means equal denotation under content-addressed sharing, not
equal runtime bytes without a serialization theorem.

\subsection{F1: operator and substitution laws}

Prove the admitted scan, selection, projection, union, and join laws; semiring
identities; associative typed substitution; and selected rewrite
equivalences. State bag assumptions and exclude unsupported operators.

\subsection{F2: finite incremental equality}

For selected positive operators, define batch and delta semantics and prove
normalized data and provenance equality. Crash recovery, connector behavior,
filesystem durability, and database transaction behavior remain systems
tests.

\subsection{F3: finite PROV projection properties}

A tractable target is that required entity, activity, and agent references
appear injectively in the projection and that the loss report marks every
collapsed circuit or value-origin component. Formalizing the whole W3C PROV
family is not an initial objective.

\subsection{F4: later security theorem}

A later profile may state noninterference for two runs that differ only in
high-confidentiality provenance observed by a low principal. Access-control
unit tests do not prove this theorem.

\status{\openclaim{}. No P13 Lean declaration exists. Even future kernel
acceptance would not establish runtime capture completeness.}

\section{Falsification conditions}
\label{sec:falsifiers}

The central engineering hypothesis is rejected or narrowed if a retained
case shows any of the following:

\begin{enumerate}
  \item two different source observations normalize to one token;
  \item the same observation normalizes differently across implementations;
  \item an admitted query disagrees with the independent oracle on rows,
  multiplicity, tokens, or circuits;
  \item composed and sequential mappings disagree;
  \item an enabled rewrite preserves rows but changes required provenance;
  \item a source, connector, or opaque activity is omitted while an answer is
  marked exact;
  \item row lineage is returned as exact value origin;
  \item a reversed reconciliation decision cannot identify affected results;
  \item incremental and full recomputation disagree on data or provenance;
  \item a crash advances a cursor without corresponding durable effects;
  \item W3C PROV export is invalid or omits declared loss;
  \item PROV import is treated as trusted internal evidence without required
  bindings;
  \item a retention or redaction event leaves an answer marked unqualified
  exact;
  \item protected participation is inferable from graph shape, counts,
  errors, continuation tokens, or timing;
  \item a hash chain is presented as proof of capture completeness;
  \item provenance overhead exceeds preregistered bounds for the target
  workload;
  \item the cross-layer envelope does not improve answer correctness over
  row-lineage and event-log baselines; or
  \item the proposed delta is fully explained by an existing system under the
  same semantic, version, decision, and disclosure profile.
\end{enumerate}

Failures are research outputs. A passing rerun cannot replace a failed run
without retaining both and documenting the cause.

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

The profile is intentionally narrow. It does not explain arbitrary SQL,
general recursion, machine-learning internals, human judgment, or remote APIs.
The positive algebra does not silently expand to negation, aggregation,
nulls, ordering, or volatile functions. Stable identifiers remain claims
within a namespace, not proof of authenticity. Retention and disclosure can
make once-available explanations incomplete.

For avoidance of doubt:

\begin{enumerate}
  \item \CatDB{} does not invent why-, where-, lineage-, or semiring
  provenance.
  \item It does not provide complete provenance for arbitrary code, APIs,
  SQL, recursion, machine-learning models, or human decisions.
  \item Category theory does not eliminate provenance-capture cost.
  \item A schema mapping does not by itself determine instance or query
  provenance.
  \item A lineage set is not a complete explanation.
  \item W3C PROV is an interoperability model, not the complete internal
  derivation semantics.
  \item Provenance does not prove truth, correctness, authority, identity,
  trust, or reproducibility.
  \item Source identity does not establish source authenticity.
  \item Vector similarity does not establish semantic identity.
  \item A hash chain does not establish completeness or immutability without
  a threat model and trusted anchors.
  \item Complete provenance is not free in runtime, storage, query, privacy,
  or operational complexity.
  \item Exact provenance is profile-relative and may be unavailable after
  retention or redaction.
  \item Partial source availability cannot yield an unqualified complete
  answer.
  \item Record lineage does not automatically provide field-level origin.
  \item Positive semiring provenance does not automatically cover difference,
  negation, aggregation, recursion, nulls, ordering, or volatile functions.
  \item Incremental data equality does not establish provenance equality.
  \item A physical execution trace does not prove semantic plan correctness.
  \item Provenance alone cannot show that a result survives schema change;
  the changed semantics must be revalidated.
  \item A finite execution DAG does not imply that the complete version
  history is acyclic.
  \item CQL's external capabilities do not establish \CatDB{}
  implementation or performance.
\end{enumerate}

These are design constraints, not rhetorical disclaimers. A future
implementation or paper result that violates one must change the profile or
narrow the claim.

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

The most immediate questions are practical:

\begin{itemize}
  \item Is the positive fragment useful enough to justify exact circuits?
  \item Should v1 store only circuits, or circuits plus a bounded expanded
  form?
  \item Which source observations are strong enough for \(\Exact\)?
  \item How are synthesized target objects tokenized?
  \item Which mapping operator supplies P4's instance-level derivation?
  \item Which reconciliation outcomes may enter results without approval?
  \item What normalization supports independent agreement without excessive
  expansion?
  \item Which graph redactions avoid participation leakage?
  \item What retention horizon is needed for audit, rollback, and practical
  reproduction?
  \item Which provenance modes are affordable in embedded SQLite and remote
  PostgreSQL?
  \item How are remote provenance statements authenticated?
  \item What is the first useful why-not profile?
  \item Which PROV extensions preserve decisions and circuit references
  without misleading consumers?
\end{itemize}

The first valid implementation artifact is the reviewed profile and fixture
suite. Drafting a stronger abstract or adding an untyped event log would not
move the central claim.

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

Provenance becomes first-class when execution cannot return an explanation
without saying what kind of explanation it is. A source token, lineage set,
value origin, derivation circuit, version reference, physical trace, decision
record, and PROV graph each carry useful information. They also each omit
something. The proposed contract keeps those omissions visible.

For the first positive fragment, the relational algebra can reuse provenance
semirings. The remaining work is the bridge: typed substitution across
mappings, immutable version and snapshot references, retrospective activity,
reconciliation evidence, materialization equality, bounded provenance
queries, W3C PROV projection with loss, and completeness that weakens honestly
under opacity, retention, or disclosure.

No such \CatDB{} runtime exists in the current repository. The manuscript
therefore ends at a falsifiable contract. Progress requires reviewed profiles,
hand-derived fixtures, an independent oracle, an owning implementation,
backend and crash conformance, retained benchmarks, and selected finite
theorems. Until those gates pass, ``first-class execution semantics'' names a
research hypothesis, not a systems result.

\appendix

\section{Claim ledger}
\label{app:claims}

\begin{longtable}{L{0.11\textwidth} L{0.41\textwidth} L{0.16\textwidth} L{0.20\textwidth}}
\caption{Manuscript claim status.}
\label{tab:claims}\\
\toprule
ID & Claim & Status & Falsifier or gate \\
\midrule
\endfirsthead
\toprule
ID & Claim & Status & Falsifier or gate \\
\midrule
\endhead
P13-C01 & why, where, lineage, how, workflow, and PROV are distinct models &
\prior{} & primary sources contradict the distinction \\
P13-C02 & positive annotations compose by semiring addition and multiplication
& \prior{} & cited result does not support stated fragment \\
P13-C03 & typed versioned envelope can answer the fixed cross-layer questions
& \enghyp{} & implementation fails correctness or utility gates \\
P13-C04 & profile-v1 normalization is deterministic and denotation preserving
& \openclaim{} & cross-language disagreement or theorem failure \\
P13-C05 & sequential and composed mapping provenance agree & \obstructed{} &
P4 semantics and fixtures required \\
P13-C06 & source tokens identify exact observed records at frontiers &
\openclaim{} & collision, drift, or unsupported connector identity \\
P13-C07 & reconciliation evidence remains distinct from truth & \obstructed{}
& P7 authority and decision profile required \\
P13-C08 & incremental and full data plus provenance agree & \openclaim{} &
retained mismatch or crash/cursor violation \\
P13-C09 & PROV projection is valid and its loss report complete &
\openclaim{} & validator or loss-oracle mismatch \\
P13-C10 & disclosure avoids protected inference & \openclaim{} & red-team
graph, count, error, token, or timing leak \\
P13-C11 & the envelope has acceptable overhead & \openclaim{} &
preregistered workload bound exceeded \\
P13-C12 & selected finite circuit laws are machine checked & \openclaim{} &
named declarations and axiom audit absent \\
\bottomrule
\end{longtable}

\section{Planned artifact layout}
\label{app:artifacts}

\begin{lstlisting}
runs/<run-id>/
  preregistration.json
  manifest.json
  environment.json
  profiles/
  fixtures/
  source-frontiers/
  artifacts/
  circuits/
  value-origins/
  activities/
  decisions/
  materializations/
  explanation-queries.jsonl
  prov-export/
  prov-loss-report.json
  schema-survival.jsonl
  incremental-equivalence.jsonl
  disclosure-audit.jsonl
  failures/
  raw/
  analysis/
  report/
  checksums.txt
\end{lstlisting}

The current repository contains no P13 run with this layout.

\section{Review checklist}
\label{app:review}

A review candidate should be rejected or returned for correction if:

\begin{enumerate}
  \item a provenance model is named imprecisely;
  \item ``exact'' lacks profile, question, granularity, frontier, retention,
  or disclosure scope;
  \item a lineage set is treated as a derivation circuit or value origin;
  \item algebraic scope silently includes an unsupported operator;
  \item a plan trace is treated as proof of semantic correctness;
  \item source identity is treated as authenticity;
  \item reconciliation evidence is treated as truth;
  \item PROV projection loss is omitted;
  \item retained security evidence tests only data-row access;
  \item incremental evidence compares data without provenance;
  \item benchmark modes use unequal provenance profiles;
  \item a formal result is generalized to runtime capture; or
  \item a \CatDB{} claim is promoted without a digest-bound artifact and
  executable witness.
\end{enumerate}

\bibliographystyle{plainnat}
\bibliography{references}

\end{document}
