Stability Framework for the Singularity of the Euler Equations on $\mathbb{R}^3$

• Finite-time singularity in the Euler equations from smooth initial data remains a central open question related to the broader PDE regularity problem.The introduction also places finite-time blowup for Navier–Stokes among the Millennium and Smale problems.Source: §1 · p. 4
• Prior Euler blowup results rely on boundaries or nonsmooth initial data, leaving the smooth-data problem on R3 unresolved in this framework.The passage notes that boundary-driven mechanisms exploit confinement, while viscosity makes the related Navier–Stokes blowup problem harder.Source: §1 · p. 4
• The numerical study produced a highly accurate Euler profile on R3, represented by splines whose residual errors were rigorously bounded by O(10^-5) in L2 and O(10^-3) in L∞.Arb interval arithmetic controlled numerical and rounding errors in the certification procedure.Source: §1 · p. 4
• The stability analysis replaces a stringent global outgoing-flow condition with a weaker local condition that pushes flow away from meridional fixed points.This weaker condition is intended to prevent perturbation concentration near those points, but requires more delicate analysis than prior work.Source: §1 · p. 4
• The paper linearizes the dynamically rescaled equations around spline profiles and combines low- and high-order energy estimates into a computable stability framework.The nonlinear stability proof is reduced to rigorously certifying a large finite collection of explicit estimates with sufficient margin, using interval arithmetic or Arb computations.Source: §1 · p. 5
• If the required constants and margins are certified and nonlinear stability holds, dynamic rescaling can yield an admissible original-variable solution that becomes singular in finite time.At critical scaling λ = 1/2, this reconstruction requires control of modulation parameters near their self-similar values; some estimates may need refinement.Source: §1 · p. 5
• The parallel LeanPDE effort formalizes key symbolic derivations in Lean and connects them with separate Julia-Arb numerical certification.The passage describes this as part of an integrated effort toward machine-checked PDE analysis (de Moura and Ullrich, 2021; The mathlib Community, 2020; George et al., 2026; Bezanson et al., 2017; Johansson, 2017).Source: §1 · p. 5

2.1 The 3D Axisymmetric Equations

• Axisymmetry sets ∂θ=0 and reduces the 3D Euler system to equations in (r,z), where rescaled swirl and streamfunction variables remove the cylindrical 1/r singularity.The meridian velocity components are recovered from the streamfunction variables.Source: §2.1 · p. 6

2.2 Traveling-Wave Ansatz

• A backward self-similar ansatz allows an approximately fixed profile shape to travel along the symmetry axis, with scaling balance fixing cu=-1, cω=-1-λ, and cψ=-1+λ.The translation is axial, preserving cylindrical symmetry and regularity at the fixed axis.Source: §2.2 · pp. 7–8

2.3 Steady-State Profile Equations

• The ansatz yields an autonomous nonlinear steady-state problem for (U, Ω, Ψ) and parameters λ and C, with the stated profile equations taking λ=1/2.λ controls spatial-scale collapse, while C specifies axial drift speed in the rescaled frame.Source: §2.3 · p. 8

2.4 Numerical Profiles

• Prior work produced a high-accuracy PINN candidate, but stability uses a certifiable spline surrogate with elliptic residual exactly zero by construction.Piecewise polynomials support certified derivative, extremum, and residual bounds; the surrogate defines ω̄ by applying the elliptic operator to ψ̄.Source: §2.4 · p. 9

3 Stability

• The framework develops linear stability estimates in weighted norms and nonlinear stability estimates using Sobolev embeddings and weighted bounds, with tunable weights optimized numerically for margin.Its proof still requires rigorous certification of the estimates and constants; finite-dimensional eigenvalue tests do not control high-frequency modes, nonlocal terms, neutral directions, or transient growth.Source: §3 · p. 12

3.1.1 Introduction

• Dynamic rescaling tracks the evolving solution in normalized coordinates, adjusting location, scale, and amplitude so a stable singularity appears as convergence to a steady profile.Fixing this modulation gauge removes apparent drift from changes in blowup time, center, or amplitude, while linking steady-state convergence to finite-time blowup in physical variables.Source: §3.1.1 · pp. 12–14

3.1.2 Dynamic Rescaling Equations for the Euler Equations

