mxym/math: Mutual-information continuity counterexample v2 — verified classical Lean proof

Abstract

This immutable v2 release supplies the independently verified classical probability-table Lean formalization of the counterexample in unchanged written-proof v1. Exact public source commit: 363224e0f7cf1d7ea7b4ed2546f8ed372da7b04c. Complete source and reproduction package. The original Lean source is byte-preserved (SHA-256 1726a70d840a8af78ccde0fb0801273a5e9acc424b258684fce21c07d6c9419d). Actual classical 3-by-3 joint probability tables, their marginals, Shannon entropies, mutual information and exact half-L1 distance are formalized. The strict violation holds at every 0 < epsilon <= 1/16, and there are valid counterexamples in every positive-distance neighborhood. Both marginals change; this does not resolve the fixed-one-marginal proposal. One freshly compiled owned module; all 38 owned declarations and the complete 16,161-declaration dependency closure passed replay in an initially empty kernel at trust level 0. Only propext, Classical.choice and Quot.sound, with their pinned actual signatures, are admitted. The invalid-proof control was rejected, dependency-cache fingerprints stayed unchanged, and separate literal-table semantic checks passed. This is an independently recorded local verification, not a claim about unrelated GitHub Actions workflows. The standalone proof source, reproducible source archive, complete replay records, losslessly compressed dependency graph, replay summary, exact commit binding and asset checksums are attached. The source archive includes the pinned toolchain/dependency metadata, reproduction driver, every command log, ownership inventory and negative test. Archived build products are evidence; the reproduction driver freshly builds its own owned module. Scope: the diagonal quantum embedding remains a written argument; no general quantum spectral-function library is formalized. The written paper's Section 5 necessary leading-coefficient lower bound is not closed in this Lean source and is not claimed formalized. Novelty/priority remain unconfirmed; no external human peer-review certificate is claimed. V1's content, original publication time and assets remain unchanged. Creator metadata correction: Yongxian Zhang is the research author; OpenAI Codex/AI assistants assisted research, formalization and manuscript preparation and are disclosed as tools, not listed as coauthors. No external funding. This record remains an automatic whole-repository software snapshot; its original CC BY 4.0 metadata, file bytes, version identifier and DOI are retained. The correction does not claim to revoke a previously published license or override third-party file licenses.