Formal replay: setup, pinned runtime, and coverage
Quantum and Circuits
README.md
1 # Reproducing Quantum and Circuits
2
3 Run these commands from the extracted release root. Keep `release_tools/`,
4 `sources/`, `volume/`, and `verification/` together. Commands locate source
5 projects relative to the wrapper, so the release may be moved without editing
6 absolute paths.
7
8 ## Formal replay
9
10 Use Python 3.10 or later and the separately stored offline
11 `Komorebi_Portable_Lean_4.34.0-rc2` kit. The kit requires Linux x86_64, including
12 a compatible WSL2 distribution. It is not a native Windows or macOS runtime.
13 Git must be installed for dependency revision checks. Allow sufficient free
14 space for the full runtime, dependency cache, and new build directories.
15
16 The pins are:
17
18 | Component | Required revision |
19 | --- | --- |
20 | Lean / Lake | `leanprover/lean4:v4.34.0-rc2` |
21 | Lean commit | `6a10ac8c22beadecabdbb0919c2b50214762f91d` |
22 | Quantum mathlib | `aeb72f1e9981b6d35b426b16dca7759be3e7ba06` |
23 | Other quantum dependencies | Exact revisions in the supplied `lake-manifest.json` |
24 | Circuit dependencies | The pinned toolchain's bundled Std; no mathlib |
25
26 Inspect the commands without installing or starting Lean:
27
28 ```sh
29 python3 release_tools/replay_formal.py \
30 --runtime /path/to/Komorebi_Portable_Lean_4.34.0-rc2 \
31 --out replay/new-run --dry-run
32 ```
33
34 Remove `--dry-run` to execute. The output directory must not already exist.
35 The wrapper runs each original verifier with its existing flags, writes
36 separate console logs, and checks the resulting JSON receipt and process exit
37 status. It performs no downloads. A failing command or receipt produces a
38 failure exit status. The original verifiers enforce their own per-command
39 timeouts and proof checks.
40
41 The quantum project writes `quantum/REPORT.json`; the circuit project writes
42 `circuits/verification.json`. `replay_summary.json` records the overall result,
43 verifier hashes, commands, and receipt hashes. A successful wrapper replay is
44 evidence for the named formal subsets, not every written theorem in the volume.
45
46 On the specific hosted Linux environment that reports **failed to locate
47 application**, explicitly add `--compat-shim` and use a new output directory.
48 This loads the existing kit's `compat/app_path.so` through a private temporary
49 path. The adapter corrects executable-path discovery; it does not alter proof
50 rules. It is never automatically enabled by this wrapper. The original kit
51 README and adapter source explain its narrow purpose.
52
53 ## Counts and supplementary control
54
55 The maintained formal counts are **96 quantum declarations and 115 circuit
56 declarations**. These include supporting lemmas and do not count independent
57 discoveries. The circuit subset covers C01, the sharing-aware degree dependency,
58 and the numerical C02 bound. Its other written claims retain their documented
59 proof status.
60
61 `verification/quantum_fresh_20261026/SUPPLEMENTAL_MODE_ONE.json` records a
62 separate control that proves the first Fourier mode equals twelve and therefore
63 is not zero, then rejects an explicitly rewritten false equality. Its two
64 helper lemmas are **not added to the 96-declaration count**. They strengthen the
65 interpretation of the original false-mode control, whose rejection involved
66 opaque-decision reduction. The supplementary source and logs are retained;
67 `replay_formal.py` runs the original project suites and does not automatically
68 repeat this supplementary experiment.
69
70 ## Exact computations and documents
71
72 The circuit scientific replay uses Python 3.10+ and a C++17 compiler, without
73 external Python packages or network access:
74
75 ```sh
76 cd sources/circuits/Komorebi_Circuit_Obstructions_Research_Edition_1.0/source/komorebi-circuit-obstructions-v1.2.0
77 python3 scripts/check_integrity.py
78 python3 scripts/verify.py --all
79 ```
80
81 Component READMEs specify their other bounded computational commands and
82 requirements. Scientific figure generation uses NumPy and Matplotlib; consult
83 each component's requirements file before rebuilding figures. Finite checks
84 retain their declared domains and do not replace universal proofs.
85
86 To compile the supplied final volume, use XeLaTeX with the packages listed in
87 `volume/preamble.tex`, Latin Modern Roman and Sans, and DejaVu Sans Mono:
88
89 ```sh
90 cd volume
91 xelatex -interaction=nonstopmode -halt-on-error volume.tex
92 xelatex -interaction=nonstopmode -halt-on-error volume.tex
93 xelatex -interaction=nonstopmode -halt-on-error volume.tex
94 ```
95
96 Compile the supplied final TeX files directly. Consolidation scripts document
97 the source lineage; rerunning them may regenerate editorial material. PDF
98 compilation is separate from Lean verification. Poppler supports visual review.
99
100 ## Wrapper validation
101
102 This release's new wrapper was checked with `--help` and both forms of
103 `--dry-run`. Those checks executed no Lean process and make no additional proof
104 claim. The preserved formal receipts record the actual earlier source builds,
105 axiom audits, kernel replays, and rejected controls.