• For a stable traveling self-similar blowup, the rescaled fields and modulation parameters are expected to converge, making the traveling-wave profile a fixed point of the dynamic equations.The equations impose normalization conditions to preserve the meridional fixed point and amplitude at the origin.Source: §3.1.2 · p. 15

3.2 Linearization

• Linearization separates first-order perturbation dynamics from higher-order remainders, identifying the operator that determines whether the candidate profile attracts nearby states in rescaled variables.The candidate blowup profile is treated as a steady state of the dynamically rescaled system.Source: §3.2 · p. 16

3.2.1 Perturbations

• Admissible perturbations inherit the profile’s symmetries, regularity, decay, and weighted energy assumptions, while normalization conditions fix translation and amplitude directions.These conditions prevent perturbations from drifting along symmetry directions instead of measuring genuine profile changes.Source: §3.2.1 · pp. 16–17

3.2.2 Choice of Variables for the Linear Stability Analysis

• Because vorticity and velocity derivatives share scaling, the linear stability analysis uses δω and derivatives of δu as a scale-consistent perturbation vector.The reduced variables u and ω scale differently, with ω carrying one extra factor under rescaling.Source: §3.2.2 · p. 17

3.2.3 Perturbation Equations

• The perturbation equations decompose each field’s evolution into linear terms, nonlinear remainders, and residuals accounting for the numerical profile’s failure to be exact.A residual amplitude offset is absorbed into the reference amplitude rate under the stated nondegeneracy condition.Source: §3.2.3 · p. 18
• The perturbation system recovers δψ elliptically from δω, reconstructs velocity, and differentiates δu equations to evolve scale-consistent variables in a closed linearized system.The linearized operator includes steady-flow transport, coupling between δu and δω, elliptic recovery, velocity reconstruction, and linearized modulation.Source: §3.2.3 · p. 19, §3.2.4 · p. 19, §3.2.6 · p. 20

3.2.5 Modulation Equations

• Modulation formulas derive from normalization and the stagnation condition; they determine δC and δcu when the reference amplitude ū0 is nonzero.Both modulation variables are linear in the perturbation, while products involving them remain quadratic nonlinear terms.Source: §3.2.5 · p. 20

3.3.2 Low-Order Weighted Energy.

• Separate weights for δω, ∂rδu, and ∂zδu create low-order damping, while high-order energy supplies pointwise, interpolation, elliptic, and modulation bounds.Low-order energy alone cannot control terms requiring L∞ or origin-point bounds.Source: §3.3.1 · p. 20, §3.3.2 · p. 21, §3.3.3 · p. 21

3.3.4 Full Energy.

• The full energy balances low- and top-order damping through μk; k = 4 is the lowest admissible derivative order, and intermediate orders follow from interpolation.Larger k increases the profile derivatives and analytic constants that must be certified.Source: §3.3.4 · p. 22

3.3.5 Constraints on the Weight Functions

• Weights must remain coercive, locally integrable near the origin, sufficiently regular, and grow at infinity enough to recover unweighted velocity control.The power-law singularity condition with exponent pi < 1 is a sufficient local-integrability criterion.Source: §3.3.5 · p. 23

3.4.1 Low-Order Energy Linear Stability and the Need for Higher-Order Energy

• Integrating the low-order differential energy estimate yields exponential decay of E0 and the scale-consistent perturbation under the closed linearized flow.Low-order energy alone does not close the linear estimates, so it must be supplemented by high-order weighted energy.Source: §3.4.1 · p. 24

3.4.2 Low-Order Linear Estimates

• Low-order estimates combine signed-matrix damping with direct bounds; high-order estimates use differentiated damping matrices and control commutators, elliptic terms, and modulation losses.Localized damping certificates can address regions where a uniform matrix margin fails, including stagnation regions for the higher-order estimate.Source: §3.4.2 · pp. 24–25, §3.4.3 · pp. 25–26

3.5 Nonlinear Stability Estimates

• The nonlinear argument reduces to a full-energy estimate separating residual, low- and high-order linear, and low- and high-order nonlinear contributions.The residual sets the allowed neighborhood for an approximate profile; nonlinear contributions are bounded by cubic and quartic powers of the full energy.Source: §3.5 · p. 26

3.5.1 Low-Order Nonlinear Estimates

