Bounded Energy and Persistent Fourier Tails in a Formally Verified Navier–Stokes Witness

Abstract

A bounded integrated quantity need not bound a pointwise observable. This distinction motivates a Base Zero (BZ) diagnostic applied to a selected periodic Navier-Stokes witness whose speed becomes unbounded near a terminal time. BZ is an author-developed framework for separating a system, its representation, and its calibrated observation; the author reports that its conceptual roots extend across four decades. We formalize a finite-band estimate using an explicit real Fourier kernel on the unit cell. Uniform boundedness of the squared spatial L2 norm bounds the contribution of every fixed finite band. A triangle-inequality argument then preserves terminal speed unboundedness after subtracting that band. For the selected witness, we derive the required uniform energy estimate from the actual forced PDE, with viscosity one and zero initial velocity. Periodic integration by parts removes the transport and pressure contributions from the total energy balance. Pointwise Young's inequality and an integrating factor yield a bound uniform up to the terminal time. Six energy-package targets were accepted through a comparator pipeline by both Lean and nanoda, using only propext, Classical.choice, and Quot.sound. The resulting witness-specific corollary has no additional energy premise. These two formal theorems are absent from the pinned original construction; they are not presented as novel energy-estimate or Fourier-analysis methods in the broader mathematical literature. Their scope is every fixed finite, sign-symmetric Fourier band, not arbitrary representations or time-varying truncations.

Keywords

Base Zero; BZ framework; Navier–Stokes; formal verification; Lean; nanoda; Fourier truncation; energy estimate; pointwise unboundedness; reproducibility.

Overview

The investigation asks what a finite observation can retain when a physical observable becomes unbounded while an integrated norm stays bounded. BZ is used here as an author-developed framework for separating the underlying field, its representation, and the calibrated readout. This study tests one explicit operator class: a fixed finite Fourier band on the unit torus.

The inquiry began on the morning of Friday, September 4, 2026, as confirmed by the author. The formal development uses the selected periodic witness from OpenAI's NavierStokesAndEuler repository at commit 8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538 . The external construction supplies the witness; the present work adds two formal theorem extensions absent from that pinned construction: a forced energy estimate and a Fourier-tail consequence.

The Verified Result

The selected witness retains unbounded speed arbitrarily close to time one after removing any fixed finite, sign-symmetric Fourier band, without an additional energy premise.

The squared spatial L ² norm remains uniformly bounded. This quantity is twice the kinetic energy for unit density. Nevertheless, pointwise speed becomes unbounded. Every fixed finite band has a uniformly bounded contribution, so subtracting it cannot remove the terminal unboundedness.

The statement concerns fixed finite bands. It does not rule out a time-dependent band, a nonlinear representation, or a singular readout. It does not determine a blowup exponent or concentration geometry.

Energy Bound from the Actual PDE

With viscosity one and zero initial velocity, the proof uses the same physical velocity, pressure, and forcing throughout. Periodic integration by parts removes the transport and pressure contributions from the total energy balance while retaining nonnegative viscous dissipation.

Pointwise Young’s inequality yields Y′ ≤ Y + F. Smooth forcing through the terminal time supplies a uniform bound F ≤ M on the closed spacetime cell. An integrating factor gives Y(t) ≤ M(e ^t − 1) ≤ M(e − 1). The generic estimate does not use speed unboundedness; the witness specialization follows afterward.

Cancellation in the total energy balance does not eliminate nonlinear transfer between Fourier bands. A finite projection remains a diagnostic, not a closed reduced evolution equation.

Verification and Reproducibility

All six energy-package targets were accepted by Lean and nanoda with only propext , Classical.choice , and Quot.sound , and no sorryAx . Build jobs are not counts of distinct mathematical modules. These command timings are not algorithmic performance comparisons.

The verification was executed by the author on an independently provisioned Linux environment with matching comparator, lean4export, landrun, and nanoda hashes across all three runs. The recorded toolchain versions, isolation configuration, accepted overlay sources, and command logs are preserved in sufficient detail to permit reproduction on a comparably provisioned Linux environment with the pinned dependencies available. The archive audit checks recorded evidence; it does not constitute an additional kernel execution.

