README.md
Certified Inference
README.md
1 # Komorebi P. Portable Lean: full compact edition
2
3 This edition preserves **every byte of the original extracted bundle**. It uses
4 stronger lossless compression. No Lean, Lake, mathlib, native compiler, cached
5 proof, source, license, or other file has been removed.
6
7 - Previous compressed archive: 2.897 GB.
8 - Compact archive: 2.220 GB, a **23.4% reduction**.
9 - Extracted directory: about 11 GB, unchanged.
10 - Download parts: 5. Allow 20 GB free space during assembly and extraction.
11
12 Download Lean_Compact_01.zip through Lean_Compact_05.zip into one folder.
13 Extract this starter ZIP into the same folder. Keep the part ZIPs intact.
14 Open a Linux or WSL terminal in that folder and run:
15
16 ```bash
17 python3 assemble.py --extract
18 ```
19
20 Assembly uses Python 3.9+ standard libraries. Extraction uses tar and xz (the xz-utils package).
21 If the ZIPs are elsewhere, add `--parts /path/to/downloads`. To check all parts
22 without creating another archive, use `--verify-only`.
23 The assembler checks ZIP CRCs, every part hash, and the combined SHA-256.
24 Existing output archives and extraction folders are not overwritten.
25
26 The assembled archive is `Lean_Portable_Compact.tar.xz`. Its uncompressed tar data has exactly
27 the same SHA-256 as the original bundle. See COMPRESSION_REPORT.json.
28 Sixteen fresh Linux runtime checks passed, including full import Mathlib,
29 the PRSC VI algebra example, and rejection of a false theorem and a placeholder.
30 See RUNTIME_CHECKS.json. The earlier 23-check report remains inside the bundle.
31
32 Inside the extracted `Komorebi_Portable_Lean_4.34.0-rc2` directory:
33
34 ```bash
35 bash run.sh verify
36 bash run.sh check workspace/PortableCheck.lean
37 ```
38
39 This is the same Linux x86_64 runtime, also intended for x86_64 WSL2. It requires
40 Bash, Python, Git and a compatible glibc Linux environment. It is not a native
41 Windows runtime. The separate native Windows setup kit has not been changed.
42
43 Lean and Lake remain pinned to 4.34.0-rc2. Mathlib remains pinned to
44 `aeb72f1e9981b6d35b426b16dca7759be3e7ba06`, with all nine dependency repositories.
45 The original README inside refers to the earlier archive filename and download
46 size. Use this outer README for the new archive's filename and assembly steps.
47 All original launch, proof-checking, and cache-attachment instructions still apply.
48
49 This changes packaging only. It does not claim to finish any remaining PRSC proofs.