A.16 Controls, failed attempts, and reproducibility
On this page · Permalink · Source line 798
The latest archive rejected a deliberately false signal sign and a proof using sorry under warnings as errors. Its false Fourier-mode control also failed, but the compiler stopped at opaque Decidable reduction. That failure alone is not a direct mathematical certificate that the proposition is false. The positive ramanujan_dft_table theorem separately establishes the correct value 12.
The control runner's broad diagnostic expression can match the word “false” in a filename. The guide does not interpret that match as a stronger arithmetic test than the actual log provides. The earlier checkpoint's four explicit refutation proofs are retained as earlier evidence and are not silently counted as current production theorems.
A supplementary current check closes the diagnostic gap for the false-mode control. It derives the exact mode-one value and its negation from the proved Fourier table, replays the supplementary module through the kernel, and rejects a false rational-coordinate equality with an explicit false-value diagnostic. These two verification lemmas do not increase the monograph count of 96 theorems.
The supplied verifier creates a fresh source project, checks dependency revisions, builds, prints all theorem axiom dependencies, replays all five modules, and runs the controls. It refuses to overwrite an existing fresh build directory and treats timeouts as failures. It makes no network requests or installations. With the pinned runtime restored, the documented command is:
python scripts/verify_lean.py \
--toolchain /path/to/Komorebi_Portable_Lean_4.34.0-rc2/toolchain \
--packages /path/to/Komorebi_Portable_Lean_4.34.0-rc2/workspace/.lake/packages \
--out verification/reproduction_newThe runner was exercised under Linux x86-64. It uses POSIX process groups and filesystem symlinks. Native Windows behavior is not tested. WSL2 with the pinned Linux runtime is the documented route for a Windows machine.
Full proof source, manifests, archived build and replay logs, the static concordance builder, and the current successful replay receipt are included. The runtime itself remains an external dependency.