Skip to main content

Executive briefing · R2/R3 — Navier-Stokes community verification package

NODE-21 executive briefing entry for the Navier-Stokes R2/R3 community verification package. The canonical evidence record lives at NODE-1; this is a short briefing pointer that states the claim boundary and the open-package / KTS-tooling-not-published position.

Claim boundary

The package proves, in Lean 4, the encoded forms of two of Fefferman's alternatives for the forced Navier-Stokes problem. The package does not claim the full Fefferman statement, does not claim that the encoding matches Fefferman's published prose, and does not claim Clay Institute acceptance. The verbatim claim text and the full limits list are on the canonical record at NODE-1 and on the publication entry at NODE-10; this briefing is a pointer, not a re-publication.

Open package; KTS verification tooling not published

The release package (Lean sources, statement files, receipts) is open and reproducible from the GitHub release. The internal verification tooling KTS uses to run the package end-to-end is not published. A third party reading the release can execute the Lean proofs against the stated kernels on the stated platform without any KTS-side tooling; the KTS tooling is a convenience layer, not a dependency of the proofs.

Verifier keys

DOI (Zenodo)
10.5281/zenodo.23535805
Wikidata
Q141803373
GitHub release tag
r2-r3-v1

Related federation surfaces