# Validating a computed fluid trajectory through every time and mode

**Engine:** 0.16.0  
**Date:** 5 September 2026  
**Evidence:** Written sufficient theorem, exact certificate witnesses, standalone recomputation, corruption challenges, and bounded refinement search. No formal logical kernel and no mathematical novelty claim.

## 1. What is now implemented

The three missing engineering components from v0.15 are implemented and exercised together:

| Component | Implemented method | Evidence from this release |
|---|---|---|
| Continuous-time residual and omitted-mode bounds | Exact time polynomials, full Fourier convolution, and Bernstein convex-hull norm witnesses | All 32 reference intervals include a nonzero full residual; 384 occurrences of omitted output modes are covered. |
| Certified error-envelope solver | Rational piecewise affine supersolutions, checked by endpoint differential inequalities | 158 affine segments keep the certified error below 0.000045 through time 4. |
| Counterexample search and independent checking | Small polynomial search, a retained-mode residual counterexample, 17 certificate corruptions, and a standalone verifier | Both false shortcut claims have exact counterexamples; all 17 corruptions are rejected; the valid certificate is accepted. |

The reference is a computed finite Galerkin/Taylor approximation. It is not assumed to satisfy the full equation. The certificate controls its error relative to the full infinite-mode equation. The current representation is finite Fourier support with piecewise polynomial time dependence, subject to explicit arithmetic budgets.