• Low-order estimates use weighted transport cancellations and weighted L2 factors with L∞ coefficients, while exact linear modulation formulas make the resulting nonlinear pairings cubic.The finitely many termwise bounds are summed to obtain ΛN,3.Source: §3.5.1 · p. 27

3.5.2 High-Order Nonlinear Estimates

• High-order estimates integrate principal transport terms by parts and bound commutators and source products using lower-order L∞ factors and higher-order weighted L2 factors.The argument retains full weight conversions, uses elliptic estimates and certified interpolation, and substitutes linear modulation formulas before counting cubic pairings.Source: §3.5.2 · pp. 27–28

3.6 PDE Residuals

• For a numerical profile, substituting it into the steady equations gives defects, while the elliptic residual is exactly zero because the spline vorticity is obtained by applying the elliptic operator to the streamfunction.The raw residuals vanish if the profile is exact.Source: §3.6 · p. 28

3.7 Stability Theorems

• Theorems 1 and 2 reduce stability to certifying finite numerical values for analytic constants, without which the proofs are not complete.The analytic argument identifies the needed constants; numerical certification is profile-, weight-, and parameter-specific.Source: §3.7 · p. 29

3.7.1 Single-Radius Stability Theorems

• Under the stated hypotheses and certified estimates, every solution starting inside E_k(0) < δ* stays inside the ball while it exists, making the ball forward invariant.The estimates must be certified with finite constants, and the perturbation equations must hold for admissible perturbations.Source: §3.7.1 · pp. 29–30

3.7.2 Two-Radii Stability Theorem

• The two-radii theorem obtains separate low- and top-order energy bounds by placing a sufficiently small invariant weighted ball inside the prescribed target region.It uses the same certified estimates and weighted-energy argument as the single-radius theorem.Source: §3.7.2 · p. 31

3.8 Computer-Assisted Strategy for Proving Stability

• The computer-assisted strategy searches weights to make the damping margin exceed optimized nonlinear and residual errors, then rigorously validates the selected radius and estimates.For fixed weights, the scalar-radius optimization balances cubic and quartic errors against the residual contribution ΛR/δ; a candidate succeeds when the gap J is negative.Source: §3.8 · pp. 32–34

Algorithm 1. Loop for optimizing the nonlinear stability certificate

• The algorithm initializes an admissible candidate and iteratively updates its weights to decrease J when J ≥ 0.Once Λstab > 0, it computes ΛR and Λ3 = ΛN,3 + ΛDαN,3 as part of the certificate search.Source: Algorithm 1. Loop for optimizing the… · p. 34
• When J < 0, the algorithm selects an admissible radius δ∗ satisfying (167), records the tentative certificate, and records final weights, radius, and bounds.The current candidate must have a nonempty admissible set of radii.Source: Algorithm 1. Loop for optimizing the… · p. 34
• The tentative proof is then rigorously validated using analytic certificates, including every radius-dependent admissibility guard at δ∗.Source: Algorithm 1. Loop for optimizing the… · p. 34

Conclusion

• The framework combines perturbation and modulation equations with coupled low- and high-order energies to reduce nonlinear stability to finitely many explicit or computable quantitative conditions.The conditions must be rigorously verified to determine whether the candidate profile is stable and complete the proof.Source: Conclusion · p. 35
• The remaining task is to certify profile-dependent constants and margins with sufficient positive margin, refining selected estimates if needed.Spline representations, interval arithmetic, certified matrix bounds, and finite-dimensional optimization provide a route to rigorous certification; insufficient margins may require further analysis, and stability would remain open.Source: Conclusion · p. 35
• If the quantitative conditions are certified with positive margin, the candidate profile is nonlinearly stable and finite-time reconstruction yields an admissible solution singular in finite physical time.The reconstructed solution remains asymptotic to the profile.Source: Conclusion · p. 35
• LeanPDE formalizes symbolic derivations while Julia and Arb generate numerical certificates, combining Lean verification with spline-based interval certification in a proposed PDE-proof pipeline.The passage attributes Lean to de Moura and Ullrich (2021), TorchLean to George et al. (2026), Mathlib to The mathlib Community (2020), and Arb to Bezanson et al. (2017) and Johansson (2017).Source: Conclusion · p. 35

Appendix A. Interpolation Between Low-Order and High-Order Energies

