Fields, Ryan: Between Qed and Truth: The Permanent Axiom Trust Boundary in Machine-Verified Mathematics: A Historical Survey of Seventeen Classical Theorems (1919–1989) Underlying the First Coq-Verified Navier-Stokes Formalisation

This paper presents an exhaustive historical and mathematical survey of the seventeen Permanent Axioms underlying the first machine-verified Coq formalisation of a global regularity result for the three-dimensional incompressible Navier-Stokes equations on the periodic torus T³. The formalisation establishes subcritical energy estimates for arbitrary smooth initial data in the Sobolev regularity class H^s for s > 3, producing a combined energy inequality that precludes finite-time blowup via a G