Sufficient Resolution

Portable serial replay

The proof runtime is supplied separately. This package contains proof sources, finite companion code, source guides, historical verification and current bounded evidence. It does not contain Lean executables or an imported Mathlib build cache.

Required proof environment:

• Linux x86_64, including x86_64 WSL2 on Windows.
• Komorebi portable Lean 4.34.0-rc2, commit 6a10ac8c22beadecabdbb0919c2b50214762f91d.
• Mathlib revision aeb72f1e9981b6d35b426b16dca7759be3e7ba06 and dependency revisions in lake-manifest.json.
• Python with SymPy 1.14.0 for the finite companion cross-checks. Use requirements-rational-tests.txt; Python is tested separately from Lean.

From this formal directory, inspect the source plan without a proof runtime:

python3 scripts/verify.py --plan-only

With the separately restored matching runtime, launch the full discovered corpus serially:

bash verify_low_memory.sh /path/to/Komorebi_Portable_Lean_4.34.0-rc2 \
  --out verification/full93-local --timeout 240

The driver requires exact Lean version/commit and dependency revisions. It freshly compiles every discovered production module, builds the root, audits every enumerated declaration, runs the stated negative controls, and replays the production modules with the same Lean kernel. Imported Mathlib artifacts are reused. The source parser is checked on this package and is not a general Lean parser. A successful full runtime run has not been performed for this edition.

The launcher sets one Lean thread, serial commands and a default per-process address-space limit of 4 GiB. To choose a different limit, set KOMOREBI_VERIFY_MEMORY_KIB. The limit is not aggregate process-tree memory. The verifier has a per-command wall timeout. --skip-kernel-replay explicitly reduces verification and is recorded in the report. It never means replay passed.

From the release root, finite Python companions can be rerun without Lean:

python3 verification/replay_finite_companions.py --plan-only
python3 verification/replay_finite_companions.py \
  --output verification/local_python_replay

Choose a new output directory for each run. The finite driver uses unchanged check scripts in private per-suite trees, records native JSON results, and validates bounded version-2 manifests. Each suite is capped at 600 wall seconds, 500 CPU seconds per process, 1 GiB address space, one inherited core, one cooperative numerical-library thread, and 1 MiB outer log output. The fixed suites use their own documented seeds. Current bundled evidence resides at verification/python_replay.

Validate a bundled manifest from the release root:

python3 formal/scripts/provenance/validate_manifest.py \
  verification/python_replay/calibration/manifest.json --root .

The bundled provenance utilities are unchanged copies from mathbox computation-audit 3.2.0. Their origin and hashes are recorded. Provenance validation checks records and hashes. It does not prove the mathematics.