Geometric certificates for the Frohmanian tether: Lie–Poisson structure, the metriplectic tethered sum, C2 degeneracy, and open items under C1–C3

We list the Lean 4/Mathlib certificates in the repository frohmanian-symplectic-tether-may-form that bear on the geometry of the tethered bracket. Proved: the field-level classical bracket on finite Fourier sums is antisymmetric and satisfies the Jacobi identity, hence is a Poisson bracket; that its symplectic leaves are the coadjoint orbits is standard background and is not formalized. The tethered sum {·,·}_LP + T splits uniquely into the antisymmetric classical part and the symmetric tether T, which is degenerate in the energy direction and negative semidefinite: it is metriplectic, and its Jacobi identity fails on explicit divergence-free test fields. Condition C2 (degeneracy on the kinetic-energy gradient u) forces every symmetric correction to see only Π_u-components, separating the conservative skeleton (span of u, where the bracket is the classical one) from the dissipative directions u⊥. Open under C1–C3 (matching the repository README): C3 enters the Lean only as an explicit hypothesis; the quartic weight is not forced by C1–C3; and no damping estimate is proved or claimed. No claim is made about Navier–Stokes regularity or the Clay Millennium Problem. All listed theorems build with no sorry and depend only on propext, Classical.choice, Quot.sound. Files: certificate note (PDF, .tex) and the Lean 4/Mathlib sources Basic.lean, Metriplectic.lean, Jacobi.lean, RouteA.lean, Main.lean, FieldJacobi.lean, FieldMetriplectic.lean, TetheredSelfBracket.lean from github.com/BenFrohman/frohmanian-symplectic-tether-may-form. The matching GitHub commit is pending a push; no commit link yet. Related: tethered self-bracket draft 10.5281/zenodo.23965512.