• The high-order energy retains only the top derivative level, with intermediate levels recovered through weighted interpolation between adjacent derivative orders.The one-step estimate converts an intermediate weighted norm into a small multiple of the next-higher norm plus a controlled multiple of the previous norm.Source: Appendix A · pp. 38–39
• The one-step interpolation requires finite comparison constants and suitable adjacent weights; its finiteness is the concrete certification required for the interpolation step.The proposition also assumes weighted weak derivatives and justified integration by parts with boundary-flux terms vanishing as cutoffs are removed.Source: Appendix A · p. 38
• Iterating certified one-step inequalities yields a finite interpolation certificate, requiring rigorous recursion data and verification of matrix invertibility, nonnegative inverse entries, and required inequalities.The resulting weighted interpolation bounds support high-order linear and nonlinear estimates; parameters can allocate the top-order contribution to damping while recording the remaining term at low order.Source: Appendix A · pp. 39, 41

B.1 Preliminaries

• Weak-derivative rules justify differentiated identities, while the weak Leibniz rule supports product expansions in the estimates.The preliminaries also fix Sobolev and Fourier normalizations and compare derivative and Bessel-potential norms.Source: §B.1 · pp. 43–44

B.2 Extension, Sobolev, and Morrey estimates

• Extension, Morrey, and Sobolev estimates explain how domain control yields full-space comparison and pointwise regularity, including H2(U) embedding into L∞(U) in two dimensions.The origin values required by the modulation formulas are controlled by the origin-kernel elliptic estimates.Source: §B.2 · pp. 48–49

B.3 Whole-plane endpoint Sobolev estimate

• The whole-plane endpoint estimate supplies the sharp Sobolev constant used after parity reflection to place lower-order factors in L∞.Its Bessel-potential normalization is converted to the paper’s Fourier convention, including the two-dimensional specialization.Source: §B.3 · p. 50

B.4 Whole-plane estimates used in the energy argument

• Parity reflection converts half-plane Sobolev control into whole-plane control when the stated trace conditions hold, enabling L∞ bounds and interpolation in energy estimates.Matching derivative traces across the axis prevents higher weak derivatives from acquiring a distribution supported there.Source: §B.4 · p. 51
• After parity reflection, the s = 2 whole-plane Sobolev bound places lower-order factors in L∞ when two additional derivatives are controlled in L2.This supplies pointwise control for lower-order perturbations, velocity factors, and non-top-order product factors.Source: §B.4 · p. 54
• Interpolation rewrites intermediate derivative norms as a small top-order term absorbed into damping and a low-order term bounded by the low-order energy.The estimate also applies to coordinate-derivative sums, with its constant adjusted using Plancherel and the Young parameter chosen for the prescribed top-order coefficient.Source: §B.4 · pp. 54–55

B.5 Leibniz product estimate for differentiated nonlinearities

• For k ≥ 4, selecting the perturbation with the most derivatives leaves each other perturbation with at most ⌊k/2⌋ derivatives, allowing two more derivatives for the 2D H2 → L∞ bound.Thus the unselected perturbative factors are controlled in L∞.Source: §B.5 · p. 56
• The finite Leibniz sum retains the full weight ratio with pointwise factors; intermediate orders use (193), and streamfunction factors are bounded through δω by Proposition 12.Source: §B.5 · p. 56

B.6 Streamfunction elliptic estimates

• The five-dimensional lift yields the Newtonian kernel Γ5(X) = (8π2)^-1|X|^-3 and a decaying convolution representation that extends to the full perturbation class.Approximation preserves the certified bounds and their constants for the perturbation streamfunction.Source: §B.6 · pp. 58–59
• For k ≥2, Proposition 12 bounds selected origin values, differentiated unweighted terms, and low-order weighted Hessians, conditional on certifying finitely many point functionals and operators.Once k is fixed, the index set of weighted operators is finite, so every constant belongs to a finite certificate.Source: §B.6 · pp. 58–59

B.6.1 Certification setup and singular-integral conventions

• Streamfunction quantities are rewritten as source functionals or integral operators, then bounded in weighted norms and converted to E0, Hk, or Ek.Reduced principal values inherit their prescription from the five-dimensional integral; the distributional Hessian also has a local term -δijδ0/5.Source: §B.6.1 · p. 60

B.6.2 Constants to be certified

