gi:proof:nscd
Lean 4 - Proof - Navier–Stokes C/D (KTS Global)
Live version in repository: 1.0.1
Formal statement
Lean declaration names (copyable):
NavierStokes.ClayC.clay_C NavierStokes.ClayD.clay_D NavierStokes.ClayChallenge.clay_navier_stokes_fefferman NavierStokes.ClayChallenge.clay_navier_stokes_fefferman_via_D NavierStokes.Comparator.navier_stokes_clay_via_C NavierStokes.Comparator.navier_stokes_clay_via_D
Verification metrics
Machine-extracted from the repository at pinned commit 9f3df6786654.
| Shipped modules (closure) | 620 |
|---|---|
| NavierStokes/ .lean files | 613 |
| ClayStatement/ .lean files | 6 |
| Declarations verified | 12 (6 target + 6 bridge) |
| Axiom-policy checks | 14 |
| ECR class | LIBRARY_SUPPORT |
| Mutation tests | 5 wrong/weakened statements + inserted sorry rejected |
Layers
| Statement & bridge layer | ClayStatement/ — 6 files (Tim Jacobs, KTS Global) |
|---|---|
| Ported upstream library | NavierStokes/ — 613 files (OpenAI’s formalization, ported to Lean 4.34.1 / Mathlib d13f23b) |
| Closure | 620-module closure = 613 (NavierStokes/) + 6 (ClayStatement/) + roots |
Port (v1.0.1): the port patch is recorded in docs/PORT_DIFF.patch and docs/PORT_SUMMARY.md (modified: 24; the exact unchanged, proofs-repaired and statements-adapted counts and the patch SHA-256 are the ones recorded in the v1.0.1 PORT_SUMMARY.md — read the file for the measured figures). The port is attributed to Tim Jacobs as operator-supplied attribution. Lean sources are byte-identical to v1.0.0. The 620-module figure is the build/closure count — not a count of ported modules.
Axiom footprint
Every checked declaration depends only on the three standard Lean/Mathlib axioms:
propext Classical.choice Quot.sound
Gates passed
- Axiom-policy — checked on every build (RESULT: PASS, 14 checks).
- ECR battery — every result returned as an accepted DECLARATION_CHECK job, zero unused-hypothesis rows.
- Mutation tests — 5 wrong/weakened statements + inserted sorry rejected.
- Non-vacuity — CDNonVacuity.zero_solR3CDNonVacuity.zero_solTorus.
What this is NOT
- It is not a proof of (A) or (B), nor of global regularity.
- It is not independent confirmation that the Lean statements transcribe the official statements (docs/STATEMENT_CORRESPONDENCE.md).
- It is not independently reviewed or reproduced: every check was run by the package builder on one Linux node.
- It carries no ECR closing record: the ECR class is LIBRARY_SUPPORT (an externally authored, kernel-verified, ECR-checked library declaration; docs/ECR.md).
Reproduce it yourself
Expected: RESULT: PASS (14 axiom-policy checks)
Tested platform: Linux x86_64 only. See the repository’s rebuild docs for online and offline profiles.
Provenance & credit
The blow-up mathematics and the Lean formalization are OpenAI’s (NavierStokesAndEuler @ f9e8bc5b38b6, Apache-2.0). The KTS Global statement and bridge layer, per-alternative packaging, and verification tooling are credited to Tim Jacobs, KTS Global.
- Toolchain
- Lean 4.34.1 · Mathlib d13f23b
- Repository
- kts-global/lean-proofs-navier-stokes-cd @
9f3df6786654 - Release
v1.0.1
Cite
- DOI
- 10.5281/zenodo.23917705
- Wikidata
- Q141986416
- ORCID
- 0009-0008-7130-1448