Geometric Exclusion of Smooth Solutions to Navier-Stokes Equations at Stationary Right-Angles under No-Slip Boundary Conditions in Lean 4

Abstract

This paper presents a proof by contradiction demonstrating that smooth solutions to the three dimensional incompressible Navier-Stokes equations do not exist for all time. Our argument is a direct consequence of a specific no-slip boundary condition: a stationary right-angle corner. Our results, verified via contradiction and geometric exclusion in Lean 4, provide a definitive counterexample, confirming that singularities must form in finite time.