Navin Dutta

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...

Bistability and Bifurcation in Chaperone-Mediated Autophagy: A Mathematical Framework for Parkinson's Disease Therapeutics (PATO v1.0)

Background: Chaperone-mediated autophagy (CMA) failure is a central mechanism in Parkinson's disease (PD), driven by a positive feedback loop in which α-synuclein (αSyn) competitively inhibits LAMP2A — its own clearance receptor. Prior models have identified bistability in CMA-αS...