Edition README
Machine Native Reasoning
README.md
1 # Machine-Native Reasoning: Reviewed Mathematical Core
2
3 Komorebi P.
4
5 This package contains the cumulative formal companion to the 27 selected results
6 in Reviewed Core v0.2. Read `release/ADMISSION_RECORD.json` and
7 `release/ACCEPTED_PROGRESS_LEDGER.md` for the actual accepted status. A theorem-map
8 entry alone is not a verification receipt. The source book and accepted earlier
9 proofs remain preserved.
10
11 The new formal target is Core 3.2, the exact memory required to retain correction
12 under partition evidence. If r cell–target pairs are attainable, the correction
13 signatures correspond exactly to all subsets of those pairs. The resulting
14 state space has 2^r elements. Exactly r fixed binary bits suffice, and no exact
15 fixed-width memory on all candidate subsets can use fewer.
16
17 ## Read and inspect
18
19 - `reader/Machine_Native_Reasoning_Reviewed_Core.pdf` is the refreshed core reader,
20 with editable sources and its own publication checks alongside it.
21 - `source/core_v0.2.tex` and its PDF preserve the unchanged source statements.
22 - `THEOREM_MAP.json` connects all selected source statements to explicit endpoints.
23 - `docs/CORE32_PROOF_GUIDE.md` explains the final target and its boundaries.
24 - `release/REPORT.md` records the completed verification and delivery result.
25 - `release/BOOK_RECOVERY.md`, when supplied, identifies the separately missing
26 expanded monograph and the authenticated reader provided instead.
27
28 The 27-result correspondence is a selected mathematical core. It does not certify
29 every specialist chapter of the larger Machine-Native Reasoning monograph, an
30 implemented intelligent system, or trained-model capabilities. The separate
31 Large Signal Model release has its own scope and evidence.
32
33 ## Reproduce the formal verification
34
35 Use the saved portable Lean 4.34.0-rc2 distribution and pinned dependencies.
36 Restore the five compact runtime parts with `tools/restore_runtime.py`, following
37 `release/RUNTIME_REPRODUCTION.md`. The runtime remains external to this package.
38
39 ```sh
40 export KOMOREBI_LEAN_RUNTIME=/absolute/path/Komorebi_Portable_Lean_4.34.0-rc2
41 python3 tools/verify_package.py
42 python3 scripts/supervise.py --runtime "$KOMOREBI_LEAN_RUNTIME" --out evidence/my_replay --whole-timeout 1800
43 ```
44
45 If the compiler reports `failed to locate application`, use the distribution's
46 preserved compatibility adapter:
47
48 ```sh
49 LD_PRELOAD="$KOMOREBI_LEAN_RUNTIME/compat/app_path.so" python3 scripts/supervise.py --runtime "$KOMOREBI_LEAN_RUNTIME" --out evidence/my_replay_with_adapter --whole-timeout 1800
50 ```
51
52 Choose a new evidence directory. The verifier cold-builds all production modules,
53 checks the source-facing interfaces, audits transitive axioms, replays substantive
54 modules through Lean's kernel, runs the rejection controls and checks the actual
55 imported dependency artifacts. Each compiler invocation uses one worker, warnings
56 as errors, a 4096 MiB internal limit and a 45-second wall limit. Dependency caches
57 are authenticated and reused, not rebuilt. This is the same Lean kernel, not an
58 independent proof checker.
59
60 ```sh
61 python3 scripts/core32_exact.py --out /tmp/core32_exact.json
62 ```
63
64 The finite enumerator derives signatures directly from event-filtered target
65 sets and compares them with occupancy. Its tested range and exact counts are
66 recorded in its output. Finite checks do not establish the universal theorem.
67
68 ## Preservation and rights
69
70 The accepted Core25 source archive is the exact predecessor. All 75 substantive
71 production modules and five source-book files are pinned in `PREDECESSOR.json`.
72 Earlier partial historical recovery remains documented. New source and objects
73 must pass two sequential cold gates and a frozen-source comparison before the
74 release records admit the final selected result.
75
76 Original software and machine-readable contributions use MIT. Original writing
77 uses CC BY 4.0, with external notices and exceptions preserved. See `licenses/`.
78 No compiler, standalone fonts or third-party research papers are bundled.