# Reproducibility: Paper 17

## Status

Paper status: **internally accepted**.

Lean Slice 3 status: **internally accepted** in
`coordination/releases/slice-3.md`.

The accepted code slice does not make this manuscript accepted. No
repository-level paper PDF, cover image, or review verdict is produced by this
work package.

## Audited formal source

The paper is tied to these SHA-256 values:

```text
8e3538e0ab5f81a3ee04927d8838c8c674e0e112838b4b3ce87ec218143276af  lean-toolchain
a1b6c42f458b66e446afba585cf8fcde183760945fe5092e8cb58ec96397a92b  lakefile.lean
971337b5c015b73116da2cabcdc2b5356196d94066cb66417d62b9dc98aec523  lake-manifest.json
c809cc62214d231ccccf8ed40e3afc9e4959f6bdf9de2e0c17af56a2240ee417  lean/CatDB.lean
9d6ee7ac1f6ad531dbe012834c2ff2a42f5cd59dfac9f6f875444578934f0a14  lean/CatDB/Path.lean
20334a5e31668f056c3335e2cd8868cf965b172040e1f8ef21619de33bf04439  lean/CatDB/Schema.lean
1b5de49323febb5448567bfb271ff86c98af6e90710658e19a35ea6308b15054  lean/CatDB/Mapping.lean
cecc2b89c5a7531c5cefbd946be3e630308f7edaadbde33d3a8c3f92d61ce773  lean/CatDB/Coverage.lean
35dd37698a6820cd166fa324edf70d3c682f9bc1d08e746317a6b1b26177f412  lean/COVERAGE.md
dd682cafaf4fcafed967acc6a14e0fea0cdc2aaf8540358e86d8a8ff440890f7  scripts/audit-lean.py
85d37aa83ae2a4ab25d880c43f33b16cc95a43685ba163dcdf0cfd526e56183f  scripts/tests/test_audit_lean.py
```

Refresh every digest and the paper's evidence tables if any source changes.

## Isolated Lean build

Create a fresh temporary directory:

```bash
paper17_lean_dir="$(mktemp -d /tmp/catdb-lean-paper17.XXXXXX)"
mkdir -p "$paper17_lean_dir/lean" "$paper17_lean_dir/scripts/tests"
cp lean-toolchain lakefile.lean lake-manifest.json "$paper17_lean_dir/"
cp -R lean/. "$paper17_lean_dir/lean/"
cp scripts/audit-lean.py "$paper17_lean_dir/scripts/"
cp scripts/tests/test_audit_lean.py "$paper17_lean_dir/scripts/tests/"
```

Run:

```bash
cd "$paper17_lean_dir"
lake env lean --version
lake clean
lake build
python3 -m unittest -v scripts.tests.test_audit_lean
python3 scripts/audit-lean.py lean
```

Expected Lean version:

```text
Lean (version 4.32.1, arm64-apple-darwin24.6.0,
commit f054605aea4b840552cca2e725580bffd1e1b704, Release)
```

The platform portion may differ on another supported host. The semantic
acceptance criteria are the toolchain version, successful build, declaration
types, and axiom inventory.

Expected build summary:

```text
Build completed successfully (7 jobs).
```

Expected axiom inventory:

```text
'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
```

Expected audit result:

```text
PASS Lean F3 source audit
coverage: PATH-02 PATH-03 PATH-04 MAP-03 MAP-04 MAP-05
```

Expected audit-test result: 3 tests, all passing.

## Full Python utility suite

From the repository root:

```bash
PYTHONDONTWRITEBYTECODE=1 \
  python3 -m unittest discover -s scripts/tests -p 'test_*.py' -v
```

Expected result: 19 tests pass.

Only three tests directly exercise `audit-lean.py`. The remaining tests cover
fixture gates and manuscript verification utilities.

## Trust and interpretation

The reproducible statement is:

> Lean 4.32.1 accepts the named declarations at the recorded source hashes and
> reports no transitive axiom dependencies for the nine declarations listed in
> `CatDB.Coverage`.

It does not establish:

- correctness of the entire Lean implementation;
- correspondence between the paper and source without source review;
- correspondence between Lean and Rust, Haskell, or JSON;
- finite instances, migrations, queries, backends, or distributed behavior.

The Python source audit is secondary hygiene. It is not a parser or a
theorem-statement verifier.

## Isolated manuscript build

The manuscript depends only on `paper.tex` and `references.bib`. Build it
outside the repository:

```bash
paper17_tex_dir="$(mktemp -d /tmp/catdb-paper17-tex.XXXXXX)"
cp papers/17-lean-formalization/paper.tex "$paper17_tex_dir/"
cp papers/17-lean-formalization/references.bib "$paper17_tex_dir/"
cd "$paper17_tex_dir"
pdflatex -interaction=nonstopmode -halt-on-error paper.tex
bibtex paper
pdflatex -interaction=nonstopmode -halt-on-error paper.tex
pdflatex -interaction=nonstopmode -halt-on-error paper.tex
pdfinfo paper.pdf
```

Do not copy the PDF back into the repository until the paper's required review
gate has been satisfied.

## Independent author verification

