A Modular Formalization of 2D Navier-Stokes Uniqueness in Lean 4: Sorry-Free 1D Gagliardo-Nirenberg and Axiomatic Reduction of the Ladyzhenskaya Argument

Abstract: We present a machine-checked modular formalization in Lean 4 (with Mathlib4) towards the formal verification of the 2D incompressible Navier-Stokes global uniqueness theorem. The package delivers two primary contributions: (1) A complete, 100% sorry-free formal proof of the 1D Gagliardo-Nirenberg interpolation inequality (||f||_{L^4}^4 ≤ 2 ||f||_{L^2}^3 ||f'||_{L^2}) derived directly from the Fundamental Theorem of Calculus, integration by parts, and a quadratic discriminant minimization for L2 integrals; (2) A complete axiomatic reduction of the classical Ladyzhenskaya uniqueness argument on an abstract Hilbert space H, formalizing the exact algebraic viscosity absorption via Young's inequality and deducing the closed differential Gronwall inequality that guarantees uniqueness of weak solutions. Package Contents: Includes paper.tex (LaTeX preprint), paper.md, GagliardoNirenberg.lean, NS2D_Uniqueness_Complete.lean, EvolutionaryAttempts.lean, lakefile.lean, lean-toolchain, reproduction scripts, and zenodo_deposit_bundle.zip.