\documentclass[12pt]{article}

\usepackage{amsmath,amssymb,amsthm}
\usepackage[margin=1in]{geometry}
\usepackage{everypage}
\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{seqsplit}
\usepackage{tikz}
\usepackage{tikz-cd}
\usepackage{url}
\usetikzlibrary{positioning}

\hypersetup{
  colorlinks=true,
  linkcolor=blue!45!black,
  citecolor=green!35!black,
  urlcolor=blue!55!black,
  pdftitle={Mechanizing CatDB: A Lean Kernel for Typed Paths and Equation-Preserving Schema Mappings},
  pdfauthor={Matthew Long; The YonedaAI Collaboration}
}

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

\newcommand{\CatDB}{\textsc{CatDB}}
\newcommand{\Path}{\operatorname{Path}}
\newcommand{\HEq}{\operatorname{HEq}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\machinechecked}{\textsc{machine-checked}}
\newcommand{\execsupported}{\textsc{executable audit evidence}}
\newcommand{\prior}{\textsc{supported by prior literature}}
\newcommand{\enghyp}{\textsc{engineering hypothesis}}
\newcommand{\openclaim}{\textsc{open conjecture}}
\newcommand{\notclaimed}{\textsc{not claimed}}
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\status}[1]{\par\noindent{\normalfont\textit{Status.} #1.}\par}
\newcolumntype{L}[1]{>{\RaggedRight\arraybackslash}p{#1}}

\setlength{\emergencystretch}{3em}
\setlist{itemsep=0.25em,topsep=0.4em}
\lstdefinelanguage{Lean}{
  morekeywords={structure,inductive,where,namespace,end,def,theorem,universe,
    import,extends,forall,fun,by,with,exact,have,change,rw,intro,constructor},
  sensitive=true,
  morecomment=[l]{--},
  morecomment=[s]{/-}{-/},
  morestring=[b]"
}
\lstset{
  basicstyle=\ttfamily\footnotesize,
  breaklines=true,
  breakatwhitespace=false,
  columns=fullflexible,
  frame=single,
  rulecolor=\color{black!20},
  showstringspaces=false
}

\definecolor{grokgray}{RGB}{110,110,110}
\AddEverypageHook{%
  \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-lean-kernel\quad
       [\,cs.DB; cs.LO\,]\quad
       23 Jul 2026};
    \end{tikzpicture}
  \fi
}

\title{Mechanizing \CatDB:\\
A Lean Kernel for Typed Paths and\\
Equation-Preserving Schema Mappings}
\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}
A formalization can make a database claim more precise, but it can also make a
small result sound larger than it is.  We report the first Lean slice of
\CatDB{}, a proposed semantic data platform in which schemas and mappings are
first-class objects.  The checked kernel contains a typed directed graph,
endpoint-indexed paths, a supplied equivalence relation on parallel paths, raw
schema mappings, and mappings carrying a proof that they preserve that
relation.  Lean 4.32.1 checks empty-path identities, typing and associativity
of path composition, lawfulness of identity and composite mappings, and
mapping unit and associativity laws under a stated extensional equality.

The result is deliberately narrow.  The theorem called
\code{comp\_typed} is a reflexive witness whose real content lies in the
dependent type of composition.  A schema presentation supplies its path
equivalence and its laws; the library does not generate or decide a
congruence.  The checked model has no finiteness witness, attributes, scalar
domains, database instances, data migration, queries, SQL, backends,
transactions, or distributed semantics.  It also has no refinement proof
connecting Lean objects to the Rust runtime, Haskell reference model, or
serialized fixtures.

We give the exact source-level statements for the six program invariants
\code{PATH-02}--\code{PATH-04} and
\code{MAP-03}--\code{MAP-05}, audit their assumptions, and reproduce the build
in an isolated directory.  The build reports no axiom dependencies for nine
covered declarations; three audit-specific Python tests and the full
19-test utility suite pass.  These facts are \machinechecked{} or
\execsupported{} only at the named boundary.  The paper's contribution is a
reproducible formalization boundary and a roadmap toward finite instances,
pullback migration, cross-language refinement, and selected query rewrites,
not a claim that the \CatDB{} database system is verified.
\end{abstract}

\tableofcontents

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

\subsection{Plain-language problem}

A database system can pass thousands of tests while still leaving its most
important semantic assumptions implicit.  Consider a mapping that sends a
source relationship to a longer path in a target schema.  The implementation
must know that the path starts and ends at the right objects.  It must preserve
the source equations that express semantic agreement between paths.  When two
mappings are composed, the result should preserve those equations as well.
These are small laws, but they sit underneath migration, query rewriting, and
integration.

Proof assistants offer one way to make such laws explicit.  Yet the phrase
``formally verified database'' is dangerous when the checked artifact contains
only a few mathematical definitions.  A proof about path append does not
verify SQL generation.  A proof that two abstract mapping constructions are
extensionally equal does not verify their serialized identifiers, provenance,
or physical effects.  A theorem accepted by Lean says exactly what its type
says and nothing about unmodeled code.

This paper therefore treats formalization scope as part of the result.  We
describe the smallest accepted Lean kernel in the \CatDB{} research program,
quote its checked statements, expose its assumptions, reproduce its axiom
inventory, and draw a hard line around everything that remains outside the
model.

\subsection{Research question}

The research question is:

\begin{quote}
\emph{What is the smallest \CatDB{} semantic kernel that can be represented
and checked in Lean without implying that the database engine, its serialized
artifacts, or its physical plans have been verified?}
\end{quote}

The answer in this slice is: typed paths and equation-preserving schema
mappings.  More precisely, the library checks path identities, endpoint
alignment through indices, path associativity, mapping preservation by
identity and composition, and mapping category laws under a chosen
extensional relation.  It does not yet check data.

\subsection{Contributions}

This paper makes five contributions.

\begin{enumerate}
  \item It gives a source-faithful account of a 346-line Lean kernel for typed
  paths and mappings.  The account distinguishes definitions, proof fields,
  theorems, and build evidence.

  \item It maps six \CatDB{} program invariants to nine declarations and states
  every assumption needed for their interpretation.

  \item It reproduces the formal build under the pinned Lean 4.32.1 toolchain,
  records the transitive axiom inventory, and separates kernel evidence from a
  Python source-hygiene audit.

  \item It compares the kernel with general category theory, mathlib, and
  categorical database theory.  The elementary mathematics is prior art; the
  contribution is the checked project boundary and its reproducibility
  discipline.

  \item It gives a staged formalization roadmap whose next proof obligations
  are finite instances, pullback migration, cross-language refinement, and a
  deliberately small query-rewrite fragment.
\end{enumerate}

\subsection{Evidence labels}

We use evidence labels literally.

\begin{itemize}
  \item \machinechecked{} means that the exact Lean declaration was accepted
  by the pinned toolchain and is named in the coverage inventory.
  \item \execsupported{} means that a command or test ran successfully.  It
  does not turn the tested program into a theorem.
  \item \prior{} means that the underlying idea is established in the cited
  primary literature.
  \item \enghyp{} marks a proposed implementation or formalization step.
  \item \openclaim{} marks a proposition for which this work supplies no proof.
  \item \notclaimed{} marks an attractive inference that the paper explicitly
  rejects.
\end{itemize}

No theorem in this paper is labeled merely ``proved'' when its authority is a
Lean declaration.  The machine-checked label points to the checked statement,
not to a prose paraphrase.

\subsection{Result boundary}

\Cref{fig:boundary} summarizes the boundary.  The top box is the entire
machine-checked semantic object.  The lower boxes are planned program layers,
not consequences of the top box.

\begin{figure}[ht]
\centering
\begin{tikzpicture}[
  node distance=8mm,
  every node/.style={draw, rounded corners, align=center, text width=0.83\linewidth,
    inner sep=7pt},
  checked/.style={fill=green!8},
  open/.style={fill=orange!8}
]
\node[checked] (k) {\textbf{Machine-checked F3 kernel}\\
typed graph, endpoint-indexed paths, supplied parallel-path equivalence,
equation-preserving mappings, named identity and associativity laws};
\node[open, below=of k] (i) {\textbf{Not modeled: semantic data}\\
finite presentations, attributes, scalar domains, instances, equation
validation, $\Delta/\Sigma/\Pi$ migration, loss analysis};
\node[open, below=of i] (r) {\textbf{Not modeled: runtime correspondence}\\
JSON decoding, Rust/Haskell refinement, query IR and denotation, SQL lowering,
SQLite/PostgreSQL execution};
\node[open, below=of r] (d) {\textbf{Not modeled: operational system}\\
transactions, provenance propagation, materialization, replication,
consistency, sharding, distributed workspaces};
\draw[->,thick] (k) --
  node[right,draw=none,font=\scriptsize,text width=0.18\linewidth]
  {\enghyp{}} (i);
\draw[->,thick] (i) -- (r);
\draw[->,thick] (r) -- (d);
\end{tikzpicture}
\caption{The checked kernel is a prerequisite for later layers, not a
verification of them.}
\label{fig:boundary}
\end{figure}

\section{A concrete example}
\label{sec:example}

Suppose a source schema has objects \(\mathsf{Order}\),
\(\mathsf{Customer}\), and \(\mathsf{Region}\), with generators
\[
  \mathsf{buyer}:\mathsf{Order}\to\mathsf{Customer},
  \qquad
  \mathsf{region}:\mathsf{Customer}\to\mathsf{Region}.
\]
The path
\[
  \mathsf{buyer};\mathsf{region}:
  \mathsf{Order}\to\mathsf{Region}
\]
is well typed because the target of \(\mathsf{buyer}\) matches the source of
\(\mathsf{region}\).  A path that attempts to traverse
\(\mathsf{region}\) first from \(\mathsf{Order}\) cannot be constructed in the
intrinsic Lean representation.

Now let a target schema represent the same meaning with different objects and
longer routes:
\[
\begin{tikzcd}[column sep=large]
\mathsf{Purchase} \arrow[r,"\mathsf{account}"] &
\mathsf{Account} \arrow[r,"\mathsf{owner}"] &
\mathsf{Party} \arrow[r,"\mathsf{territory}"] &
\mathsf{Territory}.
\end{tikzcd}
\]
A raw mapping can send \(\mathsf{Order}\) to \(\mathsf{Purchase}\),
\(\mathsf{Customer}\) to \(\mathsf{Party}\), and the generator
\(\mathsf{buyer}\) to the two-step target path
\(\mathsf{account};\mathsf{owner}\).  The path indices ensure that the image
starts at \(\mathsf{Purchase}\) and ends at \(\mathsf{Party}\).

If the source declares two parallel paths equivalent, lawfulness asks for
evidence that their mapped target paths are equivalent too.  The current Lean
slice represents that evidence as a field of the mapping.  It does not search
for a proof, inspect a database, or decide a presented equational theory.

This example illustrates both the value and the limit of the encoding.  A
misaligned path is excluded from the intrinsic model.  A law-preserving
mapping must carry a proof.  But a JSON document with misspelled identifiers
can still exist outside Lean, and no theorem here says that a production
decoder rejects it.  Likewise, no rows move from a source table to a target
table in this example.  That operational work belongs to later layers.

\section{Formal kernel}
\label{sec:kernel}

\subsection{Typed directed graphs}

The kernel begins with a universe-polymorphic typed multigraph.

\begin{lstlisting}[language=Lean,caption={The checked graph structure.}]
universe u

structure Graph where
  Obj : Type u
  Hom : Obj -> Obj -> Type u
\end{lstlisting}

For each pair of objects \(A,B\), the type \(G.\mathrm{Hom}\,A\,B\) contains
the generating arrows from \(A\) to \(B\).  Parallel generators need not be
equal.  The definition requires neither finite objects nor finite hom-types.
It also does not require decidable equality.

\begin{remark}[Universe choice]
Objects and generating arrows inhabit the same universe level in this slice.
Nothing in the covered theorems needs finiteness, enumeration, or
\code{DecidableEq}.  This simplicity is an explicit modeling choice, not a
database schema implementation.
\end{remark}

\subsection{Endpoint-indexed paths}

Paths form an indexed inductive family.

\begin{lstlisting}[language=Lean,caption={Endpoint-indexed paths.}]
inductive Path (G : Graph) : G.Obj -> G.Obj -> Type u
  | nil (A : G.Obj) : Path G A A
  | cons {A B C : G.Obj} :
      G.Hom A B -> Path G B C -> Path G A C
\end{lstlisting}

The indices \(A\) and \(B\) are part of the type
\(\Path_G(A,B)\).  The \code{nil} constructor produces the empty path at
\(A\).  The \code{cons} constructor prepends a generator \(A\to B\) to a path
\(B\to C\).  This is a standard use of indexed inductive families in dependent
type theory \cite{leanReferenceInductive,avigadTheoremProvingLean4}.

Composition follows traversal order:

\begin{lstlisting}[language=Lean,caption={Path composition.}]
def comp {G : Graph} {A B C : G.Obj} :
    Path G A B -> Path G B C -> Path G A C
  | .nil _, q => q
  | .cons f rest, q => .cons f (comp rest q)
\end{lstlisting}

Thus \code{comp p q} means first traverse \(p\), then \(q\).  The shared
middle object \(B\) occurs in both input types.  A caller inside this model
cannot supply an \(A\to B\) path and a \(C\to D\) path unless Lean can identify
\(B\) and \(C\).

\subsection{Schema presentations}

The schema structure adds a relation between parallel paths.

\begin{lstlisting}[language=Lean,caption={The checked schema-presentation boundary.}]
structure SchemaPresentation where
  graph : Graph
  Equivalent :
    {A B : graph.Obj} ->
      Path graph A B -> Path graph A B -> Prop
  equivalent_refl :
    forall {A B} (p : Path graph A B), Equivalent p p
  equivalent_symm :
    forall {A B} {p q : Path graph A B},
      Equivalent p q -> Equivalent q p
  equivalent_trans :
    forall {A B} {p q r : Path graph A B},
      Equivalent p q -> Equivalent q r -> Equivalent p r
  equivalent_comp :
    forall {A B C} {p q : Path graph A B}
      {r s : Path graph B C},
      Equivalent p q -> Equivalent r s ->
        Equivalent (Path.comp p r) (Path.comp q s)
\end{lstlisting}

This definition deserves careful interpretation.  It packages:

\begin{enumerate}
  \item a typed graph;
  \item a chosen relation on every family of parallel paths;
  \item witnesses that the relation is reflexive, symmetric, and transitive;
  \item a witness that it is compatible with composition.
\end{enumerate}

It does not package a finite equation list.  It does not construct the least
congruence containing such a list.  It does not offer a decision procedure for
\code{Equivalent}.  The relation and its laws are supplied by a value of the
structure.

Category theory ordinarily treats associativity and identity laws as part of a
category and treats functors as preserving identities and composition
\cite{maclane1998categories,leinster2014basic}.  The present representation is
closer to a typed path syntax together with a compatible equivalence relation.
A quotient category is mathematically nearby, but it is not constructed in
the source.

\subsection{Raw mappings}

A raw mapping acts on objects and generating arrows:

\begin{lstlisting}[language=Lean,caption={Raw mappings.}]
structure RawMapping (S : Graph) (T : Graph) where
  onObj : S.Obj -> T.Obj
  onHom :
    {A B : S.Obj} -> S.Hom A B ->
      Path T (onObj A) (onObj B)
\end{lstlisting}

The image of a source generator may be a composite target path.  The path
indices encode its required endpoints.  The recursive function
\code{mapPath} extends the generator action to every source path:

\begin{lstlisting}[language=Lean,caption={Extension from generators to paths.}]
def mapPath (F : RawMapping S T) :
    Path S A B -> Path T (F.onObj A) (F.onObj B)
  | .nil _ => .nil (F.onObj A)
  | .cons f rest =>
      Path.comp (F.onHom f) (mapPath F rest)
\end{lstlisting}

Three supporting lemmas establish that mapping respects path composition, that
the identity raw mapping acts identically on paths, and that path mapping
through a composite raw mapping equals sequential path mapping.

\subsection{Extensional equality}

The mapping category laws do not use Lean's structural equality on
\code{RawMapping}.  They use:

\begin{lstlisting}[language=Lean,caption={Extensional equality of raw mappings.}]
def ExtensionalEq (F G : RawMapping S T) : Prop :=
  F.onObj = G.onObj /\
    forall {A B} (f : S.Hom A B),
      HEq (F.onHom f) (G.onHom f)
\end{lstlisting}

Equality of object actions is paired with heterogeneous equality of generator
images.  Heterogeneous equality is appropriate because those images inhabit
path types whose indices depend on the object action.

\begin{remark}[What has not been bundled]
The source does not prove that \code{ExtensionalEq} is reflexive, symmetric,
and transitive.  It does not prove that composition respects it in both
arguments.  It therefore does not yet build a mathlib \code{Category} whose
morphisms are equivalence classes of lawful mappings.  The MAP-05 results are
the three named propositions only.
\end{remark}

\subsection{Lawful mappings}

A lawful mapping extends a raw mapping with a preservation witness:

\begin{lstlisting}[language=Lean,caption={Equation-preserving mappings.}]
structure LawfulMapping
    (S : SchemaPresentation)
    (T : SchemaPresentation)
    extends RawMapping S.graph T.graph where
  preserves :
    forall {A B} {p q : Path S.graph A B},
      S.Equivalent p q ->
        T.Equivalent
          (toRawMapping.mapPath p)
          (toRawMapping.mapPath q)
\end{lstlisting}

The definition expresses a semantic obligation exactly: source-equivalent
paths map to target-equivalent paths.  It does not decide that obligation.
Constructing a lawful mapping requires the caller to provide a term of the
\code{preserves} field.

\section{Machine-checked path coverage}
\label{sec:path-coverage}

\subsection{\code{PATH-02}: identities}

The first invariant is represented by two theorems.

\begin{lstlisting}[language=Lean]
theorem id_comp (p : Path G A B) :
    comp (id G A) p = p := by
  rfl

theorem comp_id (p : Path G A B) :
    comp p (id G B) = p := by
  induction p with
  | nil _ => rfl
  | cons f rest ih =>
      simp only [comp]
      rw [ih]
\end{lstlisting}

\status{\machinechecked}

The left identity follows by reduction of \code{comp}.  The right identity is
proved by induction because \code{comp} recurses on its first argument.  The
result holds for every value of the abstract \code{Graph} structure.

The original program-language statement referred to an object belonging to a
schema and an empty serialized path.  The Lean result does not model
membership in a finite schema artifact.  Its exact content is the algebraic
identity of the indexed path constructors.

\subsection{\code{PATH-03}: typed composition}

The covered theorem is:

\begin{lstlisting}[language=Lean]
theorem comp_typed
    (p : Path G A B) (q : Path G B C) :
    Exists (fun r : Path G A C => r = comp p q) :=
  Exists.intro (comp p q) rfl
\end{lstlisting}

\status{\machinechecked, with the qualification below}

The proof supplies \code{comp p q} and reflexivity.  As a proposition, the
theorem is immediate.  The substantive typing guarantee appears in the type of
\code{comp}:
\[
  \Path_G(A,B)\to\Path_G(B,C)\to\Path_G(A,C).
\]
The library's coverage record says that endpoint alignment is represented in
types.  It does not say that the theorem decides whether two serialized
identifiers match.

\begin{remark}[Why the qualification matters]
Calling \code{comp\_typed} a nontrivial typing-soundness theorem would be
misleading.  There is no extrinsic syntax, typing judgment, or failing input in
the model.  Ill-aligned inputs cannot be given to \code{comp}; the result type
already carries the outer endpoints.  The theorem simply reifies that
function application as an existential witness.
\end{remark}

\subsection{\code{PATH-04}: associativity}

The associativity theorem is:

\begin{lstlisting}[language=Lean]
theorem comp_assoc
    (p : Path G A B)
    (q : Path G B C)
    (r : Path G C D) :
    comp (comp p q) r =
      comp p (comp q r) := by
  induction p with
  | nil _ => rfl
  | cons f rest ih =>
      simp only [comp]
      rw [ih]
\end{lstlisting}

\status{\machinechecked}

The induction again follows the recursive structure of the first path.  This
is the ordinary associativity of list-like append, indexed by endpoints.  It
does not establish that reassociating a query plan preserves bag multiplicity,
null behavior, errors, ordering, cost, or backend execution.  Those properties
require a query denotation that the library does not contain.

\section{Machine-checked mapping coverage}
\label{sec:mapping-coverage}

\subsection{\code{MAP-03}: lawful identity}

For every schema presentation \(S\), the source constructs:

\begin{lstlisting}[language=Lean]
def LawfulMapping.id
    (S : SchemaPresentation) :
    LawfulMapping S S where
  toRawMapping := RawMapping.id S.graph
  preserves := by
    intro A B p q h
    change S.Equivalent
      (RawMapping.mapPath
        (RawMapping.id S.graph) p)
      (RawMapping.mapPath
        (RawMapping.id S.graph) q)
    rw [RawMapping.mapPath_id,
        RawMapping.mapPath_id]
    exact h
\end{lstlisting}

\status{\machinechecked}

The proof starts with a supplied hypothesis \(h:S.\mathrm{Equivalent}\,p\,q\).
After rewriting identity path mapping, the goal is exactly \(h\).  No
equational decision procedure is invoked.

The result excludes serialization details.  A production identity mapping may
have an artifact identifier, schema-version fields, provenance, or display
metadata.  None of those fields appears in the Lean object, so none is covered.

\subsection{\code{MAP-04}: lawfulness under composition}

For lawful mappings \(F:S\to T\) and \(G:T\to U\), the checked constructor is:

\begin{lstlisting}[language=Lean]
def LawfulMapping.comp
    (F : LawfulMapping S T)
    (G : LawfulMapping T U) :
    LawfulMapping S U where
  toRawMapping :=
    RawMapping.comp F.toRawMapping G.toRawMapping
  preserves := by
    intro A B p q h
    have mappedByF := F.preserves h
    have mappedByG := G.preserves mappedByF
    change U.Equivalent
      (RawMapping.mapPath
        (RawMapping.comp
          F.toRawMapping G.toRawMapping) p)
      (RawMapping.mapPath
        (RawMapping.comp
          F.toRawMapping G.toRawMapping) q)
    rw [RawMapping.mapPath_compMapping,
        RawMapping.mapPath_compMapping]
    exact mappedByG
\end{lstlisting}

\status{\machinechecked}

The proof is compositional in a precise but conditional sense.  It assumes
that \(F\) and \(G\) already carry preservation proofs.  It first transports
the source relation through \(F\), then transports the resulting target
relation through \(G\), and finally rewrites the raw path action of the
composite.

This is not an algorithm for discovering a schema mapping.  It is not an
algorithm for proving a candidate mapping lawful.  It does not inspect source
records, move data, or detect information loss.  It shows closure of the
proof-carrying construction.

\subsection{\code{MAP-05}: units and associativity}

The lawful-mapping namespace exposes three theorems:

\begin{lstlisting}[language=Lean]
theorem LawfulMapping.comp_id_ext
    (F : LawfulMapping S T) :
  RawMapping.ExtensionalEq
    (comp F (id T)).toRawMapping
    F.toRawMapping

theorem LawfulMapping.id_comp_ext
    (F : LawfulMapping S T) :
  RawMapping.ExtensionalEq
    (comp (id S) F).toRawMapping
    F.toRawMapping

theorem LawfulMapping.comp_assoc_ext
    (F : LawfulMapping S T)
    (G : LawfulMapping T U)
    (H : LawfulMapping U V) :
  RawMapping.ExtensionalEq
    (comp (comp F G) H).toRawMapping
    (comp F (comp G H)).toRawMapping
\end{lstlisting}

\status{\machinechecked}

The proofs delegate to the corresponding raw-mapping results.  Object actions
are definitionally equal.  Generator images are shown heterogeneously equal
using the support lemmas for mapping paths through identities and composites.

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.15\textwidth}L{0.28\textwidth}X}
\toprule
Invariant & Checked proposition & Excluded interpretation \\
\midrule
\code{MAP-03} &
Identity raw action plus a preservation proof forms a lawful mapping. &
Canonical serialized identity artifact or attribute/value mapping. \\
\code{MAP-04} &
Two proof-carrying lawful mappings compose to another. &
Automatic proof search, data migration, or information-loss analysis. \\
\code{MAP-05} &
Unit and associativity propositions under the exact
\code{ExtensionalEq}. &
Equality of mapping records, artifact IDs, provenance, or a fully bundled
category. \\
\bottomrule
\end{tabularx}
\caption{Mapping coverage and its nearest tempting overclaim.}
\label{tab:mapping-coverage}
\end{table}

