Paper IV — verification closeout v1.1.0
19 October 2026 (UTC) · Operation Komorebi · Komorebi P.
Result
The existing 68-result reviewed formal core passed a fresh pinned-source replay, exact target-kind resolution, a transitive namespace axiom audit and real compiler controls. All 119 mathematical Lean sources are unchanged. This is a verification closeout, not a new or strengthened mathematical theorem.
Start with readers/Paper_IV_Verification_Closeout_v1.1.0.pdf or REPORT.md.
verification/CLOSEOUT_REPORT.json contains the structured summary.
Contents
readers/: the latest recovered 77-page monograph, 28-page visual guide, 140-page Lean guide, and new five-page verification report.formalization/lean/: the complete active formal source, exact dependency pins, and the corrected warning policy. No external runtime or dependency cache.publication_baseline/: the intact recovered 836-file publication/source tree. Its old reports and stale font-bearing manifest remain historical evidence.verification/: source preservation, current compiler logs and objects, axiom reports, compiler controls, finite computations, test suites and failed attempts.scripts/: portable verification, replay, reporting and test programs.PROGRESS_LEDGER.md,PROGRESS_LEDGER.json,CONTINUE_HERE.md: versioned status and the next restart point.
Reproduce the checks
Use Python 3.11 or newer on Linux/WSL. Commands write new evidence outside the frozen package. They do not install software, fetch dependencies, or edit the accepted mathematical sources.
python3 -B scripts/verify_release.py
python3 -B scripts/run_checks.py --mode records --work /tmp/paper-iv-records
python3 -B scripts/run_checks.py --mode finite --work /tmp/paper-iv-finite
bash Run-Replay.sh /path/to/Komorebi_Portable_Lean_4.34.0-rc2 /tmp/paper-iv-full
Every output directory must be new. Full mode requires the matching external
Lean runtime and all cached packages specified in formalization/lean/lake-manifest.json.
Finite mode additionally requires the Python packages recorded in the finite receipt.
The report builder uses ReportLab. Native Windows execution was not tested.
verify_release.py checks stored evidence and hashes; it is not a new compiler
run. Full mode performs fresh source compilation, kind and axiom checks, and
compiler controls. Its 300-second per-command timeout and one-worker configuration
retain the accepted production settings.
Reader versions and exact scope
The older monograph and Lean reader correctly describe their own earlier edition and its historical formal evidence. The new closeout report is the authority for this execution. The October 16 standalone visual PDF is preserved, including its branch-sensitive correction. The exact updated editable source for that standalone PDF was not recovered; the October 8 editable baseline and a three-page PDF text difference record are included. No byte-identical regeneration of that later PDF is claimed.
The reviewed 68-result contract, hypotheses, branch choices and explicit research boundaries are unchanged. Imported standard fact 11.1 is outside that count. No new independent semantic reproof of all 68 statements, cold Mathlib build, independent proof kernel, external referee review, or licence decision is claimed.
The separate Paper_IV_Delivery_Verification_v1.1.0.json records the final ZIP
hash, fresh extraction and post-extraction tests. It is external to the archive
to avoid circular self-hashing.