# P1 reproducibility record

**Status:** provisional; this record does not establish implementation,
machine-check, or paper-acceptance claims  
**Research cut:** 2026-07-22  
**Working branch:** `catdb-paper-p1`

## Environment

- Host operating system: macOS on Apple Silicon.
- Shell: zsh.
- TeX: pdfTeX 3.141592653-2.6-1.40.29, TeX Live 2026.
- `latexmk`: 4.88.
- `biber`: 2.21.
- Rust compiler: `rustc 1.94.0 (4a4ef493e 2026-03-02)`.
- Cargo: `cargo 1.94.0 (85eff7c80 2026-01-15)`.
- GHC: 9.14.1.
- Cabal: 3.16.1.0.
- Lean toolchain: not pinned by the repository yet. The machine has Lean
  4.32.0 installed, but no Lean result may be reported before a
  repository-local toolchain file exists and `lake build` passes.
- Node.js: v24.14.0.
- pnpm: 11.16.0.
- AGY CLI: 1.1.5.
- Claude Code: 2.1.218.

## Source and evidence digests

Digests will be recorded for the manuscript acceptance candidate, bibliography,
shared fixture corpus, Rust workspace, Haskell package, Lean project, compiled
PDF, 300-DPI cover, and final AGY review. A missing or stale digest blocks
acceptance.

### Final P1 paper artifact record

The accepted paper source digest is
`ac7e68b4b6302440779a2aaf2e38f4a515bd13752f31a4f9e9666bb01e32d341`.
It is the digest computed by `scripts/verify-paper.py` over `paper.tex` and
`references.bib`.

| Artifact | SHA-256 |
|---|---|
| compiled 40-page `paper.pdf` | `a80fbae827f35e8dae4a7c78c87e5361646afc7a46202c8571f2ec09e515ee3a` |
| first-page 300-DPI `cover.png` | `cea52a91b82e53705bc4b9bbd0f844f780e9e724636fef2935b405ad2816f91a` |
| canonical AGY review | `8e1933abdefb17fd701f8b1e6814f9d99549800a25a19dacf653ea81ae25d1f7` |

The canonical review is byte-identical to round 3, names the exact source
digest, and ends in `VERDICT: ACCEPT`. The final verifier reports no undefined
reference, undefined citation, LaTeX error, or overfull box. Six non-gating
underfull boxes remain recorded in `paper.log`.

## Planned native commands

### Paper

```bash
latexmk -C paper.tex
latexmk -pdf -interaction=nonstopmode -halt-on-error paper.tex
pdfinfo paper.pdf
```

The build log must show no undefined references or citations. The PDF must
contain at least 20 pages and be newer than every LaTeX or bibliography input.

### Shared fixtures

```bash
python scripts/validate-fixtures.py \
  --schema fixtures/schema-v1.schema.json \
  --cases fixtures/cases
python scripts/audit-fixture-manifest.py fixtures/manifest-v1.json
```

### Rust

```bash
cargo fmt --all --check
cargo clippy --workspace --all-targets --all-features -- -D warnings
cargo test --workspace --all-features
cargo run -p catdb-cli -- fixtures verify fixtures/cases \
  --implementation rust --capability-set slice-1
```

### Haskell

```bash
cabal build all --ghc-options="-Wall -Werror"
cabal test all
```

### Cross-language comparison

```bash
cargo run -p catdb-cli -- fixtures compare fixtures/cases \
  --left rust --right haskell --capability-set slice-1
```

### Lean

```bash
lake build
python scripts/audit-lean-placeholders.py lean/CatDB
```

The Lean audit must reject `sorry`, `admit`, and undeclared axioms in the P1
coverage surface. The exact theorem-to-invariant table will be added after the
project exists.

## Evidence policy

- A successful LaTeX build establishes document reproducibility only.
- Rust and Haskell agreement establishes conformance for the admitted fixture
  corpus, not a general theorem.
- A Lean build establishes only the explicitly listed declarations under their
  exact assumptions.
- Paper acceptance requires a source digest matching the final AGY review.
- Any later source, fixture, code, or proof change reopens the acceptance
  candidate.