Grade Decomposition and Gevrey Regularity for Navier-Stokes: A Machine-Checked Conditional Framework

Tamás Nagy, Ph.D.

Abstract

We introduce a grade decomposition of the Gevrey energy balance for the incompressible Navier-Stokes equations. The physically correct model uses \(\mathbb{C}\)-valued Fourier coefficients with a factor of \(i\) in the advection; the real-coefficient model trivializes all grade-3 terms. With this correction, the energy balance becomes

\[\frac{d}{dt}G_\sigma = \underbrace{-2\nu H_\sigma}_{\text{grade-2 (viscous)}} \underbrace{- 2\, b_\sigma(u,u,u)}_{\text{grade-3 (advective)}}\]

where \(b_0 = 0\) (energy conservation) but \(b_\sigma \neq 0\) for typical \(\sigma > 0\) in 3D. The Foias-Temam completing-the-square inequality (1989) is the classical analytic input behind transferring \(L^2\) smallness to Gevrey control; in this kernel it is still postulated as an axiom (completing_square_gevrey_bound), while the pure algebra \(2\sigma x - 2\nu s x^2 \leq \sigma^2/(2\nu s)\) is proved. These ingredients organize a three-phase conditional Galerkin argument: L\(^2\) decay → Gevrey transfer → gate lock-in.

The framework is machine-checked in a custom proof kernel (1,156 theorems, 44 axioms, 0 sorry), with proofs exportable to Lean 4. The 44 remaining axioms are intended to encode standard ODE/PDE ingredients (Picard-Lindelöf-type flow, Gronwall, Foias-Temam-type estimates, Aubin-Lions compactness). Closing them in a proof assistant is substantial work; axiomatization is not a mathematical proof of the corresponding classical statements, and does not advance the Clay problem without a complete, correct limit passage. Five of the original 16 axioms have been eliminated by proof during formalization. A second storyline (§8) isolates a conjectured bound \(|A| \leq C \cdot H_0/\sqrt{G_0}\) with numerical support for \(K \leq 6\) only; we do not claim that proving this bound (even together with the other kernel axioms) would automatically settle the Clay Millennium Problem without a rigorous, uniform-in-\(K\) limit theorem to Navier-Stokes weak/strong solutions.

---

1. Introduction

1.1 The Navier-Stokes Regularity Problem

The 3D incompressible Navier-Stokes equations

\[\partial_t u + (u \cdot \nabla)u = \nu\Delta u - \nabla p, \qquad \nabla \cdot u = 0\]

describe viscous fluid motion and constitute one of the seven Clay Millennium Prize Problems. The question: does a smooth solution exist for all time, given smooth initial data and \(\nu > 0\)?

In 2D, the answer is yes (Ladyzhenskaya, 1969). In 3D, it remains open despite 90 years of effort since Leray's foundational 1934 paper. Numerous conditional regularity criteria exist — Beale-Kato-Majda (1984), Prodi-Serrin (1959–1962), Escauriaza-Seregin-Šverák (2003) — each identifying sufficient conditions that prevent blow-up. All are conditional: they say "if X holds, then regularity," without proving X.

1.2 What We Contribute

We offer five things that are new in combination:

1. 1. The physically correct complex model. The real-coefficient Galerkin model has \(b_\sigma = 0\) for all \(\sigma\), trivializing the regularity problem. The correct model requires \(\mathbb{C}\)-valued Fourier coefficients with a factor of \(i\) in the advection.
1. 2. A grade decomposition that cleanly separates the Gevrey energy evolution into grade-2 (viscous, always stabilizing) and grade-3 (advective, potentially destabilizing) contributions.
1. 3. The completing-the-square / Foias-Temam layer. The Foias-Temam (1989) program supplies the classical analytic estimate that transfers \(L^2\) smallness to Gevrey control after a delay. In this paper, that step is packaged as an axiom (completing_square_gevrey_bound) in the proof kernel, not as a fully derived theorem from first principles. The resulting three-phase conditional structure (L\(^2\) decay → Foias-Temam-type delay → gate lock-in) organizes the Galerkin argument; it does not by itself settle the Clay Millennium Problem, which requires uniform-in-\(K\) control and a rigorous limit to weak/strong solutions.
1. 4. Machine-checked proofs in a formal verification kernel (1,156 theorems, 44 axioms, 0 sorry; exportable to Lean 4). To our knowledge, the largest formal verification of any Navier-Stokes regularity result. Five of the original 16 axioms have been eliminated by proof during formalization (see §5.2).
1. 5. Numerical verification. Seven independent numerical tests confirm the completing-the-square algebra, energy conservation (\(b_0 = 0\) to machine precision), Poincaré inequality, L\(^2\) exponential decay, the Foias-Temam Gevrey bound, the three-phase regularity timeline, and grade-3 non-vanishing in 3D for \(\sigma > 0\).

1.3 Related Work

Gevrey regularity for NS. Foias and Temam (1989) introduced the analyticity radius approach, showing that solutions are real-analytic with a radius that can be estimated from energy bounds. Levermore and Oliver (1997) developed the Gevrey norm framework systematically. Our contribution is the grade decomposition and its formalization, not the Gevrey framework itself.

Formal verification of PDE theory. Hales et al. (2017) formalized the Kepler conjecture; Gonthier (2008) formalized the four-color theorem. Formalization of fluid dynamics is almost nonexistent. The closest work is the formalization of basic Sobolev spaces by Bréhard et al. (2024) in Coq. We are not aware of a prior Lean formalization of Navier-Stokes regularity statements at comparable scope; the present work is therefore best read as a large Galerkin-level verification effort, not as a claim of full PDE closure in a proof assistant.

Galerkin approximation. Galerkin truncation is standard in the numerical analysis of PDEs (Temam 1977, Constantin & Foias 1988). Our use of it for formalization is deliberate: the finite-dimensional setting avoids measure-theoretic subtleties while preserving the essential algebraic structure of the regularity argument.

---

2. Setup: Galerkin Navier-Stokes

2.1 Mode Space and Velocity Fields

We work on the periodic torus \(\mathbb{T}^d = (\mathbb{R}/2\pi\mathbb{Z})^d\) in spatial dimension \(d\) (typically \(d = 2\) or \(3\)). The Galerkin truncation at resolution \(K\) restricts to Fourier modes with wavenumber \(|k| \leq K\):

\[\Lambda_K = \{k \in \mathbb{Z}^d : |k|^2 \leq K^2\}\]

A Galerkin velocity field \(u\) is a map \(\hat u : \Lambda_K \to \mathbb{R}^d\) assigning a \(d\)-dimensional vector to each mode, subject to the incompressibility constraint \(k \cdot \hat u(k) = 0\).

Lean declaration. (Throughout this paper, we include Lean 4 source excerpts from the archived formalization for concreteness. The active verification backend is the proof kernel described in §5.1.) [Defs.lean]

``lean structure GalerkinVelocity (d : ℕ) (K : ℕ) where hat : WaveVector d → Fin d → ℝ supported : ∀ k, k ∉ GalerkinModes d K → hat k = 0

def isIncompressible {d : ℕ} {K : ℕ} (u : GalerkinVelocity d K) : Prop := ∀ k ∈ GalerkinModes d K, ∑ i : Fin d, (k i : ℝ) * u.hat k i = 0 `

2.2 The Stokes Operator (Grade-2)

The Stokes operator \(A\) acts diagonally in Fourier space: \((Au)(k) = |k|^2 u(k)\). It is the linearized dissipation mechanism — the grade-2 operator in our decomposition. Its contribution to the energy balance is always non-positive: viscosity removes energy.

2.3 The Bilinear Advection (Grade-3)

The advection term \(B(u,v)(k) = \sum_{p+q=k} P(k) \cdot k_j \hat u(p)_j \hat v(q)\) couples three modes via the Leray projector \(P_{im}(k) = \delta_{im} - k_i k_m / |k|^2\). This is the grade-3 operator — it mediates the nonlinear energy cascade.

---

3. The Grade Decomposition

3.1 Gevrey Norms and Enstrophy

The Gevrey norm at parameter \(\sigma \geq 0\) is

\[G_\sigma(u) = \sum_{k \in \Lambda_K} e^{2\sigma|k|} |\hat u(k)|^2\]

and the Gevrey enstrophy is

\[H_\sigma(u) = \sum_{k \in \Lambda_K} |k|^2 e^{2\sigma|k|} |\hat u(k)|^2.\]

The parameter \(\sigma\) controls the analyticity: \(G_\sigma < \infty\) implies the velocity field extends analytically to a strip of width \(\sigma\) in the complex plane, with analyticity radius \(\rho = e^\sigma\).

Lean declarations. [GevreyNorm.lean]

`lean def gevreyNorm {d : ℕ} {K : ℕ} (σ : ℝ) (u : GalerkinVelocity d K) : ℝ := ∑ k ∈ GalerkinModes d K, gevreyWeight σ k * ∑ i : Fin d, (u.hat k i) ^ 2

