The Frohmanian Tether: A Machine-Checked Audit of Its Architecture and Obstructions

We audit the claims of the technical compilation The Frohmanian Symplectic Tether: Architecture, Reduced Jacobi Identity, and the Frohmanian Curve (Zenodo record 23942466) against a Lean 4/Mathlib formalization. Every claim is classified as proved, conditional (proved under explicitly stated hypotheses), refuted (its negation is machine-checked), or not formalized. The library builds without sorry, and the 37 key theorems depend only on the standard axioms propext, Classical.choice, and Quot.sound. Proved results include locality and nonpositive self-pairing (C1/C3) and exact degeneracy on kinetic energy (C2). The compilation's claims of Jacobi vanishing on the reduced orbit and of energy-budget damping are refuted. Its Clay-standard global regularity claim is not established: it holds only conditionally on open hypotheses. The Frohmanian Curve and the Section 5 representations are not formalized. This paper makes no Millennium Prize claim. Code: https://github.com/BenFrohman/frohmanian-tether-verified (commit 26f16da).