cert-machine / instruments · the object a Millennium proof constructs

Navier–Stokes blowup: the certified proof, turned by hand

Turn the singularity

A smooth force drives a fluid from rest to infinite speed in finite time. This is the object the proof builds — drawn, not simulated.

what the pulses are for—

hatched: the cone (4.22) · faint rim: what the waves reach · dotted: the drawn stress

dotted curve: the stress needed, as drawn · bands: the two shares

time left—

zoom—

speed |u|—

ℓz / ℓr—

why dashedτ to an exact power, evaluated in float

h—

criteria met—

ten times longer at—

fps—

Click any verdict to see the arithmetic that decided it.

nothing here is gated · the audit that is: /reports/navier-stokes.html

τ = 1 − t → 0

the one control that matters

h, the smallness parameter1/100

The paper prints 0 < h < 1/100 and never says where the bound comes from. It comes from two places: below zero the axisymmetric Liouville theorems exclude the flow, at 1/6 the dissipation stops being integrable. Every verdict along the foot is a rational inequality in h, decided here in integers.

what the pulses are for

The core alone does not solve Navier–Stokes. §5 leaves a residual equal to −div(annular stress) plus a flat remainder; that stress is what the WAVES must produce. It is producible only if it lies in a cone (4.22)/(4.23), and then Proposition 7.5 turns it into two positive squared amplitudes whose square roots are the real wave amplitudes. Turn the stress out of the cone and one of them goes negative: no real pair supplies it, and nothing cancels the residual.

stress direction s3/10

cone slope m9/10

shear tilt ts1/4

vs = 2 + 2/m²—

cone: |s| <—

waves reach—

The wedge is turned by its slope m rather than by the paper's vs, because m = √(2/(vs − 2)) is what the drawing shows and vs = 2 + 2/m² is then an exact rational — so both crossings are equalities, not limits. ts rotates the wedge (the frame change of (4.23) has determinant 1 + ts², so it cannot fold it). The outer, faint wedge is what two real amplitudes reach; the gap to the hatched one is the margin η_c = 1/10 of Proposition 7.5's proof, which absorbs the errors of (7.28). Decided in integers. The stress path itself is chosen: a bump vanishing at both annular edges with a direction that turns across them, standing in for the paper's T₀ — so it is dotted, so is everything drawn from it, and every verdict on it holds given it. The audit is next door.

render

contour levels16

time speed0.17

Follow the core and the camera dives with the collapse; the picture stops moving, which is what self-similar means. Let it go and watch the thing vanish instead.

the dichotomy

For this scaling family there is NO h at which an axisymmetric forced blowup from rest can work. At h = 0 the swirl is bounded and the flow is exactly type I, which the axisymmetric Liouville theorems exclude. Above zero it is type II and escapes them — and the swirl diverges, which the maximum principle forbids for a flow driven from rest by a bounded force. The construction survives only by leaving the axisymmetric class, and the paper never says so.

every scale, exactly

Rational exponents of τ in h, decided with BigInt, so h = 0 and h = 1/6 are equalities rather than limits. The values beside them are those powers at the τ on screen, in float: computed, underlined dashed.

computed here

H(Z), the one closed form in the construction: the exterior solves the radial heat equation exactly; Simpson's rule evaluates it here, so the curve is dashed. Residual of (A.37) at Z = 1: —.

The shear feeds the oscillation, then shortens its wavelength until viscosity wins. Peak amplification —, : dotted.

what backs each mark

decided

exact arithmetic backs it

computed

float, or a number someone printed; nothing decided it

chosen

one member of a set the data admits

Decided. every row is a rational inequality in h with integer numerators; the tab decides it with BigInt, and the boundary cases (h = 0, h = 1/6) are decided as equalities rather than approached

Decided. the cone test (4.22)/(4.23) and the two squared amplitudes of Proposition 7.5 are exact rational arithmetic in the tab — the wedge is parametrised by its slope m so that vs = 2 + 2/m² stays rational, and both cone crossings are equalities rather than limits. The stress path they are applied to is chosen, so each verdict on it holds given it. Every formula is re-derived from the paper by instruments/navierstokes/probes/stress_cone.py, which carries six red controls — among them that a stress just outside the cone forces a negative squared amplitude, and that at angular mode zero the averages of Proposition 7.5 Step 1 both fail.

Computed. H(Z) = Γ(1+h)⁻¹∫₀^∞ e^{−v} v^h (1+Zv)^{−h} dv by Simpson in the tab; the residual of its differential equation (A.37) is printed beside it, and the battery checks the same integral to 25 digits

Chosen. one core out of those with the paper’s scalings, its profile shapes picked to be legible, so every contour, streamline and wave is dotted. The exponents are the paper’s and exact; the radial speed is solved from continuity in closed form, so the drawn flow is divergence-free and |u_r| scales as τ^{−1/2}, as the table says, which the build checks before it writes the page. No fluid is integrated anywhere on this page

The construction is OpenAI's, Finite time blowup for Navier–Stokes, 166 pages, sha256 0e779481c4da…. The audit next door built its 2,486-module Lean proof on one laptop in 140 minutes and had Comparator and a second, independently written kernel accept both theorems. What is certified is next door.