This develops established approximate-solution validation methods. Relevant primary background is [Morosi and Pizzocchero, On approximate solutions of the incompressible Euler and Navier–Stokes equations](https://arxiv.org/abs/1104.3832). The eventual small-data analyticity step uses the framework developed in `GLOBAL_FLUID_BOUND.md`; related periodic Fourier theory is in [Ambrose, Lopes Filho, and Nussenzveig Lopes](https://arxiv.org/abs/2205.12383). The constants and certificate implications used here are stated below and in `NEXT_WALL.md`.

## 2. The mathematical contract

The PDE is real, mean-zero, incompressible, unforced Navier–Stokes on the fixed torus \([0,2\pi]^3\), with positive constant viscosity \(\nu\). The initial field \(u_0\) is an exactly specified rational Fourier polynomial. Unlisted **initial** modes must be exactly zero.

Partition \([0,T]\) into finitely many consecutive intervals \([t_j,t_j+h_j]\), with \(h_j>0\). On interval \(j\), define the reference

\[
v(x,t)=\sum_{k\in K_j}\left(\sum_{a=0}^{d_j}c_{j,k,a}\theta^a\right)e^{ik\cdot x},
\qquad \theta=\frac{t-t_j}{h_j}\in[0,1].
\]

The coefficients are exact complex rational three-vectors. At every polynomial order the checker verifies conjugate symmetry and \(k\cdot c_{j,k,a}=0\). It also verifies continuity of the reference between intervals. Missing reference modes are identically zero **in the chosen approximation**, not in the exact solution.

The reference is spatially smooth and continuous, piecewise polynomial in time. Its derivative may jump at joins. There is no jump in the reference itself, so its distributional time derivative has no impulse there. The differential estimates hold almost everywhere and integrate across the finitely many joins.

Define

\[
\|f\|_{\chi^s}=\sum_{k\ne0}|k|^s\|\widehat f(k)\|_2,
\quad
r=\partial_tv-\nu\Delta v+P[(v\cdot\nabla)v].
\]

For each interval we supply certified constants

\[
\|v(t)\|_{\chi^0}\le V_j,
\qquad \|r(t)\|_{\chi^{-1}}\le R_j
\qquad\text{for every }t\in[t_j,t_j+h_j].
\tag{1}
\]

## 3. Why finitely many polynomial witnesses cover a whole interval

For a vector polynomial \(p(\theta)=\sum_{a=0}^d c_a\theta^a\), write

\[
p(\theta)=\sum_{i=0}^d b_i B_{i,d}(\theta),\qquad
B_{i,d}(\theta)=\binom di\theta^i(1-\theta)^{d-i},
\]

\[
b_i=\sum_{a=0}^i\frac{\binom ia}{\binom da}c_a.
\]

For \(0\le\theta\le1\), the Bernstein basis functions are nonnegative and sum to one. Therefore

\[
\|p(\theta)\|_2\le\sum_i B_{i,d}(\theta)\|b_i\|_2
\le\max_i\|b_i\|_2.
\tag{2}
\]

The producer constructs rational upper bounds using integer square roots. The independent checker needs **no square-root approximation**: for a proposed mode bound \(U_k\ge0\), it checks

\[
U_k^2\ge\|b_i\|_2^2
\]

for a velocity contribution, or

\[
|k|^2U_k^2\ge\|b_i\|_2^2
\]

for a \(\chi^{-1}\) residual contribution, at every Bernstein control vector. Every quantity in these comparisons is rational. Summing accepted per-mode bounds establishes (1).

This is a convex-hull proof over the interval, not an inference from sampled values. Bernstein control vectors generally are not values of the polynomial at sample times.

## 4. The full residual includes modes outside the reference support

On an interval, the derivative and diffusion terms have support in \(K_j\). The quadratic term has support in the Minkowski sum

\[
K_j+K_j=\{p+q:p,q\in K_j\}.
\]

The producer computes the exact polynomial residual at every nonzero mode in \(K_j\cup(K_j+K_j)\), retaining all nonzero coefficients. Outside that finite union, the **reference residual** is exactly zero because the reference itself has finite support. The zero mode of the convection is zero by incompressibility/periodicity, equivalently by the output-wavevector factor in divergence form.

The checker independently reconstructs the entire residual and requires its nonzero mode set to match the supplied bound records exactly. A missing nonzero omitted-output mode is rejected even if the retained-mode residual vanishes.

The exact solution may generate modes arbitrarily far beyond this set. Those are controlled by the full error norm in the next section. The proof never sets the exact solution's omitted modes to zero after the initial time.

The time derivative is taken in physical time:

\[
\partial_t\sum_a c_a\theta^a
=\frac1{h_j}\sum_{a\ge1}a c_a\theta^{a-1}.
\]

The factor \(1/h_j\) is reconstructed by the verifier and separately tested.

## 5. The exact affine-envelope certificate

Let \(u\) be the local smooth solution from the specified initial data, and let

\[
E(t)=\|u(t)-v(t)\|_{\chi^{-1}},\qquad
E_1(t)=\|u(t)-v(t)\|_{\chi^1}.
\]

The relative estimate proved in `NEXT_WALL.md` is

\[
D^+E+\frac\nu4 E_1\le\frac{4V_j^2}{\nu}E+R_j
\qquad\text{while }E\le\nu/2.
\tag{3}
\]

It follows from the full bilinear Fourier inequality, Cauchy–Schwarz, and Young's inequality. In particular, it includes the quadratic error interaction. Since nonzero frequencies have \(|k|\ge1\), set

\[
b_j=\frac{4V_j^2}{\nu}-\frac\nu4
\]

to obtain \(D^+E\le b_jE+R_j\) under the same threshold.

Subdivide the interval into equal envelope segments of length \(\Delta\). On each segment define \(q\) by linear interpolation from \(q_L\) to \(q_R\). Its slope is

\[
s=\frac{q_R-q_L}{\Delta}.
\]

The verifier checks the exact rational inequalities

\[
\boxed{
s\ge b_jq_L+R_j,\qquad s\ge b_jq_R+R_j,
\qquad 0\le q_L,q_R<\nu/2.
}
\tag{4}
\]

Because \(b_jq(t)+R_j\) is affine on that segment, its maximum occurs at an endpoint. Thus (4) proves \(q'\ge b_jq+R_j\) at every interior time, and interpolation preserves the strict threshold. These are endpoint checks on a **declared affine supersolution**, which is different from assuming an arbitrary unknown trajectory is controlled by endpoint samples.

The initial value satisfies \(q(0)\ge E(0)\), using independently checked norm witnesses. Envelope joins are continuous. Scalar comparison and a barrier argument give

\[
E(t)\le q(t)<\nu/2\quad\text{throughout the certified interval.}
\tag{5}
\]

### Constructing the envelope efficiently

For \(b=b_j\), \(R=R_j\), and current upper value \(q\), the producer chooses sufficiently short segments so that \(b\Delta<1\) whenever \(b>0\). It uses

\[
q_{\rm next}=\frac{q+\Delta R}{1-\Delta b}
\]

when \(b\ge0\), or when \(b<0\) and \(bq+R<0\). For \(b<0\) and \(bq+R\ge0\), it uses

\[
q_{\rm next}=q+\Delta(bq+R).
\]

It rounds the proposed upper value upward to its chosen dyadic grid and verifies (4). The verifier does not reproduce these update rules; it checks (4) directly. Hence any other search algorithm can propose envelope nodes, and they will be accepted only if the same inequalities hold.

## 6. Why the certificate implies full-PDE existence and all-time smoothness

All reference norms on the finite interval are finite. Integrating (3) while using (5) controls \(\int E_1\,dt\). Consequently

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

The standard high-order Sobolev energy estimate and local continuation theorem then prevent a finite smooth breakdown before or at \(T\). This argument can be applied up to a hypothetical earlier maximal time, giving the same contradiction; it does not assume existence up to \(T\) in advance. Smooth initial data start the local solution. Continuity of the reference and the envelope stitches the estimates across interval boundaries.

Finally the checker independently bounds the reference's endpoint norm and checks

\[
\boxed{B=\|v(T)\|_{\chi^{-1}}^{\rm upper}+q(T)<\nu.}
\tag{6}
\]

The small-data theorem in `GLOBAL_FLUID_BOUND.md` applies to the smooth full solution \(u(T)\), giving global smoothness and subsequent analyticity. It applies to the full Fourier norm, even though the evolved solution usually has infinitely many nonzero coefficients.

This chain uses standard local PDE existence, the tame Sobolev energy estimate, continuation, and the earlier small-data theorem. The Python checker verifies the finite algebraic hypotheses of that written analysis. It is not a formal logical kernel proving those analytic theorems from foundational axioms.

## 7. The concrete computed reference and result

The main run uses \(\nu=1\), \(\varepsilon=10^{-7}\), and

\[
u_0=(2\sin y+\varepsilon\sin z,\ \varepsilon\sin(2x),\ \varepsilon\sin y).
\]

Its total initial norm is greater than two, so v0.14's total-smallness test fails. This datum is already within v0.15's shear-perturbation theorem; we do not claim a newly discovered mathematical input class from this example. The advancement here is validation of a computed polynomial reference with nonzero residual and explicit omitted modes.

The generator retains the six signed input Fourier wavevectors and computes a degree-six Taylor approximation to their Galerkin evolution over each of 32 intervals of width \(1/8\), reaching \(T=4\). Coefficients and joins are exact rationals. For this selected support the nonlinear Galerkin output lies outside the retained set, so the retained dynamics reduce to heat decay; the full nonlinear residual is nevertheless nonzero and explicitly included.

The general generator forms the Galerkin Taylor recurrence by convolution and projection. With normalized interval variable \(\theta\), its coefficients satisfy

\[
(a+1)c_{a+1}
=h\left(\nu\Delta c_a-\sum_{r+s=a}P_K\mathcal B(c_r,c_s)\right).
\]

The checker does not assume or verify that the reference came from that generator. Any reference in the supported representation can qualify if its full residual, envelope, joins, and handoff satisfy the certificate conditions.

| Quantity | Main accepted run |
|---|---:|
| Reference intervals | 32 |
| Polynomial degree | 6 |
| Affine envelope segments | 158 |
| Intervals with nonzero full residual | 32 |
| Omitted output-mode occurrences across intervals | 384 |
| Maximum certified error bound | Less than 0.000045 |
| Full norm upper bound at time 4 | Less than 0.036664 |

An occurrence count is summed over intervals; it is not a claim of 384 distinct wavevectors. The endpoint decimals are explanatory outward comparisons; the actual certificate stores exact rational witnesses.

## 8. Independent checking and attempted falsification

The standalone `tools/verify_trajectory.py` imports only Python standard libraries. It differs from the producer in three key ways:

| Producer | Independent checker |
|---|---|
| Computes \((v\cdot\nabla)v\) with the second input wavevector | Computes \(\nabla\cdot(v\otimes v)\) with the output wavevector, then projects |
| Uses a direct binomial power-to-Bernstein transform | Uses Horner multiplication and degree elevation |
| Constructs norm bounds and affine updates | Checks squared norm witnesses and differential inequalities directly |

The equivalence of the two convection expressions depends on incompressibility, which is checked coefficient by coefficient. Shared mathematical assumptions remain; separate implementations do not constitute formal verification.

All 17 deliberate corruptions were rejected. They include enlarged claim scope, unknown proof flags, invalid viscosity, time gaps, missing conjugates, undersized bounds, omitted residual modes, a false zero error envelope, a threshold violation, reference discontinuity, and missing endpoint bounds.

One mutation adds a spatially divergence-free contribution proportional to \(\theta^2(1-\theta)^2\). Its value and first time derivative vanish at both interval endpoints, so those observations alone miss it. The Bernstein witness check rejects it between the endpoints.

The automated small-polynomial search examined 333 candidates before finding

\[
p(\theta)=-4\theta+4\theta^2,
\qquad p(0)=p(1)=0,\quad |p(1/2)|=1.
\]

That exactly refutes the proposed endpoint-only maximum bound. A second counterexample comes from the computed reference itself: at the first interval's initial time, its retained-mode residual is exactly zero, yet an omitted Fourier coefficient is nonzero. Thus a retained-mode-only residual certificate would be invalid.

Eleven new test methods passed. They include distinct residual reconstructions, Bernstein identity checks, physical-time scaling, envelope sign branches, nonzero initial error, an unresolved coarse reference, schema rejection, and an isolated run with only the verifier and certificate present. A corrupted certificate is also rejected under Python `-O`, so validation does not depend on removable `assert` statements.

## 9. Bounded automatic refinement

`tools/search_trajectory.py` tries a frozen ladder and stops at the first independently accepted candidate:

| Degree | Intervals | Outcome |
|---:|---:|---|
| 1 | 8 | Error envelope unresolved on the first interval |
| 4 | 16 | Independently accepted; the search stops |
| 6 | 32 | Listed fallback, not visited by this search; used separately in the main run |

The failed coarse bound is retained. It is not a blowup result. The search is first-success refinement over three declared configurations, not a global optimization over references, norms, or algorithms. Local elapsed times are recorded as implementation observations, not portable performance guarantees.

## 10. Files and commands

From the extracted project directory, using Python 3.10 or later:

```sh
python3 tools/trajectory_lab.py
python3 tools/verify_trajectory.py results/trajectory-certificate-v016.json
python3 tools/challenge_trajectory.py results/trajectory-certificate-v016.json
python3 tools/search_trajectory.py
python3 -m unittest discover -s tests -p 'test_trajectory.py' -v
```

On Windows, replace `python3` with `py -3`. No third-party Python package or C++ compilation is needed for these companions. To verify an existing certificate, only `verify_trajectory.py` and that certificate file are needed.

For another supported exact initial field, pass `--initial-field input.json` to `trajectory_lab.py`. The generator also accepts `--degree`, `--steps`, a canonical rational `--end`, `--bits`, and `--envelope-resolution`. Failed bounds remain unresolved results; a generated candidate must still pass the standalone checker.

The frozen records are `trajectory-certificate-v016.json`, `trajectory-verification-v016.json`, `trajectory-challenges-v016.json`, `trajectory-search-v016.json`, and the selected search certificate, all in `results/`. The generation record explicitly labels its output as pending independent verification; the standalone checker supplies acceptance.

The checker accepts only `RBE_TRAJECTORY_CERTIFICATE_V1` with the fixed global-smoothness-via-validated-trajectory claim. Current budgets are 32 initial/reference modes, wavevector components of magnitude at most 16, 64 time intervals, time-polynomial degree at most 8, at most 4,096 affine segments per interval, and a 32 MiB certificate. Residual output wavevectors may reach component magnitude 32. Exact rational strings have a length limit, and floats, nonfinite numbers, duplicate JSON keys, unsupported fields, and Boolean integer aliases are rejected. Precision metadata is limited to 16 through 128 bits; the verifier's acceptance uses rational witness inequalities rather than trusting that metadata.

## 11. What remains outside this release

All three named engineering components now work within the declared representation and have been exercised on concrete certificates. This does not imply that every input receives a certificate, that every proposed inequality can be decided, or that every possible implementation error has been eliminated.

General large-data Navier–Stokes regularity, RH for all integers, and P versus NP remain unresolved by this engine. Certificates are conditional on exact specified initial data and standard PDE analysis. They do not establish extra physical dimensions. A formal proof-assistant development of the analytic bridge is still separate work.

The next substantive improvements would be tighter reference approximations that retain nonlinear interactions, less conservative bounds, broader initial-data tail representations, and formalization of selected proof dependencies. Those should be judged by independently verified improvements on fixed inputs, not by version numbers or an assumption that a general discovery must be close.