Metriplectic Completion of the Frohmanian Symplectic Tether: An Assembled Finite-Dimensional Viscous System, the Imported Tether Kernel, and Lean 4 Checks

Working paper with Lean 4 formalization. Source: github.com/BenFrohman/frohmanian-metriplectic-ns, merge commit 344bb21ca3a6c96597b4a1a97d2e069d1ca57d67 (Lean source commit 1ecea6cf99011cd4b962e68ea05a1a03a90e3eb3). Lean v4.30.0-rc1, Mathlib 0c154d67103f74be3a0f2c509f72ccbf5be9f2a7. What Lean proves (75 declarations, each depending only on propext, Classical.choice and Quot.sound; no sorry, admit, native_decide or new axioms; the axiom output is included as axioms-344bb21.txt): Abstract metriplectic systems: energy conservation (Ḣ = 0) and entropy production Ṡ = (S,S) ≥ 0. The proof of {S,H} = 0 uses the Casimir condition at H plus skew-symmetry. An assembled finite-dimensional system on ℝⁿ × ℝ (velocity coefficients u and an entropy coordinate s). It has a Poisson bracket built from a state-dependent skew matrix J(u), a viscous metric bracket with viscosities νᵢ ≥ 0, energy H = ½‖u‖² + s and entropy S = s. All metriplectic axioms are proved. The equations of motion are u̇ᵢ = (J(u)u)ᵢ − νᵢuᵢ and ṡ = Σ νᵢuᵢ², and kinetic-energy loss equals entropy gain. A 3-mode triad instance has non-vacuity lemmas: nonzero brackets, nonconstant energy, strictly positive entropy production and nonzero reversible motion. Against the Frohmanian tether kernel, imported from frohmanian-tether-sdiff at commit 8b7bd6741f8a54587db6a95b4a5199dcf2775f97 rather than re-proved: With the tether's kinetic-energy Hamiltonian, the metric bracket vanishes against H in both slots (via the imported left_H_zero_of_C2_symm). A tether summand next to a degenerate viscous summand is forced to satisfy condition C2. The tether kernel is negative semidefinite on the diagonal and strictly negative somewhere (imported nondegeneracy theorem). So no metriplectic system has the tether kernel as its metric bracket. What is not claimed: The assembled system is finite-dimensional and is not derived from a Fourier truncation of the Navier–Stokes equations. The continuum Navier–Stokes and Navier–Stokes–Fourier equations are not recovered or formalized, and neither are the viscous term or any integration by parts. Condition C2 for the tether kernel is not proved, and no Jacobi identity is claimed. This is not a solution of the Clay Millennium problem. A kernel check is not a geometric or physical proof. Lean checking caught real errors in the original upload: a wrong rule ({S,S} = 0 used where {S,H} = 0 is needed), and a placeholder Navier–Stokes specialization (Unit state, zero brackets). Both are corrected here. Reproducibility. Exact commit: 344bb21ca3a6c96597b4a1a97d2e069d1ca57d67 (main). Lean v4.30.0-rc1; Mathlib 0c154d67103f74be3a0f2c509f72ccbf5be9f2a7. Tether dependency FrohmanianTether (frohmanian-tether-sdiff) pinned to 8b7bd6741f8a54587db6a95b4a5199dcf2775f97. One-command rebuild: lake exe cache get && lake build && ./scripts/kernel_check.sh CI run: https://github.com/BenFrohman/frohmanian-metriplectic-ns/actions/runs/42924375098 (build and axiom logs included). Scope limits: finite-dimensional system; not derived from Navier–Stokes; condition C2 for TetherKernel unproved; no Jacobi identity claimed. Licenses: this record is CC BY 4.0, and the Lean code is Apache-2.0.