\section{What the schema assumptions mean}
\label{sec:assumptions}

\subsection{The equivalence relation is an input}

The field \(S.\mathrm{Equivalent}\) can be read as the semantic equality used
by the formal profile.  Its equivalence and composition-congruence properties
are structure fields.  Every \code{SchemaPresentation} value must supply them.
The mapping theorems are parametric in that supplied relation.

This design is enough to state preservation cleanly.  It avoids committing the
first slice to a particular equational prover.  It also means that the current
formalization does not answer a central executable question: given a finite
list of path equations, how should the runtime establish equality of two
paths?

One future answer may construct the generated congruence inductively.  Another
may define a normalization algorithm for a restricted terminating rewrite
system.  A third may use proof-carrying mapping artifacts.  Each choice has
different completeness, decidability, and performance properties.  The
present code deliberately proves none of them.

\subsection{No finiteness or decidable equality}

Database schemas are finite artifacts in the implementation roadmap, but
\code{Graph.Obj} and \code{Graph.Hom} are arbitrary types.  The theorems are
therefore more general in one dimension and less executable in another.  They
apply without a finiteness assumption, but they do not produce enumeration,
validation, or diagnostics.

This difference matters for interpretation.  A production validator may need
to check that every arrow endpoint resolves and that identifiers are unique.
Those are representation-level obligations.  The indexed Lean model begins
after valid objects and arrows already exist.

