Machine Native Reasoning

Machine-Native Reasoning: Reviewed Mathematical Core

Komorebi P.

This package contains the cumulative formal companion to the 27 selected results in Reviewed Core v0.2. Read release/ADMISSION_RECORD.json and release/ACCEPTED_PROGRESS_LEDGER.md for the actual accepted status. A theorem-map entry alone is not a verification receipt. The source book and accepted earlier proofs remain preserved.

The new formal target is Core 3.2, the exact memory required to retain correction under partition evidence. If r cell–target pairs are attainable, the correction signatures correspond exactly to all subsets of those pairs. The resulting state space has 2^r elements. Exactly r fixed binary bits suffice, and no exact fixed-width memory on all candidate subsets can use fewer.

Read and inspect

• reader/Machine_Native_Reasoning_Reviewed_Core.pdf is the refreshed core reader, with editable sources and its own publication checks alongside it.
• source/core_v0.2.tex and its PDF preserve the unchanged source statements.
• THEOREM_MAP.json connects all selected source statements to explicit endpoints.
• docs/CORE32_PROOF_GUIDE.md explains the final target and its boundaries.
• release/REPORT.md records the completed verification and delivery result.
• release/BOOK_RECOVERY.md, when supplied, identifies the separately missing expanded monograph and the authenticated reader provided instead.

The 27-result correspondence is a selected mathematical core. It does not certify every specialist chapter of the larger Machine-Native Reasoning monograph, an implemented intelligent system, or trained-model capabilities. The separate Large Signal Model release has its own scope and evidence.

Reproduce the formal verification

Use the saved portable Lean 4.34.0-rc2 distribution and pinned dependencies. Restore the five compact runtime parts with tools/restore_runtime.py, following release/RUNTIME_REPRODUCTION.md. The runtime remains external to this package.

export KOMOREBI_LEAN_RUNTIME=/absolute/path/Komorebi_Portable_Lean_4.34.0-rc2
python3 tools/verify_package.py
python3 scripts/supervise.py --runtime "$KOMOREBI_LEAN_RUNTIME" --out evidence/my_replay --whole-timeout 1800

If the compiler reports failed to locate application, use the distribution's preserved compatibility adapter:

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

Choose a new evidence directory. The verifier cold-builds all production modules, checks the source-facing interfaces, audits transitive axioms, replays substantive modules through Lean's kernel, runs the rejection controls and checks the actual imported dependency artifacts. Each compiler invocation uses one worker, warnings as errors, a 4096 MiB internal limit and a 45-second wall limit. Dependency caches are authenticated and reused, not rebuilt. This is the same Lean kernel, not an independent proof checker.

python3 scripts/core32_exact.py --out /tmp/core32_exact.json

The finite enumerator derives signatures directly from event-filtered target sets and compares them with occupancy. Its tested range and exact counts are recorded in its output. Finite checks do not establish the universal theorem.

Preservation and rights

The accepted Core25 source archive is the exact predecessor. All 75 substantive production modules and five source-book files are pinned in PREDECESSOR.json. Earlier partial historical recovery remains documented. New source and objects must pass two sequential cold gates and a frozen-source comparison before the release records admit the final selected result.

Original software and machine-readable contributions use MIT. Original writing uses CC BY 4.0, with external notices and exceptions preserved. See licenses/. No compiler, standalone fonts or third-party research papers are bundled.