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 Gronwall-Bihari closure. The proof chain comprises approximately 59 Qed theorems, zero Admitted statements, and 17 Permanent Axioms encoding classical results of PDE theory and harmonic analysis spanning 1919 to 1989. Each axiom is traced to its original publication, its proof history, its modern textbook treatments, its validity in the specific setting of incompressible flow on T³, its relationship to the broader Navier-Stokes regularity literature, and its current formalisation status in proof assistants including Lean, Coq, and Isabelle. The axioms encode results by Leray (1934), Sobolev (1938), Calderón and Zygmund (1952), Gronwall (1919), Kato and Ponce (1988), Prodi (1959), Serrin (1963), Giga (1981), Beale, Kato, and Majda (1984), Batchelor (1967), Plancherel (1910), Bernstein (1912), and Stein (1970). The paper introduces the concept of the Permanent Axiom Trust Boundary: the epistemic distinction between an author's novel derivations (which are entirely machine-verified) and the classical canon of twentieth-century mathematics (which the formalisation assumes as axiomatic). This boundary defines what machine verification can and cannot certify, and constitutes a contribution to the epistemology of computer-assisted mathematical proof. The formalisation gap between classical continuous mathematics and machine-verified type theory is documented, with a projected closure timeline informed by the HALF Project at Bonn, the Carleson formalisation, and the Armstrong-Kempe De Giorgi-Nash-Moser programme. All seventeen axioms are confirmed as Classical and Standard. Zero require further justification. The trust required by the formalisation is not trust in the author but trust in the established canon of analysis and PDE theory.