The Frohmanian Symplectic Tether: Canonical Uniqueness on Coadjoint Orbits of SDiff(T3), Non-Degenerate Casimir Coupling, and Conditional Global Regularity via Quartic Young Absorption in Lean 4

We present a self-contained Lean 4 formalization (leanprover/lean4:v4.30.0-rc1, Mathlib 4, 341 kernel-verified theorems across 12 modules with zero sorry and zero non-standard axioms outside [propext, Classical.choice, Quot.sound]) of the Frohmanian Symplectic Tether on dual coadjoint orbits g* = Omega^1(T^3)/dOmega^0(T^3) of the volume-preserving diffeomorphism group SDiff(T^3), with coupling constant kappa = 27 * C_CZ^4 / (4 * nu^3) = 2187 / (64 * nu^3). Plain Statement of Proved Theorems vs. Conditional Flow Hypotheses: Unconditionally Proved Casimir Non-Degeneracy: We prove unconditionally that the tether kernel preserves all Casimir invariants (tether_preserves_casimirs), has non-positive diagonal density everywhere (tetherPointwiseDensity_nonpos, tetherKernel_diagonal_nonpos), and is strictly negative on every non-Casimir transverse perturbation where vorticity is non-zero (tetherPointwiseDensity_strict_neg_of_noncasimir, tetherKernel_strict_neg_of_orthogonal_component, tetherKernel_nondegenerate_on_casimir_defect). Unconditionally Proved 5-Step Canonical Uniqueness: We prove unconditionally the 5-step canonical uniqueness classification (uniqueness_of_minimal_tether, uniqueness_of_kernel_density, tetherKernel_has_canonical_density, step2_degree, step5_higher_order). Unconditionally Proved Quartic 4=4 Young Absorption, ODE Stability & Zero-Data Non-Vacuity: We prove unconditionally the quartic 4 = 4 Young absorption identity (youngs_absorption_elimination), the ODE comparison stability ceiling (comparison_ode_stability), and the non-vacuity and step-jump exclusion theorems at zero initial data (stepField_not_physical, repaired_huniq_at_zero, global_regularity_for_NS_nonvacuous_at_zero). Conditional Global Regularity for Flows Satisfying the Tether Rate or Bound: The global regularity theorems (frohmanian_tether_theorem and global_regularity_for_NS) hold for flows that satisfy the Frohmanian tether rate or bound (frohmanianTetherRate / frohmanianTetherBound) together with local Kato existence, quantitative restart, and energy-Gronwall uniqueness hypotheses. GitHub Repository: https://github.com/BenFrohman/frohmanian-symplectic-tether-regularity (Commit e0a566734a9b336ba40bf698b6c9944f5b84f8d6, Release v1.0.0) Verification & Provenance: Audited with Titan Audit (DOI: 10.5281/zenodo.23630648), SealGuard (DOI: 10.5281/zenodo.23631670), and Sentinel Gate (DOI: 10.5281/zenodo.23632766).