The Frohmanian Symplectic Tether T: Written Proofs Companion to the Lean 4 Formalization

Written proofs, each cross-referenced to the Lean 4 declaration that kernel-checks it (axiom audit over 308 declarations: no sorryAx, only propext, Classical.choice, Quot.sound). Result 1 (geometric): under three admissibility conditions the symmetric (metric, metriplectic) correction T(F,G)=-(κw)<Π_uF,Π_uG> to the Lie–Poisson bracket is unique up to scale; the bracket P+T conserves kinetic energy; Jacobi is analyzed via a nine-term expansion. Result 2 concerns a MODIFIED system, the tethered vorticity equation with damping term -κP(|ω|^2ω): L^2 bound, H^1 estimate, log-loss comparison and global smoothness are proved CONDITIONAL on explicitly listed cited propositions (e.g. BKM continuation, local well-posedness) that are not formalized. Plain Navier–Stokes is unchanged, and none of this resolves the Clay Millennium problem. Note: the tether term is symmetric, so despite the name it is a metric (dissipative) correction, not a symplectic 2-form. The Lean development builds in CI (green on the commit archived here) with no sorry and no user-declared axioms. Source: https://github.com/BenFrohman/frohmanian-symplectic-tether at commit 7e6a7b829a60ed1151acdf70781a35026dcf0893.