Auburn Governance Report Independent Verification of the Permanent Axiom Trust Boundary

This report documents an independent verification exercise on the Permanent Axiom trust boundary of a machine-verified Coq formalisation in the analysis of partial differential equations. The underlying formalisation consists of three independent Coq files for subcritical energy estimates of 3D incompressible Navier-Stokes on the periodic torus, verified by the Coq kernel with zero Admitted statements. The question the report addresses is narrower and more methodological than the mathematics itself: when a formal proof is accepted by the kernel, what remains to be verified by a human auditor, and how should that residual verification work be structured? The report's methodological contribution is an explicit taxonomy of the hypothesis-to-axiom pipeline in AI-assisted formal mathematics. Every Hypothesis introduced in the formalisation is classified as either (a) discharged by a corresponding Lemma whose statement is literally identical, or (b) declared as a Permanent Axiom with a documented classical reference, with no third category permitted. The trust boundary is the set of Permanent Axioms — seventeen in total — each of which is cited to a published classical result, and each of which is preserved in the audit history rather than silently inlined into the proof chain. The report argues that this explicit classification is the minimum honest standard for any independent-researcher formal verification project, and that the alternative — quietly accepting hypotheses without distinguishing between proved and axiomatised ones — produces a formalisation whose trust structure is unreadable. The report is offered as a contribution to the philosophy of mathematical practice and to the methodology of AI-assisted formal verification. The author is a historian by training. The report accompanies a full Figshare deposit containing the Coq files, the manuscript, and supporting documents, and is part of the broader FIELDS Protocol for AI-assisted machine-checked mathematics.