\subsection{No attributes or values}

The graph has only objects and arrows.  It does not distinguish entity types
from value types, nor does it model attributes, integer ranges, decimal
lexemes, UUIDs, nullability, cardinality, or identity rules.  Algebraic
database models explicitly address typeside operations and concrete data
\cite{schultz2017algebraic}.  This Lean slice does not.

\subsection{No instances}

Categorical database theory commonly models an instance as a set-valued
functor from a schema category \cite{spivak2012functorial,
spivakWisnesky2015relational}.  There is no \code{Instance} declaration in the
audited source.  Consequently:

\begin{itemize}
  \item path equality has no pointwise data interpretation;
  \item the library cannot state that a database satisfies a schema equation;
  \item no migration functor acts on data;
  \item no query returns records;
  \item no finite validator is sound or complete.
\end{itemize}

These are roadmap items, not hidden corollaries.

\section{Build, axiom inventory, and trust}
\label{sec:trust}

\subsection{Pinned environment}

The project pins:

\begin{lstlisting}[language={},caption={\code{lean-toolchain}.}]
leanprover/lean4:v4.32.1
\end{lstlisting}

The Lake package sets \code{autoImplicit} to false and warnings as errors.  Its
manifest has no external packages.  The official Lake documentation describes
\code{lean-toolchain}, the package configuration, the manifest, and
\code{.lake} build artifacts \cite{leanReferenceLake}.  The absence of
external packages keeps this slice small; it does not make Lean's standard
library or toolchain disappear from the trusted base.

