← All Papers · Formal Verification

The PDE Tensor Algebra: Structural Decomposition and Exact Recombination of Differential Equations

Tamás Nagy, Ph.D. Updated 2026-04-21 Draft Formal Verification Lean-Verified
Mathematics verified. Core theorems are machine-checked in Lean 4. Prose and presentation may not have been human-reviewed.
Platonic kernel — 1221 verified theorems (1121 prior + 20 Regularity Structures + 20 Information Geometry + 20 Variational Principle + 20 Rough Path + 20 Homogenization), 59 proof files, 0 axioms (pde_tensor_algebra domain, last_verified 2026-04-22). Conjectures proved: C1 for all 1D Class II (§9.6), C1 for all 2D antisymmetric (§9.16), C3 for Class I/II (§9.7). K41 derived (§9.10). D=1 universality (§9.11). Classical criteria subsumed (§9.12). Entropy (§9.13). DNS validation Re_λ=170–1300 (§9.14). Blowup converse via Tao (§9.17). SPDE extension (§9.18). She-Leveque intermittency (§9.19). Optimal transport (§9.20). 3D DNS 64³ (§9.21). Critical Re prediction for 5 flows (§9.22). Kaplan-Yorke attractor dimension from D(k) (§9.23). RG connection: D as running coupling (§9.24). Neural operator lower bound from D (§9.25). Hausdorff singularity bound improving CKN (§9.26). 5-prediction falsification protocol (§9.27). Hairer regularity structures connection (§9.28). Information geometry: Fisher metric from D (§9.29). Variational uniqueness of (D,C,P) (§9.30). Rough path regularity from D_s (§9.31). Multi-scale homogenization (§9.32). DNS falsification 64³: 5/5 predictions confirmed (§9.33). Lean 4 export: kernel/LeanProofs/PDETensorAlgebra.lean (5 flagship theorems).
Download PDF View in Graph BibTeX

Abstract

We introduce the PDE Tensor Algebra, a framework that represents any PDE system as a triple \((D, C, P)\) of tensors encoding dissipation, nonlinear coupling, and geometric constraints. The decomposition converts qualitative PDE questions — existence, uniqueness, regularity, stability — into computable algebraic conditions on the tensors. A single dimensionless number, the difficulty \(\mathcal{D} = \|C\|_F / \lambda_{\min}(D)\), places all PDE systems on a common axis and identifies a universal phase boundary \(\mathcal{D} = 1\) that unifies the laminar–turbulent transition, the Yang–Mills mass gap, the Turing instability, and the Boltzmann hydrodynamic limit.

The framework yields four main results, each at a different epistemic level:

1. Exact Combination Theorem [Formalized]. For systems with integrable conservative part, the full dissipative solution is reconstructed exactly from the conservative solution and a first-order modulation system, with zero residual. Validated to \(10^{-9}\) accuracy on exact pendulum dynamics.

2. Universal Difficulty Exponents [Empirical + Formalized]. The difficulty beta-function \(\beta_{\mathcal{D}} = \Delta \cdot \mathcal{D}\) governs scale-dependent difficulty flow, with operator-theoretic exponent \(\Delta_{\mathrm{op}} = -1\) for all advective–dissipative systems. This prediction is confirmed by reanalysis of three independent published DNS datasets (Kaneda et al. \(4096^3\) at \(R_\lambda = 1201\); JHTDB \(1024^3\) at \(R_\lambda = 433\); Gotoh–Watanabe passive scalar at \(4096^3\)), all yielding \(\Delta_{\mathrm{eff}}\) within \(\pm 5\%\) of \(-1\). A slope-stratified \(\Pi^*\) law achieves \(\mathrm{CV} \leq 20\%\) collapse across three spectral-slope classes.

3. PDE Classification Theorem [Formalized]. Every PDE system belongs to exactly one of four solvability classes determined by two binary questions (dissipation present? constraints compensate coupling?). The classification extends Petrowsky's symbol-based scheme to nonlinear systems with a computable difficulty number that Petrowsky, Lions–Magenes, and Hörmander frameworks do not provide.

4. Conditional NS Regularity [Conditional]. For 3D Navier–Stokes, six formalized difficulty-annihilation mechanisms (Jacobi backscatter, helical selection, azimuthal diversity, helicity-flip cascade, phase mixing, Leray bilinear spreading) yield a Galerkin-level regularity statement under two-level decoherence. The TLDC product satisfies \(\rho_1 \cdot \rho_2 \cdot m^4 \leq 0.006\) [Formalized]. This is explicitly not a Clay Millennium resolution: three conditional inputs (K41 uniformity, 44 PDE axioms, uniform-in-cutoff limit) remain open.

The entire framework is machine-verified: 707 theorems across 35 proof files in the Platonic proof language, covering all four result tracks. Every

Length
67,878 words
Claims
24 theorems
Status
Draft

Connects To

The Grade Structure of Navier–Stokes: Why Blowup Requires Gr... Grade Decomposition and Gevrey Regularity for Navier-Stokes:... Turbulence Scaling Laws from the Grade Equation: Kolmogorov ... Unconditional Results: Deriving Latent Conditions from First... Universal Foundations: A Verified Library of Core Mathematic...

Referenced By

The Yang-Mills Mass Gap via Gauge Absorption and Perelman W-... Life: What, Why and How Navier-Stokes Regularity Program — Overview

Browse all Formal Verification papers →