Two Consistency Failures in the VMS Mathematical Appendix: A Machine-Checked Lean 4 Verification

This record contains the paper “Two Consistency Failures in the VMS Mathematical Appendix” and a machine-checked Lean 4 verification of all of its mathematics. The paper shows that two derivation steps in the VMS Institute’s Mathematical Bridge — Math Appendix fail as published. First, the hydrogen calibration, energy ladder, photon relation and wavelength formula are mutually inconsistent: they differ by exactly 16π⁴. Second, the proposed square-root action does not enforce the eikonal constraint it is meant to describe, as shown by explicit counterexamples in both directions. LEAN_PROOF_50000.zip is a self-contained Lean 4 project (Lean v4.35.0-rc3, Mathlib commit c55e6e78). Its single proof file contains 300 theorems with no sorry. The 161 axiom checks show that every result depends only on Lean’s three standard axioms. To verify, run “lake exe cache get” and then “lake build”. The README maps each result in the paper to its Lean theorem. The paper’s analysis was assisted by OpenAI’s ChatGPT (Codex), as disclosed in the paper. The Lean formalization was produced with the assistance of Anthropic’s Claude (Claude Code); its correctness is certified by the Lean kernel.