• The certificate groups constants for streamfunction values at the origin, low-order weighted Hessians, high-order weighted terms, and differentiated unweighted L2 estimates.It also stores constants for profile-multiplied streamfunction terms.Source: §B.6.2 · p. 61

B.6.3 Reduced kernel and complete second-derivative operators

• For the reduced Hessian, diagonal zz carries a local -1/5 source term while mixed zr has none; Proposition 13 supplies axis-weighted bounds for both operators.The local contribution is part of the complete zz operator and should not be added separately.Source: §B.6.3 · pp. 63–64
• Geometric shell tails and comparable-shell estimates yield an ℓ1 kernel bound, extending the operator estimate by continuity from finite-shell functions.The extension proves (343).Source: §B.6.3 · pp. 66–67
• Plancherel’s theorem gives the Hessian constants κzz = 4/5 and κzr = 1/2.These constants complete the proof of (340).Source: §B.6.3 · p. 67

B.6.4 Point constants

• The origin values entering the modulation equations are bounded using weighted dual norms, and their resulting low-order constants are stored.For direct origin kernels, the high-order coefficients are zero because only the weighted low-order norm of δω is used.Source: §B.6.4 · p. 68

B.6.5 Weighted operator constants and block bounds

• Certified block-pair bounds combine through a finite matrix C whose ℓ2 norm gives a global weighted operator bound.Each entry cab controls the contribution from input block Db to output block Da.Source: §B.6.5 · pp. 69–70
• Diagonal block pairs use principal-value estimates and coefficient-weight conversion, while accounting for the local Lzz term absent from Lzr.Unbounded blocks or nonuniform weight ratios are subdivided into dyadic annuli and their interactions are summed.Source: §B.6.5 · pp. 70–71
• For separated tail blocks, a denominator lower bound and interval-enclosed numerator yield a recursive certified tail majorant.The pointwise bound is inserted into the separated-block estimate or the corresponding analytic tail integral.Source: §B.6.5 · p. 71

B.6.6 Converting source derivatives to energy norms

• Endpoint source-derivative norms fit directly into low- or top-order energy, while intermediate orders use interpolation coefficients to convert them.The conversion also accounts for the sum of top-order two-dimensional derivatives and uses E0 ≤ Ek.Source: §B.6.6 · p. 72

B.6.7 Low-order profile-multiplied terms

• Low-order profile-multiplied rows are reduced to finite source-vorticity terms, retaining cancellations in combined velocity expressions before applying bounds.Complete Hessian identities include the local −δω/5 term for the zz case; extra z-derivatives are transferred to the source.Source: §B.6.7 · p. 73

B.6.8 High-order streamfunction terms

• High-order rows reduce to direct source derivatives, complete zz or zr Hessian operators, or radial-transfer terms, then sum their certified bounds with energy-conversion factors.For 3∂r + r∂rr, the elliptic equation first converts the expression into a direct source term and a zz Hessian term.Source: §B.6.8 · pp. 74–75

B.6.9 The differentiated unweighted constant Cdiff

• The differentiated unweighted constant Cdiff collects bounds for derivatives of the streamfunction of orders 2 through k + 2 from source derivatives two orders lower.Its reduction uses complete zz and zr identities where available and radial-transfer identities otherwise, grouping contributions by source derivative.Source: §B.6.9 · p. 76

B.6.10 Proof of the streamfunction elliptic estimates

• Assuming certification of the point functionals and finite weighted operators, Proposition 12 yields origin point estimates, differentiated unweighted control, and low-order and differentiated weighted elliptic bounds.The differentiated unweighted bound uses the constant Cdiff; the differentiated weighted estimate follows from finite row-by-row contributions.Source: §B.6.10 · pp. 77–79

B.7 Modulation constants

• The modulation coefficients are linear terms in the linear operator, with no fixed-profile modulation contribution added to the nonlinear operator.Source: §B.7 · p. 80

B.8 Ray estimate and global pointwise control

• The section introduces a ray estimate for fixed-profile linear terms involving undifferentiated δu and global pointwise bounds; the required origin values are δψ0 and (∂zδψ)0.Source: §B.8 · p. 81

B.8.1 Ray estimate for fixed-profile terms

• For functions vanishing at the origin, Proposition 15 bounds fixed-profile rows containing undifferentiated δu using radial and vertical derivative norms; global δu control is separate.Source: §B.8.1 · p. 81

