Navier-Stokes covariance proof companion

Try the picture: download or clone this repository and open explainability/index.html. It runs offline in a browser. Select a worked example, move the target, then inspect the matching Lean statement. No account or private 8DB service is needed. Read the short explanation.

The companion includes four contrasting cases, five additional Lean-checked statements, and a map from the explanation to the proof. It explains one algebraic component connected to the forced Navier-Stokes construction. The surrounding PDE arguments have separate premises.

A small, runnable Lean proof accompanying the companion article.

The work has three separate scopes:

1. Upstream proof checks. The article describes checks of the public Navier-Stokes formalization. Those checks concern the upstream development. A sanitized historical replay receipt records the Windows and Linux outcomes, exact source and runtime identities, and the hashes of the sealed original records. It is a summary, not a full upstream replay kit. The separate compilation receipt in covariance/ concerns the standalone lemma below.
2. A runnable covariance lemma. The Lean source proves a sufficient normalized error margin for positive inverse weights, over arbitrary real parameters. The actual compilation receipt, seven printed axiom reports, and earlier check output are included.
3. A native evidence experiment. The article separately describes representing and checking evidence in a database. The database engine is not included here, so this repository does not reproduce that native experiment.

For

C = [[1+a, 1+b], [-1+c, 1+d]],    target = (1,s),

the lemma assumes 0 < m < 1, entry errors |a|, |b|, |c|, |d| <= m/4, and |s| <= 1-m. It proves det(C) >= 7/8 > 0, positive Cramer weights, and exact target reconstruction. More general determinant, numerator, and quantitative weight bounds are also proved.

This is conditional normalized algebra. Applying it to the manuscript's actual fields requires separate analytic error estimates, positive physical scales and column masses, an orthonormal frame, and target-cone inclusion. Smooth extension at a zero-target edge requires additional flatness estimates. The attachment does not establish those premises or a full PDE theorem, and it does not certify a numerical improvement to the separate loop work.

The source connection is Proposition 7.5, printed pages 82 and 83 of the public manuscript. The manifest records source pins and file hashes; the covariance checksum list also covers the manifest.

Check the attachment hashes

From the repository root in a Bash-compatible shell, run:

sha256sum --check SHA256SUMS
(cd covariance && tr -d '\r' < SHA256SUMS | sha256sum --check -)

The seven files in covariance/ are byte-identical to the public proof attachment, including its manifest. Its checksum list retains its original CRLF line endings; the command normalizes only the list passed to the checker. The root checksum list additionally covers this README and the sanitized formal replay receipt. Matching hashes verify the recorded bytes; they do not replace a mathematical check. Git attributes preserve those bytes across platforms.

The receipt records successful Windows library, axiom and fresh Lean-kernel checks, and successful Linux Comparator, Nanoda and default-kernel checks. Preparing this companion verified the sealed archive and its manifest but did not rerun those checks. The complete transcripts, original source bundle and runtime binaries are not included here.

Replay with the pinned environment

The public proof was compiled unchanged with Lean 4.34.0-rc2, Mathlib 85e3a25e006c35636f0e53b0e9296caca2685bc0, and one Lean worker. The recorded exit code is 0. All seven axiom reports list exactly propext, Classical.choice, and Quot.sound.

From this repository's root, use an existing upstream checkout with its dependencies and compiled Mathlib imports already available. Set UPSTREAM_ENV to that checkout, then run in Bash:

set -eu
COVARIANCE_PROOF="$(pwd)/covariance/8DB-OpenAI-Covariance-Lemma.lean"
cd "$UPSTREAM_ENV"
test "$(git rev-parse HEAD)" = "f9e8bc5b38b6e212696e8a30e3e91517af887bbd"
test "$(tr -d '\r\n' < lean-toolchain)" = "leanprover/lean4:v4.34.0-rc2"
test "$(git -C .lake/packages/mathlib rev-parse HEAD)" = "85e3a25e006c35636f0e53b0e9296caca2685bc0"
LEAN_NUM_THREADS=1 lake env lean "$COVARIANCE_PROOF"

For an environment download recipe, see the covariance attachment instructions, running those instructions from covariance/. This command checks the standalone proof with the Lean compiler/kernel. It does not run Comparator, Nanoda, or the database engine. The log contains the actual Windows compilation output; the receipt omits local machine paths.

No blanket license grant is added here. Third-party software and source material remain subject to their respective terms.