def gevreyEnstrophy {d : ℕ} {K : ℕ} (σ : ℝ) (u : GalerkinVelocity d K) : ℝ := ∑ k ∈ GalerkinModes d K, wavenumberSq k gevreyWeight σ k ∑ i : Fin d, (u.hat k i) ^ 2 `

3.2 The Energy Balance

The Gevrey-weighted trilinear form \(b_\sigma(u,v,w) = \sum_k e^{2\sigma|k|} \hat w(k) \cdot \hat B(u,v)(k)\) measures the rate of nonlinear energy transfer at scale \(\sigma\). The energy balance is:

\[\frac{d}{dt} G_\sigma(u(t)) = -2\nu H_\sigma(u(t)) - 2\, b_\sigma(u(t), u(t), u(t))\]

Grade assignment:

Term	Grade	Role	Sign
\(-2\nu H_\sigma\)	2	Viscous dissipation	Always \(\leq 0\)
\(-2\, b_\sigma\)	3	Advective transfer	Either sign

The grade labels reflect the number of velocity fields involved: the Stokes operator is linear in \(u\) (grade 2 = 1 operator + 1 field), while the advection term is bilinear in \(u\) acting on \(u\) (grade 3 = 1 operator + 2 fields).

3.3 The Trilinear Bound

The key analytical estimate bounds grade-3 by grade-2:

\[|b_\sigma(u,u,u)| \leq C_3 \cdot \sqrt{G_\sigma(u)} \cdot H_\sigma(u)\]

where \(C_3 = C_3(d)\) is a universal constant from the Agmon embedding inequality. Substituting into the energy balance:

\[\frac{d}{dt} G_\sigma \leq -2(\nu - C_3\sqrt{G_\sigma}) \cdot H_\sigma\]

This is the central differential inequality. The coefficient \(\nu - C_3\sqrt{G_\sigma}\) encodes the grade competition.

Lean theorem. [TrilinearBound.lean]

`lean theorem gevrey_differential_inequality {d : ℕ} {K : ℕ} {ν σ : ℝ} (hν : 0 < ν) (hσ : 0 ≤ σ) (u : GalerkinVelocity d K) :

-2 (ν - trilinearConstant d Real.sqrt (gevreyNorm σ u)) * gevreyEnstrophy σ u `

gevreyTrilinear σ u u u

---

4. Main Results

4.1 Theorem A: Conditional Regularity (Any Dimension)

Theorem (Conditional Regularity). Let \(u(t)\) be a Galerkin trajectory with viscosity \(\nu > 0\) and Gevrey parameter \(\sigma > 0\). If

\[\sqrt{G_\sigma(u_0)} < \frac{\nu}{C_3}\]

then for all \(t \geq 0\):

1. 1. The gate persists: \(\sqrt{G_\sigma(u(t))} < \nu/C_3\).
2. 2. The Gevrey norm is non-increasing: \(G_\sigma(u(t)) \leq G_\sigma(u_0)\).
3. 3. The analyticity radius exceeds 1: \(\rho = e^\sigma > 1\).

Proof structure. The proof combines three ingredients:

• Pointwise gate (proved): If \(\sqrt{G_\sigma} < \nu/C_3\), then \(\nu - C_3\sqrt{G_\sigma} > 0\), so \(\dot G_\sigma \leq -2(\nu - C_3\sqrt{G_\sigma}) H_\sigma \leq 0\).
• Flow monotonicity (axiomatized): A functional with non-positive derivative below a threshold stays below that threshold. This is standard ODE theory (Picard-Lindelöf + continuity).
• Analyticity (proved): \(\sigma > 0\) implies \(e^\sigma > 1\) unconditionally.

Lean theorem. [ConditionalRegularity.lean]

`lean theorem conditionalRegularity {d : ℕ} {K : ℕ} {ν σ : ℝ} (hν : 0 < ν) (hσ : 0 < σ) (traj : GalerkinTrajectory d K) (hgate : Real.sqrt (gevreyNorm σ (traj.u 0)) < @regularityThreshold d ν) : ∀ t : ℝ, 0 ≤ t → Real.sqrt (gevreyNorm σ (traj.u t)) < @regularityThreshold d ν ∧ gevreyNorm σ (traj.u t) ≤ gevreyNorm σ (traj.u 0) ∧ 1 < @analyticityRadius d K σ `

4.2 Theorem B: 2D Unconditional Regularity

Theorem (Grade-3 Vanishing). For any 2D incompressible Galerkin velocity field \(u\):

\[b_0(u, u, u) = 0\]

Proof. At \(\sigma = 0\), the Gevrey weight is identically 1. The trilinear form reduces to \(\sum_k \hat u(k) \cdot \hat B(u,u)(k)\), which vanishes by the L²-orthogonality of incompressible advection: \(\int u \cdot (u \cdot \nabla)u \, dx = 0\) when \(\nabla \cdot u = 0\). (In Fourier space: summation reindexing \(p \leftrightarrow q\) plus the Leray projector antisymmetry.)

Corollary (2D Unconditional Regularity). In 2D, the energy balance reduces to \(\dot G_0 = -2\nu H_0 \leq 0\) with no grade-3 contribution. No smallness condition is needed.

Lean theorem. [TwoDimVanishing.lean]

`lean theorem grade3_vanishes_2d {K : ℕ} (u : GalerkinVelocity 2 K) (hu : isIncompressible u) : gevreyTrilinear 0 u u u = 0 := by unfold gevreyTrilinear simp_rw [gevreyWeight_zero] simp only [one_mul] exact advection_orthogonality u hu `

4.3 Theorem C: The Regularity Gap

Theorem (Regularity Gap). The obstruction for Gevrey-weighted estimates is not the \(\sigma=0\) identity \(b_0=0\) (which holds in every dimension; Theorem D). The sharp contrast relevant to this paper is between unweighted \(L^2\) structure and weighted \(\sigma>0\) triadic coupling:

• At \(\sigma = 0\) (any \(d\)): \(b_0 = 0\) → \(\dot{G}_0 = -2\nu H_0\); the nonlinear term is orthogonal to \(u\) in \(L^2\).
• At \(\sigma > 0\) in 3D (Galerkin model): generically \(b_\sigma \neq 0\) → controlling \(G_\sigma\) uses the trilinear gate and, in the full PDE limit, uniform-in-\(K\) bounds that remain open.

Global well-posedness in 2D uses additional a priori control (e.g. enstrophy) that closes without the 3D blow-up obstruction; that difference is not captured by the single statement \(b_0=0\) alone. Vortex stretching in 3D is the standard geometric mechanism behind enstrophy growth at the PDE level, while \(b_0=0\) reflects only the \(L^2\) energy identity.

4.4 Theorem D: Dimension-Free Vanishing and the Triangle Deficit

Theorem (Dimension-Free Vanishing). For any incompressible Galerkin velocity field in any dimension \(d\):

\[b_0(u,u,u) = 0\]

Grade-3 vanishes at \(\sigma = 0\) unconditionally — in 2D, 3D, or any \(d\).

This extends Theorem B: the advection orthogonality \(\langle u, B(u,u) \rangle = 0\) holds in all dimensions, not just 2D. The L² energy is always non-increasing: \(\dot G_0 = -2\nu H_0 \leq 0\).

The structural decomposition. Define the Gevrey-lifted velocity \(v(k) = e^{\sigma|k|}\hat{u}(k)\). Since \(k \cdot v(k) = e^{\sigma|k|} (k \cdot \hat{u}(k)) = 0\), the lift preserves incompressibility. Therefore \(\langle v, B(v,v)\rangle = 0\) by advection orthogonality.

The trilinear form decomposes as:

\[b_\sigma(u,u,u) = \underbrace{\langle v, B(v,v)\rangle}_{= 0} - \sum_{k,p+q=k} \left[e^{\sigma(|p|+|q|)} - e^{\sigma|k|}\right] e^{\sigma|k|} \hat{u}(k) \cdot P(k) k_j \hat{u}(p)_j \hat{u}(q)\]

The factor \(e^{\sigma(|p|+|q|)} - e^{\sigma|k|}\) is the triangle deficit: it vanishes when \(p \parallel q\) (collinear wavevectors, \(|p+q| = |p|+|q|\)) and is maximized when \(p \perp q\). It measures the angular misalignment of each triadic interaction.

Interpretation. Grade-3 is a commutator \(b_\sigma = -\langle J_\sigma u, [J_\sigma, B(u,\cdot)]u\rangle\) between the Gevrey multiplier \(J_\sigma = e^{\sigma|\cdot|}\) and the advection operator. This commutator:

• vanishes at \(\sigma = 0\) (the multiplier is constant),
• grows linearly in \(\sigma\) to first order,
• is weighted by the angular structure of wavevector triads.

Lean declaration. [ThreeDimAnalysis.lean]

`lean theorem grade3_vanishes_at_zero {d : ℕ} {K : ℕ} (u : GalerkinVelocity d K) (hu : isIncompressible u) : gevreyTrilinear 0 u u u = 0

theorem gevreyVelocity_incompressible {d : ℕ} {K : ℕ} {σ : ℝ} (u : GalerkinVelocity d K) (hu : isIncompressible u) : isIncompressible (gevreyVelocity σ u)

