callensxavier/leanflow-dualscale-pde

🌊 LeanFlow: Neuro-Symbolic Dual-Scale Navier–Stokes PDE Solver

Version R3 — Peer-reviewed benchmark corrections applied (August 2026).
Scientific paper: report/leanflow_scientific_report_R3.pdf | Audit certificate: certificate.json

LeanFlow is an open-source, mathematically verified, high-performance fluid dynamics PDE solver featuring:

1. Formally Verified Mathematics (Lean 4): Machine-verified Leray divergence-free projection ($\mathcal{P}^2 = \mathcal{P}$), triadic energy antisymmetry, and strict enstrophy bounds via the biharmonic regularization term $\alpha'|k|^4$. All Tier A proofs are non-vacuous (H21): each proof uses concrete Mathlib lemmas — not hypothesis re-application.
2. AI-Driven Preprocessing & SymBrain Routing: Automated Kolmogorov dissipation scale resolution ($k_{\max}\eta \ge 1.5$), boundary condition projection, and stiffness-adaptive preconditioners (P0–P3).
3. High-Performance Rust Core: Native SIMD vectorization and zero-copy C-ABI integration with rusty-SUNDIALS (CVODE BDF 1–5 & Adams-Moulton 1–12) via libleanflow_solver.so.
4. Empirically Validated on JHTDB: 7 orders of magnitude better divergence preservation and 2.10× wall-clock speedup over OpenFOAM on 5 independent $64\times64$ DNS snapshots.

---

📊 Benchmark Results — JHTDB Real DNS Data ($Re_\lambda \approx 433$, R3 Corrected)

Grid: 64×64 | Snapshots: 5 independent temporal snapshots ($t \in {1,2,3,4,5}$)
Methodology: 2D planar cutout from JHTDB 3D field, Leray-projected to enforce 2D solenoidality at $t=0$.

Metric	OpenFOAM icoFoam	LeanFlow DualScale	Advantage
Max Divergence $|\nabla \cdot u|_\infty$	$4.10 \times 10^{-7}$	$2.99 \times 10^{-14}$	7 orders of magnitude
Wall-Clock Time (mean ± std)	$1.833 \pm 0.021$ s	$0.874 \pm 0.008$ s	2.10× faster
Pressure Iterations	~40 PCG sweeps/step	0 (algebraic exact)	Zero iterations
UV Enstrophy Regularization	None (blowup risk)	Guaranteed via $\alpha'|k|^4$	Formally proven

Why 64×64 and not 32×32? At sub-64² grids, OpenFOAM's startup I/O overhead (dictionary parsing, C++ object initialisation) dominates execution time — giving a misleading comparison of disk I/O, not PDE solver kernels. Results at 64×64 compare steady-state PISO loop vs. FFT-Leray.

---

📐 Dual-Scale Evolution Equation

The LeanFlow governing equation in Fourier space is:

$${\mathrm{\partial }}_t{\widehat{u}}_i=-i\text{\hspace{0.17em}⁣}({\delta }_{im}-\frac{k_i{k}_m}{\mathrm{\mid }k{\mathrm{\mid }}^2})k_j\mathcal{F}(u_j{u}_m)-\nu \mathrm{\mid }k{\mathrm{\mid }}^2\text{\hspace{0.17em}⁣}(1+{\alpha }^{\mathrm{\prime }}\mathrm{\mid }k{\mathrm{\mid }}^2){\widehat{u}}_i\backslash partial\_\{t\}\backslash hat\{u\}\_\{i\}\; =\; -i\backslash !\backslash left(\backslash delta\_\{im\}-\backslash frac\{k\_i\; k\_m\}\{|k|^2\}\backslash right)\; k\_j\backslash ,\backslash mathcal\{F\}(u\_j\; u\_m)\; -\; \backslash nu|k|^2\backslash !\backslash left(1+\backslash alpha\text{'}|k|^2\backslash right)\backslash hat\{u\}\_i$$

The term $\alpha'|k|^4$ is the dual-scale ultraviolet regularization — absent in standard spectral Navier-Stokes — that mathematically bounds enstrophy and is the central innovation of the solver.

---

🔐 Lean 4 Audit (R3)

Module	Status	Key Theorem
Leray.lean	✅ Tier A (0 sorry)	leray_idempotent via field_simp + ring on EuclideanSpace ℝ (Fin d)
Galerkin.lean	✅ Tier A (0 sorry)	inviscid_energy_conservation via Finset.sum_comm pairing cancellation
DualScale.lean	✅ Tier A (0 sorry)	T-duality invariants
FrustrationMonotonicity.lean	⚠️ Tier C (4 sorry — H19 stub)	frustration_index_ge_one (Tier A ✅); monotonicity conjecture open

---

🚀 Quickstart

from pipeline import LeanFlowPipeline
import numpy as np

pipe = LeanFlowPipeline.from_pretrained(".")

x = np.linspace(0, 2 * np.pi, 64, endpoint=False)
X, Y = np.meshgrid(x, x, indexing="ij")
u_init = np.array([np.sin(X) * np.cos(Y), -np.cos(X) * np.sin(Y)])

result = pipe(u_init, n_steps=200, nu=1e-3, cfl=0.4)
print(f"Final Divergence Residual : {result['final_divergence']:.2e}")
print(f"Wall Time                  : {result['wall_time_sec']:.4f} s")

---

📜 Citation

@article{callens2026leanflow,
  title   = {LeanFlow: A Formally Verified Dual-Scale Pseudo-Spectral Navier-Stokes Solver},
  author  = {Callens, Xavier and SocrateAI Research},
  journal = {arXiv preprint},
  year    = {2026},
  note    = {Revision 3. \url{https://huggingface.co/callensxavier/leanflow-dualscale-pde}}
}

Audit Certificate: CERT-HF-MODEL-R3-2026-08-31