REPRODUCE.md
p-adic Canonical Realization
REPRODUCE.md
1 # Reproduce Block34
2
3 ## Read-only evidence replay
4
5 PYTHONDONTWRITEBYTECODE=1 python verify_release.py
6 python validate_manifest.py COMPUTATION_MANIFEST.json --root .
7
8 The first command checks all retained exits, frozen input hashes, both complete
9 axiom inventories, original predecessor identity, compiled artifact presence and
10 archive checksums. It does not execute Lean. The second command is the retained
11 project-local schema1 validator, not the installed plugin's full schema2 validator.
12
13 ## Fresh formal verification
14
15 Use a disposable extracted copy, because the runner intentionally replaces the
16 published receipts and removes only its project-local .lake/build directory.
17 Keep the published ZIP unchanged.
18
19 export RUNTIME=/absolute/path/to/Komorebi_Portable_Lean_4.34.0-rc2
20 export PATH="$RUNTIME/toolchain/bin:$PATH"
21 python verification/prepare_offline.py "$RUNTIME"
22 lean --version
23 lake --version
24 PYTHONDONTWRITEBYTECODE=1 python verification/run_final.py
25
26 Exact Lean: 4.34.0-rc2, commit 6a10ac8c22beadecabdbb0919c2b50214762f91d.
27 Exact mathlib: aeb72f1e9981b6d35b426b16dca7759be3e7ba06. Other package revisions are
28 in lake-manifest.json. The preparation script checks every cached git revision.
29 The portable runtime SHA256 is
30 f7548038f94ea30789ce28fc2ff769c40e9c37d8879ea133e9bea821056342c7.
31
32 The runner checks clean root build, axiom audits, new concrete/universal examples,
33 immediate predecessor examples, positive and negative controls, leanchecker, and
34 exact integer computation. Each subprocess has a 600-second timeout. All
35 registered source/configuration/verification input hashes must remain unchanged.
36 No hard memory or elapsed-time theorem is inferred from this operational timeout.
37 The resource profiles and actual runtime are recorded per phase.
38
39 To run only the finite reference experiment:
40
41 PYTHONDONTWRITEBYTECODE=1 python verification/audit_residual.py
42
43 This produces a new results/audit_residual.json. It does not prove Lean theorems.
44 The theorem/example inventory generator is portable and reads the exact embedded
45 predecessor archive:
46
47 python verification/generate_block34.py
48
49 Do not run generators while the frozen verification runner is active. Generated
50 project constants in the environment audit are separate from source-declared
51 theorem counts. This release does not claim an independent dependency rebuild or
52 independently implemented kernel audit.