Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates

Download original file

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

Read the typeset paper

1 PAPER I — CURRENT FORMAL DEVELOPMENT
2 Komorebi P. | 15 October 2026
3 
4 current/PaperIRelease.lean imports the complete current development, including
5 the original foundation, Blocks 03–08, and the release additions. The frozen
6 module order and source hashes are in current/release_modules.json. Four
7 positive boundary-consumer modules are included in this closure; tests/
8 ReleaseBoundary.lean adds the retained 25-assertion predecessor suite.
9 
10 coverage/COVERAGE_108.json is the exact current manuscript correspondence.
11 Its 69 proof-level records are distinct publication records, not a count of
12 independent mathematical discoveries. Definitions, three classical inputs,
13 scope boundaries, and documentary records are classified separately.
14 Semantic review matches the printed claims to formal types. Lean checks the
15 formal types and proof terms; it does not parse or certify the English prose.
16 
17 REPRODUCE THE FORMAL CHECK
18 
19 Use the pinned Komorebi_Portable_Lean_4.34.0-rc2 runtime with its original
20 workspace and upstream dependencies. runtime_bindings.json records the
21 precise Lean binary, runtime-file hashes, and nine Git dependency revisions.
22 The small runtime_specification/ directory preserves the exact launcher,
23 workspace configuration and compatibility-adapter source from that kit.
24 Lean commit: 6a10ac8c22beadecabdbb0919c2b50214762f91d
25 Mathlib commit: aeb72f1e9981b6d35b426b16dca7759be3e7ba06
26 
27 From the release root, run:
28 
29   bash formal/verify.sh /absolute/path/to/pinned-runtime /absolute/path/to/new-output
30 
31 The output directory must not exist. The default rebuilds every frozen
32 project source, with warnings fatal and implicit-variable guards enabled.
33 It then audits every source-owned declaration, checks the axiom closure,
34 rejects twelve deliberate invalid-proof/audit controls, and checks the
35 entire logical closure starting from upstream imports only. Project objects
36 shipped as evidence are not used as build inputs.
37 
38 One generated theorem is also present upstream with exactly identical name,
39 type, universe parameters, all-list and proof body. Its body is checked by the
40 kernel under a fresh audit name; the other 3,499 logical declarations are
41 replayed normally. The union of their original names must match all 3,500
42 audited logical names exactly. A corrupted-body control checks the fresh-name
43 verification path. The 13 runtime-only helpers are separately inventoried.
44 
45 The runtime and multi-gigabyte upstream cache are external prerequisites.
46 All project Lean modules are included in current/.
47 The verifier uses Lean's official kernel, not an independent implementation;
48 runtime files and dependency revisions are checked, while the pinned upstream
49 cache is reused rather than rebuilt here.
50 Generated partial runtime helpers are inventoried separately from logical
51 declarations and are excluded from proof replay.
52 
53 EVIDENCE
54 
55 evidence/RELEASE_VERIFICATION.json is the current acceptance summary.
56 evidence/whole_closure/ contains the fresh compiler and replay logs, exact
57 source snapshots, source/object hashes, declaration inventories, controls,
58 and verifier input snapshots. evidence/semantic/ contains the five semantic
59 review reports. evidence/development/ preserves intermediate author and
60 reviewer checks with their original scopes and paths; these are provenance,
61 not substitute final acceptance records.
62 
63 The source_compilation component shares its 116 byte-identical object files
64 with whole_closure. Its original receipt is unchanged. See
65 evidence/source_compilation/OBJECT_LOCATIONS.json and README.txt for the exact
66 locations and a hash-checking helper that restores the original layout for
67 optional --base-fresh reuse. Default fresh verification needs no restoration.
68 
69 The full accepted Block08 archive is retained under source/predecessor/
70 at the release root. PREDECESSOR.json records its identity. Historical
71 coverage counts there describe that earlier checkpoint only.
72 
73 Executable Python examples and their retained lock file are in code/python/
74 at the release root. Exact manuscript visual checks are in
75 editable/traditional/visual_checks/. Their recorded limits and run receipts
76 are under verification/python/. They are bounded computational evidence,
77 not a universal proof or formal verification of the Python implementation.

Back to source controls

Back to Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates