Navier

A native Lean reconstruction of OpenAI’s forced three-dimensional Navier–Stokes breakdown construction, with analytical continuation criteria and reproducible spectral fluid solvers.

The checked theorem Navier.Breakdown.ConstructedBreakdown.wholeSpaceBreakdown inhabits the repository’s original whole-space alternative C: for every positive viscosity, there are admissible initial data and a smooth rapidly decaying force for which no global smooth bounded-energy classical solution exists. The proof supplies the constructed candidate and derives comparison with every hypothetical global competitor. Its transitive axioms are exactly propext, Classical.choice, and Quot.sound.

The native periodic alternative D is also inhabited by PeriodicConstructedBreakdown.periodicBreakdown. For every positive viscosity, the selected periodic construction supplies admissible forcing excluding every global smooth periodic velocity-pressure pair. The exact consumer and transitive axioms were independently checked. Raw compiler receipts are retained locally under reports/receipts/ and are excluded from Git history; the proof sources remain reproducible.

The analytical construction is OpenAI’s. The native source adaptation pins their released revision, preserves Apache-2.0 notices, and compiles on this repository’s current v4.34.0-rc2 toolchain (authored against 4.31.0 APIs; migrated in ad12c3d). There is no OpenAI Lake dependency. Awkronos contributes the transport into the original native PDE carrier, additional force-derivative comparisons, solver work, and interactive explanation.

The separate unforced global regularity statements A and B remain open here. Comparison before the singular time does not assert uniqueness of a weak continuation after it. The numerical tools include a finite analytic-axis stage of the construction and a separate periodic spectral solver. Their computed fields and residuals are numerical evidence, not the continuum proof. See the computed construction method.

The logical shape is easiest to see as two different paths:

FORCED CONSTRUCTION (proved)
selected compact (u, p, f)
  -> smooth, rapidly decaying force
  -> classical solution on 0 <= t < 1 with uniformly bounded energy
  -> uniqueness among smooth finite-energy competitors on every closed slab before t = 1
  -> unbounded speed as t approaches 1
  -> no same-force continuation that is smooth before t = 1, continuous through it,
     and finite-energy on every closed pre-singular slab

UNFORCED REGULARITY (open)
every admissible u0, with f = 0
  -> local classical solution                                  [native input required]
  -> continuation controlled by one critical quantity           [native input required]
  -> a uniform bound for that quantity, for arbitrary large data    [missing]
  -> global smooth bounded-energy solution

“Globally smooth” in the completed result applies to the force. The constructed velocity is smooth on every pre-singular time interval and is proved not to possess a global classical continuation satisfying the official energy contract. This distinction is part of the theorem types, not a prose caveat.

The terminal obstruction is stronger than the global endpoint needs: the excluded competitor may choose a different finite energy bound on each closed pre-singular slab. No single energy constant uniform as the slabs approach the deadline is assumed.

The periodic research now has checked native Fourier initialization and exact initial reconstruction, a correctly normalized local physical trajectory with pointwise Fourier balance, classical velocity uniqueness, energy and enstrophy identities, and local smoothing estimates. It still lacks the arbitrary-data, horizon-independent critical bound and all-order joint spacetime reconstruction needed for B. The result map records that boundary.

Mathematics

Entry point	Content
Problem.lean, OfficialProblem.lean	Exact PDE, data, smoothness, energy, and alternative statements
ConstructedBreakdown.lean	Constructed C endpoint and bounds for successive coordinate partials
ConstructedFiniteTimeObstruction.lean	One selected witness carrying finite energy, slab uniqueness, compact support, and terminal nonextension
EuclideanPDETransport.lean	Coordinate isometry, derivatives, energy, and force transport
R3FiniteEnergyComparison.lean	Comparison on every pre-singular time interval
ForceRecursivePartials.lean	Actual successive differentiation versus multilinear jets, including the initial boundary
ForceCoordinateEquivalence.lean	Exact equivalence between the force predicate and decay of every genuine ordered coordinate partial
ConstructedForceExtension.lean	The selected force is globally smooth across time zero at every positive viscosity
ConditionalAudit.lean	Selected theorem types and raw transitive axioms
Result and frontier map	Authoritative claim-to-declaration map, trust evidence, and current status
Native mathematics and solver guide	Detailed construction, useful conditional results, and numerical validation
Documentation index	Current evidence, open obligations, interpretation notes, and historical records

Formalization conventions, the construction carrier review, the open-obligation map, and the falsification ledger preserve the distinction between completed endpoints, conditional estimates, and rejected approaches.

Reproduce the proof

With the pinned Lean toolchain and Mathlib cache installed as described in REPRODUCIBILITY.md:

python3 scripts/verify_construction.py

The verifier compiles the endpoint’s local source dependencies in order and prints its exact type and raw axiom closure. Receipts include source and dependency fingerprints; source parsing determines build order, never proof status. Existing .olean files alone are not evidence of a current source check.

Run the solver

solver/ contains the Rust crate and browser build. Its Fourier method uses the rotational nonlinearity, Leray projection, componentwise 2/3 dealiasing, and integrating-factor RK4. CPU/WASM and WebGPU backends identify their precision and diagnostics explicitly.

cd solver
cargo test
cargo build --release --target wasm32-unknown-unknown

The Python adaptive solver remains canonical in the Reality development workspace. scripts/build_solver_release.py exports a deterministic standalone bundle with provenance and tests, so a release does not require access to that private workspace. The Rust crate is self-contained and tested against independently generated Python fixtures.

The interactive companion is navier.awkronos.com. It explains the construction and runs the Rust solver; this repository supplies the exact results and open obligations, triad analysis, and reproducible experiments.

The Blender optical pipeline imports the live laboratory’s computed particle paths into an editable Cycles scene. The browser traces refracted light through local cylindrical approximations of those same paths; the glass geometry is a visualization of the velocity field.