B.8.2 Global pointwise estimate

• Under positive lower bounds on low-order weights and the velocity weights’ far-field growth condition, Proposition 16 derives factor-specific pointwise estimates from weighted energy.Source: §B.8.2 · p. 82

The global velocity and streamfunction factors satisfy

• The pointwise bounds yield cubic estimates by placing one perturbative factor in L∞ with size O(Ek) and the other two in weighted L2; they also control origin values entering δC and δcu.Because both modulation coefficients are linear, their bounds enter linear modulation terms and the quadratic products already present in the nonlinear equations.Source: The global velocity and streamfunction… · p. 85

Appendix C. Low-order linear estimate

• The low-order linear estimate keeps transport and selected zeroth-order couplings in a signed symmetric 3 × 3 form certified by matrix damping, while separately estimating the 2ū coupling and remaining terms.Source: Appendix C · p. 87

C.1 Splitting the low-order linear operator

• The low-order linear pairing separates transport from non-transport terms in each component; δC and δcu enter the linear operator in full because they are exactly linear.Source: §C.1 · p. 87
• Direct terms are grouped by whether they contain undifferentiated δu, δvz, δψ or its derivatives, or δC and δcu.These groups use Proposition 15, weighted profile and pointwise bounds, weighted elliptic estimates, and linear modulation bounds, respectively.Source: §C.1 · p. 88

C.2 Low-order linear estimate

• The low-order linear estimate combines one global matrix bound with bounds for the remaining direct terms.The theorem is established after weighted integration by parts.Source: §C.2 · p. 89

Assume also that each direct label satisfies the term bound

• The matrix part comprises transport terms and five labels, with signed axial transport retained and diagonal labels added to the corresponding matrix entries.Boundary terms vanish under the admissibility, boundary-flux, and axis-parity hypotheses; density extends the identity to the weighted class.Source: Assume also that each direct label… · pp. 89–90
• Each direct label is estimated using Cauchy–Schwarz and, when its coefficient is positive, a balancing constant with Young’s inequality; the terms are then summed.The summed direct-term estimate is added to the matrix certificate.Source: Assume also that each direct label… · p. 90

R1: Terms proportional to δu

• Rule R1 treats Bω,2, Br,3, and Bz,3 as terms proportional to δu with a fixed profile coefficient, using Proposition 15.Source: §C.3 · p. 90

R2: Direct vorticity–z coupling

• Rule R2 handles the direct vorticity–z coupling using weighted Hölder and Proposition 16, with its low- and high-order costs recorded among the direct losses.Source: §C.3 · p. 91

R3: Streamfunction terms

• Rule R3 certifies each streamfunction row’s weighted operator jointly with its multiplier and target weight, avoiding a separate universal weight-comparison constant.Appendix B.6.7 denotes the resulting low- and high-order row constants by K0_i(a, T) and Kk_i(a, T).Source: §C.3 · p. 91

R4: Linear modulation terms

• Rule R4 handles linear modulation terms aδC or aδcu by combining the scalar modulation bound with the weighted norm of the fixed coefficient.Source: §C.3 · p. 91

C.4 Explicit numerical certificate

• The standard route forms the symmetric matrix ML from the transport contribution and selected matrix labels, then certifies damping on the full half-plane by finite-box enclosure and tail closure.The labels are given in (527), and the tail closure is in Appendix C.4.2.Source: §C.4 · p. 91
• After either matrix route is fixed, the remaining direct terms yield losses A0 L and Ak L; L is matrix damping, and the losses correspond to low- and high-order estimates.The direct terms are in (529)–(531); the final constants are stated for the standard global-matrix case.Source: §C.4 · p. 92

C.4.1 Matrix construction

• Only transport terms and terms in SL enter the (ω, r, z) matrix; remaining terms are reserved for the direct-term estimate.The constant modulation offset cu,res is absorbed into the reference amplitude coefficient and contributes to zeroth-order linear coefficients.Source: §C.4.1 · p. 92
• The transport coefficients are Gr=λr+ū_r and Gz=λz+C̄+ū_z, with ū_r=−r∂zψ̄ and ū_z=2ψ̄+r∂rψ̄.Source: §C.4.1 · p. 92
• The transport diagonal uses ∂rū_z=3∂rψ̄+r∂rrψ̄ and ∂zū_z=2∂zψ̄+r∂rzψ̄, alongside derivatives of Gr and Gz and weighted log-Φi gradients.Source: §C.4.1 · p. 92
• Each listed r–z coupling is split equally across the symmetric off-diagonal entries, but Bω,3=2ūδvz stays outside because its multiplier may not be finite.The coupling coefficients retain the weight conversion required by their source and target components.Source: §C.4.1 · p. 93
• Damping certification combines the finite-box enclosure with a tail estimate, with any exceptional region of positive measure handled in Appendix C.4.3.Source: §C.4.1 · p. 93

