This page maps each research claim to the declaration that actually carries it. The theorem type fixes the scope. Compiler acceptance and the raw transitive axiom list establish formal closure; neither can turn a forced counterexample into an unforced all-data regularity theorem.
The separate quantization, regularity, and Wick-rotation note maps four native comparison modules to explicit examples: smooth wavefunctions with singular decoded velocity, integer circulation and phase-lift obstruction, smooth zero-set fold events, and loss of heat damping under imaginary time. These comparisons do not inhabit A or B.
The active global-regularity construction targets are the exact A and B propositions. Current open statuses report evidence and do not constrain future proofs. The A route constructs native whole-space evolution; the B routes construct physical Fourier reconstruction, positive-time regularity and global control; The D construction now directly consumes the selected periodic candidate and preserves every clause of the native periodic contract.
| Question | Exact Lean surface | Quantifiers and force | Status |
|---|---|---|---|
| Can one choose admissible data and forcing for which no global classical solution exists? | Navier.ProblemStatements.WholeSpaceBreakdown |
For every nu > 0, there exist a divergence-free Schwartz datum and a rapidly decaying smooth force such that no global IsClassicalSolution exists |
THEOREM, inhabited by ConstructedBreakdown.wholeSpaceBreakdown |
| Can admissible periodic forcing prevent every global smooth periodic solution? | Navier.ProblemStatements.PeriodicBreakdown |
For every nu > 0, there exist an admissible periodic datum and smooth periodic time-decaying force excluding every global IsPeriodicClassicalSolution |
THEOREM, inhabited by PeriodicConstructedBreakdown.periodicBreakdown |
| Does every admissible datum produce a global classical solution with no force? | Navier.ProblemStatements.WholeSpaceGlobalRegularity |
For every nu > 0 and every divergence-free Schwartz datum, there exist global velocity and pressure fields satisfying IsClassicalSolution nu zeroForce |
OPEN in this repository |
The periodic unforced existence proposition
Navier.ProblemStatements.PeriodicGlobalRegularity (alternative B) also remains
open. A new periodic classical uniqueness theorem
proves equality of velocities at every positive viscosity under the native
classical contract, including periodic velocity and periodic pressure.
It consumes an assumed B witness to attach this proved uniqueness conclusion;
it does not discharge B's existence premise. No equality of pressures is
claimed, since a spatially constant pressure gauge remains free.
The checked mean-drift algebra
constructs the raw encoding A=-2*pi*i*u_hat, proves literal convolution phase
covariance, and identifies the constant-mean cross term and its cancellation
with the translation derivative. It preserves the off-zero amplitude, squared
energy and half-generator moment. The
Galilean Volterra transport
now proves that the mean-removed path satisfies the actual time-integrated
fixed-point equation. Removing the conserved mean contracts the completed
critical norm, so this transport retains the original chart radius. It does
not supply arbitrary-data global control.
The completed forced endpoints are whole-space C and periodic D in the official problem statement. Their proofs construct the data, forces, and pre-singular classical candidates, then rule out every hypothetical global competitor in the matching contract: a smooth bounded-energy whole-space velocity-pressure pair for C, and a smooth periodic velocity-pressure pair for D. Scope: see §"What “smooth” and “unique” mean here".
The native D proof uses the selected unit-periodic candidate directly. Smooth forcing with a uniform future cutoff has all required polynomially time-weighted derivative bounds, by continuity on a compact time slab and fundamental spatial cell. Every hypothetical native competitor transports to the construction's exact same-force comparison class, including periodic pressure. The viscosity equivalence supplies every positive viscosity. See the fresh D receipt (local report).
| Claim | Proof-bearing declaration | Premise carried by its type | Fresh verification surface |
|---|---|---|---|
| A compact Euclidean candidate exists | R3CompactCandidate.selected_compact_candidate |
None | ConditionalAudit.lean; raw axioms |
| Every admissible global competitor contradicts that candidate | ComparatorBridge.compact_candidate_excludes_global_solution |
An actual candidate and an actual GlobalSolutionRn competitor |
ConditionalAudit.lean; raw axioms |
| Euclidean construction data inhabit the native whole-space C carrier | NativeConstructionEndpoint.wholeSpaceBreakdown_of_compactCandidate |
An actual compact candidate | ConditionalAudit.lean; raw axioms |
| The selected construction proves C for every positive viscosity | ConstructedBreakdown.wholeSpaceBreakdown |
None | Direct single-file source compile plus raw axioms |
| The chosen force is smooth on all real spacetime and has an explicit half-space extension | ConstructedForceExtension.constructedWholeSpaceBreakdownWithGloballySmoothForce |
None | ConditionalAudit.lean; raw axioms |
| Every ordered successive coordinate derivative of the chosen force obeys the required weighted bound | ConstructedBreakdown.wholeSpaceBreakdown_with_successivePartials |
nu > 0 |
ConditionalAudit.lean; raw axioms |
| The formal Fréchet-bundle force condition is equivalent to smoothness plus decay of every genuine ordered coordinate partial | ForceCoordinateEquivalence.forcedDataRapidDecay_iff_successivePartials |
A concrete force f; smoothness is explicit on the coordinate-partial side |
Direct single-file compile plus raw axioms |
| The selected globally smooth force has compact support on physical spacetime and vanishes after a finite time | ConstructedFiniteTimeObstruction.selected_force_has_compact_physical_support |
None; spatial support is asserted for t ≥ 0, with a finite future cutoff |
Direct single-file source compile plus raw axioms |
| The selected force is nonzero somewhere strictly before the unit-viscosity deadline | ConstructedFiniteTimeObstruction.selected_force_nonzero_before_one |
None; ∃ t ∈ (0,1), ∃ x, f(t,x) ≠ 0 |
Direct single-file source compile plus raw axioms |
| The selected unit-viscosity candidate has uniformly finite energy before its deadline | ConstructedBreakdown.selectedFiniteEnergyCandidate |
None; interval is Set.Ico 0 1 |
ConditionalAudit.lean; raw axioms |
| One selected witness simultaneously has a globally smooth force, pre-singular finite energy, compact spatial support, no continuous terminal extension on its support, and slab uniqueness | ConstructedFiniteTimeObstruction.selected_candidate_finite_time_profile |
None | Dependency-ordered source rebuild plus raw axioms |
| Every compact candidate is unique against a smooth finite-energy competitor on a closed pre-singular slab | ComparatorBridge.compact_candidate_unique_on_Icc |
Candidate properties and the competitor's local smoothness, energy, divergence, PDE and zero initial data on that slab | Dependency-ordered source rebuild plus raw axioms |
| Every same-force competitor smooth before time one and finite-energy on each closed earlier slab develops unbounded speed at that deadline | ConstructedFiniteTimeObstruction.selected_candidate_forces_speed_blowup_in_every_smooth_competitor |
None for the selected witness; the competitor class is explicit and no terminal trace is assumed | Direct single-file source compile plus raw axioms |
| The selected witness excludes a same-force continuation smooth before the deadline and continuous through it, even when energy is assumed only separately on each closed pre-singular slab | ConstructedFiniteTimeObstruction.selected_candidate_excludes_locally_finite_energy_continuation |
None | Direct single-file source compile plus raw axioms |
The selected candidate admits no Beale–Kato–Majda control bundle on [0,1) |
BKMForcedBreakdownNecessity.selected_candidate_admits_no_BKM_control |
None; the refutation consumes the candidate's own speed_unbounded field |
Direct single-file source compile plus raw axioms |
Every same-force competitor smooth before time one and finite-energy on each closed earlier slab admits no Beale–Kato–Majda control bundle on [0,1) |
BKMForcedBreakdownNecessity.selected_candidate_forces_no_BKM_control_in_every_smooth_competitor |
None for the selected witness; the competitor class is identical to the speed-blowup row's | Direct single-file source compile plus raw axioms |
| For every viscosity and every prescribed deadline there is a parabolically rescaled candidate whose classical evolution has uniformly finite energy before the deadline and unbounded speed at it | ScaledConstructedBreakdown.exists_deadlineT_profile |
None; the deadline enters through λ = T^(−1/2) with proved endpoint law deadlineOf λ = T |
Direct single-file source compile plus raw axioms |
Alternative C holds at every prescribed positive deadline: for every ν > 0 and T > 0 there is a rapidly decaying smooth force, vanishing for t ≥ T₀·T and nonzero at some t ∈ (0,T), admitting no global classical solution |
DeadlineParameterizedWholeSpaceBreakdown.wholeSpaceBreakdown_deadlineT |
None; T₀ is the existential raw-candidate endpoint from CompactFutureTimeSupport, so the support endpoint is the proved law T₀·T, not the asserted bound T |
Direct single-file source compile plus raw axioms |
The two deadline rows share a transport boundary, not a shared function space:
the rescaled blow-up velocity profile of ScaledConstructedBreakdown (the
energy-carrier file) and the nonexistence force package of
DeadlineParameterizedWholeSpaceBreakdown (the native carrier) are parallel
carriers related by the nativeForce transport and the exact iterated-Fréchet
formula iteratedFDerivWithin_parabolicScaledForce. No unforced-regularity or
periodicity-preservation claim is made by either row.
All named completed declarations above currently report only propext,
Classical.choice, and Quot.sound. The source attribution and adaptation
boundary are recorded in
OpenAI construction provenance.
The Beale–Kato–Majda criterion of
Navier.Analysis.BealeKatoMajda is a
complete sharp pair at this repository's constructed breakdown. Sufficiency:
BKMControl.velocity_bounded and
BKMControl.excludes_pointEvaluationBreakdown. Non-vacuity of the control
class: BKMControl.controlZero and
BKMForcedBreakdownNecessity.bkmControl_class_nonvacuous. Necessity at the
endpoint: BKMForcedBreakdownNecessity
proves not_bkmControl_of_speedUnboundedBelow (a field with unbounded speed
below the horizon admits no BKMControl) and applies it through the carrier
bridge speedUnboundedBelow_of_speedUnboundedAtOne to the selected candidate
and every smooth same-force competitor from rest. The criterion's hypothesis is
fully restrictive at this endpoint: no admissible profile of the proved
blow-up mechanism satisfies it, so it cannot be weakened and remain consumable
there. The vorticity-integral divergence ∫₀¹ ‖ω(t)‖∞ dt = ∞ of the
constructed field is not claimed; that is the named OPEN residual in the file
header (it needs Sobolev–Grönwall control inputs the repository does not
construct for this profile).
The reverse force estimate is quantitative: if every ordered coordinate word
of length n is bounded by C, the full iterated Fréchet operator norm is
bounded by 4^n C, expressed in Lean as the cardinality of the four-direction
word space. All orderings are already quantified. No extra claim that merely
smooth within-derivatives commute under arbitrary permutations is needed or
made.
There are four separate statements that should not be collapsed:
- The selected force has a globally smooth spacetime extension.
- The selected velocity and pressure solve the classical equation on each
time slab strictly before the singular deadline and the velocity has one
uniform finite-energy bound on the whole half-open interval
[0,1). - Slab uniqueness compares against any competitor that is smooth and finite-energy on that closed slab; it does not require the competitor to be global or spatially compact.
- The selected velocity admits no continuous extension through time one even on its own fixed compact spatial support. In particular, a hypothetical global classical competitor cannot agree with it on all pre-singular times.
The positive speed-transfer theorem first forces every competitor in this class to have arbitrarily large speed arbitrarily close to time one, without assuming any terminal trace. The continuous-extension obstruction then excludes a regular terminal velocity on the compact occupied region. See the exact force and regularity note for the cutoff formula, viscosity scaling, future-time support, and full quantifiers.
The strongest checked continuation obstruction does not assume one competitor
energy bound uniform all the way to time one. It assumes only a finite bound on
each fixed closed slab [0,T], allows that bound to deteriorate as T tends to
one, and still derives a contradiction from pre-singular uniqueness and
terminal continuity.
The proof therefore establishes nonexistence of a global classical competitor for the selected forced data. It does not establish uniqueness among all weak solutions after the singular time.
The closest whole-space native consumer is
CriticalControlDecomposition.wholeSpaceGlobalRegularity_of_local_continuation_apriori:
LocalClassicalExistence
+
NormalizedContinuationFromCriticalControl N
+
APrioriCriticalControl N
|
v
WholeSpaceGlobalRegularity
The theorem glues pressure-normalized finite-energy classical pieces into the
exact unforced endpoint, but all three analytic inputs remain hypotheses. They
must be proved for one and the same physical critical quantity N.
The Fourier-lattice restart program isolates a more quantitative bottleneck.
CriticalMildTerminalNormBound asks for one horizon-independent terminal norm
bound for every finite original-data mild chart. The sharper
LeiLinCoerciveTerminal.CriticalMildMixedTerminalBound implies that bound by a
proved coercive estimate. What remains is to prove the mixed bound for arbitrary
large data and then transport the lattice mild object to the exact whole-space
velocity, pressure, smoothness, PDE and energy carrier. The existing scalar
heat/Duhamel majorant cannot supply a fixed positive invariant radius;
GlobalRegularityCrownCore.not_restart_scalar_budget_le_fixed_radius proves
that obstruction at its exact type.
This frontier is useful because it identifies the nonlinear estimate that must do new work. It is not a reformulation that assumes the desired global solution.
Normalization is checked; global control remains open. The raw lattice
interaction is a complex bilinear dot-product convolution, while the physical
period-one Fourier equation requires -2πi times the projected convolution and
heat rate ν(2π)²|k|². The checked change of variables is A=-2πi û,
μ=(2π)²ν, with inverse û=iA/(2π) and anti-Hermitian symmetry for physical
reality. PhysicalLocalEvolution and PeriodicInitialPhysicalEvolution
construct the normalized local trajectory from official periodic data;
PeriodicNonlinearFourierReconstruction supplies its pointwise Fourier
balance. The remaining work is horizon-independent control and all-order joint
classical reconstruction. An unrestricted bound for arbitrary complex raw data
is false, as recorded below. None of this affects the forced-C construction.
Fresh source compilers and raw axiom audits are in the periodic-evolution receipt (local report). The LSP endpoint examination (local report) separately records A/B/C/D, construction constraints, and the exact remaining terminal-bound quantifiers.
| Mathematical step | Native source | Exact scope |
|---|---|---|
| Literal Fourier initialization | PeriodicDatumFourierBridge, PeriodicDatumFourierConstraints | Every native smooth periodic datum has summable weighted coefficients; divergence freedom and Hermitian reality hold for the canonical initialized carrier. |
| Exact initial reconstruction | PeriodicNativeFourierInversion | nativeInitialReconstruction u₀ hu₀ = u₀, with no inversion hypothesis. This closes the initial-data identity, not subsequent evolution. |
| Physical Fourier reconstruction | PeriodicFourierReconstruction | A weighted carrier gives a continuous periodic field; Hermitian coefficients give a real field. Higher derivatives require additional moment control. |
| Pressure recovery | PeriodicPressureRecovery | Explicit pressure coefficients restore the unprojected mode equation from the projected one, with period-one 2π factors. Time-dependent physical PDE realization remains to be consumed. |
| Spatial pressure smoothness | PeriodicPressureSpatialSmoothReconstruction | The literal unprojected convolution maps two order-s moments to order s−1. Order-(r+2) carrier moments give order-r pressure moments. The actual bounded mild trajectory therefore has spatially C∞ pressure at each positive time, without a pressure-rapidity premise. Joint time-space and initial-boundary smoothness remain separate obligations. |
| Native energy dissipation | PeriodicNativeEnergyBalance | Every assumed native unforced periodic classical solution satisfies K(T)+ν∫₀ᵀD=K(0) and ∫₀ᵀD≤K(0)/ν. It does not assert existence. |
| Native enstrophy evolution | PeriodicEnstrophyControl | Derives Z′=S−νDω from the native physical PDE, with exact vortex stretching S. An actual cellwise gradient bound G gives Z′+νDω≤2GZ; control of G or depleted stretching remains required. |
| Moving-frame transport | PeriodicGalileanReduction | The actual velocity u(t,x+tc)-c and translated pressure preserve the complete native periodic classical contract; subtracting a constant datum changes neither existence nor viscosity. |
| Mean conservation and sharper terminal premise | CriticalMildZeroMode | The original-data mild chart preserves its zero mode. A horizon-independent bound on only the nonzero modes feeds cofinal global mild continuation. The bound remains a hypothesis. |
| Lag-separated smoothing | CriticalMildPositiveTimeSmoothing | The resolved Duhamel history has half-generator moment control for positive lag. The unestimated terminal strip is explicit. |
| Dynamic endpoint cancellation | PeriodicDynamicCriticalTail | The actual frozen nonlinear integral has moment at most ν⁻¹‖u(T)‖²; the evolving term has graph membership and a quantitative bound under an explicit Dini integral. |
| Interior time modulus | CriticalMildInteriorTimeModulus | The actual bounded mild equation derives a local quarter-Hölder modulus and terminal-window Dini integrability. Constants depend on observation time and chart radius. |
| Full positive-time raw smoothing | CriticalMildFullPositiveTimeRegularity | Consumes the Dini window and frozen-source estimate to derive full half-generator membership, an explicit local bound and two-spatial-derivative coefficient summability. Higher moments/time jets and the physical decoder remain separate inputs. |
| Higher positive-time moments | CriticalMildHigherMomentBootstrap, CriticalMildHigherUniformMoments | The actual bounded mild trajectory has uniform polynomial Fourier moments of every spatial order on each compact positive-time interval. Bounds depend on the interval and chart radius. All time jets and the full classical spacetime bridge remain to be constructed. |
| Strong evolving time derivatives | CriticalMildSecondStrongDerivative, CriticalMildTimeJetMoments | Constructs the actual first and second strong time derivatives in the completed weighted Fourier carrier on each compact positive-time interval. The second derivative uses uniform spatial moments, the differentiated two-slot convolution bound, and infinite-series interchange on the actual bounded mild trajectory. All-order time induction, joint classical reconstruction, and horizon-independent critical control for arbitrary large data remain open. |
| Unconditional small-data global mild continuation | CriticalMildSmallDataGlobal | The lattice spectral gap (latticeFrequency_gap) plus exact zero-mode cancellation make the two-branch heat gain integrable on [0,∞) with total budget 3/ν, uniformly in the horizon. smallDataGlobalMild therefore constructs, for every ν > 0 and every datum with ‖a‖ ≤ ν/16, a global continuous zero-mean divergence-free mild solution on [0,∞) with decay and uniqueness in its ball — threshold ε(ν) = ν/16 unconditional, strictly surpassing the horizon-limited charts. The single premise smallDataGlobal_navierStokesBody_on_positiveTime did not discharge — anti-Hermitian (reality) transport of the global driver — is now closed by CriticalMildGlobalTrajectoryReality: the gap contraction restricts to the closed reality subspace, uniqueness forces the chosen path real, and for every small anti-Hermitian divergence-free datum the official momentum equation holds at every positive time horizon-freely (smallDataGlobal_navierStokesBody_on_positiveTime_of_real), with Hermitian physical carrier at every time. Closure on the official carrier B for arbitrary data and the classical spacetime reconstruction remain the same named consumer obligations. |
| Evolving coefficient equation | CriticalMildModeDifferentiation | Differentiates the actual Duhamel equation and proves the normalized physical unprojected Fourier coefficient equation with recovered pressure. Passing the series to the full pointwise PDE remains separate. |
| Raw complex control obstruction | PeriodicGlobalCriticalControl | An exact exponentially growing two-mode mild trajectory refutes unrestricted raw terminal bounds. Its nonzero real mean violates physical anti-Hermitian reality; physical periodic B remains open. |
| Reality of the constructed trajectory | CriticalMildTrajectoryReality | Constructs the contraction fixed point in a closed anti-Hermitian subspace, consumes Bochner reality preservation, and proves exact real physical Fourier reconstruction. |
| First joint evolving regularity | CriticalMildSmoothBootstrap | The actual positive-time mild trajectory has decoded 2.25 spatial summability, summable mode time derivatives and pressure gradients, and the physical coefficient equation. Uniform all-order jets remain open. |
| Physical local evolution | PhysicalLocalEvolution | For every physical divergence-free weighted datum, constructs a positive local interval and the same real trajectory carrying the initial value, evolving summability, coefficient derivatives and physical mode equation. No evolving trajectory premise is assumed. |
| Official periodic initial data | PeriodicInitialPhysicalEvolution | Every official smooth periodic datum has all polynomial Fourier moments and initializes the actual local physical trajectory through the exact raw encoding, with the original datum reconstructed at time zero. |
| Pointwise Fourier balance | PeriodicNonlinearFourierReconstruction | Reindexes the actual absolutely convergent nonlinear product, reconstructs pressure-gradient coefficients, and supplies pointwise Fourier balance for the constructed local trajectory. Global continuation and the full classical smoothness bridge remain open. |
| Uniform positive-interval estimates | CriticalMildLocalUniformBootstrap | Derives one bound for second spatial moments and total coefficient time-derivative mass throughout each compact positive-time interval. Constants depend on the local trajectory bound. |
| Polynomial nonlinear moments | CriticalMildPolynomialMomentConvolution | The literal projected convolution maps two order-s moments to an order-(s−1) bound for every real s ≥ 1. Propagation of all orders is a separate evolving-flow argument. |
| Countable energy differentiation | RawHighEnergyDifferentiation, CriticalMildEnergyEvolution | Proves uniform convergence of finite energy-derivative sums using an inverse-frequency tail estimate, then differentiates the actual mild trajectory's countable high-frequency energy. No energy derivative is assumed. |
| Frequency-local energy transfer | PhysicalPeriodicHighTailFlux, RawHighEnergyConvolutionIdentity, PhysicalPeriodicTailMomentControl | Identifies the actual nonlinear pairing sum with triad flux and bounds the damped generator by the evolving high-frequency tail. The affine comparison requires bounds on the evolving critical norm and moment; it supplies no arbitrary-data global estimate. |
| Actual spectral energy balance | RawHighEnergyRateIdentity, PhysicalPeriodicEnergyBalance | Combines countable differentiation with the literal nonlinear identity to prove dE_N/dt = 2 flux_N − 2μ D_N along the actual mild trajectory on each positive local interval. |
| Datum-only physical energy control | PhysicalPeriodicTotalEnergyControl | Consumes physical triad cancellation and the actual energy derivative to prove total energy is nonincreasing, including chart endpoints. Off-zero energy is bounded by the initial datum's total spectral energy, independently of chart radius and horizon. This does not bound the higher graph moment. |
| Integrated physical dissipation | PhysicalPeriodicDissipationBudget | Proves the exact trajectory identity E₀(A t) + 2μ∫₀ᵗD₀(A s)ds = E₀(a) and the datum-only high-frequency bound 2μN²∫_δᵗE_N(A s)ds ≤ E₀(a). These estimates are independent of chart radius and horizon. Time-averaged control does not exclude narrow frequency-time concentration or supply the pointwise critical bound required for arbitrary-data global continuation. |
| Simultaneous good-time control | PhysicalPeriodicGoodTimeSelection | Every existing physical mild chart and 0 ≤ δ < t ≤ T admits one c ∈ [δ,t] with 2μ(t−δ)D₀(A c) ≤ E₀(a) and, simultaneously for all N ≥ 0, 2μ(t−δ)N²E_N(A c) ≤ E₀(a). The same time controls all cutoffs. Turning this quadratic control into future-horizon-uniform critical weighted ℓ¹ control remains required for B. |
| Direct inverse-frequency good-time control | PhysicalPeriodicCriticalGoodTime, LatticeCriticalDissipationKernel | On the actual three-dimensional lattice, `C₄ = Σ_{k≠0} |
| Actual finite-window high-energy estimate | PhysicalPeriodicHighEnergyWindow, PhysicalPeriodicHighEnergyContinuity, PhysicalPeriodicHighEnergyBootstrap | Derives the evolving energy continuity and moment budget internally, then proves exponential decay plus an explicit 4 R² H/(μ N³) bound on positive time windows. The chart radius and budget are not controlled uniformly over all future horizons. |
| Weighted nonlinear cancellation | PhysicalPeriodicWeightedFluxCommutator | Exact paired triad cancellation leaves an output-weight difference, bounded by the advecting frequency. The countable commutator is bounded by two carrier factors and a higher moment, without a proved coercive sign. |
| Whole-space heat test approximation | WholeSpaceSolenoidalHeatApproximation, WholeSpaceSolenoidalHeatDomination, WholeSpaceSolenoidalHeatMixedDomination | Constructs compact divergence-free heat tests and a uniform Gaussian envelope, then proves their momentum pairing converges on each actual finite-energy solution slice. Derivative envelopes in the evolution's right-hand side, passage through time integrals, and the time-dependent adjoint test for Leray/Oseen representation remain open. |
| Physical triad absorption obstruction | PhysicalPeriodicCoerciveShellControl | A literal transverse anti-Hermitian six-mode carrier has weighted transfer 16 r³ and participating viscous density 650 r². No amplitude-independent constant absorbs each weighted triad pair pointwise. Summed or dynamical estimates remain possible. |
| Triad symmetry | TriadUnitarySymmetry, explanation | Physical translation phases form determinant-one diagonal unitary matrices and commute with heat damping. An explicit SU(3) cycle does not commute with the actual unequal triad heat rates; full SU(3) modal symmetry does not follow from having three modes. |
| Physical energy cancellation | PhysicalPeriodicGlobalControl, PhysicalPeriodicEnergyEvolution | Physical mean drift is skew; the absolutely summable countable projected triad energy series cancels exactly. This controls the energy-transfer algebra, not the global critical norm. |
| Energy versus fine-scale control | PeriodicEnergyCriticalObstruction | Fixed-energy transverse mode examples have unbounded mixed critical quantity. This refutes a universal energy-only estimate over arbitrary fields, not a bound restricted to actual trajectories. |
The physical global-control target is:
for every viscosity ν > 0 and physically initialized datum a,
there exists a finite K(ν,a), independent of horizon T and chart radius R,
such that every actual original-data mild chart satisfies
offZeroMixedCriticalQty ν (u(T)) ≤ K(ν,a).
Local Hölder regularity and a finite Dini integral on each chart do not yield this uniform K: their constants may grow with the chart radius. The active proof lanes address the physically initialized class, nonlinear stretching, mean-drift removal, and exact reconstruction of the evolving coefficients under the normalization above. Bounds proved for the raw complex equation are not bounds for the native physical initialization. Neither A nor B is counted as closed by these providers. The unrestricted raw complex target is false; its checked counterexample and the evolving-flow results are recorded in the fresh verification receipt (local report).
The whole-space cutoff path now includes
WholeSpaceHeatThirdDerivative:
exact mixed third heat-kernel derivatives, a two-Gaussian envelope, and
integrability of their pairing with every actual finite-energy SolvesBefore
slice. The solenoidal test is identified exactly as ∇G × a. The remaining
cutoff product-rule expansion, spatial limit, interval-time domination, and
time-dependent adjoint-test bridge remain required for the full mild formula.
WholeSpaceSolenoidalHeatViscousIntegrability
uses those third derivatives to prove integrability of every actual diagonal
second derivative of backwardHeatCurlField, paired with any velocity component
of a preterminal finite-energy SolvesBefore slice. These are the cutoff-free
viscous summands in lerayWeakRhs. Convergence of the finite-radius test to this
integrand and the time-dependent adjoint argument remain separate obligations.
Further analytic inputs sharpen these routes:
-
PeriodicSpatialSmoothReconstruction converts all polynomial Fourier moments into spatial
C∞regularity using the exact period-one characters. Applied to the bounded mild trajectory, it proves spatial smoothness at every positive time. All-order time jets, joint boundary smoothness, pressure reconstruction, and global critical control remain separate requirements for B. -
WholeSpaceSolenoidalHeatConvectionIntegrability proves integrability of the actual cutoff-free convection term
D(curl(Gτ a))(u) · u_jon each finite-energy preterminal slice. A uniform bound for the heat kernel's mixed second derivatives supplies the multiplier estimate. Spatial cutoff domination and the time-integral limit remain to be proved. -
WholeSpaceSolenoidalHeatViscousCutoffLimit proves the second-derivative cutoff product rule and almost-everywhere convergence of the surviving viscous term against the actual velocity. Its limit is integrable.
-
WholeSpaceSolenoidalHeatViscousProductLimit supplies the integrable envelope and proves the integrated limit of
D_i²(χ_R curl(Gτ a)) u_jon the actual finite-energySolvesBeforeslice. The separate∇χ_R × (Gτ a)correction and time-limit interchange remain necessary before taking the full weak-evolution limit; A remains open. -
PhysicalPeriodicDissipationHeatRestart bounds the complete off-zero mixed critical quantity of the positive-lag free heat restart at a good time, using only datum energy, viscosity, window length, and a summable heat kernel. This removes chart-radius dependence from the linear restart term. Controlling the nonlinear restarted Duhamel term uniformly in the future horizon remains required for B.
The Rust crate has two separate numerical surfaces. AxisConstruction
evaluates a finite radial-series approximation to the analytic-axis profile,
reconstructs velocity and pressure in its bounded similarity chart, and
measures the profile-equation defects, divergence defect, and momentum
residual. The CPU/WASM/WebGPU spectral solver separately evolves ordinary
periodic flows. The computed-construction note
records the exact equations, defaults, sampled domain, and omitted correction
layers.
The axis evaluator does not implement the annular matching, Borel background,
covariance waves, correction cycles, or final spacetime localization that make
the selected force globally smooth. Its displayed momentum residual is the
force required by the finite reconstructed field, not the selected force of
ConstructedBreakdown.wholeSpaceBreakdown. Tests can validate implementation
identities and finite-resolution behavior. No finite grid, residual sample, or
visual trajectory establishes a continuum regularity or breakdown theorem.
For the final dependency-ordered rebuild, compiled-object hashes and raw eleven-
endpoint audit, see
reports/receipts/2026-09-08-constructed-c-final/README.md (local report).
The earlier baseline receipt (local report)
preserves the pre-enhancement endpoint snapshot.
The Madelung correspondence note records the
scalar and spinor relationships, a conditional reconstruction obstruction, and
the exact additional inputs needed for a wavefunction lift. The note's
"phase topology / zeros" input is now kernelized:
Navier/Analysis/MadelungDecoderCurlObstruction.lean proves, on the crown
SchwartzVelocity carrier and under strict axioms, that no C^∞ scalar
wavefunction nonzero at the origin decodes any rotational datum
λ > 0 — the compactly supported, divergence-free rotationalDatum λ with
|u| ≤ λ < ν₀/16 is the counterexample — so the scalar route cannot carry
the small-data lift. The remaining transport obligations
{PDE, forcing, energy class} are located in the whole-space ScaledCutoff
family.
Breakdown, uniqueness, and concentration explains the exact comparison class, the finite-energy volume bound for fast regions, and why concentration does not mean compression of fluid density.
The 2026-09-09 release recheck (local report) binds all 615 current source/object hashes and repeats the eleven raw axiom audits after the final artifact cleanup.
The physical local evolution receipt (local report) records the subsequent native verification and numerical phase/energy regressions.