README.md
Paper IV: Cyclic Analytic Functions, Reciprocal Families, and Spectral Zero Data
README.md
1 # Paper IV — verification closeout v1.1.0
2
3 19 October 2026 (UTC) · Operation Komorebi · Komorebi P.
4
5 ## Result
6
7 The existing **68-result reviewed formal core** passed a fresh pinned-source replay,
8 exact target-kind resolution, a transitive namespace axiom audit and real compiler
9 controls. All 119 mathematical Lean sources are unchanged. This is a verification
10 closeout, not a new or strengthened mathematical theorem.
11
12 Start with `readers/Paper_IV_Verification_Closeout_v1.1.0.pdf` or `REPORT.md`.
13 `verification/CLOSEOUT_REPORT.json` contains the structured summary.
14
15 ## Contents
16
17 - `readers/`: the latest recovered 77-page monograph, 28-page visual guide,
18 140-page Lean guide, and new five-page verification report.
19 - `formalization/lean/`: the complete active formal source, exact dependency pins,
20 and the corrected warning policy. No external runtime or dependency cache.
21 - `publication_baseline/`: the intact recovered 836-file publication/source tree.
22 Its old reports and stale font-bearing manifest remain historical evidence.
23 - `verification/`: source preservation, current compiler logs and objects, axiom
24 reports, compiler controls, finite computations, test suites and failed attempts.
25 - `scripts/`: portable verification, replay, reporting and test programs.
26 - `PROGRESS_LEDGER.md`, `PROGRESS_LEDGER.json`, `CONTINUE_HERE.md`: versioned status
27 and the next restart point.
28
29 ## Reproduce the checks
30
31 Use Python 3.11 or newer on Linux/WSL. Commands write new evidence outside the
32 frozen package. They do not install software, fetch dependencies, or edit the
33 accepted mathematical sources.
34
35 ```bash
36 python3 -B scripts/verify_release.py
37 python3 -B scripts/run_checks.py --mode records --work /tmp/paper-iv-records
38 python3 -B scripts/run_checks.py --mode finite --work /tmp/paper-iv-finite
39 bash Run-Replay.sh /path/to/Komorebi_Portable_Lean_4.34.0-rc2 /tmp/paper-iv-full
40 ```
41
42 Every output directory must be new. Full mode requires the matching external
43 Lean runtime and all cached packages specified in `formalization/lean/lake-manifest.json`.
44 Finite mode additionally requires the Python packages recorded in the finite receipt.
45 The report builder uses ReportLab. Native Windows execution was not tested.
46
47 `verify_release.py` checks stored evidence and hashes; it is not a new compiler
48 run. Full mode performs fresh source compilation, kind and axiom checks, and
49 compiler controls. Its 300-second per-command timeout and one-worker configuration
50 retain the accepted production settings.
51
52 ## Reader versions and exact scope
53
54 The older monograph and Lean reader correctly describe their own earlier edition
55 and its historical formal evidence. The new closeout report is the authority for
56 this execution. The October 16 standalone visual PDF is preserved, including its
57 branch-sensitive correction. The exact updated editable source for that standalone
58 PDF was not recovered; the October 8 editable baseline and a three-page PDF text
59 difference record are included. No byte-identical regeneration of that later PDF
60 is claimed.
61
62 The reviewed 68-result contract, hypotheses, branch choices and explicit research
63 boundaries are unchanged. Imported standard fact 11.1 is outside that count.
64 No new independent semantic reproof of all 68 statements, cold Mathlib build,
65 independent proof kernel, external referee review, or licence decision is claimed.
66
67 The separate `Paper_IV_Delivery_Verification_v1.1.0.json` records the final ZIP
68 hash, fresh extraction and post-extraction tests. It is external to the archive
69 to avoid circular self-hashing.