# Privacy-prepared PL1 verification evidence

This archive is a separately prepared publication copy of completed local verification evidence. The verified original project was not changed. It is not a new verification run.

- These are privacy-prepared publication copies, not the byte-identical original verification evidence. Original and copy SHA256 values are recorded separately.
- Only private machine path prefixes are replaced; JSON whitespace is compacted. Existing hashes inside copied evidence still identify ORIGINAL files, not these transformed copies.
- The report and complete summary retain their original values and links apart from prefix replacement; local path links are provenance references, not functioning website URLs.
- The raw inspection log is complete in gzip form and expands to about 194 MB; the quick extract is explicitly selective.
- The bundle is supporting evidence, not a standalone rebuild kit: source/dependency trees, compiled artifacts, giant coordinator/checkpoint maps and all per-module logs are omitted. Their hashes and references remain in the complete summary.
- The retained trust boundary includes Lean 4.34.0-rc2, its compiler/kernel, bundled libraries, runtime and OS. No independent kernel implementation or compiler bootstrap is claimed.
- The direct native source build is not a full Lake build; optional style linters and Lake cache hooks were not run.
- The official checker excludes unsafe and partial declarations. Counts are inventory measurements, not a separately emitted checker replay count. Raw reachability covers all eligible project declarations.
- There are 15 imported axiom declarations, but no project-origin axioms and only the three permitted axioms are reachable from checked project roots.
- This validates the frozen formal A/B statements and their dependencies; it does not claim every manuscript result is formalized.
- Historical Statements.lean comments describing planned proofs are preserved; actual completed endpoint declarations are in MainTheoremA.lean and MainTheoremB.lean.
- No Lean build, replay, or audit was rerun to prepare this bundle; only packaging, source identity and redaction checks were performed.

Path tokens: `{WORKSPACE_ROOT}` replaces the private workspace prefix; `{USER_HOME}` replaces any remaining private user-home prefix. Subpaths, counts, dates, native exits, proof names and original evidence hash values are retained.

Start with `FRESH_VERIFICATION_REPORT.privacy-prepared.md`, `verification-facts.json`, and `inspection/QUICK_RECORD_EXTRACT.txt`. The complete summary is `fresh-verification-summary.privacy-prepared.json`. `MANIFEST.json` lists every other archive member and distinguishes original versus prepared hashes. It deliberately does not hash itself; the archive member hashes including the manifest and the ZIP hash are in the separately supplied preparation mapping.

Quick extract tags: ALL_CONSTANTS, EXACT_FINAL_TYPE, FRESH_INSPECT, IMPORT_COUNT, INSPECTION_SCOPE, PROJECT_CONSTANTS, PROJECT_MODULE_COVERAGE, PROJECT_RECURSION_COMPANION, RAW_AXIOM_ROOT_COVERAGE, RAW_IMPORTED_AXIOM, RAW_REACHABILITY. All other raw records, the complete definition bodies, generic types, inventories and whitespace remain in `inspection/stdout.privacy-prepared.txt.gz`.

The source build had zero native module failures and one status-writer interruption after 2,955 completions. The recorded resume rebuilt the two unrecorded outputs. Widget preparation also records its initial failed launcher attempt and successful corrected run.