Work in progress: A Lean-verified conditional uniform ceiling for a cubic-tethered vorticity model

Work in progress (draft). Lean 4/Mathlib formalization. Uniform ceiling on sup|omega| for a vorticity model with cubic tether (not Navier-Stokes), conditional on the unproved named Prop FieldStretchingLogLoss plus fixed compact support, regularity and sign hypotheses. Does NOT solve the Clay problem or say anything about Navier-Stokes regularity. Source: https://github.com/BenFrohman/metriplectic-world-model at commit 9216013. © 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.