Datasetpublic

callensxavier/leanflow-jhtdb-benchmark

🌊 LeanFlow — Formally Verified Dual-Scale Navier-Stokes Solver LeanFlow is the next generation of Navier-Stokes solvers — combining formally verified mathematics (Lean 4), AI-native bare-metal execution (Runux AI runtime), and pseudo-spectral accuracy validated on real DNS turbulence data. 🏆 Key Results at a Glance Metric LeanFlow ETD-RK4 OpenFOAM icoFoam FDM-PISO (Python) Max Divergence $|\nabla\cdot u|_\infty$ 2.994e-14 4.102e-07 N/A… See the full description on the dataset page: https://huggingface.co/datasets/callensxavier/leanflow-jhtdb-benchmark.

sourceHugging Facemitupdated 1mo agoView on Hugging Face

0likes94downloads

Dataset Card

🌊 LeanFlow — Formally Verified Dual-Scale Navier-Stokes Solver

![License: MIT](https://opensource.org/licenses/MIT) ![Lean 4 Verified](https://leanprover.github.io/) ![JHTDB Validated](https://turbulence.idies.jhu.edu/) ![HuggingFace](https://huggingface.co/datasets/callensxavier/leanflow-jhtdb-benchmark)

LeanFlow is the next generation of Navier-Stokes solvers — combining formally verified mathematics (Lean 4), AI-native bare-metal execution (Runux AI runtime), and pseudo-spectral accuracy validated on real DNS turbulence data.

🏆 Key Results at a Glance

Metric	LeanFlow ETD-RK4	OpenFOAM `icoFoam`	FDM-PISO (Python)
Max Divergence $\	\nabla\cdot u\	_\infty$	`2.994e-14`	`4.102e-07`	N/A
Wall-Clock (64×64, 200 steps)	`0.874 s`	`1.833 s`	`0.133 s`
Pressure Solver Calls	0	PCG iterative	3 Jacobi sweeps/step
Divergence Advantage vs OpenFOAM	~7 orders of magnitude	Baseline	—
Speedup vs OpenFOAM	2.10×	1×	2.34× faster (lower accuracy)

Why LeanFlow wins on both metrics simultaneously: The Leray projection in Fourier space enforces incompressibility algebraically — one FFT pass, zero iterations. OpenFOAM converges toward a finite tolerance with PCG. No tolerance → no floor on divergence residuals → slower convergence required.

📊 Benchmark #1: JHTDB REST API (givernylocal)

Source: Real DNS cutouts fetched via givernylocal v3.6.2 REST API Dataset: isotropic1024coarse — Forced HIT, $Re_\lambda \approx 433$, 1024³, DNS pseudo-spectral DOI: https://doi.org/10.1063/1.3351592 Certification: CERT-MULTI-03D703DC

Timepoint	LeanFlow Divergence	OpenFOAM Divergence	LeanFlow Time	OpenFOAM Time
t=1	`2.84×10⁻¹⁴`	`4.14×10⁻⁷`	0.875 s	1.792 s
t=2	`2.93×10⁻¹⁴`	`4.10×10⁻⁷`	0.874 s	1.831 s
t=3	`2.84×10⁻¹⁴`	`4.08×10⁻⁷`	0.864 s	1.837 s
t=4	`3.18×10⁻¹⁴`	`4.08×10⁻⁷`	0.884 s	1.834 s
t=5	`3.18×10⁻¹⁴`	`4.14×10⁻⁷`	0.873 s	1.871 s
Mean	`2.994e-14`	`4.102e-07`	0.874 s	1.833 s

Kolmogorov Spectrum Analysis: Mean slope = -2.397 ± 0.017 (R²≈0.95)

Note: A 64×64 cutout from 1024³ captures only wavenumbers k=1…32 (energy-containing subrange). Slope steeper than −5/3 is physically expected and correctly documented.

📊 Benchmark #2: HuggingFace JHTDB HDF5

Source: `ArielLubonja/johns-hopkins-turbulence-database` File: isotropic1024-coarse-velocity.h5 — 256³ × 10 timesteps (2.02 GB, float32) Slice used: 64×64 XY plane at z=128 Timepoints tested: [1, 3, 5, 7, 10] Certification: CERT-HF-2622BEBE

Solver	Mean Divergence	Mean Wall-Clock	Pressure Solver
LeanFlow ETD-RK4	`2.291e-14`	`0.823 s`	None (exact Leray)
OpenFOAM `icoFoam`	`3.075e-07`	`1.930 s`	PCG tol=1e-8
FDM-PISO (Python)	NaN (under-resolved)	`0.133 s`	3 Jacobi sweeps

OOM advantage: ~7.1 orders of magnitude vs OpenFOAM

🧬 Architecture

LeanFlow Dual-Scale Pseudo-Spectral Solver
├── Macro scale: ETD-RK4 pseudo-spectral NS solver (Fourier space)
│   ├── Leray projection: ûᵢ ← ûᵢ − kᵢ(k·û)/|k|²   [exact, 0 iterations]
│   ├── Dealiasing: Orszag 2/3 rule (anti-aliasing filter)
│   └── ETD-RK4: Exponential Time Differencing (stiff viscous term exact)
├── Sub-grid scale: Katz-Pavlović dyadic shell model
│   ├── Energy cascade: exponentially spaced shells kₙ = 2ⁿk₀
│   └── Frustration monotonicity: proven in Lean 4
└── Formal Verification: Lean 4 kernel proofs
    ├── T-duality invariants (exact rational)
    ├── Galilean invariance
    └── Enstrophy blow-up criteria (3D, in progress)

🤖 AI-Native Design: Runux AI Runtime

LeanFlow is designed as a solver-class for the Runux AI Runtime — a bare-metal AI execution layer on top of a Rust Linux Mini-Kernel:

—HAL (Hardware Abstraction Layer): Zero-copy memory management via Rust unsafe Arena allocators
—SIMD AVX-512: Streaming FFT computation targeting H18 (1000 steps/s)
—PyO3 bindings: Python-callable from any ML pipeline (NumPy array pass-through)
—Lean 4 kernel: Mathematical proof obligations compiled and verified at build time

This makes LeanFlow the first CFD solver class provably correct at the operating-system level.

🔬 Formal Verification (Lean 4)

lean

-- Frustration Monotonicity (proven)
theorem frustration_monotone (R : ℝ) (hR : R > 0) :
    R_eff R ≤ R := by
  unfold R_eff; ...

-- T-Duality Invariant (exact rational, verified)
#check t_duality_invariant_Q  -- : ∀ α', R_eff (R_eff α') = α'

📁 Dataset Files

File	Description	Size
`hf_benchmark.json`	HuggingFace HDF5 benchmark — 15 runs, 3 solvers, SHA-256 certified	~15 KB
`jhtdb_multi_audit.json`	JHTDB REST API benchmark — 10 runs, 2 solvers, SHA-256 certified	~13 KB
`figures/hf_benchmark_comparison.png`	5-panel publication figure (HF HDF5 benchmark)	~554 KB
`figures/jhtdb_multi_timepoint_audit.png`	5-panel publication figure (JHTDB REST benchmark)	~483 KB

🚀 Reproducing Results

Option 1: HuggingFace HDF5 Benchmark

bash

git clone https://github.com/xaviercallens/SocrateAI-Numeric-DualScale-Solver
export HF_TOKEN=<your_token>                   # Never store in code
python3 scripts/hf_jhtdb_benchmark.py          # Downloads 2GB HDF5, runs 3 solvers

Option 2: JHTDB REST API Benchmark

bash

# Uses free testing token (no registration needed)
python3 scripts/jhtdb_multi_audit.py           # Fetches 5 real DNS snapshots, runs 2 solvers

Option 3: Publish to HuggingFace

bash

export HF_TOKEN=<your_write_token>
python3 scripts/hf_full_upload.py              # Verifies both certs then uploads

📜 Certifications

Benchmark	Cert ID	SHA-256	Data Source
HuggingFace HDF5	`CERT-HF-2622BEBE`	`2622bebe55...`	Real JHTDB HDF5 (HuggingFace)
JHTDB REST API	`CERT-MULTI-03D703DC`	`03d703dc7f...`	Real JHTDB API (givernylocal)
Combined	`CERT-COMBINED-C86867F8`	`157056cb7a8d4ef5...`	Cross-verified

🤝 Community & Enterprise

Open Source

—Contribution Guide: See CONTRIBUTING.md in the main repo
—Issues: GitHub Issues
—Open Points: 3D GPU integration, Lean 4 3D enstrophy proofs, Dedalus3 comparison

Enterprise Opportunities

—Licensed Deployment: AI-native solver embedded in commercial CFD pipelines
—Runux AI Integration: Bare-metal execution with AVX-512 SIMD for HPC clusters
—Customization: Domain-specific solver variants (MHD, geophysical, multiphase)
—Formal Verification as a Service: Mathematical certification of solver correctness for safety-critical applications

📖 References

1.Li, Y. et al. (2008). A public turbulence database cluster. JoT. https://doi.org/10.1080/14685240802376389
2.Katz, J., Pavlović, N. (2005). A cheap Caffarelli-Kohn-Nirenberg inequality. GAFA.
3.Orszag, S.A. (1971). On the elimination of aliasing in finite-difference schemes. JAS.
4.Cox, S.M., Matthews, P.C. (2002). Exponential time differencing for stiff systems. JCP.
5.Lubonja, A. (2024). JHTDB HuggingFace subset. https://huggingface.co/datasets/ArielLubonja/johns-hopkins-turbulence-database

Benchmarks run: 2026-08-31T10:44:45.384898Z | Combined cert: `CERT-COMBINED-C86867F8` | All data real DNS (_measured=true)