C.4.2 Tail closure for the matrix damping bound

• If the profile and derivatives entering ML vanish outside the numerical box, the tail matrix is diagonal because selected cross-couplings vanish, leaving the residual amplitude offset.Its diagonal entries are given by (571).Source: §C.4.2 · p. 93
• The tail eigenvalue bound reduces to a scalar condition for each weight; combining it with the finite-box bound yields a global matrix damping constant.The profile-dependent constant C̄ remains symbolic until the numerical certificate is evaluated.Source: §C.4.2 · pp. 93–94
• For exponential or algebraic radial decay, cu,res < 1 and Rbox > 2|C̄| ensure any 0 < γtail < 1 − cu,res works.The decay profiles considered are Cfloor + a exp(−bρ^p) and Cfloor + aρ^−p, respectively.Source: §C.4.2 · pp. 94–95
• Algebraically growing radial weights require p < 2(1 − cu,res); for r and z weights also requiring p ≥ 1, compatibility as Rbox → ∞ requires cu,res < 1/2.The strict finite-box inequality leaves room to choose γtail > 0.Source: §C.4.2 · pp. 95–96
• Positive exponential growth of the radial weights makes the scalar tail expression unbounded as ρ → ∞, so the tail certificate cannot hold.The summary of radial model rates likewise marks exponential growth as not possible.Source: §C.4.2 · p. 95

Localized matrix certificate

• A pointwise matrix-margin failure is harmless in isolation; finitely many neighborhoods without uniform damping are allowed when their weighted energy concentration is quantitatively controlled.Small size alone is insufficient because an L2 perturbation can concentrate most of its mass in an arbitrarily small set.Source: §C.4.3 · p. 96
• The localized pieces are bounded and separated from the normalized origin, which is handled separately by the weighted matrix estimate with Gr(0, 0) = Gz(0, 0) = 0.Source: §C.4.3 · p. 96
• The certificate requires damping outside the pieces and concentration bounds inside them; localized low-order energy reduces damping, while top-order energy adds a loss.On each non-damping piece, the matrix may lose damping or produce bounded growth; the localized estimate lowers the damping margin and adds a top-order term.Source: §C.4.3 · pp. 96–97
• Closure requires the low-order concentration losses to leave positive damping and the added top-order loss to be absorbed by the differentiated linear estimate.If the complete high-order matrix fails to damp on a neighborhood, the localization argument cannot simply be repeated at order k; a separate top-order coercive estimate is required.Source: §C.4.3 · pp. 97–98
• Because each piece stays away from the origin, its weights are bounded and ordinary local estimates can establish concentration control; shrinking pieces helps only if weight suprema and pointwise constants remain controlled.The certificate closes when the concentration estimate, positive low-order margin, and complete differentiated matrix certificate are verified with the same µk satisfying both inequalities.Source: §C.4.3 · pp. 98–99

Undifferentiated velocity labels

• For the undifferentiated velocity labels (ω, 2), (r, 3), and (z, 3), Proposition 15 is applied with the corresponding fixed coefficient and target energy weight.Source: §C.4.4 · p. 99

Direct vorticity–z coupling

• The direct vorticity–z coupling stays outside the signed matrix because the required bound is not implied by independent singularity rates; it instead contributes to direct losses, not the matrix eigenvalue.The estimate keeps ū in the Φω norm and uses a pointwise estimate for δvz.Source: §C.4.4 · p. 99

Streamfunction labels

• Each streamfunction term has the form a T(Γ5 * δω); when a multiplier is split into scalar summands, the certified K-constants are added.Source: §C.4.4 · p. 100

Modulation labels

