Paper III: Typed Transfer, Nonlinear Packets, and Obstruction Theory

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-iii.release-status/2",
3   "title": "Projector Resolved Seed Calculus III",
4   "author": "Komorebi P.",
5   "release_version": "1.0.0",
6   "release_date": "2026-10-20",
7   "classification": "FINAL_TECHNICAL_RELEASE_WITH_DECLARED_FORMAL_SCOPE",
8   "technical_release_complete": true,
9   "full_manuscript_lean_coverage": false,
10   "ordinary_mathematical_review_status": "NO_REMAINING_SUBSTANTIVE_GAP_FOUND_UNDER_STATED_HYPOTHESES",
11   "external_peer_review_claimed": false,
12   "open_technical_repairs": [],
13   "outputs": [
14     {
15       "path": "publication/Paper_III_Analytic_Supplement_v1.0.0.pdf",
16       "pages": 6,
17       "size_bytes": 321551,
18       "sha256": "6df3c0be4e11c786c02daf09c2755cb4fa3f1749f8a78110ac44970569c1090a"
19     },
20     {
21       "path": "publication/Paper_III_Complete_Reading_Edition_v1.0.0.pdf",
22       "pages": 186,
23       "size_bytes": 1404854,
24       "sha256": "4c2ae3031ace2dafc48bc1dae4b21ad1795b05311c698ad9b4aa8e149356afa4"
25     },
26     {
27       "path": "publication/Paper_III_Final_v1.0.0.pdf",
28       "pages": 99,
29       "size_bytes": 602199,
30       "sha256": "fb5d7a81487ef1e37bb4aa8fed12bd4cce9b6d9b2df667429173ed8299e8db77"
31     },
32     {
33       "path": "publication/Paper_III_Lean_Guide_v1.0.0.pdf",
34       "pages": 53,
35       "size_bytes": 207590,
36       "sha256": "4dcd44d8b79148db0fd24e2a99a5774ec65e75aa98b52017ba7c7e99b9267028"
37     },
38     {
39       "path": "publication/Paper_III_Release_Record_v1.0.0.pdf",
40       "pages": 2,
41       "size_bytes": 5914,
42       "sha256": "b64aa368894c4c33e4cdd33b330e28b167cb7de851eb72b9cdc57a967aafe7f6"
43     },
44     {
45       "path": "publication/Paper_III_Visual_Guide_v1.0.0.pdf",
46       "pages": 26,
47       "size_bytes": 154577,
48       "sha256": "6d7b928a15f71dfd77ed12f8bb7039ce2407792c523a25034cf170c40965a5f2"
49     }
50   ],
51   "manuscript_census": {
52     "total_environments": 167,
53     "theorem_lemma_proposition_corollary_environments": 98,
54     "external_standard_facts": 2,
55     "other_environments": 67,
56     "explicit_proof_environments": 95,
57     "compiled_labels": 149,
58     "statement_register": "metadata/MANUSCRIPT_STATEMENT_REGISTER_v1.0.0.json",
59     "register_sha256": "a29c38c3c392d88ced7ea5bf0feed33dc3c4cb23abaa48ed975d4d0202c0cc38"
60   },
61   "formal_verification": {
62     "status": "PASS",
63     "production_modules": 16,
64     "owned_declarations": 608,
65     "replayed_logical_declarations": 594,
66     "generated_runtime_helpers": 14,
67     "owned_outside_primary_namespace": 33,
68     "theorem_kind_entries_including_generated_support": 330,
69     "accepted_control_commands": 14,
70     "count_interpretation": "Compiler declarations and replay entries, including definitions and generated support; not manuscript theorem counts.",
71     "permitted_transitive_axioms": [
72       "Classical.choice",
73       "Quot.sound",
74       "propext"
75     ],
76     "replay_initial_owned_overlap": 0,
77     "compiler_version": "4.34.0-rc2",
78     "compiler_commit": "6a10ac8c22beadecabdbb0919c2b50214762f91d",
79     "mathlib_commit": "aeb72f1e9981b6d35b426b16dca7759be3e7ba06",
80     "summary": "formal/verification/FINAL_VERIFICATION_SUMMARY.json",
81     "summary_sha256": "4fa5e0d2dc4a985e5daab29a4b2a6bc17c4dc2300f5552fc64226c72d1d1e24e",
82     "accepted_phases": {
83       "full": {
84         "status": "PASS",
85         "report": "verification/final_release_full/report.json",
86         "report_sha256": "8de6d41d6bb1cae20d97025f928d0cb7d2ddc3e2b5473632624cdf51dd9d09a7",
87         "command_count": 16,
88         "all_commands_accepted": true,
89         "finished_utc": "2026-10-20T13:52:06.327324+00:00"
90       },
91       "audit": {
92         "status": "PASS",
93         "report": "verification/final_release_audit/report.json",
94         "report_sha256": "a450ebefddb682505ec1fbacc41e05c98341acfff8664739843173f55da1da72",
95         "command_count": 1,
96         "all_commands_accepted": true,
97         "finished_utc": "2026-10-20T13:53:27.827800+00:00"
98       },
99       "replay": {
100         "status": "PASS",
101         "report": "verification/final_release_replay/report.json",
102         "report_sha256": "6cbdd99f3f58da8dfd6e7da94d2d669be415dfcc9e3a71fc21d838afecad5833",
103         "command_count": 1,
104         "all_commands_accepted": true,
105         "finished_utc": "2026-10-20T13:53:20.655821+00:00"
106       },
107       "controls": {
108         "status": "PASS",
109         "report": "verification/final_release_controls/report.json",
110         "report_sha256": "104956faa652c23657329216aabbe70b6b92538db6708e644c198468f2d1543b",
111         "command_count": 14,
112         "all_commands_accepted": true,
113         "finished_utc": "2026-10-20T13:54:25.781357+00:00"
114       }
115     }
116   },
117   "exact_computation": {
118     "section16_assertions": 15331,
119     "original_section17_assertions": 2622,
120     "higher_calculus_assertions": 677,
121     "total_main_assertions": 18630,
122     "separate_visual_checks": 124,
123     "separate_false_visual_controls_rejected": 4,
124     "scope": "Exact finite checks with documented repetitions and finite ranges; sampled norm-vector inequalities are not exact operator norm computations."
125   },
126   "reading_quality": {
127     "distinct_component_pages": 186,
128     "main_pages": 99,
129     "analytic_supplement_pages": 6,
130     "visual_guide_pages": 26,
131     "lean_guide_pages": 53,
132     "release_record_pages": 2,
133     "all_component_pages_visually_reviewed": true,
134     "all_combined_component_renders_identical": true,
135     "link_destinations_checked": 357,
136     "bookmarks": 203,
137     "unresolved_material_visual_findings": 0,
138     "qa_directory": "evidence/qa/",
139     "main_visual_report": "evidence/review/visual_review_main.json"
140   },
141   "formal_boundaries": {
142     "ordinary_proof_only": [
143       "Packet Taylor integral identity, remainder and estimate",
144       "Stirling/Touchard decorated-partition count",
145       "Later expanded results in Sections 18\u201327"
146     ],
147     "partial_formal_correspondence": [
148       "The range-norm proposition has its sharper actual-range and ambient product bounds formalized; separate restricted-product and Hilbert norm-one corollaries are not separately formalized."
149     ],
150     "total_derivative_scope": "Reconstruction of the total iteratedFDeriv is not a claim of differentiability of an arbitrary function; composition has explicit ContDiffAt assumptions.",
151     "inherited_dependencies": "Papers I\u2013II source evidence remains inherited and was not recompiled here.",
152     "unrecovered_historical_claim": "No matched source was recovered for the October 16 2693-declaration/full-98+2 formal claim; it is not certified."
153   },
154   "provenance": {
155     "parent_release": "1.0.0-rc1",
156     "recovered_parent_zip": "Paper_III_Scoped_Release_v1.0.0-rc1_2026-10-20.zip",
157     "recovered_parent_zip_sha256": "5822e71704b4436f67f7ca72c3b44ed2db708a85b44fb88d5e5cfb84dcf38a24",
158     "unchanged_checkpoint_files": 1061,
159     "checkpoint_preservation_record": "evidence/CHECKPOINT_PRESERVATION.json",
160     "failed_attempts_retained": true
161   },
162   "distribution_verification": {
163     "manifest": "MANIFEST_SHA256.json",
164     "fresh_extraction_receipt": "Paper_III_Freeze_Delivery_Verification_v1.0.0_2026-10-20.json, delivered alongside the ZIP",
165     "gate": "Distribute only after the exact ZIP passes CRC, safe-member, full manifest and recorded-evidence checks in a fresh extraction."
166   },
167   "rights": {
168     "project_license_selected": true,
169     "public_publication_performed": false,
170     "existing_notices_retained": true,
171     "record": "LICENSE.md",
172     "open_licenses_applied": true,
173     "original_code_and_machine_readable_material": "MIT",
174     "original_writing_and_figures": "CC-BY-4.0",
175     "record_sha256": "abf951fb085eceb6dc21cde74023349dd25e757573e31c3db73a022b85fb421d",
176     "historical_unassigned_license_status_superseded": true
177   },
178   "distribution_freeze": {
179     "date": "2026-10-20",
180     "state": "FROZEN_WITHIN_ACCEPTED_SCOPE",
181     "record": "FREEZE_RECORD.json",
182     "science_and_pdf_bytes_changed": false,
183     "full_manuscript_lean_coverage": false
184   }
185 }

Back to source controls

Back to Paper III: Typed Transfer, Nonlinear Packets, and Obstruction Theory