The Riccati Vorticity Estimate M′ ≤ C − kM² Fails for 3D Navier–Stokes on T³: An Explicit Counterexample and a Lean-Checked Audit of the Symplectic-Tether Draft

An earlier unpublished draft by the author claimed global regularity for the 3D incompressible Navier–Stokes equations via a "symplectic tether". Its central step was the a-priori Riccati estimate M′(t) ≤ C − k M(t)² for the vorticity sup-norm M(t) = ‖ω(·,t)‖L∞. This note shows where that estimate fails and where it is still open. Refuted (V1): constants depending only on the viscosity ν. The explicit datum u₀ = A·U, with U = 3(−sin y, sin x, 0) + (−sin x cos z, 0, cos x sin z), has vorticity ω = A(0, 2 sin x sin z, 3(cos x + cos y)) and M(0) = 6A, and the lower right derivative of M at t = 0 is at least 6A(A − ν). The estimate fails for every fixed C, k once A = ν + 1 + |C|/k. Refuted (V2): constants depending on ν and the kinetic energy in any way at all, and also on ν and ‖u₀‖L³. The counterexample is a Navier–Stokes-scaled localized vortex, with its sup-vorticity maximum certified by rigorous interval arithmetic (Arb). Open (V3): constants allowed to depend on the initial data arbitrarily. That version is equivalent to global regularity and remains open. No claim about the Clay Millennium Problem is made. Lean-checked audit of the draft: the tether form B is symmetric, not antisymmetric, so the "2-form" is not symplectic. B(F,H) = 0 makes the flow independent of κ, so any feedback cannot come from the tether. The tanh solution formula only covers |y₀| < √(C/k). The conditional chain "Riccati estimate + BKM ⇒ no finite-time blow-up" is proved, with the estimate as an explicit hypothesis. What is machine-checked and what is cited: 50 Lean 4 declarations (Lean 4.22.0, Mathlib v4.22.0 at revision 79e94a093aff4a60fb1b1f92d9681e407124c2ca) build without sorry, using only propext, Classical.choice and Quot.sound. The following are cited or computed outside Lean, not formalized: Kato local existence and smoothness up to t = 0 (the derivative identification); the Danskin-type Dini bound; the BKM criterion; the Arb interval certificate and sympy values; decay facts. Numerical simulations are supporting only and are not part of any proof. Version 1.1.0: this version adds the certificate artifacts from the 10 November 2026 verification run, which are byte-identical to the GitHub Actions verify-logs artifacts of runs 42916652258 and 42916649801: the Lean axiom output (axioms.log), the Lean build log (lake_build.log), and the Arb certificate result (v2_maxcert.log) containing the line "CERTIFIED: max |omega1|^2 = 144 attained only at the origin; M_1 = ||omega1||_inf = 12", together with the verify.sh closing line "ALL CHECKS PASSED". SHA-256 checksums are recorded in the paper and in the certificate-artifacts bundle. The mathematical claims are unchanged from version 1.0.0. The source repository, with one-command verification (verify.sh), is at https://github.com/BenFrohman/ns-tether-key-estimate-refutation. The code (Lean, Python, scripts) is licensed under Apache-2.0; the paper is licensed under CC BY 4.0.