Quantum and Circuits

Reproducing Quantum and Circuits

Run these commands from the extracted release root. Keep release_tools/, sources/, volume/, and verification/ together. Commands locate source projects relative to the wrapper, so the release may be moved without editing absolute paths.

Formal replay

Use Python 3.10 or later and the separately stored offline Komorebi_Portable_Lean_4.34.0-rc2 kit. The kit requires Linux x86_64, including a compatible WSL2 distribution. It is not a native Windows or macOS runtime. Git must be installed for dependency revision checks. Allow sufficient free space for the full runtime, dependency cache, and new build directories.

The pins are:

Inspect the commands without installing or starting Lean:

python3 release_tools/replay_formal.py \
  --runtime /path/to/Komorebi_Portable_Lean_4.34.0-rc2 \
  --out replay/new-run --dry-run

Remove --dry-run to execute. The output directory must not already exist. The wrapper runs each original verifier with its existing flags, writes separate console logs, and checks the resulting JSON receipt and process exit status. It performs no downloads. A failing command or receipt produces a failure exit status. The original verifiers enforce their own per-command timeouts and proof checks.

The quantum project writes quantum/REPORT.json; the circuit project writes circuits/verification.json. replay_summary.json records the overall result, verifier hashes, commands, and receipt hashes. A successful wrapper replay is evidence for the named formal subsets, not every written theorem in the volume.

On the specific hosted Linux environment that reports failed to locate application, explicitly add --compat-shim and use a new output directory. This loads the existing kit's compat/app_path.so through a private temporary path. The adapter corrects executable-path discovery; it does not alter proof rules. It is never automatically enabled by this wrapper. The original kit README and adapter source explain its narrow purpose.

Counts and supplementary control

The maintained formal counts are 96 quantum declarations and 115 circuit declarations. These include supporting lemmas and do not count independent discoveries. The circuit subset covers C01, the sharing-aware degree dependency, and the numerical C02 bound. Its other written claims retain their documented proof status.

verification/quantum_fresh_20261026/SUPPLEMENTAL_MODE_ONE.json records a separate control that proves the first Fourier mode equals twelve and therefore is not zero, then rejects an explicitly rewritten false equality. Its two helper lemmas are not added to the 96-declaration count. They strengthen the interpretation of the original false-mode control, whose rejection involved opaque-decision reduction. The supplementary source and logs are retained; replay_formal.py runs the original project suites and does not automatically repeat this supplementary experiment.

Exact computations and documents

The circuit scientific replay uses Python 3.10+ and a C++17 compiler, without external Python packages or network access:

cd sources/circuits/Komorebi_Circuit_Obstructions_Research_Edition_1.0/source/komorebi-circuit-obstructions-v1.2.0
python3 scripts/check_integrity.py
python3 scripts/verify.py --all

Component READMEs specify their other bounded computational commands and requirements. Scientific figure generation uses NumPy and Matplotlib; consult each component's requirements file before rebuilding figures. Finite checks retain their declared domains and do not replace universal proofs.

To compile the supplied final volume, use XeLaTeX with the packages listed in volume/preamble.tex, Latin Modern Roman and Sans, and DejaVu Sans Mono:

cd volume
xelatex -interaction=nonstopmode -halt-on-error volume.tex
xelatex -interaction=nonstopmode -halt-on-error volume.tex
xelatex -interaction=nonstopmode -halt-on-error volume.tex

Compile the supplied final TeX files directly. Consolidation scripts document the source lineage; rerunning them may regenerate editorial material. PDF compilation is separate from Lean verification. Poppler supports visual review.

Wrapper validation

This release's new wrapper was checked with --help and both forms of --dry-run. Those checks executed no Lean process and make no additional proof claim. The preserved formal receipts record the actual earlier source builds, axiom audits, kernel replays, and rejected controls.