Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets

Download original file

This is the original source text. Reading it does not run or verify the program.

Read the typeset paper

1 {
2   "schema": "komorebi.paper-ii.reviewed-release/3",
3   "edition_date": "2026-10-19",
4   "version": "1.1.1",
5   "created_utc": "2026-10-20T15:05:41.108484+00:00",
6   "author": "Komorebi P.",
7   "state": "READY_FOR_RELEASE",
8   "decision": "All 53 enumerated proof-level manuscript scopes retain accepted source correspondence and exact-source kernel replay. All three reading editions retain their reviewed bytes. Open project licenses are applied, third-party terms are preserved, and fresh source/publication binding checks and all 48 existing Python tests pass.",
9   "all_enumerated_proof_scopes_covered": true,
10   "publication": {
11     "path": "publication/FINAL_PUBLICATION_REVIEW.json",
12     "sha256": "667cc5d149b8d6e2ad6915b6dd8be87747faa5ebda0d5a28bc2e6fd59bdc4138",
13     "total_pages": 157,
14     "all_page_visual_review": "PASS",
15     "documents": [
16       {
17         "path": "papers/Paper_II_Traditional_Final.pdf",
18         "pages": 80,
19         "sha256": "460efdb92bbd39bb304fbd535ecbfe814d89f704de3dd4563e1e40af1abd6eee"
20       },
21       {
22         "path": "papers/Paper_II_Visual_Guide_Final.pdf",
23         "pages": 26,
24         "sha256": "9ed63381f0c0a0c4c6f463064db128b28ad324f4942dd5a05829afdc6a2c4f90"
25       },
26       {
27         "path": "papers/Paper_II_Lean_Guide_Final.pdf",
28         "pages": 51,
29         "sha256": "e3776d3648eacb5ce887d7a46ca0cf107f651a9ed154c1b54d64c19f06f8552e"
30       }
31     ]
32   },
33   "formal": {
34     "verification": {
35       "path": "verification/closeout_2026-10-19/attempt02_m4096/verification.json",
36       "sha256": "93b9af1a15e5ad431f169aa29bb2e12694559e176a103d0ca9b91062f4e16512"
37     },
38     "correspondence": {
39       "path": "formal/coverage/Paper_II_Current_Correspondence_2026-10-19.json",
40       "sha256": "c37ac1a5a4b95f5e9c9f89a43dc371b9bd1d2febb778b4e465b624cfdafa680f"
41     },
42     "toolchain": "Lean (version 4.34.0-rc2, x86_64-unknown-linux-gnu, commit 6a10ac8c22beadecabdbb0919c2b50214762f91d, Release)",
43     "mathlib_revision": "aeb72f1e9981b6d35b426b16dca7759be3e7ba06",
44     "fresh_production_modules": 75,
45     "owned_declarations": 2120,
46     "kernel_replayed_logical_declarations": 2112,
47     "reviewed_runtime_helpers": 8,
48     "negative_controls": 9,
49     "upstream_duplicate_fresh_body_rechecks": 1,
50     "manuscript_records": 81,
51     "proof_level_records": 53,
52     "accepted_complete_scopes": 53,
53     "partial_scopes": 0,
54     "mapped_owned_and_replayed_names": 352,
55     "open_statements": [],
56     "remaining_bridges_within_enumerated_scopes": [],
57     "limitations": [
58       "Pinned upstream cache reused, not independently rebuilt.",
59       "Replay uses Lean own kernel, not an independent implementation.",
60       "Source ownership and kernel validity do not establish manuscript correspondence.",
61       "Only exact reviewed generated runtime helpers are excluded from logical replay. The sole exact reviewed upstream-generated theorem is separately kernel body-checked under a fresh name; all other overlaps are rejected."
62     ],
63     "scope_boundary": "Counts cover the 53 enumerated proof-level records under their displayed hypotheses. They do not certify every explanatory sentence or assert a general admissible-contour existence theorem outside those records. Canonical values are defined whenever the relevant admissible data exist."
64   },
65   "bounded_computation": {
66     "path": "verification/release_2026-10-15/paper2_work/computation_final/reviewed_evidence.json",
67     "sha256": "46577f5d5285c764a5baf98b270c0805173899639b2ba9375ba4735a9a668b39",
68     "status": "PASS_FOR_RECORDED_FINITE_CONTRACT",
69     "final_current_input_hashes_rechecked": 101,
70     "exact_visual_checks": 118,
71     "canonical_summary_rows": 9,
72     "figure_data_paths": 13,
73     "byte_identical_atlas_sources": 22,
74     "expanded_mathematical_groups": 9,
75     "historical_48_pytest_cases_freshly_rerun": false,
76     "scope": "Finite examples and stated numerical tolerances; no universal proof claim.",
77     "current_input_rebind": {
78       "path": "verification/closeout_2026-10-19/computation/COMPUTATION_REBIND.json",
79       "sha256": "2c66d2c0d47eaee8d9fd40e51f4e4bb23ea2c598c23f7ba814e4efb738c7868f"
80     },
81     "fresh_numerical_rerun": false,
82     "record_context": "The preceding fields retain the 19 October baseline computation record. The fresh 20 October 48-test rerun is separately recorded in open_release_verification.python_tests."
83   },
84   "license": {
85     "project_license": "MIT (original software) AND CC-BY-4.0 (original content)",
86     "status": "OPEN_LICENSES_APPLIED",
87     "scope": {
88       "path": "LICENSE.md",
89       "sha256": "ff7c5810809485a586c902f65e7f274ec47792a1279e4605a07652a2e9008398"
90     },
91     "details": {
92       "path": "LICENSE_STATUS.json",
93       "sha256": "f8e3e88efe9fe5dcd14ea608beaf45af1baea9ae1846ad4445eff90a04ec6624"
94     },
95     "third_party_notices": {
96       "path": "LICENSES/THIRD_PARTY_NOTICES.md",
97       "sha256": "c56fc59cdefaa8483eec46194205cc7e6c3315c26ab70d5965326392a5bb7d8d"
98     }
99   },
100   "historical_evidence": "Predecessor maps, unrecovered October16 claims and failed development/replay attempts are retained and identified as history. The current decision uses only the successful exact-source receipt above.",
101   "integrity_manifest": "MANIFEST_SHA256.json",
102   "packaging_exclusions": [
103     "__pycache__ directories",
104     "*.pyc"
105   ],
106   "release_date": "2026-10-20",
107   "open_release_verification": {
108     "date": "2026-10-20",
109     "source_bindings": {
110       "path": "verification/open_release_2026-10-20/source_binding_audit.json",
111       "sha256": "5c730b7ab2cb3d53d1fc49a5f3ac6230a6b5c44313004033c90766e15e57da35"
112     },
113     "publication_bindings": {
114       "path": "verification/open_release_2026-10-20/publication_binding_audit.json",
115       "sha256": "b3105c78404126982505f323e740137af298d6512e2b1f6d6c70092a8509b710"
116     },
117     "python_tests": {
118       "path": "verification/open_release_2026-10-20/python_test_result.json",
119       "sha256": "e7446d4fb1c11f62d397f168e7c3cfe62913a5386e0415e77dec1bf0e48943bf"
120     },
121     "python_tests_passed": 48,
122     "warnings_as_errors": true,
123     "fresh_lean_replay": false,
124     "unchanged_scientific_evidence": "The mathematical sources, correspondence, successful Lean receipt, reviewed PDFs and page-QA evidence retain their prior exact bytes.",
125     "reproduction": "REPRODUCIBILITY.md",
126     "runtime": "External pinned Linux runtime, not bundled."
127   }
128 }

Back to source controls

Back to Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets