# Reproduce Block34

## Read-only evidence replay

    PYTHONDONTWRITEBYTECODE=1 python verify_release.py
    python validate_manifest.py COMPUTATION_MANIFEST.json --root .

The first command checks all retained exits, frozen input hashes, both complete
axiom inventories, original predecessor identity, compiled artifact presence and
archive checksums. It does not execute Lean. The second command is the retained
project-local schema1 validator, not the installed plugin's full schema2 validator.

## Fresh formal verification

Use a disposable extracted copy, because the runner intentionally replaces the
published receipts and removes only its project-local .lake/build directory.
Keep the published ZIP unchanged.

    export RUNTIME=/absolute/path/to/Komorebi_Portable_Lean_4.34.0-rc2
    export PATH="$RUNTIME/toolchain/bin:$PATH"
    python verification/prepare_offline.py "$RUNTIME"
    lean --version
    lake --version
    PYTHONDONTWRITEBYTECODE=1 python verification/run_final.py

Exact Lean: 4.34.0-rc2, commit 6a10ac8c22beadecabdbb0919c2b50214762f91d.
Exact mathlib: aeb72f1e9981b6d35b426b16dca7759be3e7ba06. Other package revisions are
in lake-manifest.json. The preparation script checks every cached git revision.
The portable runtime SHA256 is
f7548038f94ea30789ce28fc2ff769c40e9c37d8879ea133e9bea821056342c7.

The runner checks clean root build, axiom audits, new concrete/universal examples,
immediate predecessor examples, positive and negative controls, leanchecker, and
exact integer computation. Each subprocess has a 600-second timeout. All
registered source/configuration/verification input hashes must remain unchanged.
No hard memory or elapsed-time theorem is inferred from this operational timeout.
The resource profiles and actual runtime are recorded per phase.

To run only the finite reference experiment:

    PYTHONDONTWRITEBYTECODE=1 python verification/audit_residual.py

This produces a new results/audit_residual.json. It does not prove Lean theorems.
The theorem/example inventory generator is portable and reads the exact embedded
predecessor archive:

    python verification/generate_block34.py

Do not run generators while the frozen verification runner is active. Generated
project constants in the environment audit are separate from source-declared
theorem counts. This release does not claim an independent dependency rebuild or
independently implemented kernel audit.