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. 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. 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. 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. 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$.

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:

$$\partial{t}\hat{u}{i} = -i\!\left(\delta{im}-\frac{ki km}{|k|^2}\right) kj\,\mathcal{F}(uj um) - \nu|k|^2\!\left(1+\alpha'|k|^2\right)\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)

🚀 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