Work in progress: The Frohmanian Tethered Metriplectic World Model in Lean 4: Canonical Bracket Splitting, Encoding Obstructions, and the Newton Potential

Work in progress (draft). Companion paper to the Lean 4/Mathlib repository, on a tethered metriplectic model (not Navier-Stokes). Its ceiling results are conditional on named, unproved Props. Does NOT solve the Clay problem or say anything about Navier-Stokes regularity. Source: https://github.com/BenFrohman/metriplectic-world-model at commit 9216013. Sibling reduction paper: 10.5281/zenodo.23842298. © 2026 Benjamin Stanley Frohman (ORCID 0009-0006-7068-3718). Licensed under Apache-2.0. New version: corrected PDF (banner/DOI wording, updated status). Work in progress; does not solve the Clay problem. New version (v3): typeset with new LaTeX harness; claims unchanged. Work in progress; does not solve the Clay problem.