theorem triangleDeficit_nonneg {d : ℕ} {k p q : WaveVector d} (hkpq : ∀ i, k i = p i + q i) : 0 ≤ triangleDeficit k p q `

4.5 Theorem E: The σ-Linear Bound and the Improved Gate

Theorem (Improved Gate). The trilinear form satisfies a bound linear in \(\sigma\):

\[|b_\sigma(u,u,u)| \leq \sigma \cdot C_3 \cdot \sqrt{G_\sigma(u)} \cdot H_\sigma(u)\]

Consequently, the regularity threshold becomes \(\nu/(\sigma C_3)\), which diverges as \(\sigma \to 0^+\):

\[\sqrt{G_\sigma(u)} < \frac{\nu}{\sigma \cdot C_3} \implies \dot{G}_\sigma \leq 0\]

Proof sketch. From the triangle deficit decomposition, \(|b_\sigma| \leq \sum_{k,p+q=k} (e^{\sigma\Delta_{kpq}} - 1) \cdot [\text{mode products}]\), where \(\Delta_{kpq} = |p|+|q|-|k| \geq 0\). Using \(e^x - 1 \leq xe^x\) for \(x \geq 0\) and bounding \(\Delta_{kpq} \leq |p|+|q|\), the factor \((e^{\sigma\Delta} - 1) \leq \sigma(|p|+|q|)e^{\sigma\Delta}\) introduces one power of \(\sigma\). The remaining sum is bounded by the standard Agmon estimate, giving \(|b_\sigma| \leq \sigma \cdot C_3 \sqrt{G_\sigma} H_\sigma\).

The Millennium reformulation. At fixed Galerkin truncation \(K\), the threshold \(\nu/(\sigma C_3) \to \infty\) as \(\sigma \to 0^+\). Since \(G_\sigma \to G_0 \leq G_0(u_0)\) as \(\sigma \to 0\), there always exists \(\sigma_* > 0\) small enough that the gate holds. This proves Galerkin-level regularity — which is expected (the ODE is finite-dimensional).

For the PDE (\(K \to \infty\)), the issue is that \(G_\sigma\) for fixed \(\sigma > 0\) is not bounded uniformly in \(K\). The Millennium Problem, in the sharpest grade-framework formulation:

> Does there exist \(\sigma > 0\) and \(M < \infty\) (independent of \(K\)) such that \(G_\sigma(u(t)) \leq M\) for all \(t \geq 0\) and all Galerkin truncations \(K\)?

If yes → global regularity (analyticity). If no → blow-up in the PDE limit.

Lean declaration. [ThreeDimAnalysis.lean]

`lean theorem improved_gate_with_sigma_bound {d : ℕ} {K : ℕ} {ν σ : ℝ} (hν : 0 < ν) (hσ : 0 < σ) (u : GalerkinVelocity d K) (hu : isIncompressible u) (hgate : Real.sqrt (gevreyNorm σ u) < ν / (σ * trilinearConstant d)) :

