# Paper 17 related-work ledger

Status: paper-local author ledger; not peer review

Date: 23 July 2026

## Lean and proof engineering

| Sources | Established result used | CatDB boundary |
|---|---|---|
| `demoura2015lean`, `demoura2021lean4` | Lean's elaboration, dependent type theory, kernel checking, and metaprogrammable implementation model. | These sources explain the proof environment; they do not validate CatDB declarations. |
| `leanReferenceInductive`, `avigadTheoremProvingLean4` | Indexed inductive families can encode endpoints in types. | CatDB's `Path` encoding is project-specific, not a new dependent-type technique. |
| `leanReferenceAxioms` | `#print axioms` reports transitive axiom dependencies for a declaration. | An empty report is relative to the exact source and trusted Lean toolchain; it is not a whole-system correctness theorem. |
| `leanReferenceLake` | Lake supplies the pinned Lean build workflow. | A reproducible build does not prove correspondence to Rust, Haskell, JSON, or prose. |
| `mathlib2020`, `mathlibCategoryBasic` | Mathlib provides mature category-theory infrastructure and a `Category` interface. | The current CatDB Lean package deliberately has no mathlib dependency and does not instantiate `Category`. |

## Category theory and categorical databases

| Sources | Established result used | CatDB boundary |
|---|---|---|
| `maclane1998categories`, `leinster2014basic` | Categories satisfy identity and associativity laws; free categories arise from paths on graphs. | Paper 17 claims no new category-theory theorem. |
| `spivak2012functorial`, `spivakWisnesky2015relational` | Schemas, instances, and functorial data migration have established categorical formulations. | The current Lean slice stops before instances and does not define Delta, Sigma, or Pi. |
| `schultz2017algebraic`, `brown2019categorical` | Algebraic databases and categorical data integration extend beyond bare graphs. | Attributes, value domains, equations as finite presentations, and integration execution are absent from the checked kernel. |

## Mechanized query reasoning

| Sources | Established result used | CatDB boundary |
|---|---|---|
| `chu2017cosette`, `chu2017hottsql` | Mechanized reasoning can prove bounded SQL rewrite equivalences under explicit semantics. | Paper 17 contains no query language, bag semantics, SQL denotation, optimizer, or rewrite theorem. |

## Disposition

The paper's positive delta is an audited, source-faithful Lean representation
of six CatDB invariant IDs plus reproducible axiom/build evidence. The
mathematics, dependent-type techniques, categorical database foundations, and
mechanized-query precedents are prior art.