\subsection{Isolated reproduction}

For this paper, the formal sources and configuration were copied to a newly
created temporary directory.  The build did not reuse the repository's
\code{.lake} directory.  The observed compiler was:

\begin{lstlisting}[language={}]
Lean (version 4.32.1, arm64-apple-darwin24.6.0,
commit f054605aea4b840552cca2e725580bffd1e1b704, Release)
\end{lstlisting}

The clean build completed seven jobs successfully.

\subsection{Transitive axiom inventory}

\code{CatDB.Coverage} executes \code{\#print axioms} for nine declarations.
Lean's reference manual states that this command reports the axioms used by a
declaration transitively \cite{leanReferenceAxioms}.  The isolated build
reported:

\begin{lstlisting}[language={}]
'CatDB.Path.id_comp' does not depend on any axioms
'CatDB.Path.comp_id' does not depend on any axioms
'CatDB.Path.comp_typed' does not depend on any axioms
'CatDB.Path.comp_assoc' does not depend on any axioms
'CatDB.LawfulMapping.id' does not depend on any axioms
'CatDB.LawfulMapping.comp' does not depend on any axioms
'CatDB.LawfulMapping.comp_id_ext' does not depend on any axioms
'CatDB.LawfulMapping.id_comp_ext' does not depend on any axioms
'CatDB.LawfulMapping.comp_assoc_ext' does not depend on any axioms
\end{lstlisting}

\status{\machinechecked{} build evidence for these declarations and this source
state}

An empty reported inventory rules out transitive use of user axioms and
\code{sorryAx} in the covered declarations.  It does not eliminate the trusted
computing base.  We trust the Lean 4.32.1 elaborator and kernel, the standard
library needed by these declarations, the platform on which they ran, and the
accuracy with which this paper maps prose to source.  Lean 4's system design is
described by de Moura and Ullrich \cite{demoura2021lean4}; dependent type
checking remains the formal authority, not the manuscript.

\subsection{Why source scans are secondary}

The checked-in Python audit strips comments and strings, rejects
\code{sorry}, \code{admit}, \code{sorryAx}, and declarations introduced by
\code{axiom}, then searches for required symbol substrings.  Three unit tests
cover placeholder rejection, comment/string handling, and unterminated block
comments.

The audit is useful because it fails quickly on common proof holes.  It is not
a Lean parser.  It does not compare fully elaborated theorem types with a
coverage contract.  Required-name substring checks can be spoofed.  Its
prohibited-token list is narrower than a comprehensive trusted-code policy.
For these reasons the kernel's axiom inventory is normative, while the Python
script is source hygiene.

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.25\textwidth}L{0.25\textwidth}X}
\toprule
Evidence & What it establishes & What it does not establish \\
\midrule
Lean elaboration and kernel checking &
The declaration has the checked type under the toolchain. &
The prose means the same thing, or production code refines the definition. \\
\code{\#print axioms} &
Transitive axiom dependencies reported by Lean. &
Absence of bugs in Lean or correctness of unmodeled components. \\
Python source audit &
Named tokens are absent after its lexical stripping, and names appear. &
Theorem semantics, axiom freedom, or a secure trusted-code policy. \\
Python unit tests &
The audit behaves as expected on three cases. &
Coverage of all lexical edge cases or Lean constructs. \\
Historical code review &
An independent reviewer reproduced and critiqued the slice. &
Peer review of this paper or permanent correctness of later source. \\
\bottomrule
\end{tabularx}
\caption{Evidence sources are complementary, not interchangeable.}
\label{tab:evidence}
\end{table}

\section{Relationship to prior work}
\label{sec:prior}

\subsection{Lean and mathlib}

Lean is both an interactive theorem prover and a functional programming
language based on dependent type theory \cite{demoura2015lean,
demoura2021lean4}.  Indexed inductive families are a standard Lean mechanism;
the endpoint-indexed \code{Path} is a direct use of that mechanism
\cite{leanReferenceInductive}.

The mathlib library contains general category, functor, and natural
transformation infrastructure \cite{mathlib2020,mathlibCategoryBasic}.  The
current \CatDB{} package has no external Lean dependency, including no mathlib
dependency.  It uses a small bespoke structure because the F3 gate targets
specific path and mapping invariants.  This choice reduces the dependency
surface, but it leaves general categorical bundling and interoperability for
later work.

\subsection{Category theory}

Identity, associativity, functors, and composition are elementary category
theory \cite{maclane1998categories,leinster2014basic}.  The checked path
theorems resemble the laws of a free category on a graph.  The supplied
equivalence relation resembles the congruence needed to pass from path syntax
to a presented category.  However, the source neither constructs the free
category as a library object nor forms a quotient by a generated congruence.

Accordingly, the paper claims no new mathematical theorem.  Its value is
engineering precision: the \CatDB{} invariant IDs are tied to terms that a
kernel checks, and the assumptions are visible.

\subsection{Categorical databases}

Schemas as categories, instances as functors, and data migration along schema
mappings are established ideas.  Spivak develops functorial data migration
\cite{spivak2012functorial}.  Spivak and Wisnesky connect the categorical
construction to relational foundations and describe the induced
\(\Sigma_F\), \(\Delta_F\), and \(\Pi_F\) functors
\cite{spivakWisnesky2015relational}.  Algebraic databases extend the
set-valued-functor model with typeside algebra for concrete data
\cite{schultz2017algebraic}.  Categorical data integration has also been
demonstrated in scientific applications \cite{brown2019categorical}.

The current Lean library stops before all of those instance-level
constructions.  It mechanizes only typed paths and preservation structure.  In
particular, no result about \(\Delta\) migration should be attributed to this
paper even though such a result is a planned next step.

\subsection{Mechanized query reasoning}

Cosette and HoTTSQL show that meaningful query-equivalence verification
requires a query language and a carefully defined semantics
\cite{chu2017cosette,chu2017hottsql}.  SQL multiplicities, nulls, correlated
subqueries, aggregation, and other features cannot be reduced to path
associativity without additional modeling.

The contrast is useful.  \code{PATH-04} may eventually support a proof about a
typed path-navigation rewrite.  It does not currently express a SQL query,
much less prove an optimizer correct.

\subsection{Novelty assessment}

\begin{longtable}{L{0.29\textwidth}L{0.19\textwidth}L{0.43\textwidth}}
\caption{Novelty ledger.}\label{tab:novelty}\\
\toprule
Item & Status & Assessment \\
\midrule
\endfirsthead
\toprule
Item & Status & Assessment \\
\midrule
\endhead
Endpoint-indexed paths &
\prior &
Standard indexed-family technique applied to the \CatDB{} kernel. \\
Path identity and associativity &
\prior{} and \machinechecked &
Elementary mathematics, checked in this exact encoding. \\
Equation-preserving schema mappings &
\prior{} and \machinechecked &
Categorical preservation is established; the project-specific structure and
proof terms are checked. \\
Mapping unit and associativity laws &
\prior{} and \machinechecked &
Checked under the exact \code{ExtensionalEq}, without a bundled category. \\
Axiom-visible invariant coverage &
\execsupported &
Project-specific reproducibility practice that ties program IDs to build
output. \\
Verified finite \CatDB{} instances &
\notclaimed &
No instance type exists in the audited source. \\
Verified data migration or query compilation &
\notclaimed &
No migration, query, or backend semantics exists in the audited source. \\
Cross-language semantic equivalence &
\openclaim &
No refinement relation connects Lean with Rust, Haskell, or JSON. \\
\bottomrule
\end{longtable}

\section{Exact nonclaims}
\label{sec:nonclaims}

The following exclusions are part of the theorem statement at program scale.

\subsection{Representation and validation}

The library does not verify that:

\begin{itemize}
  \item serialized schema identifiers are unique;
  \item arrow endpoints resolve;
  \item a JSON path is well typed;
  \item normalization is deterministic;
  \item diagnostic codes or JSON pointers are correct;
  \item artifact identifiers survive mapping composition.
\end{itemize}

These obligations concern a decoder and normalized runtime representation that
are absent from the formal model.

\subsection{Database semantics}

The library has no:

\begin{itemize}
  \item finite carriers or database records;
  \item total arrow interpretations;
  \item attributes or scalar values;
  \item pointwise equation-satisfaction relation;
  \item instance homomorphisms;
  \item bag, set, null, or error semantics.
\end{itemize}

Therefore it proves no fact about a database state.

\subsection{Migration and integration}

The library does not define \(\Delta\), \(\Sigma\), or \(\Pi\).  It does not
prove migration totality, identity, composition, adjunctions, or
information-loss properties.  It does not say that semantic mappings replace
physical ETL, nor that a mapping can be written back safely.

\subsection{Compilation and execution}

The library does not define queries, logical plans, physical plans, SQL,
SQLite, PostgreSQL, APIs, materialization, incremental maintenance, or cost
models.  A path theorem is not execution evidence.

\subsection{Distributed semantics}

The library does not define operations, replicas, clocks, causality, CRDTs,
partitions, consensus, consistency levels, workspaces, or merge policies.
Category theory does not remove distributed-systems tradeoffs, and this
formalization does not model them.

\subsection{Whole-system verification}

The phrase ``\CatDB{} is verified'' is false on the evidence in this paper.
The defensible statement is:

\begin{quote}
Lean 4.32.1 machine-checks the named typed-path and
equation-preserving-mapping declarations at the recorded source hashes, and
reports no transitive axiom dependencies for the nine covered declarations.
\end{quote}

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

\subsection{R1: harden the current boundary}

The first improvements should make the present claim easier to audit.

\begin{enumerate}
  \item Replace required-name substring matching with a machine-readable
  coverage contract tied to elaborated declaration types.
  \item Prove that \code{ExtensionalEq} is an equivalence relation.
  \item Prove that raw mapping composition respects \code{ExtensionalEq}.
  \item Bundle schemas and lawful mappings into a category only after the
  equality and congruence obligations are complete.
  \item Add an independent \code{leanchecker} replay to the release gate.
\end{enumerate}

Each item is an \enghyp{} until implemented and checked.

\subsection{R2: finite presentations and equation evidence}

The current \code{SchemaPresentation} should not be overloaded with executable
finiteness.  A later layer should separately define:

\begin{itemize}
  \item a finite collection of object and generator identifiers;
  \item a finite collection of parallel path equations;
  \item an intrinsic semantic graph obtained from validated input;
  \item the generated congruence or a named decidable fragment;
  \item soundness of any normalization or proof-search procedure.
\end{itemize}

Completeness should be claimed only for a precisely bounded fragment.  General
equality in finitely presented categories is not made decidable by calling the
schema finite.

\subsection{R3: attributes and finite instances}

The next high-value semantic layer is a finite instance model.  It should
include:

\begin{enumerate}
  \item one finite carrier for every entity;
  \item total functions for every relationship generator;
  \item a bounded scalar profile for attributes;
  \item target-carrier membership and scalar typing;
  \item pointwise satisfaction of path equations.
\end{enumerate}

The principal theorem targets are soundness and completeness of the finite
validator for its exact model.  Completeness must not silently include nulls,
partial arrows, SQL constraints, or infinite domains.

\subsection{R4: pullback migration}

Once instances exist, the first migration target is the contravariant
pullback \(\Delta_F\).  The intended obligations are:

\begin{itemize}
  \item a lawful \(F:S\to T\) and valid \(T\)-instance produce a valid
  \(S\)-instance;
  \item \(\Delta_{\id}\) is extensionally the identity;
  \item
  \(\Delta_{G\circ F}\) agrees with
  \(\Delta_F\circ\Delta_G\).
\end{itemize}

These are established categorical patterns
\cite{spivak2012functorial,spivakWisnesky2015relational}, but they remain
\openclaim{} for the \CatDB{} finite model.

\(\Sigma\) and \(\Pi\) should wait.  Their practical formalization depends on
quotients, representatives, finite computation, and complexity choices that
the current program has not fixed.

\subsection{R5: cross-language refinement}

Shared fixture names are not a refinement proof.  A credible correspondence
among Lean, Haskell, Rust, and JSON requires:

\begin{enumerate}
  \item versioned external syntax;
  \item a decoder relation from syntax to semantic objects;
  \item explicit error cases for malformed data;
  \item agreement on composition order and equality;
  \item separation of semantic values from artifact identifiers;
  \item executable or proved correspondence claims.
\end{enumerate}

The Haskell model can serve as an executable oracle and the Rust code as the
production kernel, but neither role transfers Lean theorems automatically.

\subsection{R6: selected query rewrites}

Only after a query language and denotation are fixed should the project prove
rewrites.  A modest first target is reassociation of pure, total path
navigation over finite instances.  Filter fusion, projection pushdown, join
reassociation, aggregation, and SQL lowering require explicit choices for
nulls, errors, multiplicity, order, volatility, and backend capabilities.

Backend differential tests should remain separate from semantic proofs.
Passing them is execution evidence; it is not a theorem about every backend
version.

\section{Falsification and adversarial checks}
\label{sec:falsification}

A formalization paper should say what would disprove its own claims.

\subsection{Source-level falsifiers}

The machine-checked coverage claim fails if:

\begin{itemize}
  \item any quoted source statement differs from the elaborated declaration;
  \item the recorded source hashes do not reproduce the build;
  \item any covered declaration reports an axiom dependency;
  \item a later source change is discussed using stale build evidence;
  \item a theorem name remains while its type is weakened.
\end{itemize}

The final item is why name-substring checks cannot be the semantic gate.

\subsection{Interpretive falsifiers}

The paper's interpretation fails if it:

\begin{itemize}
  \item calls \code{comp\_typed} a runtime decision procedure;
  \item treats \code{Equivalent} as a generated or decidable congruence;
  \item calls \code{ExtensionalEq} categorical equality without proving its
  relation and congruence laws;
  \item treats proof-carrying lawfulness as automatic mapping validation;
  \item infers instance, migration, query, backend, or distributed behavior
  from the F3 kernel;
  \item says that a Python token scan proves theorems;
  \item says that exact mathematics implies cross-language implementation
  equivalence.
\end{itemize}

\subsection{Counterexample-oriented extensions}

Later slices should make negative evidence first class.  An extrinsic path
validator needs malformed endpoint cases.  An instance validator needs
single-fault inputs with missing assignments or broken equations.  A query
rewrite needs finite countermodel search alongside proof attempts.  A
cross-language refinement needs fixtures that distinguish composition order
and semantic equality from artifact identity.

Formal proof is strongest when the modeled proposition is clear.  Persisted
counterexamples are strongest when the intended proposition was wrong or the
implementation violated it.  The research program needs both.

\section{Reproducibility}
\label{sec:reproducibility}

\subsection{Commands}

The formal build can be reproduced from the repository root:

\begin{lstlisting}[language=bash]
lake env lean --version
lake clean
lake build
python3 scripts/audit-lean.py lean
python3 -m unittest -v scripts.tests.test_audit_lean
PYTHONDONTWRITEBYTECODE=1 \
  python3 -m unittest discover \
  -s scripts/tests -p 'test_*.py' -v
\end{lstlisting}

For isolation, copy \code{lean-toolchain}, \code{lakefile.lean},
\code{lake-manifest.json}, the \code{lean/} directory, and the audit files to a
new directory before running the first five commands.  The manuscript build is
separate and described in the accompanying \code{reproducibility.md}.

\subsection{Expected outcomes}

\begin{itemize}
  \item Lean reports version 4.32.1.
  \item \code{lake build} completes seven jobs.
  \item Nine lines say that the named declarations do not depend on axioms.
  \item The Lean source audit reports coverage for
  \code{PATH-02 PATH-03 PATH-04 MAP-03 MAP-04 MAP-05}.
  \item Three audit-specific tests pass.
  \item Nineteen total Python utility tests pass.
\end{itemize}

Only the first five bullets concern the formal slice directly.  Of the 19
Python tests, 16 test other fixture and paper-verification utilities.

\subsection{Source digests}

\begin{longtable}{L{0.31\textwidth}L{0.60\textwidth}}
\caption{Audited source digests.}\label{tab:hashes}\\
\toprule
Artifact & SHA-256 \\
\midrule
\endfirsthead
\toprule
Artifact & SHA-256 \\
\midrule
\endhead
\code{lean-toolchain} &
{\ttfamily\seqsplit{8e3538e0ab5f81a3ee04927d8838c8c674e0e112838b4b3ce87ec218143276af}} \\
\code{lakefile.lean} &
{\ttfamily\seqsplit{a1b6c42f458b66e446afba585cf8fcde183760945fe5092e8cb58ec96397a92b}} \\
\code{lake-manifest.json} &
{\ttfamily\seqsplit{971337b5c015b73116da2cabcdc2b5356196d94066cb66417d62b9dc98aec523}} \\
\code{lean/CatDB.lean} &
{\ttfamily\seqsplit{c809cc62214d231ccccf8ed40e3afc9e4959f6bdf9de2e0c17af56a2240ee417}} \\
\code{lean/CatDB/Path.lean} &
{\ttfamily\seqsplit{9d6ee7ac1f6ad531dbe012834c2ff2a42f5cd59dfac9f6f875444578934f0a14}} \\
\code{lean/CatDB/Schema.lean} &
{\ttfamily\seqsplit{20334a5e31668f056c3335e2cd8868cf965b172040e1f8ef21619de33bf04439}} \\
\code{lean/CatDB/Mapping.lean} &
{\ttfamily\seqsplit{1b5de49323febb5448567bfb271ff86c98af6e90710658e19a35ea6308b15054}} \\
\path{lean/CatDB/Coverage.lean} &
{\ttfamily\seqsplit{cecc2b89c5a7531c5cefbd946be3e630308f7edaadbde33d3a8c3f92d61ce773}} \\
\code{lean/COVERAGE.md} &
{\ttfamily\seqsplit{35dd37698a6820cd166fa324edf70d3c682f9bc1d08e746317a6b1b26177f412}} \\
\code{scripts/audit-lean.py} &
{\ttfamily\seqsplit{dd682cafaf4fcafed967acc6a14e0fea0cdc2aaf8540358e86d8a8ff440890f7}} \\
\path{scripts/tests/test_audit_lean.py} &
{\ttfamily\seqsplit{85d37aa83ae2a4ab25d880c43f33b16cc95a43685ba163dcdf0cfd526e56183f}} \\
\bottomrule
\end{longtable}

\subsection{Reproducibility status}

The fresh reproduction was performed on
\code{arm64-apple-darwin24.6.0}.  No external Lean packages are listed in the
manifest.  Reproduction on another supported platform should compare
declaration types and axiom output, not binary build artifacts.

This manuscript itself remains unreviewed.  Successful LaTeX compilation does
not satisfy the program's peer-review gate and must not be treated as
acceptance.

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

\subsection{A small theorem boundary}

The accepted slice is intentionally small.  It checks the algebra of a
list-like indexed path syntax and the closure properties of proof-carrying
mappings.  That is useful infrastructure, but it is not yet the part of a
database system that handles data.

\subsection{Intrinsic versus extrinsic correctness}

Intrinsic typing excludes malformed paths after they have entered the model.
Production software still receives untrusted external syntax.  The missing
refinement layer must show that a decoder either produces an intrinsically
well-typed value with the intended meaning or returns a precise error.

An intrinsic model can simplify later proofs.  It cannot replace boundary
validation.

\subsection{Equality design}

The supplied \code{Equivalent} relation avoids premature commitment, but it
moves a hard problem into an assumption.  The program must decide whether
future mapping artifacts carry proofs, use a decidable equational fragment, or
defer obligations for human review.  Different schema classes may need
different answers.

\subsection{Extensional equality}

\code{ExtensionalEq} is adequate for the three current MAP-05 statements, but
it is not yet a finished quotient or setoid interface.  Its interaction with
proof fields, serialization identity, stable schema versions, and provenance
is open.

\subsection{No performance claim}

The Lean package contains no benchmark.  Proof checking time for this tiny
kernel says nothing about schema-compilation latency, query-planning overhead,
or physical execution.  The claim that a categorical layer can remain outside
the hot path is a systems hypothesis for other papers.

\subsection{No cross-language theorem}

Rust and Haskell components in the broader program may implement similarly
named operations.  The present paper has not proved that their definitions
match Lean.  Cross-checking shared fixtures can find disagreements, but only a
stated refinement relation can say what agreement means.

\subsection{Open questions}

\begin{enumerate}
  \item What finite presentation and congruence representation gives useful
  executable equality while preserving a clear completeness boundary?
  \item Should lawful production mappings carry proof objects, validation
  certificates, or unresolved obligations?
  \item What is the right extensional equality for mappings once version and
  provenance fields exist?
  \item Can a finite-instance model support a simple, machine-checked
  \(\Delta\) implementation that remains aligned with Rust and Haskell?
  \item Which query rewrites have enough semantic value to justify Lean
  mechanization before a full relational semantics exists?
  \item How should proof coverage be versioned when the executable schema
  profile changes?
\end{enumerate}

\section{Discussion}
\label{sec:discussion}

The main lesson is not that six invariants are difficult theorems.  Most are
elementary.  The lesson is that mechanization forces a program to choose what
its words mean.

``Typed path'' can mean an external list that a validator checks, or an
intrinsic value whose endpoints occur in its type.  The current Lean slice
chooses the latter.  ``Schema presentation'' can mean a finite graph and
equations, their generated category, or a graph equipped with a supplied
equivalence relation.  The current slice chooses the third.  ``Lawful
mapping'' can mean a record that passed an algorithm, or a mapping paired with
a preservation proof.  The current slice chooses proof-carrying lawfulness.

These choices are legitimate as long as their translation to the runtime is
not assumed.  The next research risk is not a failed induction proof.  It is a
semantic gap between intrinsic Lean objects and versioned production
artifacts.  That gap should be addressed with explicit decoding and refinement
relations, not with stronger prose.

The result also clarifies the role of category theory in \CatDB{}.  Identity,
composition, and preservation give a coherent algebra for schema mappings.
They do not remove physical data movement, decide every mapping, or solve
distributed consistency.  Their value is compositional structure.  Formal
verification can protect that structure once the modeled boundary reaches the
operations that matter.

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

The first \CatDB{} Lean slice establishes a precise, reproducible base.  Typed
paths carry endpoints in their types.  Empty paths are identities and
composition is associative.  Raw mappings extend from generators to paths.
Lawful mappings carry equation-preservation evidence.  Identity and composite
mappings are lawful, and their unit and associativity propositions hold under
the library's extensional equality.

That is the complete positive result.  The isolated Lean 4.32.1 build reports
no axiom dependencies for the nine covered declarations.  The source audit and
its tests pass.  The theorem types, assumptions, commands, and hashes are
recorded so that the claim can be checked again.

The larger \CatDB{} thesis remains ahead.  Finite schemas, attributes,
instances, migration, query semantics, backend refinement, provenance, and
distributed behavior are not verified here.  The next milestone should be a
finite-instance model and pullback migration, preceded by a stronger equality
and coverage boundary.  Until those artifacts exist, the honest conclusion is
not that \CatDB{} is verified.  It is that a small semantic kernel has become
exact enough to verify, criticize, and extend.

\appendix

\section{Complete coverage inventory}
\label{app:coverage}

\begin{longtable}{L{0.12\textwidth}L{0.27\textwidth}L{0.25\textwidth}L{0.255\textwidth}}
\caption{Exact program coverage.}\label{tab:complete-coverage}\\
\toprule
ID & Declarations & Assumptions & Exact boundary \\
\midrule
\endfirsthead
\toprule
ID & Declarations & Assumptions & Exact boundary \\
\midrule
\endhead
\code{PATH-02} &
\code{Path.id\_comp}, \code{Path.comp\_id} &
Arbitrary typed graph and a well-formed indexed path. &
Left and right identity of the empty path. \\
\code{PATH-03} &
\code{Path.comp\_typed} and the type of \code{Path.comp} &
Inputs share the same middle object in their indices. &
An \(A\to C\) result exists and equals composition; no external alignment
decision. \\
\code{PATH-04} &
\code{Path.comp\_assoc} &
Three endpoint-aligned indexed paths in an arbitrary graph. &
Syntactic composition is associative. \\
\code{MAP-03} &
\code{LawfulMapping.id} &
The schema supplies a path equivalence with the stated laws. &
Identity raw mapping preserves that relation. \\
\code{MAP-04} &
\code{LawfulMapping.comp} &
Both mappings carry preservation witnesses. &
The proof-carrying composite preserves the relation. \\
\code{MAP-05} &
{\ttfamily\seqsplit{LawfulMapping.comp\_id\_ext}},
{\ttfamily\seqsplit{LawfulMapping.id\_comp\_ext}},
{\ttfamily\seqsplit{LawfulMapping.comp\_assoc\_ext}} &
The exact object-action equality plus heterogeneous equality of generator
images. &
Two units and associativity under \code{ExtensionalEq}; no serialized IDs. \\
\bottomrule
\end{longtable}

\section{Coverage source}
\label{app:coverage-source}

The full coverage module is:

\begin{lstlisting}[language=Lean]
import CatDB.Mapping

#print axioms CatDB.Path.id_comp
#print axioms CatDB.Path.comp_id
#print axioms CatDB.Path.comp_typed
#print axioms CatDB.Path.comp_assoc
#print axioms CatDB.LawfulMapping.id
#print axioms CatDB.LawfulMapping.comp
#print axioms CatDB.LawfulMapping.comp_id_ext
#print axioms CatDB.LawfulMapping.id_comp_ext
#print axioms CatDB.LawfulMapping.comp_assoc_ext
\end{lstlisting}

The inventory includes the identity and composition constructors because they
contain proof fields and are part of the machine-checked mapping coverage.

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

\begin{longtable}{L{0.31\textwidth}L{0.18\textwidth}L{0.41\textwidth}}
\caption{Claim ledger.}\label{tab:claims}\\
\toprule
Claim & Label & Evidence and qualification \\
\midrule
\endfirsthead
\toprule
Claim & Label & Evidence and qualification \\
\midrule
\endhead
Endpoint-indexed paths compose at a shared middle object. &
\machinechecked &
Type of \code{Path.comp}; says nothing about JSON identifiers. \\
Empty paths are two-sided identities. &
\machinechecked &
\code{id\_comp}, \code{comp\_id}; arbitrary graph. \\
Path composition is associative. &
\machinechecked &
\code{comp\_assoc}; syntactic paths only. \\
The PATH-03 theorem is nontrivial typing-soundness. &
\notclaimed &
Its witness proof is immediate; the dependent function type is substantive. \\
Identity mappings preserve the supplied equivalence. &
\machinechecked &
\code{LawfulMapping.id}; the relation and laws are structure fields. \\
Lawful mappings are closed under composition. &
\machinechecked &
\code{LawfulMapping.comp}; both inputs already carry proofs. \\
Mapping units and associativity hold under the exact extensional relation. &
\machinechecked &
Three MAP-05 theorems; no artifact fields. \\
\code{ExtensionalEq} is a proved composition congruence and equivalence
relation. &
\notclaimed &
Those theorems are absent. \\
The nine covered declarations are axiom-free in the audited build. &
\machinechecked &
Transitive \code{\#print axioms} reports at recorded hashes and toolchain. \\
The source audit proves theorem semantics. &
\notclaimed &
It is lexical hygiene and name coverage only. \\
Finite database instances are verified. &
\notclaimed &
No instance declaration exists. \\
Pullback migration is verified. &
\openclaim &
F4 roadmap target only. \\
Lean, Haskell, and Rust have equivalent semantics. &
\openclaim &
No refinement proof exists. \\
The database runtime is verified. &
\notclaimed &
Runtime behavior is outside the formal model. \\
\bottomrule
\end{longtable}

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

Before this manuscript can advance from unreviewed status, reviewers should
answer the following.

\subsection{Formal methods review}

\begin{enumerate}
  \item Do all quoted Lean declaration types match the source?
  \item Is every \machinechecked{} statement limited to a checked declaration?
  \item Is PATH-03 characterized without inflating its proof content?
  \item Is \code{Equivalent} described as a supplied relation with laws?
  \item Is \code{ExtensionalEq} described without assuming missing structure?
  \item Is the axiom inventory interpreted according to Lean's documentation?
\end{enumerate}

\subsection{Category-theory review}

\begin{enumerate}
  \item Does the paper avoid claiming construction of a quotient category?
  \item Are identity, associativity, functor-like mapping, and preservation
  placed correctly relative to prior literature?
  \item Does the paper distinguish a practical schema presentation from an
  arbitrary graph with a supplied equivalence?
\end{enumerate}

\subsection{Database-systems review}

\begin{enumerate}
  \item Are external validation and intrinsic typing kept separate?
  \item Are instances, migration, queries, and physical execution excluded?
  \item Does the discussion avoid transferring formal laws to SQL,
  transactions, or distribution?
  \item Is the proposed refinement roadmap testable?
\end{enumerate}

\subsection{Reproducibility review}

\begin{enumerate}
  \item Do the source hashes match?
  \item Does the isolated build use Lean 4.32.1 and complete seven jobs?
  \item Are nine empty axiom inventories printed?
  \item Do the three audit-specific tests and the 19-test suite pass?
  \item Does the manuscript compile without errors or material overfull boxes?
  \item Has every PDF page been visually inspected?
\end{enumerate}

\bibliographystyle{plain}
\bibliography{references}

\end{document}