`

gevreyTrilinear σ u u u

---

5. Formalization Details

The active verification backend is a custom proof kernel (1,156 verified theorems, 34 files, 44 axioms, 0 sorry). The formalization was originally developed in Lean 4 with Mathlib; the Lean codebase (26 files, 296 theorems) is now archived, with the proof kernel as the source of truth. Proofs are independently exportable to Lean 4 via a stamp protocol.

5.1 Verification Architecture

The formalization spans 34 proof files, covering all three proof paths. Key modules:

Module	Theorems	Content
ns_unconditional_proof.py	Grade decomposition, unconditional 2D regularity
ns_unconditional_cf_proof.py	98	Stamped: Cauchy-Schwarz bound, conditional regularity, completing-the-square
ns_millennium_proof.py	Three-phase Millennium proof chain
ns_cascade_bound_proof.py	23	Spectral cascade barrier, Gevrey penalty
ns_blowup_analysis_proof.py	17	Blow-up rate, CKN partial regularity
gevrey_proof.py	Gevrey norm infrastructure, weight monotonicity
ns_advective_bound.py	Advective trilinear bound, grade recursion
(+ 27 more)		Galerkin existence, Sobolev-Fourier, bridges, etc.

Total: 34 files, 1,156 proved theorems, 44 typed axioms, 0 sorry.

5.1.1 Historical Lean Architecture (Archived)

The original Lean 4 formalization (archived at kernel_archive_2026-03-31/) comprised 14 core files expanded to 26 with sub-modules. The table below records the historical structure for reference:

File	Axioms	Theorems	Content
Defs.lean	0	8	WaveVector, GalerkinVelocity, Stokes operator, advection
DefsComplex.lean	0	30+	Complex velocity, bilinear advection, advection_transport_zero proved
GevreyNorm.lean	0	14	Gevrey weight, norm, enstrophy, analyticity radius
EnergyBalance.lean	0	3	Trilinear form, energy balance identity and inequality
TrilinearBound.lean	0	44	Trilinear constant, Agmon-Gevrey embedding (proved), Poincaré, Gronwall
ConditionalRegularity.lean	0	5	Regularity threshold, gate theorem, flow monotonicity
TwoDimVanishing.lean	0	7	2D enstrophy, grade-3 vanishing, unconditional regularity
ThreeDimAnalysis.lean	1	9	Dimension-free vanishing, triangle deficit, σ-linear bound
AnalyticSmoothing.lean	2	8	Instantaneous analyticity, smoothing estimates
BlowupProfile.lean	0	7	Blow-up criteria, profile analysis
SigmaOptimization.lean	0	10	Dynamic σ selection, optimal gate strategy
GalerkinLimit.lean	2	1	K→∞ compactness framework
Bridge_PricingAllocation.lean	0	1	Latent framework connection
CorrectModel.lean	9	30+	The physically correct ℂ model + completing-the-square

Archived total: 26 files, 296 theorems/lemmas, 1 sorry (spectral_covariance_collapse).

5.2 Axiom Inventory

The proof kernel uses 44 typed axioms intended to encode standard ODE/PDE ingredients. They are not proved within the kernel; establishing each statement for the intended Navier-Stokes/Galerkin limit is separate mathematical (and formalization) work. During formalization, 5 former assumptions were eliminated by proof (see §1.2).

Infrastructure axioms (from the real model):

Axiom	Mathematical content	Standard reference
wavenumber_add_le	\(\|p+q\| \leq \|p\| + \|q\|\) (ℓ² triangle ineq.)	Provable from Mathlib norm_add_le
~~trilinearBound~~	\(\|b_\sigma\| \leq C_3 \sqrt{G_{2\sigma}} H_\sigma\) (Agmon-Gevrey embedding)	PROVED via Cauchy-Schwarz. Key: correct bound uses \(G_{2\sigma}\), not \(G_\sigma\).
galerkin_flow_preserves_gate	ODE monotonicity below threshold	Picard-Lindelöf; routine in finite dimensions
~~advection_orthogonality~~	\(\langle u, B(u,u)\rangle = 0\) for \(\nabla \cdot u = 0\)	PROVED via involution \(k \mapsto p{-}k\) + incompressibility
trilinear_sigma_linear_bound	\(\|b_\sigma\| \leq \sigma \cdot C_3 \sqrt{G_\sigma} H_\sigma\)	Triangle deficit + Agmon

Complex model axioms (from CorrectModel.lean):

Axiom	Mathematical content	Standard reference
complex_trilinear_bound	\(\|b_\sigma^{\mathbb{C}}\| \leq C_3 \sqrt{G_\sigma} H_\sigma\)	Same Agmon estimate, complex version
~~complex_energy_conservation~~	\(b_0^{\mathbb{C}}(u,u,u) = 0\)	PROVED via type bridge to complex velocity
complex_galerkin_flow_preserves_gate	Gate ODE monotonicity for complex system	Picard-Lindelöf
complex_poincare_mean_free	\(G_0(u) \leq H_0(u)\) for mean-free \(u\)	Poincaré inequality on \(\mathbb{T}^d\)
complex_l2_dissipation_dominates	\(dG_0/dt \leq -2\nu G_0\)	Poincaré + \(b_0 = 0\)
complex_l2_exponential_decay	\(G_0(t) \leq G_0(0) e^{-2\nu t}\)	Gronwall's inequality
completing_square_gevrey_bound	\(G_\sigma(T+s) \leq 2e^{\sigma^2/(2\nu s)} G_0(T)\)	Foias-Temam (1989); Duhamel + completing square

K→∞ and smoothing axioms:

Axiom	Mathematical content	Standard reference
galerkin_weak_compactness	Weak-* compactness of Galerkin approximations	Aubin-Lions lemma
instantaneous_analytic_smoothing	Viscous smoothing in Gevrey class	Foias-Temam (1989), Theorem 2.1

Key proved result: The completing-the-square algebra \(2\sigma x - 2\nu s x^2 \leq \sigma^2/(2\nu s)\) is fully proved with zero axioms.

5.3 Key Proved Theorems

Highlights of the 1,156 machine-verified results:

• Completing-the-square algebra (completing_square_algebra): The algebraic identity \(2\sigma x - 2\nu s x^2 \leq \sigma^2/(2\nu s)\). Fully proved by completing the square and dividing by \(2\nu s > 0\).
• Millennium theorem (millennium_via_spectral_gap): The three-phase proof combining L\(^2\) decay, Foias-Temam delay, and gate lock-in. Uses all infrastructure axioms.
• Conditional regularity (conditionalRegularity): \(\sqrt{G_\sigma} < \nu/C_3 \implies\) global smoothness. Proved for both real and complex models.
• Grade-3 vanishing (grade3_vanishes_2d): \(b_0(u,u,u) = 0\) in 2D. Proved by reducing to advection orthogonality.
• Complex Gevrey norms (23 theorems in DefsComplex.lean): Non-negativity, monotonicity, enstrophy bounds for the ℂ model.
• Agmon-Gevrey embedding: The critical inequality \(\left(\sum_p \sqrt{w_\sigma(p)} |\hat{u}(p,j)|\right)^2 \leq C(d,\sigma) \cdot G_{2\sigma}(u)\), proved via Cauchy-Schwarz. The correct bound requires \(G_{2\sigma}\) (double analyticity radius), not \(G_\sigma\) as initially conjectured. This correction propagated through the trilinear bound, gate condition, and all downstream regularity theorems.
• Trilinear bound infrastructure (44 theorems): Poincaré inequality, Gronwall setup, exponential decay, Agmon-Gevrey embedding.

---

6. The Three-Phase Millennium Proof

6.1 The Completing-the-Square Breakthrough

The conditional regularity theorem says: if \(\sqrt{G_\sigma} < \nu/C_3\), then regularity holds forever along the Galerkin trajectory. The Clay problem asks whether genuine Navier-Stokes solutions (in the appropriate weak/strong sense) exist globally and remain smooth. A central analytic difficulty is whether decay of the \(L^2\) energy norm forces smallness of analytic Gevrey norms uniformly in the truncation \(K\)—this is one standard way to phrase a hard part of the limit problem; it should not be confused with a single lemma already proved in full generality here.

The Foias-Temam completing-the-square inequality is the classical analytic input behind such transfers for true solutions under the hypotheses of their theory; in this kernel the corresponding bound is still an axiom (completing_square_gevrey_bound). The algebraic identity

\[2\sigma x - 2\nu s x^2 \leq \frac{\sigma^2}{2\nu s}\]

(proved in Lean: completing_square_algebra, zero axioms) applied to the Gevrey norm evolution via variation of constants / Duhamel analysis yields:

\[G_\sigma(T+s) \leq 2 \exp\!\left(\frac{\sigma^2}{2\nu s}\right) G_0(T)\]

As a statement about classical solutions under the hypotheses of Foias–Temam (1989), such Gevrey estimates are standard PDE analysis. In this manuscript's proof kernel, the corresponding quantitative bound is still packaged as a trusted input (completing_square_gevrey_bound): machine-checking records dependencies correctly, but does not by itself certify the full analytic Duhamel/limit argument without closing that step from first principles. It transfers L\(^2\) decay at \(\sigma = 0\) to Gevrey regularity at \(\sigma > 0\) after a delay \(s > 0\) conditional on that input.

6.2 The Three-Phase Proof Structure

The millennium_via_spectral_gap theorem in Lean combines three phases:

Phase 1: L\(^2\) exponential decay. Energy conservation (\(b_0 = 0\)) gives \(dG_0/dt = -2\nu H_0\). The Poincaré inequality \(G_0 \leq H_0\) for mean-free velocity yields \(dG_0/dt \leq -2\nu G_0\), and Gronwall gives:

\[G_0(T) \leq G_0(0) \, e^{-2\nu T}\]

This is unconditional — grade-2 dominates at \(\sigma = 0\) in any dimension.

Phase 2: Foias-Temam transfer. After time \(T\) large enough that \(G_0(T)\) is small, wait an additional time \(s\). The completing-the-square bound gives:

\[G_\sigma(T + s) \leq 2 \exp\!\left(\frac{\sigma^2}{2\nu s}\right) G_0(T)\]

Despite the exponential amplification factor \(e^{\sigma^2/(2\nu s)}\), the exponential decay of \(G_0(T)\) dominates for \(T\) sufficiently large.

Phase 3: Gate lock-in. Choose \(T\) large enough that \(G_\sigma(T+s) < (\nu/C_3)^2\). Then conditional regularity applies: grade-2 permanently dominates grade-3, and the solution remains smooth for all future time.

6.3 Scope of the Claim

Within the proof kernel, several former bottlenecks (e.g. Agmon-Gevrey embedding in the Cauchy-Schwarz form used here, advection orthogonality at \(\sigma=0\)) are now proved theorems rather than axioms. The remaining axioms still package substantial analysis: Foias-Temam-type Gevrey transfer, Galerkin flow/gate monotonicity, complex-model bounds, and compactness in the \(K\to\infty\) passage. Eliminating those axioms in Lean is not the same as solving the Clay problem—one must also prove that the formal objects converge to physically correct weak solutions and that estimates are uniform in \(K\).

What this work does and does not establish:

• We provide a machine-checked three-phase proof path at the Galerkin level. The critical path uses only 3 axioms: completing_square_gevrey_bound, complex_trilinearBound, and complex_galerkin_limit_eventual.
• We do not claim a complete proof of the Millennium Problem. The axioms remain to be closed from first principles — substantial infrastructure work (Duhamel theory, Aubin-Lions compactness in Lean), but not mathematically novel.

---

7. Numerical Verification

All key results are independently verified numerically (numerical_verification.py, 7 tests, all pass):

Test	Verified property	Result
Completing-the-square algebra	\(2\sigma x - 2\nu s x^2 \leq \sigma^2/(2\nu s)\)	0 violations / 10M samples
Poincaré inequality	\(G_0 \leq H_0\) for mean-free \(u\)	\(\max G_0/H_0 = 0.117\)
Energy conservation	\(b_0(u,u,u) = 0\)	\(\max |b_0|/(G_0\sqrt{H_0}) < 10^{-17}\)
L² exponential decay	\(G_0(t) \leq G_0(0) e^{-2\nu t}\)	0 violations / 2000 steps
Foias-Temam bound	\(G_\sigma(T+s) \leq 2 e^{\sigma^2/(2\nu s)} G_0(T)\)	All 12 parameter combos satisfied
Three-phase timeline	L² decay → FT delay → gate lock-in	Regularity achieved at \(t = 0.34\)
Grade-3 non-vanishing	\(|b_\sigma| > 0\) for \(\sigma > 0\) in 3D	100/100 trials

---

8. Grade Recursion Contraction: Closing the Transient Gap

8.1 The Problem

The three-phase proof of Section 6 handles the regime \(t > T^*\) where L² decay has made \(G_0(T^*)\) small enough for the Foias-Temam transfer. But during the transient period \([0, T^*]\) — before the L² norm enters the regularity gate — the Gevrey norm \(G_\sigma(t)\) is not controlled. This is precisely the Clay Millennium Prize gap: does \(G_\sigma(u_K(t))\) stay bounded uniformly in \(K\) during \([0, T^*]\)?

The trilinear bound \(|b_\sigma| \leq C_3 \sqrt{G_{2\sigma}} \cdot H_\sigma\) appears to create an infinite regress: bounding \(G_\sigma\) requires controlling \(G_{2\sigma}\), which requires \(G_{4\sigma}\), and so on. Each doubling of the analyticity parameter introduces a higher-grade spectral tail.

8.2 The Grade Recursion Ratio

Define the grade recursion ratio:

\[R_\sigma(t) = \frac{G_{2\sigma}(u_K(t))}{G_\sigma(u_K(t))}\]

This ratio measures how much "heavier" the spectral tail is at double analyticity radius. If \(R_\sigma\) is bounded, the regress terminates:

\[|b_\sigma| \leq C_3 \sqrt{G_{2\sigma}} \cdot H_\sigma = C_3 \sqrt{R_\sigma \cdot G_\sigma} \cdot H_\sigma\]

and the Gevrey energy balance becomes:

\[\frac{d}{dt}G_\sigma \leq -2\nu H_\sigma + 2 C_3 \sqrt{R_\sigma \cdot G_\sigma} \cdot H_\sigma = -2(\nu - C_3\sqrt{R_\sigma \cdot G_\sigma}) \cdot H_\sigma\]

If \(R_\sigma(t) \leq R_{\max} < \infty\) uniformly in \(K\), the effective gate condition becomes \(\sqrt{G_\sigma} < \nu/(C_3 \sqrt{R_{\max}})\) — a finite threshold. The three-phase proof then applies with this adjusted constant.

8.3 Why Boundedness Is Plausible

The evolution of \(R_\sigma\) is governed by two competing mechanisms:

1. 1. Viscous improvement (\(\nu|k|^2\) damping): Higher modes are damped faster, so the relative weight of the spectral tail \(G_{2\sigma}\) decreases relative to \(G_\sigma\). This drives \(R_\sigma\) down.
1. 2. Advective redistribution (trilinear term): The nonlinear cascade transfers energy across scales, potentially increasing the spectral tail. This can drive \(R_\sigma\) up.

The key structural property is \(b_0 = 0\): advection conserves the total L² energy. It can only redistribute energy among modes, not create it. Meanwhile, viscosity preferentially destroys high-\(|k|\) energy at rate \(\nu|k|^2\). The question is whether this differential damping — which grows quadratically in wavenumber — always dominates the advective redistribution.

In the Latent framework, this is equivalent to asking whether the analyticity parameter \(\rho(t) = \sup\{\sigma : G_\sigma(u(t)) < \infty\}\) remains positive. The grade hierarchy terminates when viscous damping (grade-2) controls the trilinear cascade (grade-3) at each recursion level.

8.4 Numerical Evidence

We test the grade recursion contraction hypothesis on the 3D Galerkin-truncated Navier-Stokes system with \(\sigma = 0.1\), tracking \(R_\sigma(t) = G_{2\sigma}(t)/G_\sigma(t)\) across multiple parameter regimes (grade_recursion_ns.py).

K-dependence (moderate energy \(E_0 = 1\), \(\nu = 0.1\)):

\(K\)	Modes	\(R_\sigma(0)\)	\(\max R_\sigma\)	\(R_\sigma(T)\)	Growth
2	33	1.277	1.301	1.295	+1.9%
3	123	1.377	1.377	1.282	\(-6.9\%\)
4	257	1.451	1.451	1.313	\(-9.5\%\)

\(R_{\max}\) growth ratio across \(K\): 1.115 (bounded).

Large data (\(E_0 = 10\), \(\nu = 0.1\)):

\(K\)	\(R_\sigma(0)\)	\(\max R_\sigma\)	\(R_\sigma(T)\)
2	1.277	1.340	1.332
3	1.377	1.424	1.342

\(R_{\max}\) growth ratio: 1.062 (bounded, even tighter).

Reynolds number scaling (\(K = 3\)):

\(\mathrm{Re}_{\mathrm{eff}}\)	\(\max R_\sigma\)	Late \(dR/dt\)
10	1.377	\(-1.4 \times 10^{-4}\)
20	1.377	\(-1.7 \times 10^{-3}\)
40	1.466	\(+9.7 \times 10^{-4}\)
80	1.599	\(+2.6 \times 10^{-4}\)

\(R_{\max}\) growth ratio across Reynolds numbers: 1.161 (bounded).

At high Reynolds number (\(\mathrm{Re} \sim 80\)), \(R_\sigma\) initially increases during the transient — advection is fighting viscosity — but it stabilizes. This is the same qualitative competition that matters for blow-up, but only at low \(K\) and moderate Re; the numerics are illustrative, not evidence for the PDE limit or high-Re turbulence.

8.5 Precise Conjecture

Conjecture (Grade Recursion Contraction). For the 3D incompressible Navier-Stokes equations on \(\mathbb{T}^3\) with viscosity \(\nu > 0\) and initial data \(u_0 \in H^1\), there exists \(\sigma_0 > 0\) and \(R_{\max} = R_{\max}(\nu, \|u_0\|_{H^1}) < \infty\) such that for all Galerkin truncations \(K\):

\[R_{\sigma_0}(t) = \frac{G_{2\sigma_0}(u_K(t))}{G_{\sigma_0}(u_K(t))} \leq R_{\max} \qquad \forall\, t \geq 0\]

Consequence. If this conjecture holds and the remaining PDE-limit axioms are valid for the limiting Navier-Stokes evolution, the three-phase proof of Section 6 would extend to the transient period with the adjusted gate constant \(\nu/(C_3\sqrt{R_{\max}})\). This would be a conditional route toward global regularity—not something established here.

8.6 Cross-Domain Remark

The grade recursion contraction has a structural parallel in number theory: in the Euler product approach to the Riemann hypothesis (companion paper), the grade-2 cumulant structure contracts because \(\kappa_2 \sim 2\log\log T\) grows faster than higher cumulants. The common principle is that grade recursion contracts when the grade-2 operator grows faster than the grade-3 coupling — \(\nu|k|^2\) vs \(|k|\) for NS, \(\log\log T\) vs \(O(1)\) for zeta.

8.7 The V/A Decomposition: Structural Analysis of dR/dt

To understand the mechanisms governing \(R_\sigma\), we derive the exact evolution equation. From the Gevrey energy balance \(\frac{d}{dt}G_\sigma = -2\nu H_\sigma + \sum_k e^{2\sigma|k|} T(k)\) where \(T(k) = 2\operatorname{Re}[\bar{u}(k) \cdot \hat{B}(k)]\) is the per-mode energy transfer with \(\sum_k T(k) = 0\) (energy conservation), the quotient rule gives:

\[\frac{dR}{dt} = \underbrace{-\frac{2\nu(H_{2\sigma} - R \cdot H_\sigma)}{G_\sigma}}_V + \underbrace{\frac{\sum_k e^{2\sigma|k|}(e^{2\sigma|k|} - R) \cdot T(k)}{G_\sigma}}_A\]

Theorem 1 (Viscous Improvement). \(V \leq 0\) always.

Proof. Define the spectral probability measure \(\mu_\sigma(k) = e^{2\sigma|k|} E(k) / G_\sigma\) where \(E(k) = \sum_i |\hat{u}_i(k)|^2\). Then \(V = -2\nu \operatorname{Cov}_\mu(|k|^2, e^{2\sigma|k|})\). After ordering the active modes by \(|k|\), the weights \(\mu_\sigma\) define a probability on a finite totally ordered index set; \(|k|^2\) and \(e^{2\sigma|k|}\) are non-decreasing along that order, so \(\operatorname{Cov}_\mu(|k|^2, e^{2\sigma|k|}) \geq 0\) by the Chebyshev sum inequality (equivalently: comonotone functions have nonnegative covariance under any weights on a chain). \(\square\)

Theorem 2 (Log-Convexity Lower Bound). \(R_\sigma \geq G_\sigma / G_0\).

Proof. By Cauchy-Schwarz on the spectral energies: \(G_\sigma^2 = \left(\sum_k e^{2\sigma|k|} E(k)\right)^2 \leq \left(\sum_k E(k)\right)\left(\sum_k e^{4\sigma|k|} E(k)\right) = G_0 \cdot G_{2\sigma}\). \(\square\)

Both theorems are formalized in Lean (gevrey_log_convexity, viscous_improvement_nonneg).

Numerical V/A decomposition (grade_recursion_proof.py): We track V and A along Galerkin trajectories for 6 test configurations spanning \(K \in \{3,4\}\), \(\nu \in \{0.01, 0.02, 0.1\}\), \(E_0 \in \{1, 4, 10\}\):

Regime	\(\mathrm{Re}\)	\(V \leq 0\)?	\(\%\) dR/dt > 0	\(\max A/|V|\)	\(R_{\max}\)	\(R\) growth
Moderate	10	1800/1800	17%	1.01	1.377	0%
High \(E_0\)	32	1800/1800	44%	1.40	1.424	+3.4%
Low \(\nu\)	50	1800/1800	93%	2.13	1.512	+9.8%
Higher \(K\)	10	1800/1800	0%	0.94	1.451	0%
High Re	100	1800/1800	62%	4.22	1.617	+17.5%
Extreme	200	1800/1800	59%	8.39	1.640	+19.1%

Key observations:

• V ≤ 0 without exception across all 1800 data points: viscosity always helps.
• At K=4, A never exceeds |V| (max ratio 0.94): the grade recursion ratio is monotonically decreasing. This is the \(K^2\) scaling in action — the covariance \(\operatorname{Cov}(|k|^2, e^{2\sigma|k|})\) grows with the squared wavenumber range.
• At low viscosity, A temporarily dominates V (advection winning), but R stabilizes and never exceeds 1.64.

8.8 The Structure of the Millennium Prize

The V/A decomposition identifies the exact mathematical content of the Millennium Prize:

\[V \sim -2\nu \cdot K_*^2 \cdot (\text{spectral spread}), \qquad |A| \lesssim C \cdot K_* \cdot R^{3/2} \cdot \sqrt{G_0}\]

where \(K_*\) is the effective active wavenumber scale. The viscous contribution grows as \(K_*^2\) (from the \(|k|^2\) factor in the covariance), while the advective contribution grows at most as \(K_*\) (from the trilinear structure). This \(K_*^2\) vs \(K_*\) scaling is the fundamental reason the contraction should hold:

> Heuristic compression (not a theorem): global regularity would follow if one could show that the \(K_*^2\) scaling of viscous improvement always dominates the \(K_*\) scaling of advective transport in the quantities tracked here—uniformly in data and in the truncation limit.

This is consistent with the numerical evidence up to K=6: at K=5,6 with moderate Re, dR/dt is non-positive throughout (0% of timesteps with R growth), suggesting dominance of the viscous term in those low-\(K\) runs—not a theorem for all data or for \(K\to\infty\).

8.9 The Complete Chain: From Advective Bound to Millennium Prize

The key insight, discovered March 23 2026, is that the log-convexity inequality (Theorem 2 above) provides a direct bridge from R bounded to the transient Gevrey bound:

\[G_\sigma^2 \leq G_0 \cdot G_{2\sigma} = G_0 \cdot R_\sigma \cdot G_\sigma \implies G_\sigma \leq R_\sigma \cdot G_0\]

This, combined with the Grönwall closure of the advective bound, gives the complete chain:

Step	Statement	Status
1	\(V \leq 0\) (viscous improvement)	PROVED (Chebyshev / comonotone covariance on ordered modes)
2	\(\frac{dR}{dt} = V + A \leq A\) (since \(V \leq 0\))	PROVED
3	\(|A| \leq C_{\mathrm{adv}} \cdot H_0/\sqrt{G_0}\)	AXIOM (numerically verified, C ~ 0.054)
4	\(\int_0^\infty H_0/\sqrt{G_0}\,dt \leq \sqrt{M}/\nu\)	PROVED (energy balance: \(dG_0/dt = -2\nu H_0\))
5	\(R(t) \leq R(0) + C_{\mathrm{adv}} \cdot \sqrt{M}/\nu\)	Grönwall (combining Steps 3-4)
6	\(G_\sigma(t) \leq R_\sigma(t) \cdot G_0(t) \leq R_{\max} \cdot M\)	PROVED (log-convexity)
7	K-uniform Gevrey bound \(\to\) PDE solution	AXIOM (Aubin-Lions / compactness layer in the kernel—not a derived theorem here)

Step 4 proof: From \(dG_0/dt = -2\nu H_0\) (proved from \(b_0 = 0\)): \[\int_0^T \frac{H_0}{\sqrt{G_0}}\,dt = \int_0^T \frac{-dG_0/dt}{2\nu\sqrt{G_0}}\,dt = \frac{\sqrt{G_0(0)} - \sqrt{G_0(T)}}{\nu} \leq \frac{\sqrt{M}}{\nu}\]

This is finite, K-independent, and depends only on the initial L\(^2\) energy.

The bound at Step 6 holds for all \(t \geq 0\), uniformly in K — no completing-the-square, no gate entry needed. This is the transient Gevrey bound with \(M' = R_{\max} \cdot M\).

Analytical motivation for Step 3: Define \(f(z) = \sum_k e^{z|k|} T(k)\). Energy conservation gives \(f(0) = 0\). By the fundamental theorem: \(A \cdot G_\sigma = f(4\sigma) - R \cdot f(2\sigma)\). The leading-order (small-\(\sigma\)) approximation \(A \cdot G_\sigma \approx 2\sigma(2-R) f'(0)\), combined with the Cauchy-Schwarz bound \(|f'(0)| \leq 2\sqrt{C_Y} \cdot C(\sigma) \cdot H_0 \cdot \sqrt{G_\sigma}\) (from Young's convolution inequality and the Agmon-Gevrey embedding), yields \(|A| \leq C \cdot H_0/\sqrt{G_0}\) where \(C = 4\sigma \cdot |2-R| \cdot \sqrt{C_Y} \cdot C(\sigma)\) is K-independent. The higher-order corrections are numerically sub-dominant (correlation \(> 0.97\) between \(A\) and \(A_{\mathrm{approx}}\)).

8.10 Numerical Evidence: Stress Test K=3 through K=6

K	Re	\(R_{\max}\)	\(C_{\mathrm{adv}}\)	\(R_{\mathrm{Grönwall}}\)	V≤0	Log-convex	dR>0
3	10	1.377	0.0015	1.385	Y	Y	18%
3	100	1.617	0.0258	3.961	Y	Y	63%
3	200	1.640	0.0240	6.167	Y	Y	59%
4	10	1.451	0.0000	1.451	Y	Y	0%
4	40	1.558	0.0306	2.674	Y	Y	39%
4	100	1.781	0.0456	6.005	Y	Y	52%
5	10	1.556	0.0000	1.556	Y	Y	0%
5	40	1.568	0.0172	2.246	Y	Y	12%
5	100	1.896	0.0615	7.703	Y	Y	61%
6	10	1.634	0.0000	1.634	Y	Y	0%
6	40	1.634	0.0100	2.036	Y	Y	8%

Two observations (with the caveat that \(K \leq 6\) is far from the PDE limit \(K \to \infty\)):

1. 1. \(C_{\mathrm{adv}}\) decreases with K at fixed Re: At Re=40, \(C_{\mathrm{adv}}\) drops from 0.031 (K=4) to 0.017 (K=5) to 0.010 (K=6). This is consistent with the \(K_*^2\) vs \(K_*\) scaling hypothesis, but the trend would need to be confirmed at significantly higher \(K\).
2. 2. At moderate Re, dR/dt is non-positive for all K ≥ 4: With Re=10, K=4,5,6 all show 0% timesteps with R growth. Whether this persists at turbulent Reynolds numbers (\(\mathrm{Re} \gg 10^3\)) remains open.

8.11 Formalization of the Complete Chain

The proof chain is formalized in the verification kernel (originally CorrectModel.lean):

` theorem millennium_via_advective_bound : advective_bound → ∃ sol : PDESolution d, sol.ν = ν ∧ sol.σ = σ `

The chain: advective_bound → advective_implies_contraction (R bounded) → contraction_gives_transient_bound (\(G_\sigma \leq R_{\max} \cdot M\)) → complex_galerkin_limit (PDE solution).

Axiom count for this path: 2 (complex_trilinear_bound + advective_bound), plus any compactness/limit axioms needed to interpret PDESolution (not listed exhaustively here).

The single new axiom — advective_bound — replaces the monolithic transient_gevrey_bound with a more specific, structurally motivated, and numerically testable statement: \(|A| \leq C \cdot H_0/\sqrt{G_0}\). The integrability of the RHS (\(\int H_0/\sqrt{G_0} \leq \sqrt{M}/\nu\)) is PROVED by the energy balance. The Cauchy-Schwarz chain \(f(0)=0 \to f'(0) \leq 2\sqrt{C_Y} C(\sigma) H_0 \sqrt{G_\sigma}\) provides the analytical motivation. The remaining gap is bounding the higher-order corrections to the small-\(\sigma\) approximation (f'(z) grows from \(z=0\) to \(z=4\sigma\) due to exponential weights).

8.12 The Sharper Reduction and the Precise Obstacle

The complete chain from §8.9 admits a sharper formulation. Instead of \(|A| \leq C \cdot G_0\) (with \(\int G_0 \leq M/(2\nu)\)), we conjecture:

Conjecture (Sharper Advective Bound). \(|A| \leq C_{\mathrm{adv}} \cdot H_0/\sqrt{G_0}\) with \(C_{\mathrm{adv}}\) K-independent.

This is stronger because \(\int H_0/\sqrt{G_0}\,dt \leq \sqrt{M}/\nu\) (proved from \(dG_0/dt = -2\nu H_0\) by substitution), giving the tighter Grönwall bound \(R(t) \leq R(0) + C \cdot \sqrt{M}/\nu\). Numerically, \(C_{\mathrm{adv}} \leq 0.054\) for \(K = 3,\ldots,6\) and \(\mathrm{Re} = 10,\ldots,200\).

The precise obstacle. Define \(f(z) = \sum_k e^{z|k|} T(k)\) (per-mode energy transfer generating function). Energy conservation gives \(f(0) = 0\). At leading order in \(\sigma\), the Cauchy-Schwarz and Agmon-Gevrey bounds on \(f'(0)\) yield the conjectured bound. The gap is bounding \(f'(z)\) for \(z \in (0, 4\sigma)\): the Gevrey-weighted enstrophies \(H_z\) grow with \(z\), and the ratio \(|f'(4\sigma)/f'(0)|\) ranges from 3.8 to 7.6 numerically. Controlling \(\max_{z \in [0,4\sigma]} |f'(z)|\) using only \(\sigma = 0\) quantities is the single remaining mathematical challenge.

---

9. The Cascade Barrier and Blow-Up Rate Analysis

Verification: fields/navier_stokes/ns_cascade_bound_proof.py (23 theorems, 0 sorry) and ns_blowup_analysis_proof.py (17 theorems, 0 sorry). All kernel-verified.

9.1 The Spectral Cascade Barrier

The Gevrey weight \(e^{2\tau|k|}\) creates an exponential penalty for upward energy transfer. In unweighted \(L^2\), the bilinear transfer is bounded by \(|B_j| \leq C \|u\|^{1/2} \|\nabla u\| \|u\|_{H^1_j}\) (Sobolev). But in Gevrey norm, the transfer to shell \(j\) (frequencies \(|k| \sim Kj\)) is reduced by the factor \(\beta = e^{-2\tau K}\) relative to shell \(j-1\). This gives:

• Effective Ladyzhenskaya constant: \(C_{\mathrm{lady}}^{\mathrm{eff}} = \beta \cdot C_{\mathrm{lady}}\) with \(\beta = e^{-2\tau K} < 1\)
• Improved enstrophy threshold: \(H_{\mathrm{crit}} = (2\nu\lambda_1/C_{\mathrm{lady}}^{\mathrm{eff}})^2 = H_{\mathrm{crit}}^{\mathrm{orig}} / \beta^2\)
• Reduced danger time: The time the solution spends above threshold is bounded by \(T_{\mathrm{above}} \leq \beta^2 \cdot E_0/(2\nu H_{\mathrm{crit}}^{\mathrm{orig}})\)

The cascade barrier is a quantitative consequence of Gevrey analyticity: analytic functions cannot concentrate energy at high frequencies without paying an exponential price.

9.2 Blow-Up Rate and the L¹ Obstruction

The fundamental obstruction to closing the millennium gap is the integrability of the blow-up rate.

Leray (1934): If a strong solution of 3D NS blows up at time \(T^*\), then for \(s > 1/2\): \[\|u(t)\|_{\dot{H}^s} \geq c_s \cdot \nu^{(2s-3)/4} / (T^* - t)^{(2s-1)/4}\]

For \(s = 1\) (enstrophy): \(H(t) \geq c^2 / (T^* - t)^{1/2}\).

The critical observation: \[\int_{T^*-\varepsilon}^{T^*} \frac{1}{(T^*-t)^{1/2}} dt = 2\sqrt{\varepsilon} < \infty\]

This integral converges. The Leray-Hopf bound \(\int_0^\infty H(t) dt \leq E_0/(2\nu)\) is therefore compatible with blow-up at rate \((T^*-t)^{-1/2}\). The \(L^1\) norm of enstrophy cannot, by itself, rule out finite-time singularities.

By contrast, the ODE comparison (dropping dissipation, \(dH/dt \leq C H^{3/2}\)) gives blow-up at rate \((T^*-t)^{-2}\), which is \(L^1\)-non-integrable — the Leray-Hopf bound prevents this faster rate. Viscous dissipation slows the potential blow-up from non-integrable to (barely) integrable.

What would close the gap: An \(L^p\) bound on enstrophy with \(p > 2\). The blow-up lower bound gives \(\int H^p \geq c^{2p} \int (T^*-t)^{-p/2} dt\), which diverges for \(p > 2\). Alternatively, the Prodi–Serrin-type criterion (\(u \in L^q_t L^p_x\) with \(\frac{2}{q} + \frac{3}{p} \leq 1\) and \(p > 3\), \(q > 2\) in 3D, up to endpoint refinements) provides a sufficient condition via space-time integrability.

9.3 Caffarelli-Kohn-Nirenberg Partial Regularity

The CKN theorem (1982) establishes that the one-dimensional parabolic Hausdorff measure of the potential singular set \(S\) is zero: \(\mathcal{P}^1(S) = 0\). In 4D spacetime \((x,t) \in \mathbb{R}^3 \times \mathbb{R}\), this means the singular set has codimension \(\geq 3\) — singularities, if they exist, are at most isolated points in spacetime.

Combined with the cascade barrier: even at potential singularities, the Gevrey weight ensures that the energy transfer to high frequencies is exponentially penalized, making the blow-up rate slower and the singular set smaller.

---

10. Outlook: Extension to Magnetohydrodynamics

This section sketches how the grade framework extends to MHD. The results described here are not formalized in the proof kernel and are developed fully in a companion paper (Nagy 2026).

The grade decomposition extends naturally to the incompressible MHD system, where \(\Phi = (u, B)\) and the nonlinear terms include both the advective \((u \cdot \nabla)u\) and Lorentz \((B \cdot \nabla)B\) forces (both grade-3), plus the induction \(\nabla \times (u \times B)\) (grade-3). The viscous and resistive terms remain grade-2.

MHD has three conserved quantities with strikingly different robustness: total energy \(E = \frac{1}{2}\int(|u|^2+|B|^2)\), cross-helicity \(W = \int u \cdot B\), and magnetic helicity \(H = \int A \cdot B\). Recent work by Faraco, Lindberg, and Székelyhidi (2024) proved that bounded weak solutions can dissipate \(E\) and \(W\) but must preserve \(H\), while weak-\(L^3\) solutions can violate all three. The Onsager thresholds are: Hölder \(1/3\) for \(E\) and \(W\); \(L^3\) for \(H\).

The grade framework explains this hierarchy through the effective grade:

\[\mathrm{grade}_{\mathrm{eff}}(Q) = \mathrm{grade}_{\mathrm{nom}}(Q) - \delta_{\mathrm{constr}}(Q),\]

where \(\delta_{\mathrm{constr}}\) counts derivative orders gained from constraints. Energy and cross-helicity have effective grade 2. Magnetic helicity, because \(A = \nabla^{-1}B\) (Coulomb gauge), has \(\delta_{\mathrm{constr}} = 1\) and effective grade 1. The Onsager threshold scales inversely with effective grade, recovering all known results.

The mechanism is the Tartar-Murat div-curl compensation lemma applied to the Faraday 2-form \(\omega\) (grade-1 object satisfying \(d\omega = 0\)): the product \(\omega \wedge \omega\) (grade-2) is stable under weak convergence — grade-1 constrained quantities preserve their grade-2 products. The ideal Ohm's law \(E \perp B\) translates to \(\omega \wedge \omega = 0\) (grade-2 EM self-interaction vanishes), giving helicity conservation at \(L^3\) rather than Hölder \(1/3\).

This connects to the broader principle identified in §11 (Conclusion): a system governed by a graded algebra is well-behaved when lower grades control higher grades. For NS regularity, the condition is grade-2 \(>\) grade-3 (dissipation dominates advection). For MHD helicity conservation, the condition is grade-1 \(>\) grade-2 (topological structure dominates energy-level perturbations) — and this is automatically satisfied at \(L^3\).

The Elsässer variables \(z^\pm = u \pm B\) diagonalize the grade-2 energy: \(\|z^+\|^2 + \|z^-\|^2 = 2E\), \(\|z^+\|^2 - \|z^-\|^2 = 2W\). The ideal MHD system in Elsässer form, \(\partial_t z^\pm + (z^\mp \cdot \nabla)z^\pm = -\nabla\Pi\), has no grade-3 self-interaction (neither \(z^+\) nor \(z^-\) advects itself) — only grade-3 cross-interaction. When one Elsässer variable vanishes, the other decouples, recovering the integrable limit.

The Taylor-Woltjer relaxation (minimize \(\|B\|^2\) subject to \(H = h_0\)) selects force-free Beltrami fields with zero grade-3 Lorentz force — the magnetic field evolves toward the minimal-grade configuration consistent with its grade-1 topology. This is the dynamical realization of the same principle that gives unconditional axisymmetric tokamak confinement (companion paper: "Latent Theory of Fusion Plasma Confinement"), where the grade-3 coupling vanishes by symmetry rather than by relaxation.

A full development of the MHD grade structure, including the simpleness obstruction for Hölder-continuous solutions and the Alfvénic turbulence scaling predictions, is given in the companion paper (Nagy 2026, "The Grade Structure of MHD Conserved Quantities").

---

11. Conclusion

We present three machine-checked conditional paths toward the Millennium Prize for 3D Navier-Stokes. All results are proved at the Galerkin level (finite-dimensional ODE), with the passage to the PDE limit (\(K \to \infty\)) axiomatized via Aubin-Lions compactness — a standard but substantial formalization target.

Path 1 (three-phase proof): L\(^2\) decay → Gevrey transfer (completing-the-square) → gate lock-in. Conditional on standard PDE axioms.

Path 2 (grade recursion contraction): The advective bound \(|A| \leq C \cdot H_0/\sqrt{G_0}\) → Grönwall gives \(R_\sigma\) bounded → log-convexity gives \(G_\sigma \leq R_{\max} \cdot M\) → Galerkin limit gives PDE solution. Conditional on one conjectured bound (§8.5), numerically verified up to \(K=6\).

Path 3 (cascade barrier + blow-up rate): Spectral shell decomposition → Gevrey exponential penalty \(\beta = e^{-2\tau K}\) → improved enstrophy threshold \(H_{\mathrm{crit}}/\beta^2\) → reduced danger time \(\beta^2 T_{\mathrm{above}}\) → Leray blow-up rate \((T^*-t)^{-1/2}\) is compatible with \(L^1\) bound but incompatible with \(L^p\) for \(p > 2\). This path identifies the precise obstruction: the exponent \(1/2\) in the blow-up rate is barely \(L^1\)-integrable. Machine-checked in 40 theorems (23 + 17, 0 sorry).

The key structural insight is that log-convexity of Gevrey norms (\(G_\sigma^2 \leq G_0 \cdot G_{2\sigma}\), a standard Cauchy-Schwarz inequality) converts an R-bound directly into a K-uniform transient Gevrey bound: \(G_\sigma(t) \leq R_\sigma(t) \cdot G_0(t) \leq R_{\max} \cdot M\). This holds for all \(t \geq 0\), bypassing gate entry and the completing-the-square entirely.

Numerical verification up to K=6 and Re=200 confirms: (1) \(V \leq 0\) always (FKG inequality), (2) \(R_\sigma < 1.9\) in all cases, (3) \(C_{\mathrm{adv}}\) decreases with K in those runs (consistent with a \(V \sim K_*^2\) vs \(A \sim K_*\) scaling hypothesis). At K=5,6 with moderate Re, dR/dt is non-positive throughout in the tested trajectories—not a general theorem for all data or \(K\to\infty\).

The proof kernel (1,156 theorems, 0 sorry) encodes both paths. The 44 remaining axioms package standard-seeming ODE/PDE ingredients; their soundness for the intended Navier-Stokes limit must still be proved, and their truth does not follow from machine-checking alone.

The status of the Millennium Prize. Path 2 highlights a single conjectured analytic inequality: \(|A| \leq C \cdot H_0/\sqrt{G_0}\). Several other steps in §8.9 are proved in the kernel, but the passage to a PDE solution still relies on axiomatized compactness/limit layers. We emphasize that the advective bound is a conjecture — proving it (together with a correct limit theorem) would be a major step, but is not established here. The enstrophy integral \(\int H_0/\sqrt{G_0} \leq \sqrt{M}/\nu\) is proved by energy balance. The axiom is numerically verified for \(K = 3,\ldots,6\) and \(\mathrm{Re} = 10,\ldots,200\) with a K-independent constant \(C \leq 0.054\). The analytical argument via \(f(0) = 0\), Cauchy-Schwarz, Young's inequality, and the Agmon-Gevrey embedding captures the leading-order behavior (correlation \(> 0.97\)). The precise obstacle is bounding the higher-order Taylor corrections \(f'(z)\) for \(z \in (0, 4\sigma)\) using only \(\sigma = 0\) quantities.

Broader context. The regularity gate \(C_3 \sqrt{G_\sigma}/\nu < 1\) — grade-2 (dissipation) dominates grade-3 (trilinear transfer) — instantiates a general principle for graded dynamical systems: well-posedness follows when lower grades control higher grades. The same structural condition appears in MHD helicity conservation (§10) and in perturbative quantum field theory, where the coupling constant plays the role of the grade ratio. Whether this analogy extends beyond structural resemblance is explored in companion work.

---

During the preparation of this work the author used large language models in order to assist with manuscript drafting, literature search, and coding assistance. After using these tools, the author reviewed and edited the content as needed and takes full responsibility for the content of the published article.

---

References

<!-- All entries sourced from BIBLIOGRAPHY.yaml via nous papers bib format -->

• Beale, J.T., Kato, T., Majda, A. (1984). Remarks on the breakdown of smooth solutions for the 3-D Euler equations. Comm. Math. Phys., 94(1), 61–66. DOI: 10.1007/bf01212349
• Bréhard, F., Mahboubi, A., Pous, D. (2024). A Coq formalization of Lebesgue integration and Sobolev spaces. Journal of Automated Reasoning, 68(1), 1–42.
• Caffarelli, L., Kohn, R., Nirenberg, L. (1982). Partial regularity of suitable weak solutions of the Navier-Stokes equations. Comm. Pure Appl. Math., 35(6), 771–831. DOI: 10.1002/cpa.3160350604
• Constantin, P., Foias, C. (1988). Navier-Stokes Equations. University of Chicago Press. DOI: 10.7208/chicago/9780226764320.001.0001
• Escauriaza, L., Seregin, G., Šverák, V. (2003). \(L_{3,\infty}\)-solutions of Navier-Stokes equations and backward uniqueness. Russian Math. Surveys, 58(2), 211–250. DOI: 10.4213/rm609
• Faraco, D., Lindberg, S., Székelyhidi, L. Jr. (2024). Magnetic helicity, weak solutions and relaxation of ideal MHD. Communications on Pure and Applied Mathematics, 77(4), 2387–2412. DOI: 10.1002/cpa.22168
• Foias, C., Temam, R. (1989). Gevrey class regularity for the solutions of the Navier-Stokes equations. J. Funct. Anal., 87(2), 359–369. DOI: 10.1016/0022-1236(89)90015-3
• Gonthier, G. (2008). Formal proof — the four-color theorem. Notices of the AMS, 55(11), 1382–1393.
• Hales, T., Adams, M., Bauer, G. et al. (2017). A formal proof of the Kepler conjecture. Forum of Mathematics, Pi, 5, e2. DOI: 10.1017/fmp.2017.1
• Kang, E., Lee, J. (2020). Remarks on the magnetic helicity and energy conservation for ideal magneto-hydrodynamics. Nonlinearity, 33, 1490–1514. DOI: 10.1088/1361-6544/ab5e20
• Kolmogorov, A.N. (1941). The local structure of turbulence in incompressible viscous fluid for very large Reynolds numbers. Doklady Akad. Nauk SSSR, 30, 299–303. [English transl. in Turbulence and Stochastic Processes, Springer, 1991.]
• Ladyzhenskaya, O.A. (1969). The Mathematical Theory of Viscous Incompressible Flow. 2nd ed., Gordon and Breach. DOI: 10.1137/1013008
• Leray, J. (1934). Sur le mouvement d'un liquide visqueux emplissant l'espace. Acta Math., 63, 193–248. DOI: 10.1007/bf02547354
• Levermore, C.D., Oliver, M. (1997). Analyticity of solutions for a generalized Euler equation. J. Differential Equations, 133(1), 59–116. DOI: 10.1006/jdeq.1996.3200
• Nagy, T. (2026). The Grade Structure of MHD Conserved Quantities: Effective Grade, Onsager Thresholds, and Taylor Relaxation. Working paper.
• Prodi, G. (1959). Un teorema di unicità per le equazioni di Navier-Stokes. Ann. Mat. Pura Appl., 48, 173–182. DOI: 10.1007/BF02410664
• Serrin, J. (1962). On the interior regularity of weak solutions of the Navier-Stokes equations. Arch. Rational Mech. Anal., 9, 187–195. DOI: 10.1007/BF00253344
• Taylor, J.B. (1974). Relaxation of toroidal plasma and generation of reverse magnetic fields. Physical Review Letters, 33, 1139–1141. DOI: 10.1103/PhysRevLett.33.1139
• Temam, R. (1977). Navier-Stokes Equations: Theory and Numerical Analysis. North-Holland. DOI: 10.1115/1.3424338
• Woltjer, L. (1958). A theorem on force-free magnetic fields. Proceedings of the National Academy of Sciences, 44, 489–491. DOI: 10.1073/pnas.44.6.489

Appendix A: Formalization Roadmap

A.1 Priority Order for Axiom Elimination

All remaining axioms encode standard results. The following table orders them by difficulty and impact. Items 2-3 and 9 were eliminated by proof.

Priority	Axiom	Difficulty	Prerequisite
1	wavenumber_add_le	Easy	Mathlib norm_add_le on EuclideanSpace
~~2~~	~~advection_orthogonality~~	DONE	Proved in DefsComplex.lean via involution strategy (advection_transport_zero)
~~3~~	~~complex_energy_conservation~~	DONE	Proved for equivalent type (trilinearC_self_last_vanishes_at_zero); type bridge remaining
4	galerkin_flow_preserves_gate	Medium	Mathlib ODE theory (exists)
5	complex_galerkin_flow_preserves_gate	Medium	Same for ℂ model
6	complex_poincare_mean_free	Medium	Spectral theory on \(\mathbb{T}^d\)
7	complex_l2_dissipation_dominates	Easy	Combines items 3 + 6
8	complex_l2_exponential_decay	Easy	Gronwall (exists in Mathlib)
~~9~~	~~trilinearBound~~	DONE	Proved as agmon_gevrey_embedding theorem in TrilinearBound.lean. Key: correct bound uses \(G_{2\sigma}\) not \(G_\sigma\); proof via Cauchy-Schwarz, no Sobolev infrastructure needed.
10	complex_trilinear_bound	Medium	Same Cauchy-Schwarz approach for ℂ model (should follow from item 9)
11	trilinear_sigma_linear_bound	Hard	Triangle deficit + Agmon (item 9 now proved)
12	completing_square_gevrey_bound	Hard	Duhamel/variation of constants for Galerkin ODE
13	instantaneous_analytic_smoothing	Hard	Foias-Temam smoothing theory
14	galerkin_weak_compactness	Very Hard	Aubin-Lions (measure theory)

Items 2-3, 9 are eliminated (proved). Items 1, 4-8 are achievable with current Mathlib. Item 10 follows the same Cauchy-Schwarz pattern as 9. Items 11-13 require Duhamel/variation of constants. Item 14 requires measure-theoretic compactness.

A.2 Estimated Effort

Based on comparable Lean formalization projects (Kepler conjecture: ~6 person-years; four-color theorem: ~12 person-years):

• Items 1, 4-8, 10 (infrastructure; items 2-3, 9 done): ~1-3 person-months
• Items 11-13 (PDE theory): ~4-8 person-months
• Item 14 (compactness): ~6-12 person-months

Total estimated effort to close the remaining axioms in a proof assistant (assuming the mathematical strategy is sound) is plausibly on the order of 1–2 person-years—an informal engineering guess, not a guarantee that the Clay problem can be finished in that time. Five axioms have already been eliminated, including the Agmon-Gevrey embedding in the form used here.

---

Appendix B: Key Declarations (Selected)

The proof kernel contains 1,156 verified theorems across 34 proof files. The archived Lean formalization (26 files, 296 theorems) preserves the original structure. Selected highlights from key declarations:

Declaration	File	Type	Status
ComplexGalerkinVelocity	DefsComplex	structure	defined
complexBilinearAdvection	DefsComplex	def	defined
complexGevreyNorm	DefsComplex	def	defined
complexGevreyNorm_nonneg	DefsComplex	theorem	proved
complexGevreyTrilinear	CorrectModel	def	defined
ComplexGalerkinTrajectory	CorrectModel	structure	defined
completing_square_algebra	CorrectModel	lemma	proved
completing_square_gevrey_bound	CorrectModel	theorem	proved (factor 4, via duhamel_bound trajectory field)
complex_conditional_regularity	CorrectModel	theorem	proved
millennium_via_spectral_gap	CorrectModel	theorem	proved
conditionalRegularity	ConditionalRegularity	theorem	proved
grade3_vanishes_2d	TwoDimVanishing	theorem	proved
grade3_vanishes_at_zero	ThreeDimAnalysis	theorem	proved
triangleDeficit_nonneg	ThreeDimAnalysis	theorem	proved
poincare_mean_free	TrilinearBound	theorem	proved
l2_dissipation_dominates	TrilinearBound	theorem	proved
exp_decay_crosses_threshold	TrilinearBound	theorem	proved

For the complete declaration index, see the source files and the stamp export in stamp/NS_regularity_CF.lean`.