# Fresh verification report

The complete fresh verification **passed**. The direct source build, official fresh kernel replay, raw declaration inspection, and final identity checks all completed successfully. Final identity check: 2026-09-13T17:16:21.213916+00:00.

| Stage | Verified scope | Actual duration |
| --- | --- | ---: |
| Native Lean source build | 3,399 modules: 222 project, 2,920 Mathlib, 257 other dependencies | 13,182.94 s (219.72 min) |
| Official `leanchecker --fresh --verbose PL1FreshAudit` | Newly rebuilt imported closure; native exit 0 | 1,063.60 s (17.73 min) |
| Raw environment inspection | All 222 project modules, four exact scalar A/B types, 157 claim records (155 distinct), 5,683 eligible project declarations | 391.98 s (6.53 min) |
| Fresh ProofWidgets assets | 22 bundles; 19 checked JavaScript inclusions; both native exits 0 | Install 48.64 s (0.81 min); build 103.08 s (1.72 min) |

The source build used a new, initially empty output directory and reused no compiled project or non-toolchain dependency artifacts. All 10,259 immutable copied files, their originals, all generated Lean artifacts, embedded widget assets, and actual replay inputs were hash-verified. Four identity checkpoints cover build completion, immediately before replay, after replay, and after inspection. Sources and inputs remained unchanged. Isolated root: `{WORKSPACE_ROOT}/tmp/pl1_fresh_20260913T121046Z`.

The retained toolchain is Lean 4.34.0-rc2, including its compiler, bundled libraries, runtime and official checker. The replay inventory contains 3,400 fresh modules including the audit root and 1,552 retained toolchain modules. This was a **direct native Lean build**, not a full Lake build; optional Mathlib style linters and Lake cache hooks were not run. The compiler was not bootstrapped, and the checker uses Lean's own kernel rather than an independent implementation.

The official checker excludes unsafe and partial declarations. The imported inventory records 435,310 eligible declarations and 3,608 excluded declarations; these are inventory counts, not an independently emitted replay counter. All 18 project exclusions were verified as matching compiler recursion companions. Raw traversal of types and stored bodies found **no unsafe, partial, missing, or nonstandard-axiom dependency** in any requested claim or eligible project declaration. The only permitted reachable axioms were `propext`, `Classical.choice`, and `Quot.sound`; there were no project-origin axiom declarations. This traversal did not use exported axiom caches.

The four checked scalar theorem types match the reviewed real and complex A/B statement constants exactly, with no additional premises. The stored types and bodies of 23 reviewed definitions were recorded. This validates the frozen formal statements and their proof dependencies; it does not certify that every manuscript result has been formalized.

Earlier evidence and failures remain preserved. The source build records 0 unsuccessful module attempts across 2 sessions, plus 1 separately recorded coordinator interruptions. After 2,955 successful modules, Windows denied replacement of the coordinator's JSON status file (WinError 5). There were 0 native module failures at that stop. Recovery changed only the status writer, adding a 15-second bounded retry for Windows errors 5, 32 and 33. The pinned compiler, options, sources and proofs were unchanged. The actual resumed session used the recorded new runner and started from 2,955 verified completions. 2 completed but unrecorded module outputs were archived and those modules were compiled again; they were not promoted silently. [Preserved interruption and recovery evidence](<{WORKSPACE_ROOT}/output/pl1_updated_lean_2026-09-12/verification/Fresh-20260913T121046Z/source-build-recovery-1/recovery-summary.json>).

The widget report discloses the initially copied Git-tracked generated files, their removal before use, the Windows npm launcher failure, and the corrected evidence-only hash comparison. No failure was converted into a successful native exit, and the original project was preserved.

Evidence: [full source build](<{WORKSPACE_ROOT}/output/pl1_updated_lean_2026-09-12/verification/Fresh-20260913T121046Z/source-build-status.json>), [official replay](<{WORKSPACE_ROOT}/output/pl1_updated_lean_2026-09-12/verification/Fresh-20260913T121046Z/kernel-replay-1/status.json>), [raw inspection](<{WORKSPACE_ROOT}/output/pl1_updated_lean_2026-09-12/verification/Fresh-20260913T121046Z/inspection/status.json>), [final identity checkpoint](<{WORKSPACE_ROOT}/output/pl1_updated_lean_2026-09-12/verification/Fresh-20260913T121046Z/final-checks-1/after-inspection.json>), [widget provenance and logs](<{WORKSPACE_ROOT}/output/pl1_updated_lean_2026-09-12/verification/Fresh-20260913T121046Z/widget-build/README.md>), [machine-readable summary](<{WORKSPACE_ROOT}/output/pl1_updated_lean_2026-09-12/verification/Fresh-20260913T121046Z/fresh-verification-summary.json>). The summary records exact commands, native exits, durations, source/artifact manifest references, final input hashes, and retained trust boundaries.