← Work

NS Check

In Progress

Inspect what each step of a recorded Navier–Stokes formal audit establishes.

Recorded formal audit · C/D only

What each check establishes

Five recorded checks for the same pinned target. Open a step to see what it establishes and what it leaves open.

Scope
Navier–Stokes Clay alternatives C and D only
Run completed
Upstream revision
8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538
Target buildRecorded result: passed

The pinned target built in the recorded environment.

Limit: Build success alone does not establish statement correspondence.

Statement and primitive comparisonRecorded result: passed

The compiled statements and primitives passed the recorded comparison.

Limit: Manual correspondence with the mathematical problem remains a separate review.

Axiom closureRecorded result: passed

The recorded closure contains propext, Classical.choice and Quot.sound.

Limit: This is an axiom check for the selected roots, not a trust-free foundation.

NanodaRecorded result: accepted

The independent checker accepted the recorded export.

Limit: Checker implementation and the execution environment remain trusted.

Lean replay and quotient postcheckRecorded result: accepted

The recorded replay and quotient postcheck accepted the export.

Limit: The receipt applies only to the pinned target and retained run.

Manual correspondence review

The source assessment reports no mismatch in its manual statement correspondence review. There is no separate specialist sign-off.

Numerical work is separate

The source assessment withdraws the historical point/rectangle Volterra tail and W* enclosure claims. Formal replay does not restore those claims. No numerical results are included here.

Trust and limits

  • These are recorded results. Preparing this projection does not rerun the build, checkers or proof replay.
  • The official Mathlib cache was trusted; the entire library was not rebuilt from source.
  • The checkers, checking environment, OS and hardware remain part of the trust base.
  • This receipt does not map every clause of paper Theorem 1.1 or independently reconstruct all analytic ideas.
  • Forced C/D breakdown does not resolve unforced A/B.
  • The receipt does not determine a Clay award or establish general mathematical acceptance.
  • Results do not transfer to a later upstream revision.
  • The export digest identifies retained bytes; it is neither a signature nor an additional proof check.
Roots, axioms and checker revisions
  • NavierStokes.Comparator.navier_stokes_breakdown_R3
  • NavierStokes.Comparator.navier_stokes_breakdown_periodic

Axioms: propext, Classical.choice, Quot.sound

Comparator
19e111e2141cf333c7daff0f64c5f24acc91dd2e
lean4export
cacf989bd75f608700820f6afc595f32e7a99a4d
Nanoda
05055695879dfebb6628a67da88ceca6cd6b0421
Landrun
811cfff51ceaf3d9843708aa6d22e9b84ccac8b4
Retained export and receipt metadata

1,071,397,994 bytes

Export SHA-256
429d30a8d9110faeb84ae0919b5d1b074f3ceea236254eda104f2007262e492f

Metadata only; the retained export is not included in this package.

Source receipt SHA-256
087bdb17135777ec1af0964cb0193200c1473e31a703b82e895b4984453fb8cd

Command receipt SHA-256
d4fd94ee1a880d2e5249dc99031bea9ad0cc82dfe095dc13e293ca2e99fdc788

One target, several different checks

This exhibit presents a selected receipt from an audit of the pinned Navier–Stokes C/D target. A successful build, statement comparison, axiom closure, and proof replay answer different questions. Each recorded result keeps its own scope and limitations.

The receipt is an account of a retained run. Opening this page does not execute a proof checker. Its export digest identifies stored bytes; it is not a signature or a claim of mathematical acceptance.

leanformal-verification

Added