# The next proof obstacle and a first extension beyond it

**Engine:** 0.15.0  
**Date:** 5 September 2026  
**Status:** An implemented sufficient theorem for perturbations of an exact shear; a development specification for general trajectory validation. No mathematical novelty or Millennium solution is claimed.

## 1. The obstacle worth targeting next

Version 0.14 certifies a whole fluid trajectory when the total initial Fourier norm is smaller than viscosity. A field outside that sufficient condition receives no conclusion. The most useful next capability is to exploit a good approximation to the trajectory and rigorously control its error.

This revision implements a first special case: a possibly large exact decaying shear, plus a small fully three-dimensional perturbation. It certifies a concrete field that v0.14 could not certify. It does not yet validate arbitrary numerical trajectories.

The broader approach is established: [Morosi and Pizzocchero, On approximate solutions of the incompressible Euler and Navier–Stokes equations](https://arxiv.org/abs/1104.3832), use estimates of approximate-solution error to control existence times and distances to exact solutions. Their Sobolev formulation provides primary background for this development direction. The explicit Fourier estimate below is derived here for the project's normalization; its novelty is not asserted.

## 2. A relative error inequality

All fields are real, mean-zero, divergence-free and spatially periodic on \([0,2\pi]^3\); viscosity \(\nu\) is positive. Start with a local smooth solution \(u\) of unforced Navier–Stokes. Let \(v\) be a chosen smooth reference field, and write

\[
w=u-v,\qquad
\|f\|_{\chi^j}=\sum_{k\ne0}|k|^j\|\widehat f(k)\|_2.
\]

Use \(\mathcal B(f,g)=P[(f\cdot\nabla)g]\), with \(P\) the Leray projection. Define the **full projected residual**

\[
r=\partial_tv-\nu\Delta v+\mathcal B(v,v).
\]

An exact reference solution has \(r=0\). Set

\[
E=\|w\|_{\chi^{-1}},\quad E_0=\|w\|_{\chi^0},\quad
E_1=\|w\|_{\chi^1},\quad V=\|v\|_{\chi^0},\quad R=\|r\|_{\chi^{-1}}.
\]

The subscript in \(E_0\) denotes norm order; initial error will be written \(E(0)\). Subtracting the equations gives

\[
\partial_tw-\nu\Delta w
=-\mathcal B(v,w)-\mathcal B(w,v)-\mathcal B(w,w)-r.
\]

Incompressibility of the first argument and \(\|P_k\|\le1\) yield

\[
\|\mathcal B(f,g)\|_{\chi^{-1}}
\le\|f\|_{\chi^0}\|g\|_{\chi^0}.
\]

Taking upper Dini derivatives of Fourier coefficient norms and summing,

\[
D^+E+\nu E_1\le 2VE_0+E_0^2+R.
\tag{1}
\]

On compact intervals of the local smooth lifespan, every required polynomially weighted Fourier tail is summable; the coefficient inequalities pass to the full sums. This is an infinite-spectrum estimate.

By Cauchy–Schwarz, \(E_0^2\le EE_1\). Young's inequality gives

\[
2V\sqrt{EE_1}\le\frac{\nu}{4}E_1+\frac{4V^2}{\nu}E.
\]

Consequently, **as long as \(E\le\nu/2\)**,

\[
\boxed{D^+E+\frac{\nu}{4}E_1\le\frac{4V^2}{\nu}E+R.}
\tag{2}
\]

Since \(|k|\ge1\), \(E_1\ge E\), so

\[
D^+E\le\left(\frac{4V^2}{\nu}-\frac{\nu}{4}\right)E+R.
\tag{3}
\]

This estimate explains why the decomposition matters: the smallness restriction concerns the error, while the reference flow enters through an explicitly controlled amplification factor.

## 3. The general validation condition, still to be implemented

Suppose a smooth reference \(v\), on a finite time interval \([0,T]\), has certified bounds \(V(t)\le\overline V(t)\) and \(R(t)\le\overline R(t)\). Put

\[
a(t)=\frac{4\overline V(t)^2}{\nu},\qquad
q'(t)=\left(a(t)-\frac{\nu}{4}\right)q(t)+\overline R(t),
\qquad q(0)\ge E(0).
\]

The scalar equation has the variation-of-constants expression

\[
q(t)=e^{\int_0^t(a(s)-\nu/4)\,ds}
\left[q(0)+\int_0^t e^{-\int_0^s(a(\tau)-\nu/4)\,d\tau}\overline R(s)\,ds\right].
\tag{4}
\]

If a rigorous enclosure establishes \(\sup_{0\le t\le T}q(t)<\nu/2\), comparison and a barrier argument give \(E(t)\le q(t)\). Integrating (2) gives a finite bound for \(\int_0^T E_1(t)\,dt\), provided the supplied envelopes are integrable and bounded as needed.

For smooth \(v\) on the closed interval, \(\int_0^T\|v\|_{\chi^1}\,dt<\infty\). Therefore

\[
\int_0^T\|\nabla u\|_\infty\,dt
\le\int_0^T\left(\|v\|_{\chi^1}+E_1\right)dt<\infty.
\]

The standard high-order Sobolev energy estimate

\[
\frac{d}{dt}\|u\|_{H^m}^2
\le C_m\|\nabla u\|_\infty\|u\|_{H^m}^2,\qquad m>5/2,
\]

together with local existence and continuation, prevents breakdown before or at \(T\). This estimate follows by differentiating the equation, cancelling the divergence-free transport term, applying the standard tame commutator estimate, and dropping nonpositive viscous dissipation. These are explicit analytic dependencies; they are not established by the software tests.

If, additionally,

\[
\boxed{\|v(T)\|_{\chi^{-1}}+q(T)<\nu,}
\tag{5}
\]

then v0.14's small-data theorem applies at time \(T\), giving smoothness forever after. A finite validated interval can therefore connect an initially large flow to an all-time theorem.

Equation (4) is a specification, not an implemented general solver in v0.15. Sampling a numerical residual at a finite list of times does not certify its supremum over the interval. Likewise, evaluating only retained Fourier modes can miss the entire omitted-mode residual.

## 4. An implemented all-time special case

Take the exact shear

\[
v(x,t)=(Ae^{-\nu t}\sin y,0,0).
\]

It satisfies the full equation with constant pressure: \((v\cdot\nabla)v=0\) and \(\partial_tv=\nu\Delta v\). Thus

\[
R=0,\qquad V(t)=|A|e^{-\nu t},\qquad
K=\int_0^\infty\frac{4V(t)^2}{\nu}\,dt=2(A/\nu)^2.
\]

**Theorem.** Let \(u(0)=v(0)+w(0)\) be any smooth, real, mean-zero, divergence-free initial field. If

\[
\boxed{E(0)e^{2(A/\nu)^2}<\frac{\nu}{2},}
\tag{6}
\]

then the full three-dimensional solution is globally smooth. An upper bound \(M\) with
\(E(0)e^K\le M<\nu/2\) gives

\[
\boxed{
\|u(t)-v(t)\|_{\chi^{-1}}
\le E(0)e^{K(1-e^{-2\nu t})-\nu t/4}
\le Me^{-\nu t/4},\qquad t\ge0.
}
\tag{7}
\]

**Proof.** Under the error threshold, integrate (3) with \(R=0\). The resulting upper bound is at most \(M<\nu/2\), so the error cannot reach the threshold. This closes the bootstrap on the entire local smooth lifespan. Equation (2) further implies

\[
\int_0^t E_1(s)\,ds
\le\frac4\nu\left(E(0)+MK\right)
\tag{8}
\]

for every time in that lifespan. Also \(\int_0^\infty\|v\|_{\chi^1}dt=|A|/\nu\). The continuation argument in Section 3 excludes any finite maximal smooth time. This proves (7) for all future time. In the zero-error case the result also follows directly by uniqueness of the exact shear.

The theorem holds for any finite real amplitude \(A\), with a correspondingly smaller permitted perturbation. The present checker limits \(|A|/\nu\le8\) to keep its exponential arithmetic within a declared budget. That implementation limit is not a mathematical regularity threshold.

For the supported range, choose \(T=4/\nu\). Then

\[
\|u(T)\|_{\chi^{-1}}
\le|A|e^{-4}+Me^{-1}
<\nu\left(8e^{-4}+\tfrac12e^{-1}\right)<\nu.
\]

The checker bounds these exponentials exactly and issues a v0.14 handoff bound. After \(T\), the earlier analyticity theorem applies with time origin shifted to \(T\).

The handoff invokes the written theorem, not the old finite-input parser: \(u(T)\) generally has infinitely many coefficients. Its full norm is bounded by the reference norm plus the rigorous error envelope. No unlisted-mode-zero assumption is imposed on the evolved solution.

## 5. A field newly certified by the engine

Use \(\nu=1\), \(A=2\), \(\varepsilon=10^{-5}\), and

\[
u(x,0)=
\begin{pmatrix}
2\sin y+\varepsilon\sin z\\
\varepsilon\sin(2x)\\
\varepsilon\sin y
\end{pmatrix}.
\]

Its divergence is exactly zero. Its nonzero Fourier wavevectors span three dimensions; it is not restricted to dependence on two spatial coordinates. Its projected nonlinearity is nonzero: at \(k=(2,1,0)\), the coefficient of \(P[(u\cdot\nabla)u]\) is

\[
-\frac{i}{4}
\begin{pmatrix}-3A\varepsilon/5\\6A\varepsilon/5\\\varepsilon^2\end{pmatrix}\ne0.
\]

Exact Fourier convolution independently checks that coefficient. The total initial norm is

\[
\|u(0)\|_{\chi^{-1}}
=\sqrt{4+\varepsilon^2}+\frac32\varepsilon>2>\nu.
\]

Thus the old total-smallness condition fails. Relative to the known shear,

\[
E(0)=\frac52\varepsilon=\frac1{40000},\qquad K=8,
\]

\[
E(0)e^K=\frac{e^8}{40000}\approx0.07452395<\frac12.
\]

The new theorem certifies global smoothness. At \(T=4\), its handoff bound is below \(0.065\), well inside the old threshold of one. Decimal values here are explanatory; every acceptance comparison uses rational enclosures.

This is a strict expansion of the engine's certificate coverage. It is a known type of stability result around a smooth solution, not a new general regularity theorem. The permitted perturbation shrinks exponentially with the background amplitude in this conservative estimate. Arbitrary large-data regularity remains outside its scope.

## 6. Reproduction and arithmetic

Run from the extracted source directory with Python 3.10 or later:

```sh
python3 tools/relative_fluid_certificate.py examples/relative-fluid/large_shear_small_3d_perturbation.json
python3 -m unittest discover -s tests -p 'test_relative_fluid.py' -v
python3 tools/relative_fluid_examples.py --output results/my-relative-fluid.json
```

On Windows, use `py -3` instead of `python3`. No C++ compilation or third-party Python packages are required for this companion. Input uses the unchanged exact finite Fourier schema from `GLOBAL_FLUID_BOUND.md`. All unlisted initial modes must be exactly zero.

The checker extracts the \(x\)-component \(\sin y\) amplitude automatically, or accepts a canonical rational `--amplitude`. It constructs and subtracts the exact shear internally; it never trusts a user flag asserting zero residual. A poor reference choice can make the sufficient condition fail without changing the input field.

Square-root contributions are enclosed with the prior exact integer method. Exponentials use the prior outward dyadic Taylor routine with 192 terms and a proved geometric upper bound on the infinite remainder. An independent 240-term exact rational series challenges those enclosures in the new tests. The main certificate accepts only if the upper amplified-error bound is strictly below \(\nu/2\). A lower bound at or above the threshold means the sufficient condition fails; a straddling interval means unresolved precision. Resource limits and invalid input have distinct outcomes.

The CLI returns zero for certification, one for invalid input, and two for an unmet or unresolved sufficient condition or unsupported resource budget. Nine new test methods and six example outcomes are recorded in the release. The report is `results/relative-fluid-v015.json`. Written analysis, implementation checks, and formal proof verification remain different evidence levels; no formal kernel has checked these new arguments.

The independent convolution test first rejected an incomplete hand calculation of the example's coefficient: its third component was written as zero, omitting the \(-i\varepsilon^2/4\) term. The corrected value is included above, and the rejected value is retained in the report. Inequality (1) already includes the quadratic perturbation interaction, so the correction changes the example calculation without changing the theorem or acceptance condition.

## 7. What would accelerate useful progress most

The following priority order is an engineering recommendation based on the current missing dependencies, not a measured claim about time to discovery.

| Priority | Upgrade | What it enables | Concrete acceptance test |
|---|---|---|---|
| 1 | Continuous-time residual and Fourier-tail bounds for computed reference trajectories | Applies the Section 3 theorem beyond exact shear backgrounds | A full-interval bound includes every omitted output mode and survives an injected omitted-mode defect. |
| 2 | A rigorous solver for the scalar comparison envelope \(q\) | Converts a reference trajectory into an existence/error certificate and possible all-time handoff | Certify \(q<\nu/2\) throughout the interval and (5), including rational outward rounding. |
| 3 | Automated choice of reference flow, norm weights, and time slabs | Searches for tighter valid estimates where one certificate fails | A frozen previously unresolved input obtains a stronger certificate; counterexamples to false candidate inequalities are retained. |
| 4 | A small independent certificate checker, followed by selected formalization | Reduces shared implementation and proof-assumption errors | Altered residual, missing tails, unjustified constants, and enlarged claim scope are rejected. |

The first two priorities should be developed together. A finite Fourier reference with a polynomial or otherwise rigorously represented time dependence has computable full residual: its quadratic term can populate frequencies up to twice its support. Modes outside the reference support must be included in the residual. Error analysis then controls the exact solution's further modes through the full norm inequality; it must not assume they vanish.

The fast experimental loop should be:

1. State a candidate bound with its exact assumptions and quantifiers.
2. Search cheaply for counterexamples and compare with the current baseline.
3. Spend rigorous arithmetic on candidates that survive.
4. Freeze the complete witness, tail bounds, and failure reasons.
5. Check relevant primary literature before claiming novelty.

Measure progress by newly certified input classes, stronger proved constants, fewer unresolved cases in a frozen suite, or a proved reduction in computational work. Larger version numbers and more sampled cases do not measure distance to a Millennium proof. Optimize wall-clock performance after profiling identifies an arithmetic bottleneck; faster sampling cannot replace a missing continuum bound.

For now, focus the proof-development effort on this fluid trajectory capability. The RH all-integer step and general P-versus-NP argument require different mathematics, and this error estimate does not transfer to them automatically. A new coordinate representation earns its place by improving a valid estimate, preserving information with lower cost, or making a previously inaccessible theorem computable.