Navier–Stokes R2/R3 community verification package, V1 (release r2-r3-v1)

Claim

Proved (Lean 4.34.1, Comparator on two kernels): the encoded forms of Fefferman's alternatives (C) and (D) for forced Navier–Stokes, and A ∨ B ∨ C ∨ D through them. Not claimed: (A) or (B); that the encoding matches Fefferman's published prose; Clay acceptance.

Contribution attribution

OpenAI — inherited mathematics and underlying formalization at commit f9e8bc5b38b6e212696e8a30e3e91517af887bbd. Tim Jacobs, KTS Global — statement and bridge layer, R3 per-alternative packaging, public verification tooling and documentation. Verification is publisher-executed; not an independent replication.

Limits

• Publisher-executed, not an independent replication.
• One platform (native Ubuntu 24.04 x86_64); no native Windows, offline or cold-cache verification.
• landrun not byte-reproducible.
• The Lean encoding has not been independently reviewed against Fefferman's published prose.
• Alternatives A and B are shipped as statement files only; they remain open.
• No Clay acceptance.

Artefact

Release asset: R2_FINAL_S524_COMMUNITY_V1.tar.gz · release page: https://github.com/kts-global/lean-proofs-public/releases/tag/r2-r3-v1 · licence: Apache-2.0

Single origin

Every field on this page is read from the live record at https://ktsglobal.live/api/authority-network/evidence/r2-r3-v1.json at build time. If the release body ever changes, this page is regenerated and a build-time check fails the build on any difference. The release body itself is at https://github.com/kts-global/lean-proofs-public/releases/tag/r2-r3-v1.