The formal source was copied to
`/var/folders/6z/np99jwkj4ys5z6l5y0xpwdx80000gn/T/catdb-p17-lean.LZI3ff1xjA`.
A clean Lean 4.32.1 build completed all seven jobs. The nine covered
declarations reported no axiom dependencies, all three audit-specific tests
passed, the source audit reported the six required coverage IDs, and the
remaining sixteen fixture/paper-verifier utility tests passed. The combined
19-test log has SHA-256
`3de43004814c5d7f0ca0810f46796cd96eecf5ddf09af5efa6dafad79a37227a`;
the Lean build/audit log has SHA-256
`4ac5b3ee59803848d73bc58575dfbc4ddeff27bac2d23e7ada352e3af773d265`.

The exact manuscript source was independently built in
`/var/folders/6z/np99jwkj4ys5z6l5y0xpwdx80000gn/T/catdb-p17-root.AdvtWR4qGh`.
`texcount` reports 5,754 words. The PDF is 30 US-letter pages, PDF 1.7,
and 329,878 bytes. The log contains zero errors, undefined citations,
undefined references, or overfull boxes and five cosmetic underfull-box
warnings. All 30 pages were rendered at 95 DPI to
`/var/folders/6z/np99jwkj4ys5z6l5y0xpwdx80000gn/T/catdb-p17-visual.47ketpo4RB`;
the contact sheet was inspected for clipping, overlap, code-listing overflow,
hash wrapping, equation defects, and unreadable tables.

| Build artifact | SHA-256 |
|---|---|
| `paper.pdf` | `42dfd0960e6f16f147e7c5fb1413a80ba198b1d4376d84f71f9e3295bed60e7b` |
| `paper.log` | `875dee3deaff3a3e73a72d81b28e0eebd86ec70c1ab0f0807611715aba0471d9` |
| `paper.bbl` | `781d566af9b58f5a0ad7a7a3c00be1e69d3770b3f7862f86321156f4af6e63a1` |
| `paper.blg` | `34272912ba175236183a8f24d34457ae0178fca673f4b48eb9e75e676da5ec28` |

The TeX-plus-BibTeX source digest is
`11ebf8979bcfb348d7675c3ce6d19dc132f12ab561ad2fc3c1a2d97a419568c8`.
All sixteen bibliography keys are cited and represented in both paper-local
bibliographic ledgers.

| Peer artifact | SHA-256 |
|---|---|
| `disputed-claim-ledger.md` | `b618b512dfe0c4fdce7ffa8d8713dd152c00a88aa455d973f3ec0d3ed743d221` |
| `humanizer-scope.md` | `f9e4a62ccdd15c930f941f22a4a9f4b7ec59ae351b984411f2c1e58026cc72d0` |
| `novelty-ledger.md` | `209c52b78dffb8a254df8ae3ca174205ea699dfb5fe86595327622d2308ade61` |
| `paper.tex` | `5f7f5684fc153bda6b8a7d876a9552341fca86516f03fe2c68566759032a122c` |
| `primary-source-bibliography.md` | `60a6f670a409c2b7b7bb2f81863798d76ead90901be69746e08986d8de6ca45d` |
| `references.bib` | `69967ddf6422be6c41c17972bf795ef229a5d31c84679fbeac2db037defd6bea` |
| `related-work-ledger.md` | `621f976fc91959f6633e188f8d2e5503f42df414ccd60a72d1647f95c132d56f` |
| `review-contract.md` | `c82432a6c713492e54fd0f0c6ee64bedcf5750f3b0cc0684a08d53107905e7f7` |

This record cannot contain its own stable digest; the final acceptance commit
binds its release state.

## Terminal acceptance artifacts

AGY round 1 reviewed source digest
`11ebf8979bcfb348d7675c3ce6d19dc132f12ab561ad2fc3c1a2d97a419568c8`
and ended in `VERDICT: ACCEPT`; the canonical review is byte-identical to
round 1.

| Artifact | SHA-256 |
|---|---|
| repository `paper.pdf` | `42dfd0960e6f16f147e7c5fb1413a80ba198b1d4376d84f71f9e3295bed60e7b` |
| repository `paper.log` | `875dee3deaff3a3e73a72d81b28e0eebd86ec70c1ab0f0807611715aba0471d9` |
| 300-DPI `cover.png` | `0d0eadae4f99098c2df32f00b44166c5135ad3ae6d0046c0aa934c87520b42d6` |
| canonical AGY review | `76e952c650cf17c4a9433888fa789fe91cf689efa07847de33e3646838644615` |

## Manuscript verification

Check the build log:

```bash
rg -n \
  'LaTeX Error|Undefined control sequence|Citation.*undefined|Reference.*undefined|Overfull \\\\hbox' \
  paper.log
```

Every page must be rasterized and visually inspected:

```bash
mkdir pages
pdftoppm -png -r 120 paper.pdf pages/page
```

The inspection should check:

- first-page sidebar and metadata;
- title and abstract wrapping;
- tables and code listings;
- hyperlinks and bibliography;
- no clipped hashes or long identifiers;
- no overlapping equations, text, or page furniture;
- no blank or truncated final pages.

## Falsifiers

Stop and refresh the paper if:

- a formal source digest differs;
- Lean does not report the pinned version;
- the build fails or reports an axiom dependency;
- a quoted theorem type differs from the source;
- the source audit or any audit-specific unit test fails;
- the manuscript has unresolved citations or material overfull boxes;
- visual inspection finds overlap, clipping, or unreadable text.