• Modulation terms are built from linear modulation bounds, with origin evaluation constants certified for s = 0, k.The labels are (ω, 7), (ω, 8), (r, 9), (r, 10), (z, 9), and (z, 10).Source: §C.4.4 · p. 100

C.4.5 Assembly

• The localized matrix certificate updates the low-order constants while preserving the form of the low-order linear estimate.The assembly also identifies the direct-term set as the complement of five matrix labels within the non-transport list.Source: §C.4.5 · p. 101

Appendix D. High-Order Linear Estimate

• Terms with exactly one derivative on a transport coefficient remain top order, while terms with at least two such derivatives enter the remainder.The nonlocal linear terms are controlled by streamfunction estimates.Source: Appendix D · p. 102

4. Conclude the estimate. Combining (657) and (649) gives

• Summing certified remainder bounds yields (649), closing the estimate when all differentiated linear terms outside the matrix satisfy that bound.This conclusion follows after the complete signed matrix has been extracted.Source: Appendix D · p. 104, §2 · p. 106

Appendix D. High-Order Linear Estimate

• Theorem 8 states the high-order linear estimate assuming the damping certificate (648) and the bounds in (649).The estimate is conditional on both requirements.Source: Appendix D · p. 104

2. Compute the signed top-order form. For each i, q, weighted integration by parts gives

• The complete signed top-order form is extracted before absolute-value bounds are applied, retaining first-commutator contributions.Even where the transport field vanishes, weight-gradient terms vanish but first-commutator terms involving its gradient remain.Source: §2 · pp. 105–106

Appendix E. Low-Order Nonlinear Estimate

• Transport nonlinearities use weighted integration by parts, while non-transport products use weighted Hölder with two weighted L2 factors and a remaining multiplier bounded by O(Ek).Pointwise, streamfunction, and modulation estimates control the multiplier.Source: Appendix E · p. 107
• The modulation coefficients are exactly linear in the perturbation and belong to the linear operator, leaving no fixed-profile modulation sources in the nonlinear operator.The coefficients are δC = −2δψ0 and δcu = −2(∂zδψ)0.Source: Appendix E · p. 107
• Theorem 9 states a low-order nonlinear estimate for the nonlinear terms.The excerpt describes the bound but does not provide its formula.Source: Appendix E · p. 107

Appendix F. High-Order Nonlinear Estimate

• Weighted integration by parts removes the only potential derivative loss in the principal transport estimate.The apparent loss comes from differentiating the transport factor; the remaining terms are estimated using two weighted L2 factors and a combined L∞ multiplier.Source: Appendix F · pp. 109–110
• Transport commutators are bounded by splitting at |β| ≤ k − 2: lower-order factors go in L∞, while the high-derivative factor stays in weighted L2.For |β| ≥ k − 1, the complementary factor is placed in L∞; k ≥ 4 supplies the additional derivatives needed for the H2 → L∞ bound.Source: Appendix F · p. 110
• Each non-transport source-product summand is bounded by C(3)E_k^3 after selecting its maximal-order perturbative spatial factor.Fixed profiles use certified pointwise bounds, and streamfunction factors are reduced using Proposition 12; fixed-profile quadratic modulation terms are absent because their contributions are included in the linear operator.Source: Appendix F · pp. 110–111
• For fixed k, summing the finitely many transport, commutator, and source-product summands gives a high-order nonlinear estimate with certified nonnegative constants.The theorem assumes k ≥ 4 and the standing certified product, interpolation, elliptic, modulation, and profile bounds.Source: Appendix F · pp. 109, 111

Appendix G. Proofs of the Stability Theorem

• If E_k(0) < δ* and the certified estimates apply, every solution remains in the energy ball E_k(t) < δ* for as long as it exists.The theorem assumes the perturbation equations hold for admissible perturbations and that the required estimates are certified with finite constants.Source: Appendix G · p. 112
• The energy estimate combines low-order pairings with (δω, ∂rδu, ∂zδu) and kth-order pairings weighted by μ_k.The proof adds the low- and high-order estimates, multiplying the high-order estimate by μ_k before combining the nonlinear and residual bounds.Source: Appendix G · p. 113
• The proof establishes forward invariance by contradiction, showing that a first boundary contact would conflict with the energy inequality.It assumes an initial energy below δ*, considers the first boundary-contact time, and derives a contradiction from the left derivative and the inequality at contact.Source: Appendix G · p. 113