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 measurement (v1.0.1)
Machine-measured in the repository at tag v1.0.1 (evidence/port_measurement/measurement.json, printed by measure_port.py, run twice with identical output). Against upstream OpenAI NavierStokesAndEuler @ f9e8bc5b:
NavierStokes/ files (this package) | 613 |
|---|---|
| Shared with upstream | 609 |
| Byte-identical to upstream | 588 |
| Modified Lean files | 21 |
| Present here, not upstream (solution files) | 4 |
| Upstream files modified (Lean + build) | 24 |
| Port patch | docs/PORT_DIFF.patch — 48 hunks, 43042 bytes |
A position heuristic over the 21 modified Lean files finds 6 declarations changed in their statement region and 40 changed in their proof body only (1 edit lies outside any declaration). This records where text changed, not what was repaired or why. The port is attributed to Tim Jacobs as operator-supplied attribution. 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