Analytical proofs and spectral correspondences in mathematical physics,
verified across 11 programming languages
- Overview
- Research Programs
- Multi-Language Verification Framework
- Project Structure
- Quick Start
- Documentation
- Citation
- Contributing
- Security
- Changelog
- License
- Acknowledgements
- Contact
Analytical proof of 3D Navier–Stokes regularity without artificial dissipation, grounded in the universal polarization correction b ≈ 0.0785 from Kirchhoff point-vortex equations, together with the AB-Cloud — a 36³ non-Hermitian Hofstadter Hamiltonian whose spectrum is statistically indistinguishable from the Riemann ζ-zeros, realising the Hilbert–Pólya conjecture, Montgomery–Dyson GUE correspondence, and a concrete bridge to the Langlands programme.
This repository contains two independent research programs in mathematical physics by Isaev Iskhak Khamzatovich, each supported by rigorous analytical arguments and a comprehensive multi-language formal verification framework. The verification spans 11 programming languages — including four proof assistants (Lean 4, Coq/Rocq, Isabelle-HOL, Agda) and seven computational languages (Python, Julia, Rust, C++, Haskell, CMake, Shell) — providing unprecedented cross-verification depth for results of this significance.
| Feature | Description |
|---|---|
| 🧮 NSE Regularity | Global-in-time smoothness for 3D Navier–Stokes via polarization correction b ≈ 0.0785 |
| 🌌 AB-Cloud | 36³ non-Hermitian Hofstadter Hamiltonian matching Riemann ζ-zeros (KS p = 0.27–0.88) |
| ✅ 11-Language Verification | Lean 4, Coq, Isabelle, Agda, Haskell, Rust, C++, Python, Julia, CMake, Shell |
| 📊 Statistical Rigor | Permutation test Z = 14.10σ, p < 10⁻⁴⁴; BKM integral reduced 3.5× |
| 🔒 Formal Proofs | Machine-checked proofs in 4 independent proof assistants |
| 📖 14 Research Papers | Full PDF papers + LaTeX sources included |
| 🌐 Documentation Site | MkDocs Material with MathJax, dark/light mode, live at GitHub Pages |
The cornerstone result is an analytical proof of global-in-time smoothness for the three-dimensional Navier–Stokes equations without the introduction of artificial dissipation mechanisms. The proof is grounded in the discovery of a universal polarization correction b ≈ 0.0785 derived from Kirchhoff point-vortex equations.
Key quantitative results:
- The correction b ≈ 0.0785 induces a rotation angle θ_b ≈ 7.07° that stabilizes the Navier–Stokes evolution
- The BKM blow-up criterion integral is reduced by a factor of 3.5× through this stabilization
- The polarization correction emerges naturally from the Kirchhoff point-vortex system and is universal — independent of the specific flow configuration
The AB-Cloud is a 36³ non-Hermitian Hofstadter Hamiltonian whose spectrum exhibits a remarkable statistical indistinguishability from the non-trivial zeros of the Riemann zeta function. This construction provides a concrete realization of several deep conjectures in number theory and mathematical physics.
Key quantitative results:
- Kolmogorov–Smirnov test: p = 0.27–0.88 (cannot distinguish from Riemann zeros)
- Permutation test: Z = 14.10σ with p < 10⁻⁴⁴ (extremely significant)
- Realizes the Hilbert–Pólya conjecture — a self-adjoint operator whose eigenvalues correspond to Riemann zeros
- Confirms the Montgomery–Dyson GUE correspondence — spectral statistics match Gaussian Unitary Ensemble predictions
- Provides a concrete bridge to the Langlands programme
Additional research programs include analysis of the Korteweg–de Vries (KdV) equation with novel soliton interaction results, and the study of the Klein attractor dynamics with connections to ergodic theory and dynamical systems.
All research results are independently verified across 11 programming languages, providing one of the most comprehensive cross-verification frameworks in mathematical physics. The framework is organized in two tiers:
| Language | Version | Role | Status |
|---|---|---|---|
| Lean 4 | v4.14 | Machine-checked proofs of NSE stability bounds & AB-Cloud spectral properties |  |
| Coq/Rocq | 8.18 | Verified KdV soliton interactions & Klein attractor dynamics | |
| Isabelle-HOL | 2024 | Independent proof of NSE energy estimates & BKM criterion reduction | |
| Agda | 2.6 | Constructive proofs of spectral convergence for AB-Cloud | |
| Language | Version | Role | Status |
|---|---|---|---|
| Python | 3.10–3.12 | High-precision NSE simulations, KS/permutation tests, AB-Cloud spectral analysis | |
| Julia | 1.10+ | High-performance NSE time-stepping, GUE statistics, spectral methods | |
| Rust | 1.75+ | Memory-safe NSE integrator, AB-Cloud eigenvalue computation | |
| C++ | C++17 | Optimized BLAS/LAPACK AB-Cloud solver, KdV pseudospectral method | |
| Haskell | 9.4 | Functional NSE verification, symbolic KdV computation | |
| CMake | 3.28+ | Cross-platform build orchestration for all verification targets | |
research-papers/
├── .github/ # GitHub Actions, issue templates, PR template
│ ├── workflows/ # 14 CI/CD workflows
│ ├── ISSUE_TEMPLATE/ # Structured bug report & feature request
│ ├── dependabot.yml # Automated dependency updates
│ └── PULL_REQUEST_TEMPLATE.md
├── papers/ # 14 research papers (PDF)
├── docs/ # Documentation sources (MkDocs)
├── src/ # LaTeX sources + AB-Cloud core code
├── verification/ # Multi-language verification framework
│ ├── lean4/ # Lean 4 formal proofs
│ ├── coq/ # Coq/Rocq formal proofs
│ ├── isabelle/ # Isabelle-HOL proofs
│ ├── agda/ # Agda constructive proofs
│ ├── python/ # Python numerical verification
│ ├── julia/ # Julia high-performance verification
│ ├── rust/ # Rust memory-safe verification
│ ├── cpp/ # C++ optimized verification
│ └── haskell/ # Haskell functional verification
├── CITATION.cff # Citation metadata (CFF 1.2.0)
├── .zenodo.json # Zenodo deposit metadata
├── CHANGELOG.md # Keep-a-Changelog format
├── CODE_OF_CONDUCT.md # Contributor Covenant v2.1
├── CONTRIBUTING.md # Contribution guidelines
├── SECURITY.md # Security policy
├── AUTHORS.md # Author information
├── LICENSE # CC-BY-4.0
├── Makefile # Build automation
├── pyproject.toml # Python packaging & tool config
├── environment.yml # Conda environment
├── mkdocs.yml # Documentation site config
├── .pre-commit-config.yaml # Pre-commit hooks
├── .editorconfig # Editor consistency
└── .gitattributes # Git LFS & linguist overrides
- Python 3.10+ (with
piporconda) - Make (for build automation)
- Git (for cloning)
# Clone the repository
git clone https://github.com/wild8highlander/research-papers.git
cd research-papers
# Quick setup (Python environment)
make install
# OR with conda:
conda env create -f environment.yml
# Run all Python verifications
make verify-all
# Run extended language verifications (requires additional toolchains)
make verify-extended# Build and run the verification container
make docker-up
# OR directly:
docker build -t research-papers .
docker run --rm research-papers make verify-allAll research papers are available in the papers/ directory as PDFs. LaTeX sources are in src/.
The full documentation is built with MkDocs Material and hosted on GitHub Pages:
🌐 wild8highlander.github.io/research-papers
Features:
- MathJax rendering for all mathematical expressions
- Dark/Light mode toggle
- Code copy buttons for all code blocks
- Full-text search with coverage of all pages
- Navigation with instant loading
Build locally:
pip install mkdocs-material mkdocs-macros-plugin
mkdocs serve # Live reload at http://localhost:8000If you use this software or reference these results in your work, please cite:
@software{isaev2026research,
author = {Isaev, Iskhak Khamzatovich},
title = {Research Papers: {NSE} Regularity, {AB-Cloud}, and {Riemann} Zeros},
year = {2026},
version = {1.3.0},
publisher = {Zenodo},
doi = {10.5281/zenodo.21825394},
url = {https://github.com/wild8highlander/research-papers},
orcid = {0009-0003-7299-0701}
}Isaev, I. K. (2026). Research Papers: NSE Regularity, AB-Cloud, and Riemann Zeros (Version 1.3.0). Zenodo. https://doi.org/10.5281/zenodo.21825394
The citation metadata is also available in CITATION.cff (CFF 1.2.0 format) — compatible with GitHub's "Cite this repository" feature.
We welcome contributions from the mathematical physics and formal verification communities! Please see our detailed Contributing Guide for:
- 🐛 Bug reports — Use the structured issue template
- 💡 Feature requests — New verification targets or languages
- 🔧 Pull requests — Code improvements, proof extensions, documentation
- 📐 Formal proofs — New verification in additional proof assistants
- 📊 Numerical verification — Reproducibility checks and benchmarks
All contributions are checked by pre-commit hooks (black, ruff, codespell) and 9+ CI workflows.
This project takes security seriously. Please see our Security Policy for:
- 🛡️ Vulnerability reporting — Private disclosure via GitHub Security Advisories
- 🔍 CodeQL analysis — Automated security scanning on every push
- 📋 OpenSSF Scorecard — Continuous security posture assessment
- 🔐 Dependabot — Automated dependency updates and vulnerability alerts
Do not report security vulnerabilities through public GitHub issues.
All notable changes are documented in CHANGELOG.md following the Keep a Changelog format. The project adheres to Semantic Versioning.
| Version | Date | Highlights |
|---|---|---|
| 1.3.0 | 2026-08-14 | Extended language verifications, enhanced documentation |
| 1.2.0 | 2026-08-10 | Cross-language verification framework, CI/CD pipelines |
| 1.1.0 | 2026-08-06 | Additional formal proofs, benchmark suite |
| 1.0.0 | 2026-07-29 | Initial release — NSE regularity proof, AB-Cloud results |
Multi-language verification suite addressing 3 reviewer objections about the AB-Cloud methodology.
10 languages: Python, C++, Fortran, Julia, Rust, R, MATLAB, JavaScript, Go, Haskell
3 Objections addressed:
- GUE Universality (Bohigas-Giannoni-Schmit)
- Circularity of Embedding
- Selective Interpretation
Quick start:
# Python (recommended)
python3 ab-cloud-verification/python/ab_cloud_verify.py --interactive
# All languages
bash ab-cloud-verification/run_all.sh
# Russian
python3 ab-cloud-verification/python/ab_cloud_verify.py --lang ru --allSee ab-cloud-verification/README.md for full documentation.
This project is licensed under the Creative Commons Attribution 4.0 International license — see LICENSE for details.
This is the most permissive Creative Commons license, maximizing compatibility with Zenodo/DOI deposition, open science requirements, and reproducibility standards.
This research leverages the following tools and frameworks:
- Proof assistants: Lean 4, Coq/Rocq, Isabelle-HOL, Agda
- Numerical computing: NumPy, SciPy, Julia, LAPACK, BLAS
- Documentation: MkDocs Material, MathJax
- CI/CD: GitHub Actions, CodeQL, OpenSSF Scorecard, Dependabot
- Code quality: pre-commit, Black, Ruff, Codespell
Isaev Iskhak Khamzatovich — Independent Researcher
