The Frohmanian Tether on the Coadjoint Orbit: A Lean-Synchronized Statement

Scope: not a Clay Millennium claim. Not peer reviewed. Nothing here proves existence, smoothness or global regularity of solutions of the 3D Navier–Stokes equations. On 4 November 2026 the author wrote a short draft, “The Frohmanian Tether on the Coadjoint Orbit”, synchronized by name with the Lean categories of the tether development (CoadjointOrbit, SDiffActionHyp, TetherKernel, TetheredBracket, FunctionalDerivative). This note reproduces that draft verbatim and, after each section, gives the status of every claim in the Lean 4 development BenFrohman/frohmanian-tether-sdiff at commit 4aba751, with the exact Lean name and file:line. Where the draft and the Lean disagree, the Lean wins, and the disagreement is shown in a marked “Lean correction” box rather than silently rewritten. Proved (standard axioms only): the kernel definition with the global enstrophy weight and κ = 3/2; symmetry of the kernel (tetherKernel_comm); the C3 quadratic form as an equality (tetherKernel_quadratic_form, tetherKernel_C3); nondegeneracy (tetherKernel_nondegenerate); antisymmetry of the classical bracket; polarization on differentiable functionals; locality as a corollary of factorization; transported (equivariant) C1 for translations; uniqueness of classical periodic solutions (imported pillar); and periodic Beale–Kato–Majda continuation (periodicBKMContinuation_of_classical in FrohmanianTether/Pillars/BKMContinuation.lean). Conditional: restricted canonicity (uniqueness_of_minimal_symmetric_tether, from symmetry, saturation and polarization, for functionals with functional gradients); factorization through Πu (on the named hypothesis h_proj); Casimir conservation (on IsCoadjointMotion); energy conservation and the C2/C3 obstruction (on C2); Clay (B) from the periodic tether closing bound alone (clay_B_exact_of_periodic_tether_closing_bound and clay_B_exact_unique_of_periodic_tether_closing_bound; BKM continuation is now proved, so only hclose remains). The repaired rate FrohmanianTetherRateSmooth plus the named classical continuation hypothesis R3BKMContinuation implies Fefferman's Problem (A) (FeffermanClayA.clay_A_fefferman_of_frohmanianTetherRateSmooth); both of those hypotheses remain open for general data and are only shown satisfiable at u0 = 0. This is not a proof of Clay (A) or Clay (B). Open: C2 for the tether kernel; C1 for an abstract action (TetherKernelInvariant); functional Jacobi identity for the classical bracket; real-space curl ∘ Biot–Savart = id; IsCoadjointMotion; the periodic tether closing bound (as hard as Clay (B)); FrohmanianTetherRateSmooth and R3BKMContinuation for general data. Lean corrections to the draft: the field transitive_on_casimir_levels is refuted and removed; δH/δω = u is refuted as a universal statement; fixed-functional C1 is refuted for the concrete action; unrestricted polarization is refuted; the tether rate, as written, is refuted; Πu is an L² Gram–Schmidt projector, not a pointwise one; the classical bracket is named ClassicalBracket; T3 is ℝ³, so the kernel vanishes on continuous periodic vorticities. Reproducibility: commit 4aba751d2d365faf0cc48c5b46e9aa0113519273; toolchain leanprover/lean4:v4.30.0-rc1; Mathlib 0c154d67103f74be3a0f2c509f72ccbf5be9f2a7; CI run 43107567565 (VERIFY OK); axiom audit: 1886 theorems, 2546 declarations, 0 violations, only propext, Classical.choice, Quot.sound. Rebuild: git clone https://github.com/BenFrohman/frohmanian-tether-sdiff && cd frohmanian-tether-sdiff && git checkout 4aba751d2d365faf0cc48c5b46e9aa0113519273 && bash scripts/verify.sh. Files: main.pdf (preview), LaTeX source (main.tex, frohman-paper.sty), the raw draft (original_draft.md), a source archive of the pinned commit, the axiom audit output, README.md and SHA256SUMS. Related works (cross-referenced, not re-released): 10.5281/zenodo.24081999, 10.5281/zenodo.23956935, 10.5281/zenodo.23942463, 10.5281/zenodo.23971661.