The evidence deposit is ns_bz_publication_bundle.tar.gz . The accepted energy proof is inside its nested bz_energy_evidence.zip , at proof/NavierStokes/BZForcedEnergy.lean . The outer sources/BZForcedEnergy.lean is a statement-only comparator reference. The separately preserved BZForcedEnergy_accepted_v1.zip is an audit checkpoint, not a fourth verification run.

Relationship to the BZ Framework

The current BZ vocabulary distinguishes intrinsic divergence, projection caustic, observer amplification, and bounded concentration. It also includes mixed_or_unresolved as a catch-all and the newly proposed evolution_closure_failure for dynamics that fail to close. These labels are interpretive tools, not additional kernel-verified results.

The formal result establishes bounded squared L ² norm together with unbounded speed. It does not identify a geometric caustic, an observer-gain mechanism, or a universal causal explanation across all possible representations. A future lift must separately specify normalization, calibration, reconstruction, and evolution closure.

Core Contributions

• A documented independent checking run of the pinned external construction, without an earliest-verification claim.
• A formal fixed-band obstruction using an explicit bounded integral operator and terminal-unboundedness predicate.
• A forced energy estimate assembled from existing periodic integration machinery, without assuming speed unboundedness.
• A selected-witness Fourier-tail corollary with the energy premise discharged.
• A reproducible source-and-log evidence chain separating formal acceptance, interpretation, and open obligations.

Scope and Non-Claims

The article does not establish Clay recognition, a complete prose-to-formal equivalence certificate, general BZ closure, a general impossibility theorem for finite-dimensional models, or computational energy savings. It does not determine a blowup rate, unique singularity mechanism, or concentration geometry. Broader applications to latent models, engineering readouts, and other equations remain research directions.

Article and Evidence Access

Open Full PDF Article

Zenodo DOI: 10.5281/zenodo.22689025

Supporting evidence: ns_bz_publication_bundle.tar.gz and BZForcedEnergy_accepted_v1.zip , deposited with this publication under the DOI above.

Author: ORCID 0009-0005-2284-8891

Paper Details

• Journal: Carlonoscopen Journal of Coherence Intelligence.
• Publisher: Carlonoscopen, LLC.
• ISSN: 3069-874X (digital); 3071-0022 (print).
• Issue: Volume 1, Issue 25.
• CJCI identifier: CJCI-V1I25-2026-001.
• Version: 1.3 FINAL.
• Publication date: September 9, 2026.
• DOI: 10.5281/zenodo.22689025.
• Language: English.
• PDF: 7 physical pages.
• PDF SHA-256: f2f99a6ed9b3f79207c8eda26f7756bf05bbcaa0fdc24b7132325155ea54f452
• License: CC BY 4.0 for article text; third-party software retains its own license.

Suggested Citation

Silva, I. (2026). Bounded Energy and Persistent Fourier Tails in a Formally Verified Navier–Stokes Witness: A BZ-motivated diagnostic and dual-kernel verification study. Carlonoscopen Journal of Coherence Intelligence, 1(25), CJCI-V1I25-2026-001. Version 1.3 FINAL. https://doi.org/10.5281/zenodo.22689025. Full article PDF.

References and Source Records

1. OpenAI. NavierStokesAndEuler. Repository at the audited commit.
2. Tao, T. (September 7, 2026). Finite time blowup with smooth forcing term for the incompressible porous medium, Boussinesq, and incompressible Euler equations.
3. Fefferman, C. L. Existence and Smoothness of the Navier–Stokes Equation. Clay Mathematics Institute problem description.
4. Silva, I. (2026). Primary verification: verification_complete_record.tar.gz within the evidence bundle deposited under the publication DOI.
5. Silva, I. (2026). Fourier-tail verification: bz_fourier_evidence.tar.gz within the evidence bundle deposited under the publication DOI.
6. Silva, I. (2026). Energy verification: bz_energy_evidence.zip within the evidence bundle deposited under the publication DOI; separate audited checkpoint BZForcedEnergy_accepted_v1.zip . Evidence DOI: 10.5281/zenodo.22689025.

The PDF contains the full mathematical exposition, formal target statements, attributions, and scope restrictions. This page provides a publication summary and access to the article.