Other material · A dividing-plane barrier in the OpenAI forced Navier-Stokes blow-up construction
The ledger as data, version 1.0, September 30, 2026
The first version of the ledger (see ledger.md) in machine-readable form, generated on September 30, 2026, and kept frozen as exactly what the three small open models of Hypnos, the research harness this site describes (Gemma 4 31B, Gemma 4 26B and Qwen3 32B), were shown in a one-time test on the manuscript's moves with the reasons withheld: in 16,018 lines of their output, graded blind by Claude Opus 5.5 sessions, they never recovered the reason for a move. It is shown here in pages of whole records.
- Written by
- Claude Opus sessions and Claude Fable 5.1 (Anthropic)
- Size
- 897,753 bytes
- SHA-256
f2f7a98d815175f32ec70f1d694bf138920b250608d0376a13191fe89b8120a2
The note's pageEvery file published with itThis file on GitHub
{
"id": "M7.3",
"kind": "move",
"name": "ns-m7-3-principal-amplitude-equation-and-pressure-eliminating",
"title": "Principal amplitude equation and pressure-eliminating projection",
"section": "7",
"pages": "75",
"refs": [
"p. 75",
"(7.5), (7.6), (7.7), (7.8)",
"omitted terms in (9.1), (9.2), pp. 101 to 102."
],
"statement": "For a harmonic tm e^{ikmΦ} with source coefficient fm, find tm ∈ C^3 and πm ∈ C with nΦ·tm = 0 and (7.5): t'm + Ktm + m^2 d tm + ikm nΦ πm = -fm, d = εk^2|nΦ|^2, where (7.6) K has rows (0, -2F, 0), (2F + R∂RF, 0, 0), (∂RG, 0, 0) in the order (r, θ, z), and AΦ = -K + nΦ(nΦ^T K - (n'Φ)^T)/|nΦ|^2 is the projected evolution operator. The explicit coordinates (7.7) Ka, Na, sa and the frame (7.8) U = [er - saKa, Na], B = U M for the plane orthogonal to nΦ are defined here.",
"description": "For a harmonic tm e^{ikmΦ} with source coefficient fm, find tm ∈ C^3 and πm ∈ C with nΦ·tm = 0 and (7.5): t'm + Ktm + m^2 d tm + ikm nΦ πm = -fm, d = εk^2|nΦ|^2, where (7.6) K has rows (0, -2F, 0), (2F + R∂RF, 0, 0), (∂RG, 0, 0) in the order (r, θ, z), and AΦ = -K + nΦ(nΦ^T K - (n'Φ)^T)/|nΦ|^2 is the projected evolution operator. The explicit coordinates (7.7) Ka, Na, sa and the frame (7.8) U = [er - saKa, Na], B = U M for the plane orthogonal to nΦ are defined here. OBLIGATION: Cancels the principal part of the linearized residual L_{uB}(w, π) for every harmonic of every. ANTECEDENT: Section 7 cites nothing. The introduction (p. 2) names Lifschitz-Hameiri [17] and Friedlander-Vishik [14] for polarization evolution along a background flow and Craik-Criminale [9] and Singh-Sridhar [19] for exact viscous shearing waves. (Digest's observation, not in the manuscript: when F = 0 and G = G(R), (7.4) gives n'Φ = -K^T nΦ, and AΦ reduces to -K + 2nΦ nΦ^T K/|nΦ|^2, the Craik-Criminale amplitude operator for a frozen shear; with swirl, the connection terms break n'Φ = -K^T nΦ, which is why the projection is written with n'Φ explicitly.) REFS: p. 75; (7.5), (7.6), (7.7), (7.8);",
"obligation": "Cancels the principal part of the linearized residual L_{uB}(w, π) for every harmonic of every label: transport in the pulse coordinate, coupling to the base shear and to the rotating cylindrical frame, and the viscous term with both derivatives on the exponential. Without it the linear term of the exact increment identity R(uB + w, pB + π) = R(uB, pB) + L_{uB}(w, π) + ∇·(w ⊗ w) (Section 3.3) would be as large as the wave itself.",
"backward_question": "What is the smallest linear equation along a pulse that keeps base transport, the shear and frame-rotation coupling, and viscous damping, and removes the pressure so that the amplitude stays orthogonal to the phase gradient?",
"mechanism": "Freeze the slow variables and follow the pulse coordinate; at leading order the amplitude sees the base only through its gradient and the frame rotation. K is the linearization of cylindrical advection about (0, RF, G): the entries -2F and 2F collect the connection terms (radial motion rotates the tangential frame) together with the base swirl, while R∂RF and ∂RG are the radial shears. Viscosity gives εk^2 m^2|nΦ|^2 because both derivatives fall on the exponential. Pressure enters only through its gradient ikm nΦ πm, which is normal to the admissible plane; differentiating nΦ·tm = 0 along v and solving for πm removes it and yields AΦ, whose extra term -nΦ(n'Φ)^T/|nΦ|^2 accounts for the rotation of that plane as the phase normal tilts. Slow transport, the defect Eik, and amplitude derivatives are deliberately left out and estimated in Proposition 9.1.",
"antecedent": "Section 7 cites nothing. The introduction (p. 2) names Lifschitz-Hameiri [17] and Friedlander-Vishik [14] for polarization evolution along a background flow and Craik-Criminale [9] and Singh-Sridhar [19] for exact viscous shearing waves. (Digest's observation, not in the manuscript: when F = 0 and G = G(R), (7.4) gives n'Φ = -K^T nΦ, and AΦ reduces to -K + 2nΦ nΦ^T K/|nΦ|^2, the Craik-Criminale amplitude operator for a frozen shear; with swirl, the connection terms break n'Φ = -K^T nΦ, which is why the projection is written with n'Φ explicitly.)",
"cost": "Pressure coefficients of relative size ε^{1/2} (factor (km)^{-1}); the non-principal linear terms are postponed to (9.2) and Proposition 9.1, where their common gain is at least 1/2 - 3κs.",
"checkable": "(a) For random smooth nΦ(v) with |nΦ| bounded below, sample (F, R∂RF, ∂RG), and a random source f(v), integrate (7.13) from tm(0) = 0; confirm nΦ·tm stays at round-off and that (tm, πm), with πm from (7.13), satisfies (7.5) to round-off. (b) With F = 0, G = G(R), nΦ,z = pz, confirm n'Φ = -K^T nΦ and AΦ = -K + 2nΦ nΦ^T K/|nΦ|^2 numerically. (c) Symbolically linearize cylindrical advection (u·∇)u about (0, RF(R), G(R)) for a perturbation a e^{ikmΦ} with θ-independent a, and confirm the terms without derivatives of a (other than the phase transport) equal Ka.",
"depends_on": [
"M7.2",
"M5.14",
"M6.6",
"M7.1",
"ME.3"
],
"constrains": [],
"reasons": {
"M7.2": "The harmonic e^{ikmΦ} uses the phase Φ, its normal n_Φ and the carrier k, and viscosity εk²m²|n_Φ|² comes from both derivatives on the exponential.",
"M5.14": "K is the linearization of cylindrical advection about the background, with entries from its swirl F and shears R∂_R F, ∂_R G.",
"M6.6": "The prime is the derivative in the pulse coordinate v, which advances at unit speed under the normalized time derivative.",
"M7.1": "The frame (7.8), B = UM, is built from the shear frame N, K and eigen-directions involving c0.",
"ME.3": "Its amplitude equation (7.5) uses A_Phi = -K + n_Phi(n_Phi^T K - n_Phi'^T)/|n_Phi|^2, the pressure-projected operator of (2.4), with viscous damping added."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 75"
},
{
"id": "M7.4",
"kind": "move",
"name": "ns-m7-4-moving-frame-and-reference-diagonalization-lemma-7-1",
"title": "Moving frame and reference diagonalization (Lemma 7.1)",
"section": "7",
"pages": "75-77",
"refs": [
"pp. 75 to 77",
"(7.7), (7.8), (7.9), (7.10), (7.11)."
],
"statement": "Lemma 7.1: on 0 < q < q∗, with one q∗ for all labels and derivative orders, B of (7.8) maps C^2 onto {t : nΦ·t = 0}, has a uniformly bounded left inverse Bℓ, and (7.10): Bℓ(AΦB - B') = diag(λ, -λ) + E, λ(v) = λ0/√(1 + s(v)^2), |E| ≤ C/S∗; and (7.11): |d - dref| ≤ C/S∗ with dref = εk^2 Bs^2(1 + s^2). All fixed derivatives of nΦ and of the frames have polynomial bounds in S∗.",
"description": "Lemma 7.1: on 0 < q < q∗, with one q∗ for all labels and derivative orders, B of (7.8) maps C^2 onto {t : nΦ·t = 0}, has a uniformly bounded left inverse Bℓ, and (7.10): Bℓ(AΦB - B') = diag(λ, -λ) + E, λ(v) = λ0/√(1 + s(v)^2), |E| ≤ C/S∗; and (7.11): |d - dref| ≤ C/S∗ with dref = εk^2 Bs^2(1 + s^2). All fixed derivatives of nΦ and of the frames have polynomial bounds in S∗. OBLIGATION: Reduces the constrained 3D amplitude equation to a 2D ODE whose undamped part is diagonal up to O(1/S∗), with explicit rates ±λ and a scalar damping. This is what yields the propagator bound (7.19), the pinned polarization of Lemma 7.4, and hence the covariance directions in (7.28). MECHANISM: At the reference normal nref = Bs(s, K) write t = x(er - sK) + yN. Using g0 = |g0|N and K·g0 = 0, one finds e·(-K0e) = 0, e·(-K0N) = 2F0Nθ, N·(-K0e) = -(2F0Nθ + |g0|) for e = er - sK, so the undamped reference matrix in (x, y) is off-diagonal, with entries 2F0Nθ/(1 + s^2) and -(2F0Nθ + |g0|). ANTECEDENT: None cited. REFS: pp. 75 to 77; (7.7), (7.8), (7.9), (7.10), (7.11).",
"obligation": "Reduces the constrained 3D amplitude equation to a 2D ODE whose undamped part is diagonal up to O(1/S∗), with explicit rates ±λ and a scalar damping. This is what yields the propagator bound (7.19), the pinned polarization of Lemma 7.4, and hence the covariance directions in (7.28).",
"backward_question": "Is there a frame on the plane orthogonal to the moving phase gradient in which the undamped evolution is diagonal up to O(1/S∗), with explicit rates ±λ(v), uniformly over bands?",
"mechanism": "At the reference normal nref = Bs(s, K) write t = x(er - sK) + yN. Using g0 = |g0|N and K·g0 = 0, one finds e·(-K0e) = 0, e·(-K0N) = 2F0Nθ, N·(-K0e) = -(2F0Nθ + |g0|) for e = er - sK, so the undamped reference matrix in (x, y) is off-diagonal, with entries 2F0Nθ/(1 + s^2) and -(2F0Nθ + |g0|). Its eigenvalues are ±λ0/√(1 + s^2) = ±λ and its eigenvectors are the columns (1, ±c0√(1 + s^2)) of M in (7.8): tilting cuts the growth rate by the factor (1 + s^2)^{-1/2}. The actual frame (Ka, Na, sa) differs from the reference by O(1/S∗), and the moving-plane term and B' are O(1/S∗) because n'Φ and s' are. Denominators |nΦ,tan| and det M = -2c0√(1 + s^2) stay bounded below once S∗^2(ε + ε^2 + k^{-1}) ≤ 1 and the phase-normal error is below half the lower bound of Bs; higher derivatives impose no further smallness, so one q∗ serves every derivative order.",
"antecedent": "None cited.",
"cost": "A single threshold q∗ (a lower bound on the band index ℓ); frame and damping errors of size C/S∗ that, integrated over Ls ≍ S∗, cost only bounded factors; derivative bounds with polynomial growth in S∗.",
"checkable": "Build K0 from sample (F0, g0); confirm the three scalar products above, that the 2 × 2 reference matrix has eigenvalues ±λ0/√(1 + s^2) with eigenvectors equal to the columns of M, and det M = -2c0√(1 + s^2). Then, with the actual nΦ(v) from M7.2, form U, M, B, Bℓ and compute max over v of |Bℓ(AΦB - B') - diag(λ, -λ)| and of |d - dref| for ℓ = 10, 20, 40; confirm decay like ℓ^{-2}.",
"depends_on": [
"M7.3",
"M7.2",
"M7.1",
"ME.14",
"L.9",
"L.10"
],
"constrains": [],
"reasons": {
"M7.3": "Diagonalizes the projected operator A_Φ in the frame B of (7.8) and compares the damping d = εk²|n_Φ|² with its reference value.",
"M7.2": "Uses |n_Φ − Bs(s(v), K)| + |n′_Φ| ≤ C/S* from (7.9) to bound the frame and damping errors by C/S*.",
"M7.1": "The reference rates ±λ0/√(1+s²) and eigenvectors (1, ±c0√(1+s²)) come from λ0, c0 and the frame N, K at the representative.",
"ME.14": "Its moving frame of the plane orthogonal to n_Phi reduces the dynamics to diag(lambda, -lambda) + E, |E| <= C/S*, as ME.14 reduces (2.4) to an ideal model with small errors.",
"L.9": "Pulses are, at leading order, transverse plane waves like the exact Craik-Criminale waves on affine flows; Lemma 7.1 gives their dynamics in a moving frame.",
"L.10": "Lemma 7.1 gives the pulse's phase and amplitude dynamics along the base flow, equations of the [17, 14] kind for wavevectors and polarizations."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 75-77"
},
{
"id": "M7.5",
"kind": "move",
"name": "ns-m7-5-gaussian-pulse-envelope-from-balanced-growth-and-damping",
"title": "Gaussian pulse envelope from balanced growth and damping",
"section": "7",
"pages": "77-78",
"refs": [
"pp. 77 to 78",
"(7.12), (7.16)",
"(6.16) for ψ."
],
"statement": "(7.12): P(v) = exp(∫ from Ls/2 to v of (λ(w) - dref(w)) dw). The net rate anet(y) = λ0/√(1 + y^2) - λ0(1 + y^2)/(1 + u∗^2)^{3/2}, y = |s(v)|, vanishes at y = u∗; its v-derivative lies between -C/Ls and -c/Ls; hence (7.16): e^{-C(v-Ls/2)^2/Ls} ≤ P(v) ≤ e^{-c(v-Ls/2)^2/Ls} ≤ 1 (proof of Proposition 7.2, Step 1, p. 78).",
"description": "(7.12): P(v) = exp(∫ from Ls/2 to v of (λ(w) - dref(w)) dw). The net rate anet(y) = λ0/√(1 + y^2) - λ0(1 + y^2)/(1 + u∗^2)^{3/2}, y = |s(v)|, vanishes at y = u∗; its v-derivative lies between -C/Ls and -c/Ls; hence (7.16): e^{-C(v-Ls/2)^2/Ls} ≤ P(v) ≤ e^{-c(v-Ls/2)^2/Ls} ≤ 1 (proof of Proposition 7.2, Step 1, p. 78). OBLIGATION: Provides the pointwise envelope weight Pv in the wave class W_{α} of (6.29); the exponential smallness at both pulse ends that makes the temporal cutoff errors flat (M7.13); and the concentration of x^2 ψ^2 near the midpoint that fixes the covariance direction in (7.28). MECHANISM: The choice of Bs in (7.2) gives dref = λ0(1 + s^2)/(1 + u∗^2)^{3/2}, so λ - dref vanishes exactly where |s| = u∗, at the midpoint v = Ls/2. As |s(v)| increases linearly across [u∗/2, 3u∗/2], the growth rate λ0/√(1 + s^2) falls and the damping rises, so the net rate decreases at a rate of order 1/Ls: log P is concave, equal to 0 with zero slope at the midpoint, with second derivative of order -1/Ls. ANTECEDENT: None cited (described physically in Section 2.2, p. 6, and Figure 3(b), p. 9). REFS: pp. 77 to 78; (7.12), (7.16); (6.16) for ψ.",
"obligation": "Provides the pointwise envelope weight Pv in the wave class W_{α} of (6.29); the exponential smallness at both pulse ends that makes the temporal cutoff errors flat (M7.13); and the concentration of x^2 ψ^2 near the midpoint that fixes the covariance direction in (7.28).",
"backward_question": "Can the wavevector magnitude be tuned so that growth minus damping vanishes exactly at the pulse midpoint and decreases at a rate of order 1/Ls, making the envelope Gaussian and exponentially small at both ends?",
"mechanism": "The choice of Bs in (7.2) gives dref = λ0(1 + s^2)/(1 + u∗^2)^{3/2}, so λ - dref vanishes exactly where |s| = u∗, at the midpoint v = Ls/2. As |s(v)| increases linearly across [u∗/2, 3u∗/2], the growth rate λ0/√(1 + s^2) falls and the damping rises, so the net rate decreases at a rate of order 1/Ls: log P is concave, equal to 0 with zero slope at the midpoint, with second derivative of order -1/Ls. Integrating twice gives a Gaussian of width √Ls. With Ls ≍ S∗ = ℓ^2 the envelope at the ends is e^{-cS∗}, so each pulse is amplified by a factor e^{cS∗} from start to midpoint; this is the grow-then-decay picture of Section 2.2 and Figure 3(b).",
"antecedent": "None cited (described physically in Section 2.2, p. 6, and Figure 3(b), p. 9).",
"cost": "Every wave bound carries the factor Pv; responses are compared with P only up to polynomial factors of S∗; each pulse lasts Ls ≍ S∗ in the pulse coordinate.",
"checkable": "For fixed λ0, u∗ and Ls = 10, 10^2, 10^3, 10^4, compute log P(v) by quadrature of anet(|s(v)|) with s(v) = u∗/2 + u∗v/Ls. Confirm anet(u∗) = 0; that -log P(v)·Ls/(v - Ls/2)^2 stays in one interval [c, C] independent of Ls; and that the log of max{P(v) : |v - Ls/2| ≥ Ls/5} is at most -c'Ls.",
"depends_on": [
"M7.4",
"M7.2",
"M6.6",
"ME.15",
"L.1",
"L.2",
"L.3"
],
"constrains": [],
"reasons": {
"M7.4": "The envelope integrates the reference growth rate λ(v) minus the reference damping d_ref(v) of Lemma 7.1.",
"M7.2": "The choice of Bs in (7.2) makes growth equal damping at |s| = u*, and the linear tilt s(v) makes the net rate fall at rate order 1/L_s.",
"M6.6": "P(v) lives on the pulse interval 0 ≤ v ≤ L_s with L_s ≍ S*, which sets the Gaussian width √L_s.",
"ME.15": "The envelope P(v) = exp(integral (lambda - d_ref)) quantifies transverse growth like ME.15's exp(b0/sqrt(beta)), but viscous damping then makes each pulse decay.",
"L.1": "Shares the dynamical amplification of [6]: the background shear grows each pulse, whose Gaussian envelope comes from growth outpacing viscous damping until damping wins.",
"L.2": "The manuscript groups [8] with [6] as amplification across scales and says its construction also exploits dynamical amplification, here shear-driven pulse growth.",
"L.3": "Right after the successive amplification of oscillatory layers in [7], the manuscript says it also exploits dynamical amplification: oscillatory pulses grow, then decay, in the shear."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 77-78"
},
{
"id": "M7.6",
"kind": "move",
"name": "ns-m7-6-linear-inverse-for-harmonic-sources-proposition-7-2",
"title": "Linear inverse for harmonic sources (Proposition 7.2, Corollary 7.3)",
"section": "7",
"pages": "77-80",
"refs": [
"pp. 77 to 80",
"(7.13) to (7.15), (7.17) to (7.20)",
"(6.21), (6.22)",
"Corollary 7.3 on p. 80."
],
"statement": "Proposition 7.2: for harmonics 0 < |m| ≤ M and source coefficients fm that descend to a common torus H = Y_{i0}, are supported in the label's slow, transverse, and closed shell supports with smooth zero extension, and satisfy |D^I fm| ≤ CI ε^α S∗^{bI} √ζ δ^{-aI} P(v), there is a unique solution of (7.13): t'm = AΦtm - m^2 d tm - proj fm, tm(0) = 0, with πm = (i/(km))(nΦ·Ktm - n'Φ·tm + nΦ·fm)/|nΦ|^2 (proj = orthogonal projection onto the plane orthogonal to nΦ).",
"description": "Proposition 7.2: for harmonics 0 < |m| ≤ M and source coefficients fm that descend to a common torus H = Y_{i0}, are supported in the label's slow, transverse, and closed shell supports with smooth zero extension, and satisfy |D^I fm| ≤ CI ε^α S∗^{bI} √ζ δ^{-aI} P(v), there is a unique solution of (7.13): t'm = AΦtm - m^2 d tm - proj fm, tm(0) = 0, with πm = (i/(km))(nΦ·Ktm - n'Φ·tm + nΦ·fm)/|nΦ|^2 (proj = orthogonal projection onto the plane orthogonal to nΦ). OBLIGATION: This is the inverse applied in Step 1 of every correction cycle (Proposition 9.6) to cancel the principal part of each nonzero angular harmonic of the residual. It loses no power of ε (α is preserved), keeps the source's envelope and supports, absorbs the normal component of the source into the pressure, and descends to the common torus, so its output is again an admissible wave coefficient. Corollary 7.3 is what lets Lemma 9.7 put all finite stages on one domain. ANTECEDENT: None cited (the text names Duhamel's formula). REFS: pp. 77 to 80; (7.13) to (7.15), (7.17) to (7.20); (6.21), (6.22); Corollary 7.3 on p. 80.",
"obligation": "This is the inverse applied in Step 1 of every correction cycle (Proposition 9.6) to cancel the principal part of each nonzero angular harmonic of the residual. It loses no power of ε (α is preserved), keeps the source's envelope and supports, absorbs the normal component of the source into the pressure, and descends to the common torus, so its output is again an admissible wave coefficient. Corollary 7.3 is what lets Lemma 9.7 put all finite stages on one domain.",
"backward_question": "Can every later harmonic source be removed by one linear inverse on one fixed domain, with the response inheriting the source's size, envelope, support, and descent, and with higher harmonics only more damped?",
"mechanism": "Write tm = B zm. Damping is a scalar multiple of the identity, so the m-th propagator is the m = 1 propagator times exp(-(m^2 - 1)∫d), a factor at most one: higher harmonics are only more damped, and no smaller domain is needed as harmonics accumulate. For m = 1, ∂v|z| ≤ (λ - dref + C/S∗)|z|, and since Ls/S∗ is bounded this integrates to ||V1(v, w)|| ≤ C P(v)/P(w). In Duhamel's formula the factor P(w) in the source cancels the denominator, so the response carries P(v) times one factor Ls = O(S∗). Coefficient derivatives commute with ∂v and obey (7.20), handled by induction with polynomial losses in S∗. The solution runs along the path Hw of (6.21) on the common torus, which holds slow and transverse variables fixed, so uniqueness for zero data gives descent and support preservation without identifying values at distinct preimages. Finally (nΦ·tm)' = -m^2 d(nΦ·tm) propagates the constraint from zero data, and the pressure formula reproduces the normal part of (7.5).",
"antecedent": "None cited (the text names Duhamel's formula).",
"cost": "Constants and polynomial degrees depend on M, the derivative order, the source bounds, and the stage (never the domain); the solution has no temporal zero extension until multiplied by ψ (M7.13); every source must meet the support and descent hypotheses, which Proposition 9.3 re-verifies at each stage.",
"checkable": "Integrate z' = Am z + gm for m = 1 to 5 with a random smooth E of size 1/S∗, d = dref + O(1/S∗), and gm(w) = P(w)g̃(w), |g̃| ≤ 1. Compare (i) max over w ≤ v of ||Vm(v, w)||P(w)/P(v), which should stay bounded independent of m and Ls; (ii) Vm against exp(-(m^2 - 1)∫d)V1, equal to round-off; (iii) |zm(v)|/(Ls P(v)), bounded as Ls grows.",
"depends_on": [
"M7.3",
"M7.4",
"M7.5",
"M6.10",
"ME.7"
],
"constrains": [],
"reasons": {
"M7.3": "Inverts the principal amplitude equation (7.5), with the pressure removed by projection onto the plane orthogonal to n_Φ.",
"M7.4": "Writing t_m = Bz_m, the nearly diagonal frame system (7.10), (7.11) gives the m-uniform propagator bound (7.19).",
"M7.5": "The propagator bound ‖V_m(v, w)‖ ≤ C P(v)/P(w) is stated against the Gaussian envelope, whose factor P(w) in the source cancels.",
"M6.10": "Integrates along the pulse path H_w on the common torus, so zero-data solutions descend and keep supports without averaging over preimages.",
"ME.7": "Solves each phase harmonic's amplitude ODE with the pressure read off the n_Phi component and envelope-weighted bounds, as ME.7 does label by label with (3.29) and profile g."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 77-80"
},
{
"id": "M7.7",
"kind": "move",
"name": "ns-m7-7-homogeneous-primary-pulse-with-pinned-polarization-lemma",
"title": "Homogeneous primary pulse with pinned polarization (Lemma 7.4)",
"section": "7",
"pages": "80-81",
"refs": [
"pp. 80 to 81",
"(7.21)."
],
"statement": "Lemma 7.4: for each σ, the real solution t^h_σ = B(z+, z-)^T of (t^h_σ)' = AΦ t^h_σ - d t^h_σ with z+(0) = P(0), z-(0) = 0 (m = 1, pressure from (7.13) with f = 0), written t^h_σ = x(er - saKa) + yNa, satisfies (7.21): cP(v) ≤ x(v) ≤ CP(v) and y/x = c0√(1 + s(v)^2) + O(S∗^{-1}). Every fixed derivative is bounded by CI S∗^{bI} P(v); the homogeneous pressure has an extra factor ε^{1/2}.",
"description": "Lemma 7.4: for each σ, the real solution t^h_σ = B(z+, z-)^T of (t^h_σ)' = AΦ t^h_σ - d t^h_σ with z+(0) = P(0), z-(0) = 0 (m = 1, pressure from (7.13) with f = 0), written t^h_σ = x(er - saKa) + yNa, satisfies (7.21): cP(v) ≤ x(v) ≤ CP(v) and y/x = c0√(1 + s(v)^2) + O(S∗^{-1}). Every fixed derivative is bounded by CI S∗^{bI} P(v); the homogeneous pressure has an extra factor ε^{1/2}. OBLIGATION: Produces the primary waves used in Proposition 7.5: sourceless (their only forcing is the flat cutoff tail of M7.13), with radial amplitude comparable to P, and polarization pinned to the growing eigenvector of M7.4 through both growth and decay. The polarization ratio fixes the covariance direction; the lower bound x ≥ cP gives the positive scalars hσ. MECHANISM: The ratio r = z-/z+ solves the Riccati equation r' = E21 + (-2λ + E22 - E11)r - E12 r^2. The scalar damping cancels out of it, so r feels only the contraction rate 2λ ≥ 2cλ > 0, and the interval |r| ≤ Kb/S∗ is invariant for a fixed large Kb (±r' < 0 at r = ±Kb/S∗). ANTECEDENT: None cited. REFS: pp. 80 to 81; (7.21).",
"obligation": "Produces the primary waves used in Proposition 7.5: sourceless (their only forcing is the flat cutoff tail of M7.13), with radial amplitude comparable to P, and polarization pinned to the growing eigenvector of M7.4 through both growth and decay. The polarization ratio fixes the covariance direction; the lower bound x ≥ cP gives the positive scalars hσ.",
"backward_question": "Does a pulse started in the growing eigendirection keep that polarization through both growth and viscous decay, so its momentum-flux direction is predictable?",
"mechanism": "The ratio r = z-/z+ solves the Riccati equation r' = E21 + (-2λ + E22 - E11)r - E12 r^2. The scalar damping cancels out of it, so r feels only the contraction rate 2λ ≥ 2cλ > 0, and the interval |r| ≤ Kb/S∗ is invariant for a fixed large Kb (±r' < 0 at r = ±Kb/S∗). Then (log(z+/P))' = -(d - dref) + E11 + E12 r = O(1/S∗), which integrates over Ls ≍ S∗ to O(1), so z+ ≍ P on the whole interval, including the decaying half. Multiplying by M gives x = z+(1 + r) and y = c0√(1 + s^2) z+(1 - r).",
"antecedent": "None cited.",
"cost": "Seed amplitude P(0), of size e^{-cS∗}; polarization known only to O(1/S∗); homogeneous pressure of relative size ε^{1/2}.",
"checkable": "Integrate the homogeneous frame system from (z+, z-) = (P(0), 0) with random E and d - dref of size C/S∗, for Ls proportional to S∗ with S∗ = 10^2, 10^3, 10^4. Track r = z-/z+ (confirm |r| ≤ Kb/S∗), z+/P (confirm it stays in [c, C]), and y/x - c0√(1 + s(v)^2) (confirm O(1/S∗)).",
"depends_on": [
"M7.4",
"M7.5",
"M7.3",
"ME.16",
"L.1",
"L.2",
"L.3",
"L.9",
"L.10"
],
"constrains": [],
"reasons": {
"M7.4": "The Riccati equation for z_-/z_+ uses the frame rates ±λ and O(1/S*) errors, pinning the polarization to the growing eigenvector.",
"M7.5": "The pulse starts at z_+(0) = P(0), and the bounds cP ≤ x ≤ CP are stated against the envelope.",
"M7.3": "The primary pulse solves the homogeneous projected equation t′ = A_Φ t − d t, the m = 1 case of (7.5) with f = 0.",
"ME.16": "Keeps the exact homogeneous pulse within the envelope and pins its polarization up to O(1/S*), as ME.16 keeps the exact transverse solution near the ideal growing one.",
"L.1": "The amplified disturbance is a sourceless pulse held on the growing eigenvector; the manuscript shares the amplification of [6] but gives the disturbance a different role.",
"L.2": "Shear-amplified primary pulses fill the amplified-disturbance role of [6, 8], redirected to supplying a mean momentum flux on the collapsing vortex.",
"L.3": "The amplified disturbances are oscillatory pulses, as the layers of [7] were oscillatory, given the different role of carrying a mean momentum flux.",
"L.9": "Lemma 7.4 solves the amplitude equation of a transverse plane wave on the base shear, the wave dynamics for which Craik-Criminale [9] is listed as a precedent.",
"L.10": "Lemma 7.4 pins the pulse polarization to the growing eigenvector through growth and decay, the velocity-polarization evolution described by [17, 14]."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 80-81"
},
{
"id": "M7.8",
"kind": "move",
"name": "ns-m7-8-energy-transfer-identity-along-a-pulse",
"title": "Energy-transfer identity along a pulse",
"section": "7",
"pages": "81",
"refs": [
"p. 81",
"(7.22)."
],
"statement": "For the real homogeneous amplitude t, t·Kt = g·(tr(tθ, tz)) and (7.22): (1/2) d|t|^2/dv = -g·(tr(tθ, tz)) - εk^2|nΦ|^2|t|^2. At the representative point, with T = TN N + TK K, the energy transfer is -g0·T = -|g0|TN (p. 81).",
"description": "For the real homogeneous amplitude t, t·Kt = g·(tr(tθ, tz)) and (7.22): (1/2) d|t|^2/dv = -g·(tr(tθ, tz)) - εk^2|nΦ|^2|t|^2. At the representative point, with T = TN N + TK K, the energy transfer is -g0·T = -|g0|TN (p. 81). OBLIGATION: Not invoked by any later proof. It exposes the structure behind M7.1 and M7.9: a pulse that grows by extracting energy carries a flux with TN < 0, so the target must satisfy T0,∗·N < 0, while the covariance construction must also prescribe the energy-neutral component TK, which is why both components have to be matched. MECHANISM: Dotting t' = AΦt - dt with t, the normal (pressure) part of AΦt drops out because t is orthogonal to nΦ. In t·Kt the connection entries -2F and +2F cancel, leaving the contraction of the shear vector g with the flux vector tr(tθ, tz), the radial transport of azimuthal and axial momentum. Viscosity dissipates at rate εk^2|nΦ|^2, which grows as the tilt increases |nΦ|. ANTECEDENT: None cited in Section 7; it is the pulse-coordinate form of the energy identity for the homogeneous linearized model in Section 3.3 (p. 12). (Classically the Reynolds-Orr energy balance; the manuscript does not use that name.) REFS: p. 81; (7.22).",
"obligation": "Not invoked by any later proof. It exposes the structure behind M7.1 and M7.9: a pulse that grows by extracting energy carries a flux with TN < 0, so the target must satisfy T0,∗·N < 0, while the covariance construction must also prescribe the energy-neutral component TK, which is why both components have to be matched.",
"backward_question": "Where does the pulse's energy come from, and which component of its momentum flux is tied to that energy transfer?",
"mechanism": "Dotting t' = AΦt - dt with t, the normal (pressure) part of AΦt drops out because t is orthogonal to nΦ. In t·Kt the connection entries -2F and +2F cancel, leaving the contraction of the shear vector g with the flux vector tr(tθ, tz), the radial transport of azimuthal and axial momentum. Viscosity dissipates at rate εk^2|nΦ|^2, which grows as the tilt increases |nΦ|.",
"antecedent": "None cited in Section 7; it is the pulse-coordinate form of the energy identity for the homogeneous linearized model in Section 3.3 (p. 12). (Classically the Reynolds-Orr energy balance; the manuscript does not use that name.)",
"cost": "None.",
"checkable": "Verify t·Kt = g·(tr(tθ, tz)) for random t ∈ R^3 and random (F, R∂RF, ∂RG) (exact identity); verify that t·[nΦ(nΦ^T K - (n'Φ)^T)t] = 0 whenever nΦ·t = 0; along a numerical solution of t' = AΦt - dt, confirm (1/2) d|t|^2/dv + g·(tr(tθ, tz)) + εk^2|nΦ|^2|t|^2 = 0 to integration accuracy.",
"depends_on": [
"M7.3",
"M7.7",
"M7.1"
],
"constrains": [],
"reasons": {
"M7.3": "Dotting the homogeneous equation with t removes the normal part of A_Φ, and t·Kt reduces to the shear g contracted with the flux.",
"M7.7": "The identity is computed for the real homogeneous pulse amplitude of Lemma 7.4.",
"M7.1": "At the representative, the transfer −g0·T = −|g0|T_N is written in the shear frame N, K."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 81"
},
{
"id": "M7.9",
"kind": "move",
"name": "ns-m7-9-two-pulse-covariance-and-positive-squared-amplitudes",
"title": "Two-pulse covariance and positive squared amplitudes (Proposition 7.5)",
"section": "7",
"pages": "81-83",
"refs": [
"pp. 81 to 83",
"(7.23) to (7.29)",
"uses (4.27), (6.16), (6.13)."
],
"statement": "(7.23): C(w) = ⟨⟨wr wtan⟩θ⟩Y and B(w, v) = ⟨⟨wr vtan + vr wtan⟩θ⟩Y, so DC(w)[v] = B(w, v). With bσ = χg(ξg)ψ(v) t^h_σ cos(kΦσ) on the sign's rectangle (zero elsewhere) and H = [C(b+) | C(b-)], disjointness gives C(a+b+ + a-b-) = H(a+^2, a-^2)^T. Proposition 7.5: after one further decrease of q∗, H is invertible on each enlarged slow neighborhood and H^{-1}T0,∗ has positive components on Xa < X < Xb; (7.24): y = H^{-1}T0,∗, aσ = √yσ, W0 = √ε Σσ aσbσ;",
"description": "(7.23): C(w) = ⟨⟨wr wtan⟩θ⟩Y and B(w, v) = ⟨⟨wr vtan + vr wtan⟩θ⟩Y, so DC(w)[v] = B(w, v). With bσ = χg(ξg)ψ(v) t^h_σ cos(kΦσ) on the sign's rectangle (zero elsewhere) and H = [C(b+) | C(b-)], disjointness gives C(a+b+ + a-b-) = H(a+^2, a-^2)^T. Proposition 7.5: after one further decrease of q∗, H is invertible on each enlarged slow neighborhood and H^{-1}T0,∗ has positive components on Xa < X < Xb; (7.24): y = H^{-1}T0,∗, aσ = √yσ, W0 = √ε Σσ aσbσ; OBLIGATION: Realizes the order-zero stress target exactly by the averaged quadratic products of the leading wave, (7.26), with real amplitudes that are smooth up to and across the shell edges. After assembly (M7.10) this cancels the leading negative stress divergence in the background residual (5.41), the obligation set up in Sections 3.2 and 4.3. ANTECEDENT: Section 7 cites nothing. The introduction (p. 2) credits Daneri-Szekelyhidi [10] with the use of oscillations to realize a prescribed stress; Section 3.2 (Figure 4) and Section 4.3 (Lemma 4.5) set up the positive representation T = c1v1 + c2v2. REFS: pp. 81 to 83; (7.23) to (7.29); uses (4.27), (6.16), (6.13).",
"obligation": "Realizes the order-zero stress target exactly by the averaged quadratic products of the leading wave, (7.26), with real amplitudes that are smooth up to and across the shell edges. After assembly (M7.10) this cancels the leading negative stress divergence in the background residual (5.41), the obligation set up in Sections 3.2 and 4.3.",
"backward_question": "Which stresses are nonnegative combinations of the two pulse covariances in a slow box, and is the leading stress inside that cone with enough room to absorb O(S∗^{-1/2}) errors?",
"mechanism": "Because kp is a nonzero integer, the angular average of cos^2(kΦσ) is exactly 1/2. The auxiliary Haar average over a band rectangle becomes an integral over the pulse coordinate with Jacobian |det(vr, vt)| ci dv, ci ≍ S∗^{-1}: at a fixed physical point the auxiliary variable samples every phase of the pulse, so the covariance is a time average over the pulse. The weight x^2ψ^2 is a Gaussian of width √Ls, so hσ ≍ ci√Ls ≍ S∗^{-1/2}, and the average concentrates at the midpoint, where s = σu∗ and, by (7.21), the tangential polarization per unit radial amplitude is -σu∗K + c0√(1 + u∗^2)N = -σu∗K - AcN. The two columns are mirror images about -N. Ignoring eσ, h+y+ = (1/2)(-TN/Ac - TK/u∗) and h-y- = (1/2)(-TN/Ac + TK/u∗), so positivity is exactly TN < 0 and |TK| < (u∗/Ac)(-TN), which the choice of u∗ in M7.1 guarantees with a fixed margin ηc; the O(S∗^{-1/2}) errors and the frame-freezing errors do not destroy it for large bands. C(W0) = εHy = εT0,∗ holds exactly, since H is the exact covariance matrix of the chosen pulses and the cross term vanishes by disjoint rectangles. Since |T0| ≥ cζ and |∂^α T0| ≤ Cα ζ δ^{-mα} by (4.27), yσ is bounded below by c√S∗ ζ and its derivatives by ζ δ^{-a}; the chain-rule expansion on p. 83 then bounds every derivative of aσ = √yσ by √ζ δ^{-a'}, which vanishes at the edges and gives smooth zero extension.",
"antecedent": "Section 7 cites nothing. The introduction (p. 2) credits Daneri-Szekelyhidi [10] with the use of oscillations to realize a prescribed stress; Section 3.2 (Figure 4) and Section 4.3 (Lemma 4.5) set up the positive representation T = c1v1 + c2v2.",
"cost": "One further decrease of q∗; polynomial losses ||H^{-1}|| ≤ C√S∗ and yσ ≍ √S∗|T0,∗|; the primary wave has normalized size √ε (class W_{1/2}); only the order-zero target T0,∗ is realized.",
"checkable": "(a) With orthonormal N, K and Ac, u∗ > 0, solve [-AcN - u∗K | -AcN + u∗K] y = T and compare with the closed forms h±y± = (1/2)(-TN/Ac ∓ TK/u∗) (hσ = 1); confirm y > 0 exactly when TN < 0 and |TK| < (u∗/Ac)(-TN). (b) Discretize (ξg, v) in [-r0, r0] × [0, Ls] and θ in [0, 2π); build bσ from the Lemma 7.4 ODE solution; compute C(bσ) by the averages (7.23) with Jacobian |det(vr, vt)| ci; compare with (7.27) and with hσ(-AcN - σu∗K), confirming the relative discrepancy decays like S∗^{-1/2}; then with y = H^{-1}T0,∗ confirm C(W0) = εT0,∗ to quadrature accuracy.",
"depends_on": [
"M7.7",
"M7.1",
"M6.7",
"M4.8",
"L.7",
"L.12"
],
"constrains": [],
"reasons": {
"M7.7": "The covariance columns come from the primary pulses t^h_σ, whose pinned polarization and amplitude x ≍ P fix the directions −A_cN − σu*K.",
"M7.1": "Positivity of H^{-1}T_{0,*} is the cone (7.1), met with a margin by the choice of u* on the closed annulus.",
"M6.7": "Disjoint rectangles for the two signs remove cross terms, giving C(a+b+ + a−b−) = H(a+², a−²)^T.",
"M4.8": "The target is the leading stress T0 of Theorem 4.6, whose bounds (4.27) give y_σ ≥ c√S*ζ, so a_σ = √y_σ extends smoothly by zero.",
"L.7": "arXiv:2609.20803 reads this stress-realization step as using convex-integration ideas and lists [4] in that program; the manuscript itself states no borrowing from [4].",
"L.12": "Uses oscillations to realize a prescribed stress, central to Daneri-Székelyhidi [10]: two pulse families whose averaged quadratic products give the annular stress with positive weights."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 81-83"
},
{
"id": "M7.10",
"kind": "move",
"name": "ns-m7-10-physical-assembly-of-the-leading-stress-7-30",
"title": "Physical assembly of the leading stress (7.30)",
"section": "7",
"pages": "84",
"refs": [
"p. 84",
"(7.30)",
"(6.9), (6.13)."
],
"statement": "(7.30): Σ over β = (ℓ, a) of Q^{-2A} ηβ^2 εT0,∗ = q^{-A-1/2}T0, from Q^{-2A}εT0,∗ = Q^{-2A+h}(Q/q)^{A+1/2}T0 = Q^{-A+h+1/2} q^{-A-1/2}T0 = q^{-A-1/2}T0 (using A = 1/2 + h), Σβ ηβ^2 = 1, and vanishing cross-label products.",
"description": "(7.30): Σ over β = (ℓ, a) of Q^{-2A} ηβ^2 εT0,∗ = q^{-A-1/2}T0, from Q^{-2A}εT0,∗ = Q^{-2A+h}(Q/q)^{A+1/2}T0 = Q^{-A+h+1/2} q^{-A-1/2}T0 = q^{-A-1/2}T0 (using A = 1/2 + h), Σβ ηβ^2 = 1, and vanishing cross-label products. OBLIGATION: The physical covariance of the assembled leading wave equals exactly the physical leading stress q^{-A-1/2}T0 of Theorem 4.6(ii), the leading term of Tphys in (5.41), across overlapping bands and boxes and including derivatives of the slow partition (as used on p. 107), with no cross terms. MECHANISM: Physical velocity is Q^{-A} times its chart representative, so covariances scale by Q^{-2A}. The amplitude normalization √ε with ε = Q^h and the target normalization (Q/q)^{A+1/2} combine so every power of the chart scale Q cancels, leaving the band-independent q^{-A-1/2}T0 at each point. The slow cutoffs form a squared partition (6.9) and each covariance carries ηβ^2, so the sum returns one copy of the target; labels with overlapping slow supports sit on disjoint auxiliary rectangles (Lemma 6.1, (6.13)), so all cross products vanish pointwise. ANTECEDENT: None cited; internal (6.9) and Lemma 6.1. REFS: p. 84; (7.30); (6.9), (6.13).",
"obligation": "The physical covariance of the assembled leading wave equals exactly the physical leading stress q^{-A-1/2}T0 of Theorem 4.6(ii), the leading term of Tphys in (5.41), across overlapping bands and boxes and including derivatives of the slow partition (as used on p. 107), with no cross terms.",
"backward_question": "With what amplitude normalization do the local covariances, rescaled to physical units and summed with a squared partition over boxes and bands, reproduce exactly q^{-A-1/2}T0 with no cross terms?",
"mechanism": "Physical velocity is Q^{-A} times its chart representative, so covariances scale by Q^{-2A}. The amplitude normalization √ε with ε = Q^h and the target normalization (Q/q)^{A+1/2} combine so every power of the chart scale Q cancels, leaving the band-independent q^{-A-1/2}T0 at each point. The slow cutoffs form a squared partition (6.9) and each covariance carries ηβ^2, so the sum returns one copy of the target; labels with overlapping slow supports sit on disjoint auxiliary rectangles (Lemma 6.1, (6.13)), so all cross products vanish pointwise.",
"antecedent": "None cited; internal (6.9) and Lemma 6.1.",
"cost": "Depends on the squared partition and the disjoint rectangles of Section 6; realizes only the leading stress, leaving Tphys - q^{-A-1/2}T0 (relative size q^{2h} by (5.43)) to the correction cycle.",
"checkable": "Symbolic: confirm Q^{-2A}·Q^h·(Q/q)^{A+1/2} = q^{-A-1/2} when A = 1/2 + h. Numeric: build χℓ(q) with Σℓ χℓ^2 = 1 (support q/Q in [1/2, 2]) and product partitions χℓ,a on a mesh of size S∗^{-3}; at sample points covered by two adjacent bands, confirm Σβ Q^{-2A}ηβ^2 εT0,∗ = q^{-A-1/2}T0 for a test profile T0.",
"depends_on": [
"M7.9",
"M6.5",
"M6.7",
"M6.1",
"L.12"
],
"constrains": [],
"reasons": {
"M7.9": "Each box's leading wave has covariance exactly εT_{0,*} by (7.26).",
"M6.5": "The slow cutoffs form a squared partition, Σβ ηβ² = 1, so the local covariances sum to one copy of the target.",
"M6.7": "Labels with overlapping slow supports have disjoint auxiliary supports, so all cross-label products vanish.",
"M6.1": "The chart normalizations Q^{-2A} for covariances, ε = Q^h and T_{0,*} = (Q/q)^{A+1/2}T0 cancel every power of Q.",
"L.12": "The assembled leading wave's physical covariance equals the prescribed stress q^{-A-1/2}T0 exactly, the Daneri-Székelyhidi-style realization in physical variables."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 84"
},
{
"id": "M7.11",
"kind": "move",
"name": "ns-m7-11-signed-stress-increments-by-linearization-at-fixed",
"title": "Signed stress increments by linearization at fixed positive amplitudes (Proposition 7.6, (7.35), (7.36))",
"section": "7",
"pages": "84-85",
"refs": [
"pp. 84 to 85",
"(7.31) to (7.36)."
],
"statement": "For real Σ(R, Z, T) ∈ M_{α} independent of angular and auxiliary variables, (7.31): dΣ = H^{-1}(Σ/ε), δaσ = (dΣ)σ/(2aσ), LΣ = √ε Σσ δaσ bσ. Proposition 7.6, (7.32): ηβLΣ ∈ W_{α-1/2}, B(W0, LΣ) = Σ, C(ηβLΣ) ∈ M_{2α-1}; (7.33): |D^I δaσ| ≤ CI ε^{α-1} S∗^{b'I} √ζ δ^{-a'I}; (7.34): B(W0, LΣ) = εH(2a ⊙ δa) = εH dΣ = Σ. Hence C(W0 + LΣ) = εT0,∗ + Σ + C(LΣ), so L is a right inverse of DC(W0).",
"description": "For real Σ(R, Z, T) ∈ M_{α} independent of angular and auxiliary variables, (7.31): dΣ = H^{-1}(Σ/ε), δaσ = (dΣ)σ/(2aσ), LΣ = √ε Σσ δaσ bσ. Proposition 7.6, (7.32): ηβLΣ ∈ W_{α-1/2}, B(W0, LΣ) = Σ, C(ηβLΣ) ∈ M_{2α-1}; (7.33): |D^I δaσ| ≤ CI ε^{α-1} S∗^{b'I} √ζ δ^{-a'I}; (7.34): B(W0, LΣ) = εH(2a ⊙ δa) = εH dΣ = Σ. Hence C(W0 + LΣ) = εT0,∗ + Σ + C(LΣ), so L is a right inverse of DC(W0). OBLIGATION: Supplies the stress corrections of Step 2 of every correction cycle ((9.13), Proposition 9.6), which may have either sign and any direction; the proposition places no sign or relative-size restriction on Σ. Because the denominators 2aσ are the fixed primary amplitudes, L is linear with fixed coefficients and is defined on the same domain at every stage (used in Lemma 9.7, p. 112). MECHANISM: Vary only the scalar amplitudes, aσ to aσ + δaσ, keeping the pulse shapes bσ. Disjoint rectangles and averaging-independent scalar coefficients give the exact expansion εH((a + δa) ⊙ (a + δa)) = εT0,∗ + εH(2a ⊙ δa) + εH(δa ⊙ δa). Solving the linear 2 × 2 system for the first-order term needs no square root, so every Σ is reachable; ANTECEDENT: None cited. REFS: pp. 84 to 85; (7.31) to (7.36).",
"obligation": "Supplies the stress corrections of Step 2 of every correction cycle ((9.13), Proposition 9.6), which may have either sign and any direction; the proposition places no sign or relative-size restriction on Σ. Because the denominators 2aσ are the fixed primary amplitudes, L is linear with fixed coefficients and is defined on the same domain at every stage (used in Lemma 9.7, p. 112).",
"backward_question": "How can later stress corrections of either sign be supplied without taking square roots of an accumulated stress that might leave the positive cone?",
"mechanism": "Vary only the scalar amplitudes, aσ to aσ + δaσ, keeping the pulse shapes bσ. Disjoint rectangles and averaging-independent scalar coefficients give the exact expansion εH((a + δa) ⊙ (a + δa)) = εT0,∗ + εH(2a ⊙ δa) + εH(δa ⊙ δa). Solving the linear 2 × 2 system for the first-order term needs no square root, so every Σ is reachable; the quadratic term is a remainder of order 2α - 1. The factor 2 in the cross term, against the 1/2 from cos^2 already inside H, explains the denominator 2aσ. Near the shell edges dΣ carries the weight ζ while aσ carries √ζ, so δaσ keeps a √ζ weight and extends smoothly by zero. Auxiliary independence of Σ is what lets δaσ be pulled out of the auxiliary average; the auxiliary-dependent part of the mean residual is left to the temporal inverse of Section 8.",
"antecedent": "None cited.",
"cost": "Inputs restricted to auxiliary-independent stresses (stronger than membership in M_{α}); a stress of order ε^α needs amplitude increments of order ε^{α-1/2}; the quadratic remainder C(ηβLΣ) ∈ M_{2α-1} must be retained; the primary amplitudes aσ are frozen as denominators for all stages.",
"checkable": "For random y in (0, ∞)^2, invertible H, ε > 0, and random signed Σ (including components of opposite sign and large norm), compute dΣ and δa by (7.31); confirm εH(2a ⊙ δa) = Σ to round-off and εH((a + δa) ⊙ (a + δa)) = εHy + Σ + εH(δa ⊙ δa) exactly. With the discretized fields of the M7.9 check, confirm B(W0, LΣ) = Σ by quadrature.",
"depends_on": [
"M7.9",
"M6.7",
"M6.12",
"M7.10",
"L.12"
],
"constrains": [],
"reasons": {
"M7.9": "Linearizes the covariance at the fixed positive amplitudes a_σ = √y_σ of the pulses b_σ, dividing by 2a_σ and inverting the same matrix H.",
"M6.7": "Disjoint rectangles give the exact expansion εH((a + δa)⊙(a + δa)) with no cross-label terms.",
"M6.12": "The class algebra gives η_βL_Σ ∈ W_{α−1/2} and the quadratic remainder C(η_βL_Σ) ∈ M_{2α−1}.",
"M7.10": "The assembled forms (7.35), (7.36) sum the local maps over boxes and bands with the squared partition, as in (7.30).",
"L.12": "Signed stress increments are realized by oscillations, linearizing the covariance at fixed amplitudes: prescribed-stress realization as in Daneri-Székelyhidi [10]."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 84-85"
},
{
"id": "M7.12",
"kind": "move",
"name": "ns-m7-12-exact-incompressibility-by-curls-of-vector-potentials",
"title": "Exact incompressibility by curls of vector potentials (Lemma 7.7)",
"section": "7",
"pages": "85-86",
"refs": [
"pp. 85 to 86",
"(7.37), (7.38), (7.39)",
"(6.32)."
],
"statement": "For tm ∈ W_{α} with nΦ·tm = 0, supported compactly inside the pulse interval and in the prescribed slow and transverse supports, (7.38): Cm = i nΦ × tm/(km|nΦ|^2), Am = Cm e^{ikmΦ}, curl∗Am = (tm + rm)e^{ikmΦ}, with curl∗ from (7.37) and rm = (-Dz(Cm)θ, Dz(Cm)r - Dr(Cm)z, (Dr + R^{-1})(Cm)θ). Lemma 7.7: Cm ∈ W_{α+1/2}, rm ∈ W_{α+1/2-κs}; the velocity is exactly divergence-free for the normalized operators and after evaluation at the phase map;",
"description": "For tm ∈ W_{α} with nΦ·tm = 0, supported compactly inside the pulse interval and in the prescribed slow and transverse supports, (7.38): Cm = i nΦ × tm/(km|nΦ|^2), Am = Cm e^{ikmΦ}, curl∗Am = (tm + rm)e^{ikmΦ}, with curl∗ from (7.37) and rm = (-Dz(Cm)θ, Dz(Cm)r - Dr(Cm)z, (Dr + R^{-1})(Cm)θ). Lemma 7.7: Cm ∈ W_{α+1/2}, rm ∈ W_{α+1/2-κs}; the velocity is exactly divergence-free for the normalized operators and after evaluation at the phase map; OBLIGATION: The increment identity of Section 3.3 and the final force require exactly divergence-free velocity increments, while the amplitudes from M7.6 and M7.7 are transverse only at leading order. This makes every wave exactly solenoidal while keeping the prescribed amplitude as its leading part; (7.39) controls the longitudinal component, which Lemma 9.2 uses to cancel an apparent half-power loss in wave-wave transport (p. 103). MECHANISM: The curl of Cm e^{ikmΦ} has leading part ikm nΦ × Cm = -nΦ × (nΦ × tm)/|nΦ|^2 = tm - nΦ(nΦ·tm)/|nΦ|^2 = tm. ANTECEDENT: None cited; within the manuscript it is anticipated in Section 3.3 (p. 12: w = ∇ × A_wave). REFS: pp. 85 to 86; (7.37), (7.38), (7.39); (6.32).",
"obligation": "The increment identity of Section 3.3 and the final force require exactly divergence-free velocity increments, while the amplitudes from M7.6 and M7.7 are transverse only at leading order. This makes every wave exactly solenoidal while keeping the prescribed amplitude as its leading part; (7.39) controls the longitudinal component, which Lemma 9.2 uses to cancel an apparent half-power loss in wave-wave transport (p. 103).",
"backward_question": "How can a wave with a prescribed transverse amplitude be made exactly divergence-free, and how large is the unavoidable correction?",
"mechanism": "The curl of Cm e^{ikmΦ} has leading part ikm nΦ × Cm = -nΦ × (nΦ × tm)/|nΦ|^2 = tm - nΦ(nΦ·tm)/|nΦ|^2 = tm. The rest, rm, differentiates Cm or the cylindrical frame, so it is smaller by (km)^{-1} = O(ε^{1/2}) up to the loss κs from one Dr, whose chain-rule term along the phase map costs ε^{-κs} (6.32). The identity div∗curl∗ = 0 holds exactly because the normalized derivatives commute (the only variable coefficient is a function of r times a constant torus direction) and (Dr + R^{-1})(R^{-1}f) = R^{-1}Dr f. Expanding div∗(am e^{ikmΦ}) = 0 for θ-independent am gives (7.39): the longitudinal component equals the amplitude's divergence divided by km.",
"antecedent": "None cited; within the manuscript it is anticipated in Section 3.3 (p. 12: w = ∇ × A_wave).",
"cost": "A curl remainder of class W_{α+1/2-κs}; the κs loss (κs = 10^{-5}, (6.2)) recurs each time Dr is applied; the potential needs compact support inside the pulse interval, hence the cutoff ψ of M7.13.",
"checkable": "Symbolic: (i) confirm ikm nΦ × Cm = tm - nΦ(nΦ·tm)/|nΦ|^2 for Cm in (7.38); (ii) with Dr = ∂R + c(R)L (L a constant-coefficient derivative in an auxiliary variable, c(R) = M dr R^{dr-1} as in (6.6)), Dθ = R^{-1}∂θ, Dz = ε∂Z, confirm div∗curl∗A = 0 identically for arbitrary smooth A using (3.11) and (7.37); (iii) confirm (7.39) by expanding div∗(am e^{ikmΦ}).",
"depends_on": [
"M7.2",
"M6.12",
"M6.3",
"M6.2",
"ME.7"
],
"constrains": [],
"reasons": {
"M7.2": "The potential C_m = i n_Φ × t_m/(km|n_Φ|²) uses the phase normal and the carrier k, so the leading part of its curl returns t_m.",
"M6.12": "The cost table gives C_m ∈ W_{α+1/2} from (km)^{-1} = O(ε^{1/2}) and r_m ∈ W_{α+1/2−κ_s} from one D_r.",
"M6.3": "curl* and div* are built from the normalized operators D_r, D_z, D_θ of (6.6), for which div*curl* = 0 holds exactly.",
"M6.2": "Divergence-freeness survives evaluation because the chain-rule radial and time operators commute with ∂_z and ∂_θ on the extended domain.",
"ME.7": "Its potential C_m = i n_Phi x t_m/(km|n_Phi|^2) matches ME.7's Q_A = -d_theta^{-1}(m x A)/D_m: a curl of the potential makes the oscillation exactly divergence free."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 85-86"
},
{
"id": "M7.13",
"kind": "move",
"name": "ns-m7-13-temporal-cutoff-and-flatness-of-the-tails-7-40",
"title": "Temporal cutoff and flatness of the tails ((7.40))",
"section": "7",
"pages": "86-87",
"refs": [
"pp. 86 to 87",
"(7.40)",
"(6.16), (7.16)."
],
"statement": "With t̂m = ψtm and π̂m = ψπm (ψ = 1 on |v - Ls/2| ≤ Ls/5 by (6.16)), (7.40): t̂'m + Kt̂m + m^2 d t̂m + ikm nΦ π̂m + fm = (1 - ψ)fm + ψ'tm. The right side lives where |v - Ls/2| ≥ Ls/5 and gains S∗^C e^{-cS∗} in every coefficient derivative; in physical variables q^{-N}Q^{-M}S∗^C e^{-cS∗} ≤ CN exp(-cℓ^2 + (M + N)ℓ log 2 + 2C log ℓ), which tends to 0, so these terms are O(q^N) for every N. Also π̂m ∈ W_{α+1/2} and r̂m ∈ W_{α+1/2-κs}. The same argument treats homogeneous cutoff tails.",
"description": "With t̂m = ψtm and π̂m = ψπm (ψ = 1 on |v - Ls/2| ≤ Ls/5 by (6.16)), (7.40): t̂'m + Kt̂m + m^2 d t̂m + ikm nΦ π̂m + fm = (1 - ψ)fm + ψ'tm. The right side lives where |v - Ls/2| ≥ Ls/5 and gains S∗^C e^{-cS∗} in every coefficient derivative; in physical variables q^{-N}Q^{-M}S∗^C e^{-cS∗} ≤ CN exp(-cℓ^2 + (M + N)ℓ log 2 + 2C log ℓ), which tends to 0, so these terms are O(q^N) for every N. Also π̂m ∈ W_{α+1/2} and r̂m ∈ W_{α+1/2-κs}. The same argument treats homogeneous cutoff tails. OBLIGATION: Turns pulse solutions, which reach both ends of [0, Ls] and have no temporal zero extension, into fields supported inside the labeled rectangle, and shows the truncation error is flat. These terms stay as separate additive flat residuals through all later corrections (the retained F^[j] of (9.3), (9.5)), are never fed back into forward pulse solves, and end up in the force. With fm = 0 the tail is consistent with Section 2.2's statement that an exponentially small external force seeds each pulse (p. 6). ANTECEDENT: None cited. REFS: pp. 86 to 87; (7.40); (6.16), (7.16).",
"obligation": "Turns pulse solutions, which reach both ends of [0, Ls] and have no temporal zero extension, into fields supported inside the labeled rectangle, and shows the truncation error is flat. These terms stay as separate additive flat residuals through all later corrections (the retained F^[j] of (9.3), (9.5)), are never fed back into forward pulse solves, and end up in the force. With fm = 0 the tail is consistent with Section 2.2's statement that an exponentially small external force seeds each pulse (p. 6).",
"backward_question": "When a pulse is truncated in time, where does the truncation error live, and is it small to every order in q?",
"mechanism": "Multiplying the solved equation by ψ leaves only the uncancelled source (1 - ψ)fm and ψ'tm, both supported where ψ ≠ 1. There both source and response carry the envelope, and by (7.16) P(v) ≤ e^{-c(Ls/5)^2/Ls} = e^{-cLs/25}, which is e^{-c'S∗}. Since S∗ = ℓ^2 while Q = 2^{-ℓ} and q ≍ Q, the factor e^{-cℓ^2} beats every fixed power Q^{-M} lost in converting to physical derivatives and every power q^{-N}.",
"antecedent": "None cited.",
"cost": "Flat terms must be tracked additively through all stages and through the final summation; forward solves act only on the supported sources.",
"checkable": "(i) Symbolic: given (tm, πm) satisfying (7.5), confirm (7.40) for (ψtm, ψπm). (ii) Numeric: for Ls = cℓ^2 with ℓ = 10 to 60, compute the log of max{P(v) : |v - Ls/2| ≥ Ls/5} and confirm it is at most -c'ℓ^2; evaluate -cℓ^2 + (M + N)ℓ log 2 + 2C log ℓ for fixed (M, N, C) and confirm it tends to minus infinity.",
"depends_on": [
"M7.5",
"M7.6",
"M6.6",
"M6.1"
],
"constrains": [],
"reasons": {
"M7.5": "Where ψ < 1 the Gaussian envelope (7.16) is at most e^{−cS*}, which makes the cutoff errors small.",
"M7.6": "Multiplies the pulse solutions (t_m, π_m) of (7.5), (7.13) by ψ, leaving only (1 − ψ)f_m + ψ′t_m.",
"M6.6": "The cutoff ψ of (6.16) equals one on |v − L_s/2| ≤ L_s/5, with L_s ≍ S*.",
"M6.1": "Since S* = ℓ² while Q = 2^{-ℓ}, the factor e^{−cℓ²} beats every power of q lost in converting to physical derivatives."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 86-87"
},
{
"id": "M7.14",
"kind": "move",
"name": "ns-m7-14-exact-covariance-expansion-for-the-actual-velocities",
"title": "Exact covariance expansion for the actual velocities (Corollary 7.8)",
"section": "7",
"pages": "87-88",
"refs": [
"pp. 87 to 88",
"(7.41), (7.42)",
"applied in (9.13), p. 109."
],
"statement": "Corollary 7.8: let U = W^as_0 + E be a real divergence-free wave field (curl remainders included) with U ∈ W_{1/2} and E ∈ W_{ρ}, and let Σ ∈ M_{α} be independent of angular and auxiliary variables. Applying Lemma 7.7 to L^asΣ gives the divergence-free increment V = L^asΣ + R with R ∈ W_{α-κs}, and (7.41): C(U + V) - C(U) = Σ + B(E, L^asΣ) + B(U, R) + C(V), with (7.42): B(E, L^asΣ) ∈ M_{ρ+α-1/2}, B(U, R) ∈ M_{α+1/2-κs}, C(V) ∈ M_{2α-1}. Taking a radial divergence costs at most a further κs.",
"description": "Corollary 7.8: let U = W^as_0 + E be a real divergence-free wave field (curl remainders included) with U ∈ W_{1/2} and E ∈ W_{ρ}, and let Σ ∈ M_{α} be independent of angular and auxiliary variables. Applying Lemma 7.7 to L^asΣ gives the divergence-free increment V = L^asΣ + R with R ∈ W_{α-κs}, and (7.41): C(U + V) - C(U) = Σ + B(E, L^asΣ) + B(U, R) + C(V), with (7.42): B(E, L^asΣ) ∈ M_{ρ+α-1/2}, B(U, R) ∈ M_{α+1/2-κs}, C(V) ∈ M_{2α-1}. Taking a radial divergence costs at most a further κs. OBLIGATION: Justifies using L during the iteration, where the increment is added to a wave that already contains earlier corrections and curl remainders and the increment carries its own curl remainder. The prescribed stress appears exactly and every other change is of higher order, with no positivity condition on the accumulated stress. Section 9 applies it in (9.13) with ρ = 0.68 and α = C∗ - κs, obtaining remainder orders C∗ + 0.18 - κs, C∗ + 1/2 - 2κs, and C∗ + σj - 2κs (p. 109). MECHANISM: C is quadratic, so C(U + V) - C(U) = B(U, V) + C(V). Splitting U = W^as_0 + E and V = L^asΣ + R, the term B(W^as_0. ANTECEDENT: None cited. REFS: pp. 87 to 88; (7.41), (7.42); applied in (9.13), p. 109.",
"obligation": "Justifies using L during the iteration, where the increment is added to a wave that already contains earlier corrections and curl remainders and the increment carries its own curl remainder. The prescribed stress appears exactly and every other change is of higher order, with no positivity condition on the accumulated stress. Section 9 applies it in (9.13) with ρ = 0.68 and α = C∗ - κs, obtaining remainder orders C∗ + 0.18 - κs, C∗ + 1/2 - 2κs, and C∗ + σj - 2κs (p. 109).",
"backward_question": "When a signed increment is added to the actual wave field, which already contains earlier corrections and curl remainders, what is the exact covariance change, and is every term besides the prescribed one of higher order?",
"mechanism": "C is quadratic, so C(U + V) - C(U) = B(U, V) + C(V). Splitting U = W^as_0 + E and V = L^asΣ + R, the term B(W^as_0, L^asΣ) equals Σ by (7.36); the rest are the cross term of the old corrections with the new signed amplitudes, the cross term of the whole wave with the new curl remainder, and the self-interaction of the increment. Their classes follow from the product rules of Proposition 6.6 and κs < 1/2, which gives V ∈ W_{α-1/2}.",
"antecedent": "None cited.",
"cost": "Three remainders carried into the next cycle; one more κs when their radial divergence is taken.",
"checkable": "Exact algebra: on a discretized (θ, auxiliary) grid at a fixed slow point, draw fields U = W0 + E and V = LΣ + R with B(W0, LΣ) = Σ enforced as in M7.11; compute C(U + V) - C(U) and Σ + B(E, LΣ) + B(U, R) + C(V) and confirm equality to round-off. The class statements (7.42) are pure estimates.",
"depends_on": [
"M7.11",
"M7.12",
"M6.12"
],
"constrains": [],
"reasons": {
"M7.11": "The identity B(W^as_0, L^asΣ) = Σ of (7.36) supplies the prescribed term exactly.",
"M7.12": "Lemma 7.7 applied to L^asΣ gives the divergence-free increment V = L^asΣ + R with R ∈ W_{α−κ_s}.",
"M6.12": "The product rules give the classes (7.42) of the three remainders."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 87-88"
},
{
"id": "M8.1",
"kind": "move",
"name": "ns-m8-1-mean-decomposition-and-the-two-preserved-moments",
"title": "Mean decomposition and the two preserved moments",
"section": "8",
"pages": "88-89",
"refs": [
"pages 88 to 89",
"(8.1), (8.2)",
"consumer (9.10) on page 106."
],
"statement": "In a common chart the normalized velocity is u = (b + β, V + v, G + γ) + w with ⟨w⟩_θ = 0 and W_ab = ⟨w_a w_b⟩_θ, a, b ∈ {r, θ, z} (8.1). Here (b, V, G) is the slow base, (β, v, γ) the angularly invariant correction (allowed to depend on the auxiliary torus), and w the sum of curls of wave potentials, so W contains every curl remainder.",
"description": "In a common chart the normalized velocity is u = (b + β, V + v, G + γ) + w with ⟨w⟩_θ = 0 and W_ab = ⟨w_a w_b⟩_θ, a, b ∈ {r, θ, z} (8.1). Here (b, V, G) is the slow base, (β, v, γ) the angularly invariant correction (allowed to depend on the auxiliary torus), and w the sum of curls of wave potentials, so W contains every curl remainder. OBLIGATION: Fixes the unknowns of the mean problem and the two linear functionals that must never drift. M_z = 0 is what lets an axial increment come from a compactly supported azimuthal potential (Proposition 8.3(ii)). M_θ = M_z = 0 remove the time-derivative and axial-viscosity terms from the weighted radial integrals of the tangential residuals (Proposition 8.4); ANTECEDENT: None cited. Internal: the same weights r^2 and r appear in the leading stress formulas T_rθ = −r^{-2}∫_0^r s^2 R_θ^{(0)} ds, T_rz = −r^{-1}∫_0^r s R_z^{(0)} ds and in the zero-moment conditions ∫r^2 R_θ^{(0)} dr = ∫r R_z^{(0)} dr = 0 of Section 3.2 (supplied by Lemma A.8). REFS: pages 88 to 89; (8.1), (8.2); consumer (9.10) on page 106.",
"obligation": "Fixes the unknowns of the mean problem and the two linear functionals that must never drift. M_z = 0 is what lets an axial increment come from a compactly supported azimuthal potential (Proposition 8.3(ii)). M_θ = M_z = 0 remove the time-derivative and axial-viscosity terms from the weighted radial integrals of the tangential residuals (Proposition 8.4); without them those integrals would contain −ε∂_T M_θ and −ε∂_T M_z, which are linear in the correction, are not axial derivatives of fluxes, and are not improved by the cycle. They become the exactly preserved moments (9.10) of every correction state.",
"backward_question": "Which integrals of an axisymmetric, compactly supported correction must be held at zero so that the integrated tangential equations contain only axial derivatives of fluxes and nothing the iteration cannot improve?",
"mechanism": "The correction is a \"mean\" only in the angle: it may oscillate on the auxiliary torus, and after evaluation at Y = Y(r, t) it is a physically axisymmetric field with fast radial and temporal variation, because the phase map (6.3) depends only on (r, t). Every later mean map is designed to preserve both moments: compactly supported azimuthal potentials preserve M_z automatically, since ∫R(∂_R + 1/R)Ψ dR = ∫∂_R(RΨ) dR = 0; increments with zero auxiliary mean at every point preserve both; the five-equation map imposes both as its first two rows.",
"antecedent": "None cited. Internal: the same weights r^2 and r appear in the leading stress formulas T_rθ = −r^{-2}∫_0^r s^2 R_θ^{(0)} ds, T_rz = −r^{-1}∫_0^r s R_z^{(0)} ds and in the zero-moment conditions ∫r^2 R_θ^{(0)} dr = ∫r R_z^{(0)} dr = 0 of Section 3.2 (supplied by Lemma A.8).",
"cost": "Two exact constraints at every (Z, T) that every later mean update must preserve exactly ((9.10)). The covariance must be recomputed from the complete wave field, curl remainders included, after each update.",
"checkable": "For Ψ(R, Z) compactly supported in R, compute ∫R(∂_R + 1/R)Ψ dR by quadrature (vanishes identically), and confirm that ∫R^2 v dR does not vanish for a generic compactly supported v (it has to be imposed).",
"depends_on": [
"M5.14",
"M7.12",
"M6.8",
"M7.2"
],
"constrains": [],
"reasons": {
"M5.14": "The slow base (b, V, G) is the realized background in chart units.",
"M7.12": "w is the sum of curls of wave potentials, so the covariance W includes every curl remainder.",
"M6.8": "The decomposition is written in a common chart, and the angular-mean correction may depend on the common auxiliary torus.",
"M7.2": "⟨w⟩_θ = 0 because every wave phase has a nonzero integer angular frequency."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 88-89"
},
{
"id": "M8.2",
"kind": "move",
"name": "ns-m8-2-conservative-angular-mean-momentum-balance",
"title": "Conservative angular-mean momentum balance",
"section": "8",
"pages": "89",
"refs": [
"page 89",
"Proposition 8.1, (8.3)",
"(5.41) on page 60."
],
"statement": "Proposition 8.1: with the base flat residual set aside as a separate additive error, the angular mean of the remaining normalized residual is (D_r p_m − g_r, E_θ, E_z), where, with ∆_0 = D_r^2 + R^{-1}D_r + D_z^2 and Σ_a = Q^{2A} T_{phys,a} from (5.41), E_θ = t_* v + (D_r + 2/R)(bv + βV + βv + W_rθ) + D_z(Gv + Vγ + γv + W_zθ) − ε(∆_0 − R^{-2})v − (D_r + 2/R)Σ_θ, E_z = t_* γ + (D_r + 1/R)(bγ + βG + βγ + W_rz) + D_z(2Gγ + γ^2 + W_zz + p_m) − ε∆_0 γ − (D_r + 1/R)Σ_z, g_r = −t_* β − (D_r +.",
"description": "Proposition 8.1: with the base flat residual set aside as a separate additive error, the angular mean of the remaining normalized residual is (D_r p_m − g_r, E_θ, E_z), where, with ∆_0 = D_r^2 + R^{-1}D_r + D_z^2 and Σ_a = Q^{2A} T_{phys,a} from (5.41), E_θ = t_* v + (D_r + 2/R)(bv + βV + βv + W_rθ) + D_z(Gv + Vγ + γv + W_zθ) − ε(∆_0 − R^{-2})v − (D_r + 2/R)Σ_θ, E_z = t_* γ + (D_r + 1/R)(bγ + βG + βγ + W_rz) + D_z(2Gγ + γ^2 + W_zz + p_m) − ε∆_0 γ − (D_r + 1/R)Σ_z, g_r = −t_* β − (D_r +. OBLIGATION: Identifies exactly what remains in the angular mean after the waves, including every quadratic wave product and the torus dependence, and writes each radial flux as a cylindrical divergence, so that weighted radial integrals become boundary terms (used in Proposition 8.4). ANTECEDENT: None cited. Recognizable classical ingredient (not cited): angular Reynolds averaging of the cylindrical Navier-Stokes equations in conservative form, W being the angular Reynolds stress. Internal: (5.41), the normalized operators (6.6) and (3.11). REFS: page 89; Proposition 8.1, (8.3); (5.41) on page 60.",
"obligation": "Identifies exactly what remains in the angular mean after the waves, including every quadratic wave product and the torus dependence, and writes each radial flux as a cylindrical divergence, so that weighted radial integrals become boundary terms (used in Proposition 8.4). The radial component is posed as a pressure equation D_r p_m = g_r, so it is never corrected by velocity directly.",
"backward_question": "In what form should the angularly averaged residual be written so that its weighted radial integrals, which decide whether compactly supported corrections exist, can be read off as boundary terms?",
"mechanism": "Incompressibility puts transport in conservative form: (u·∇u)_r = (D_r + 1/R)u_r^2 + R^{-1}∂_θ(u_θ u_r) + D_z(u_z u_r) − u_θ^2/R; (u·∇u)_θ = (D_r + 2/R)(u_r u_θ) + R^{-1}∂_θ u_θ^2 + D_z(u_z u_θ); (u·∇u)_z = (D_r + 1/R)(u_r u_z) + R^{-1}∂_θ(u_θ u_z) + D_z u_z^2. The frame rotation supplies the centrifugal term and the extra u_r u_θ/R, which is why the θ-flux carries (D_r + 2/R) (angular momentum conservation). Angular averaging kills every ∂_θ term and every product with exactly one wave factor; subtracting the pure base terms leaves the displayed fluxes. The angular-derivative terms of the vector Laplacian average out, leaving ∆_0 − R^{-2} in the r and θ rows and ∆_0 in the z row, each with the normalized viscous factor ε. The base stress contributes −(D_r + 2/R)Σ_θ and −(D_r + 1/R)Σ_z by (5.41). Excluded pulse tails carry nonzero harmonics, so their angular mean is zero. The normalized time derivative t_* = −ε∂_T + c_{i0}N_{i0} contains the fast auxiliary-time derivative.",
"antecedent": "None cited. Recognizable classical ingredient (not cited): angular Reynolds averaging of the cylindrical Navier-Stokes equations in conservative form, W being the angular Reynolds stress. Internal: (5.41), the normalized operators (6.6) and (3.11).",
"cost": "Nothing new, but W must include every curl remainder, and the pressure p_m sits inside the axial flux D_z(... + p_m), coupling the z-equation to the radial pressure reconstruction (the origin of the c_ρ P term in M8.7).",
"checkable": "Computer algebra: for u = (b + β, V + v, G + γ) + Re(â(R, Z)e^{imθ}) with m ≠ 0 and ∇·u = 0, average the cylindrical (u·∇)u and the vector Laplacian over θ, subtract base terms, and compare with (8.3); in particular the centrifugal term (2Vv + v^2 + W_θθ)/R and the factor (D_r + 2/R).",
"depends_on": [
"M8.1",
"M5.14",
"M6.3",
"M6.12"
],
"constrains": [],
"reasons": {
"M8.1": "Averages the residual of u = (b + β, V + v, G + γ) + w, with W = ⟨w_a w_b⟩_θ collecting the wave products.",
"M5.14": "The base residual (5.41) contributes −(D_r + 2/R)Σ_θ and −(D_r + 1/R)Σ_z plus a flat error that is set aside.",
"M6.3": "Writes the balance with the normalized operators t* = −ε∂_T + c_{i0}N_{i0}, D_r and D_z = ε∂_Z, with viscous factor ε.",
"M6.12": "Angular averaging removes every term with exactly one wave factor, since a single nonzero harmonic has zero angular mean."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 89"
},
{
"id": "M8.3",
"kind": "move",
"name": "ns-m8-3-phase-following-compactly-supported-radial-primitive",
"title": "Phase-following compactly supported radial primitive",
"section": "8",
"pages": "89-91",
"refs": [
"pages 89 to 91",
"(8.4) to (8.7), (8.9)",
"Lemma 8.2, Steps 1 and 2."
],
"statement": "For a shell-supported g(r, z, t, Y), I g(r, Y) = ∫_0^r g(r′, Y + ((r′)^{d_r} − r^{d_r})v_r) dr′, J g = the same integral over (0, ∞), and I_c g = I g − χ_m J g (8.4); the chart version (8.5) uses the shift M((R′)^{d_r} − R^{d_r})v_r on the common torus y = Y_{i0}, with M = Λ_g^{i0} Q^{d_r/2}. Here d_r is the radial phase exponent of (6.2), not a differential. For e ∈ {0, 1, 2}: D_e = D_r + e/R, T_e f = R^{-e} I_c(R^e f), A_e f = R^{-e}(∂_R χ_m) J(R^e f) (8.6).",
"description": "For a shell-supported g(r, z, t, Y), I g(r, Y) = ∫_0^r g(r′, Y + ((r′)^{d_r} − r^{d_r})v_r) dr′, J g = the same integral over (0, ∞), and I_c g = I g − χ_m J g (8.4); the chart version (8.5) uses the shift M((R′)^{d_r} − R^{d_r})v_r on the common torus y = Y_{i0}, with M = Λ_g^{i0} Q^{d_r/2}. Here d_r is the radial phase exponent of (6.2), not a differential. For e ∈ {0, 1, 2}: D_e = D_r + e/R, T_e f = R^{-e} I_c(R^e f), A_e f = R^{-e}(∂_R χ_m) J(R^e f) (8.6). OBLIGATION: Supplies one inverse for all three cylindrical divergences needed later (e = 0 pressure; e = 1 axial vector potential and axial stress H_z; e = 2 azimuthal stress H_θ) that (a) inverts the physical radial derivative r = ∂_r + d_r r^{d_r − 1} L_abs, which also moves the torus variable, and (b) produces outputs that vanish for X ≤ X_a and X ≥ X_b, so neither the axis region nor the heat exterior is touched. ANTECEDENT: None cited. Recognizable classical ingredient (not cited): integration along characteristics of a first-order operator. Internal: phase map (6.3), chain-rule operators (6.4) and (6.6), common torus (Lemma 6.2), edge weights (6.23). REFS: pages 89 to 91; (8.4) to (8.7), (8.9); Lemma 8.2, Steps 1 and 2.",
"obligation": "Supplies one inverse for all three cylindrical divergences needed later (e = 0 pressure; e = 1 axial vector potential and axial stress H_z; e = 2 azimuthal stress H_θ) that (a) inverts the physical radial derivative r = ∂_r + d_r r^{d_r − 1} L_abs, which also moves the torus variable, and (b) produces outputs that vanish for X ≤ X_a and X ≥ X_b, so neither the axis region nor the heat exterior is touched.",
"backward_question": "How do you invert a radial derivative that also drags the auxiliary torus variable along the phase map, and still get a primitive that vanishes outside the shell?",
"mechanism": "Integrating along the characteristics of r, along which the torus point shifts by ((r′)^{d_r} − r^{d_r})v_r, gives r(I g) = g, while the full-line integral satisfies r(J g) = 0. I g vanishes below the shell and equals J g above it, so subtracting χ_m J g, where χ_m is a fixed radial cutoff equal to 0 on an inner collar and 1 on an outer collar and varying only in a fixed interior portion of the shell, makes I_c g vanish on both sides. The price is r(I_c g) = g − (∂_r χ_m)J g; conjugating by R^e gives (8.7). For the estimates, the substitution U = R^{d_r} writes J g = A_− + A_+ and I_c g = (1 − χ_m)A_− − χ_m A_+ with half-line integrals A_± whose shifts depend on neither U nor (Z, T) (8.9), so coefficient derivatives never produce a factor of M. The flat edge weight is inherited because s ↦ e^{−a_a/s^2}s^{−B} is increasing for small s: integrating forward from the inner edge (or backward from the outer edge), the input weight is dominated by its value at the endpoint.",
"antecedent": "None cited. Recognizable classical ingredient (not cited): integration along characteristics of a first-order operator. Internal: phase map (6.3), chain-rule operators (6.4) and (6.6), common torus (Lemma 6.2), edge weights (6.23).",
"cost": "A fixed interior cutoff χ_m and the cutoff remainder A_e f, supported where χ_m varies, which must either be shown flat (M8.4) or retained. Full slow derivatives do not commute with I_c; they are estimated through the fixed-shift representation (8.9) instead.",
"checkable": "On a grid in (r, Y) with d_r ≈ 1.13 and v_r = (1, 1 − √2), compute I_c g by quadrature along the shifted path; check by finite differences that (∂_r + d_r r^{d_r − 1} v_r·∂_Y) I_c g = g − (∂_r χ_m) J g, and that I_c g vanishes below X_a and above X_b.",
"depends_on": [
"M6.2",
"M6.8",
"M6.11",
"M6.3"
],
"constrains": [],
"reasons": {
"M6.2": "Inverts the physical radial derivative, which also moves the torus point along v_r, by integrating along the phase map's radial characteristics.",
"M6.8": "The chart version shifts along v_r on the common torus y = Y_{i0}, with M = Λ_g^{i0}Q^{d_r/2}.",
"M6.11": "The output stays in M^α because the flat edge weight ζ, increasing near each edge, dominates the integrand from the nearer edge.",
"M6.3": "The shift rate M is the radial winding M_i ≍ ε^{-κ_s}S*^{-ρ_g} of the chart operator D_r."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 89-91"
},
{
"id": "M8.4",
"kind": "move",
"name": "ns-m8-4-flatness-of-the-cutoff-remainder-under-the-weighted-mean",
"title": "Flatness of the cutoff remainder under the weighted mean condition",
"section": "8",
"pages": "90-92",
"refs": [
"pages 90 to 92",
"(8.8), (8.10)",
"Lemma 8.2, Step 3",
"(6.7) on page 64."
],
"statement": "Lemma 8.2, remainder clause: if ∫R^e ⟨f⟩_Y dR = 0 at every (Z, T), then ⟨A_e f⟩_Y = 0 and, for every fixed I and integer p ≥ 1, |∂^I A_e f| ≤ C_{j,I,p} ε^{α + pκ_s} S_*^{B_{j,I,p}} ζ δ^{−B_{j,I,p}} (8.8). If f is Y-independent with ∫R^e f dR = 0, then A_e f ≡ 0. The torus inverse obeys ‖L^{−p}H‖_{C^m_y} ≤ C_{m,p}‖H‖_{C^{m+p+3}_y} for zero-mean H, L = v_r·∂_y (8.10).",
"description": "Lemma 8.2, remainder clause: if ∫R^e ⟨f⟩_Y dR = 0 at every (Z, T), then ⟨A_e f⟩_Y = 0 and, for every fixed I and integer p ≥ 1, |∂^I A_e f| ≤ C_{j,I,p} ε^{α + pκ_s} S_*^{B_{j,I,p}} ζ δ^{−B_{j,I,p}} (8.8). If f is Y-independent with ∫R^e f dR = 0, then A_e f ≡ 0. The torus inverse obeys ‖L^{−p}H‖_{C^m_y} ≤ C_{m,p}‖H‖_{C^{m+p+3}_y} for zero-mean H, L = v_r·∂_y (8.10). OBLIGATION: Makes the inverse exact up to a flat error even when the source depends on the torus, which is precisely the case of the axial increments produced by the temporal inverse (8.20). Without it, the torus-oscillating part of J g would leave a non-flat error where χ_m varies. MECHANISM: Haar invariance gives ⟨J g⟩_Y = ∫⟨g⟩_Y dR, which vanishes by hypothesis for g = R^e f. ANTECEDENT: None cited. Internal: the Diophantine inequality (6.7), proved in Section 6 by multiplying v_r·n = (n_1 + n_2) − √2 n_2 by its algebraic conjugate, which gives a nonzero integer. Recognizable classical ingredients (not cited): small divisors for a linear flow on T^2 with a badly approximable slope, and repeated integration by parts. REFS: pages 90 to 92; (8.8), (8.10); Lemma 8.2, Step 3; (6.7) on page 64.",
"obligation": "Makes the inverse exact up to a flat error even when the source depends on the torus, which is precisely the case of the axial increments produced by the temporal inverse (8.20). Without it, the torus-oscillating part of J g would leave a non-flat error where χ_m varies.",
"backward_question": "When a torus-dependent source has zero weighted torus-mean integral but a nonzero full radial integral at each torus point, is the oscillating part of that integral small, and how small?",
"mechanism": "Haar invariance gives ⟨J g⟩_Y = ∫⟨g⟩_Y dR, which vanishes by hypothesis for g = R^e f. The zero-mean part is a nonstationary-phase integral: along u ↦ (U + u, y + Mu v_r) a torus mode k oscillates at frequency 2πM(v_r·k). Since d/du of L^{-1}F° along the path equals ∂_U L^{-1}F° + M F°, integrating p times gives the exact identity J g = (−M^{−1})^p ∫_R ∂_U^p L^{−p} F°(U + u, y + Mu v_r) du, with no endpoint terms by compact support. L^{−1} exists on zero-mean functions with finite derivative loss because of the Diophantine bound |v_r·k| ≥ c/(1 + |k|) of (6.7). Because M^{−1} ≤ C ε^{κ_s} S_*^{ρ_g}, each integration gains ε^{κ_s}; for a target flatness order N and a physical derivative order with q-loss L, choose p with h(α + pκ_s) > N + L, and the strict excess absorbs the fixed powers of S_* = ℓ^2 (only logarithmic in 1/Q). Near-resonant frequencies (v_r·k small, |k| comparable to M) are paid for by the extra torus derivatives in (8.10); with only finite regularity one would get only finite flatness.",
"antecedent": "None cited. Internal: the Diophantine inequality (6.7), proved in Section 6 by multiplying v_r·n = (n_1 + n_2) − √2 n_2 by its algebraic conjugate, which gives a nonzero integer. Recognizable classical ingredients (not cited): small divisors for a linear flow on T^2 with a badly approximable slope, and repeated integration by parts.",
"cost": "Flatness holds only at each fixed derivative order. The number of torus derivatives needed grows like m + p + 3, constants depend on p, and no estimate uniform in p is asserted. Since κ_s = 10^{−5}, p must be of order (N + L)/(hκ_s), so every torus-dependent source must be controlled at every derivative order.",
"checkable": "Take F(U, y) = exp(−U^2)cos(2πk·y) with k ≠ 0; compute ∫F(U + u, y + Mu v_r) du by quadrature for increasing M and compare with the closed form, whose amplitude is √π exp(−π^2 M^2 (v_r·k)^2), faster than any power of M. Separately check that |v·n|(1 + |n|) stays bounded below for v = v_r, v_t. Run while digesting: the minimum over 0 < max(|n_1|, |n_2|) ≤ 300 is about 0.385 for both.",
"depends_on": [
"M8.3",
"M6.4",
"M6.3",
"M6.8"
],
"constrains": [],
"reasons": {
"M8.3": "Estimates the cutoff remainder A_e f = R^{-e}(∂_Rχ_m)J(R^e f) of the primitive T_e.",
"M6.4": "The torus inverse L^{-p} on zero-mean functions loses only p + 3 derivatives by the Diophantine bound (6.7) for v_r.",
"M6.3": "Each integration by parts along the path gains M^{-1} ≤ Cε^{κ_s}S*^{ρ_g}, the radial winding of the covering.",
"M6.8": "Haar invariance on the common torus gives ⟨Jg⟩_Y = ∫⟨g⟩_Y dR, which vanishes under the weighted mean condition."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 90-92"
},
{
"id": "M8.5",
"kind": "move",
"name": "ns-m8-5-compactly-supported-pressure-with-the-defect-p-isolated",
"title": "Compactly supported pressure with the defect P isolated on a bump",
"section": "8",
"pages": "92-93",
"refs": [
"pages 92 to 93",
"(8.11), (8.12), (8.13)",
"Proposition 8.3(i)."
],
"statement": "Proposition 8.3(i): with a fixed bump ρ_phys = q^{−1/2} ρ̂(r/√q) in the mean patch, ∫ρ̂ = 1, ρ = Q^{1/2} ρ_phys, define P = ∫⟨g_r⟩_Y dR and p_m = T_0(g_r − ρP) (8.12). Then D_r p_m − g_r = −ρP − A_0(g_r − ρP) and ∂_R⟨p_m⟩_Y = ⟨g_r⟩_Y − ρP (8.13). If g_r ∈ M^α then P ∈ S^α and p_m ∈ M^α, changes of g_r in M^α give pressure changes in M^α, and the remainder has zero auxiliary mean and is flat.",
"description": "Proposition 8.3(i): with a fixed bump ρ_phys = q^{−1/2} ρ̂(r/√q) in the mean patch, ∫ρ̂ = 1, ρ = Q^{1/2} ρ_phys, define P = ∫⟨g_r⟩_Y dR and p_m = T_0(g_r − ρP) (8.12). Then D_r p_m − g_r = −ρP − A_0(g_r − ρP) and ∂_R⟨p_m⟩_Y = ⟨g_r⟩_Y − ρP (8.13). If g_r ∈ M^α then P ∈ S^α and p_m ∈ M^α, changes of g_r in M^α give pressure changes in M^α, and the remainder has zero auxiliary mean and is flat. OBLIGATION: Solves the radial mean balance by pressure alone while keeping p_m compactly supported in the shell. A direct radial integral of g_r would leave the constant P beyond the shell and alter the exterior pressure normalization of (3.5). The obstruction is compressed into one scalar P(Z, T) times a fixed interior bump, to be cancelled later by the third row of (8.25). MECHANISM: The shifted source g_r − ρP has zero weighted auxiliary-mean integral, P − P∫ρ dR = 0, so Lemma 8.2 with e = 0 applies and its. ANTECEDENT: None cited. Internal parallel: the pressure increment C_p among the five cumulative profile integrals (4.15), whose preservation keeps the exterior pressure unchanged across profile joins (Lemma 4.4). REFS: pages 92 to 93; (8.11), (8.12), (8.13); Proposition 8.3(i).",
"obligation": "Solves the radial mean balance by pressure alone while keeping p_m compactly supported in the shell. A direct radial integral of g_r would leave the constant P beyond the shell and alter the exterior pressure normalization of (3.5). The obstruction is compressed into one scalar P(Z, T) times a fixed interior bump, to be cancelled later by the third row of (8.25).",
"backward_question": "The pressure obtained by integrating the centrifugal balance outward is a nonzero constant beyond the shell; how can the pressure stay compactly supported, and where should the obstruction go?",
"mechanism": "The shifted source g_r − ρP has zero weighted auxiliary-mean integral, P − P∫ρ dR = 0, so Lemma 8.2 with e = 0 applies and its remainder is flat with zero auxiliary mean; after auxiliary averaging, ∂_R⟨p_m⟩_Y = ⟨g_r⟩_Y − ρP holds exactly. P ∈ S^α follows by integrating derivatives over the bounded shell; ρP ∈ M^α because ρ is an interior bump. Since ρ is fixed independently of the velocity, the same argument bounds pressure differences by source differences.",
"antecedent": "None cited. Internal parallel: the pressure increment C_p among the five cumulative profile integrals (4.15), whose preservation keeps the exterior pressure unchanged across profile joins (Lemma 4.4).",
"cost": "The defect P ∈ S^α and a standing term −ρP in the radial equation until it is corrected. The pressure must be reconstructed after every velocity change; the radial residual of every correction state is −ρP plus a flat remainder (Definition 9.4).",
"checkable": "For Y-independent compactly supported g_r(R) and a unit-mass bump ρ, compute P = ∫g_r dR and p_m(R) = ∫_0^R (g_r − ρP) dR′, and check p_m = 0 beyond the shell and ∂_R p_m − g_r = −ρP. Run while digesting inside the (8.16) test of M8.7: p_m vanishes exactly at the outer edge.",
"depends_on": [
"M8.3",
"M8.4",
"M8.2"
],
"constrains": [],
"reasons": {
"M8.3": "Defines p_m = T_0(g_r − ρP) with the e = 0 primitive, compactly supported in the shell, with D_r T_0 f = f − A_0 f.",
"M8.4": "The shifted source has zero weighted auxiliary-mean integral, so the remainder A_0(g_r − ρP) has zero mean and is flat.",
"M8.2": "Solves the radial row D_r p_m = g_r of the angular-mean balance, with g_r from (8.3)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 92-93"
},
{
"id": "M8.6",
"kind": "move",
"name": "ns-m8-6-axial-increments-realized-by-a-compactly-supported",
"title": "Axial increments realized by a compactly supported azimuthal potential",
"section": "8",
"pages": "93",
"refs": [
"page 93",
"(8.14)",
"Proposition 8.3(ii)."
],
"statement": "Proposition 8.3(ii): for a shell-supported desired axial increment γ_d with ∫R⟨γ_d⟩_Y dR = 0 at every (Z, T), set Ψ = r^{−1} I_c(r γ_{d,phys}) using (8.4), and Ψ_* = T_1 γ_d, ∆β = −ε∂_Z Ψ_*, ∆γ = (D_r + 1/R)Ψ_* = γ_d − A_1 γ_d (8.14). The increment (∆β, 0, ∆γ) is exactly divergence-free and ⟨∆γ⟩_Y = ⟨γ_d⟩_Y. If γ_d ∈ M^α then Ψ_*, ∆γ ∈ M^α and ∆β ∈ M^{α+1}; if γ_d is Y-independent, ∆γ = γ_d pointwise. Pressure and potential stay in the shell and in the (Z, T)-projection of the source.",
"description": "Proposition 8.3(ii): for a shell-supported desired axial increment γ_d with ∫R⟨γ_d⟩_Y dR = 0 at every (Z, T), set Ψ = r^{−1} I_c(r γ_{d,phys}) using (8.4), and Ψ_* = T_1 γ_d, ∆β = −ε∂_Z Ψ_*, ∆γ = (D_r + 1/R)Ψ_* = γ_d − A_1 γ_d (8.14). The increment (∆β, 0, ∆γ) is exactly divergence-free and ⟨∆γ⟩_Y = ⟨γ_d⟩_Y. If γ_d ∈ M^α then Ψ_*, ∆γ ∈ M^α and ∆β ∈ M^{α+1}; if γ_d is Y-independent, ∆γ = γ_d pointwise. Pressure and potential stay in the shell and in the (Z, T)-projection of the source. OBLIGATION: Lets later steps prescribe the axial mean velocity (from the temporal inverse and from the five-equation map) while preserving exact incompressibility, required by Theorem 3.1(i), and compact support, and supplies the induced radial velocity without solving an elliptic problem. MECHANISM: The potential Ψe_θ generates the meridional velocity (−∂_z Ψ, 0, (r + 1/r)Ψ); ANTECEDENT: None cited. Recognizable classical ingredient (not cited): the Stokes streamfunction (azimuthal vector potential) of an axisymmetric meridional flow. Internal: the same device builds the background, A_n = (S_n/r)e_θ in (5.27). REFS: page 93; (8.14); Proposition 8.3(ii).",
"obligation": "Lets later steps prescribe the axial mean velocity (from the temporal inverse and from the five-equation map) while preserving exact incompressibility, required by Theorem 3.1(i), and compact support, and supplies the induced radial velocity without solving an elliptic problem.",
"backward_question": "How can one prescribe the axial mean velocity inside a thin shell and keep the field exactly divergence-free and compactly supported, and what does the anisotropic geometry say about the size of the radial velocity this forces?",
"mechanism": "The potential Ψe_θ generates the meridional velocity (−∂_z Ψ, 0, (r + 1/r)Ψ); because r and ∂_z commute after phase evaluation, (r + r^{−1})(−∂_z Ψ) + ∂_z((r + r^{−1})Ψ) = 0 identically. The weighted primitive identity (8.7) with e = 1 gives ∆γ = γ_d − A_1 γ_d, and the zero axial-flux integral makes the remainder mean-zero and flat and makes Ψ vanish beyond the shell. The radial component gains ε = Q^{1/2 − D} = Q^h because axial lengths Q^D exceed radial lengths Q^{1/2}: in the slender geometry, induced radial flows are one order smaller.",
"antecedent": "None cited. Recognizable classical ingredient (not cited): the Stokes streamfunction (azimuthal vector potential) of an axisymmetric meridional flow. Internal: the same device builds the background, A_n = (S_n/r)e_θ in (5.27).",
"cost": "Every desired axial increment must have zero axial flux. The realized ∆γ differs from γ_d by the flat remainder A_1 γ_d, which must be carried, since its products can acquire nonzero auxiliary means (M8.13).",
"checkable": "For γ_d(R) with ∫Rγ_d dR = 0, compute Ψ_* = R^{−1}∫_0^R R′γ_d dR′; verify (∂_R + 1/R)Ψ_* = γ_d, Ψ_* = 0 beyond the support, and symbolically (∂_R + 1/R)(−ε∂_Z Ψ_*) + ε∂_Z((∂_R + 1/R)Ψ_*) = 0.",
"depends_on": [
"M8.3",
"M8.4",
"M8.1",
"M6.12"
],
"constrains": [],
"reasons": {
"M8.3": "Ψ* = T_1γ_d uses the e = 1 primitive, so (D_r + 1/R)Ψ* = γ_d − A_1γ_d and Ψ vanishes beyond the shell.",
"M8.4": "Under zero axial flux the remainder A_1γ_d has zero auxiliary mean and is flat, and it vanishes when γ_d is Y-independent.",
"M8.1": "The increment has the mean-correction form (β, 0, γ), and its zero-flux hypothesis is the moment M_z of (8.2).",
"M6.12": "∆β = −ε∂_ZΨ* is one order smaller because D_z = ε∂_Z raises the class exponent by one."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 93"
},
{
"id": "M8.7",
"kind": "move",
"name": "ns-m8-7-the-three-compatibility-defects-and-the-integrated",
"title": "The three compatibility defects and the integrated identities",
"section": "8",
"pages": "93-94",
"refs": [
"pages 93 to 94",
"(8.15), (8.16), (8.17)",
"Proposition 8.4",
"consumer (9.12) on page 108."
],
"statement": "Define J_θ = ∫R^2⟨Gv + Vγ + γv + W_zθ⟩_Y dR, J_z = ∫R⟨2Gγ + γ^2 + W_zz⟩_Y dR − (1/2)∫R^2⟨g_r⟩_Y dR, and c_ρ = (1/2)∫R^2 ρ dR (8.15). Proposition 8.4: if (8.2) holds at every (Z, T) and p_m is reconstructed by (8.12), then ∫R^2⟨E_θ⟩_Y dR = ε∂_Z J_θ and ∫R⟨E_z⟩_Y dR = ε∂_Z(J_z + c_ρ P) (8.16). Physical and normalized moments are related by (8.17).",
"description": "Define J_θ = ∫R^2⟨Gv + Vγ + γv + W_zθ⟩_Y dR, J_z = ∫R⟨2Gγ + γ^2 + W_zz⟩_Y dR − (1/2)∫R^2⟨g_r⟩_Y dR, and c_ρ = (1/2)∫R^2 ρ dR (8.15). Proposition 8.4: if (8.2) holds at every (Z, T) and p_m is reconstructed by (8.12), then ∫R^2⟨E_θ⟩_Y dR = ε∂_Z J_θ and ∫R⟨E_z⟩_Y dR = ε∂_Z(J_z + c_ρ P) (8.16). Physical and normalized moments are related by (8.17). OBLIGATION: Characterizes exactly when the auxiliary-averaged tangential residuals can be written as radial divergences of compactly supported stresses (their R^2- and R-weighted integrals must vanish), reducing an infinite-dimensional obstruction to three scalar functions P, J_θ, J_z of (Z, T). It also shows the weighted moments carry an explicit factor ε∂_Z, a free gain of one order that Section 9 uses as (9.12). MECHANISM: The weights are exactly those that turn the cylindrical divergences into exact derivatives: R^2(∂_R + 2/R)F = ∂_R(R^2 F) and R(∂_R + 1/R)F = ∂_R(RF). ANTECEDENT: None cited. Internal: the zero-moment conditions with the same weights for the leading stress in Section 3.2 and Lemma A.8. REFS: pages 93 to 94; (8.15), (8.16), (8.17); Proposition 8.4; consumer (9.12) on page 108.",
"obligation": "Characterizes exactly when the auxiliary-averaged tangential residuals can be written as radial divergences of compactly supported stresses (their R^2- and R-weighted integrals must vanish), reducing an infinite-dimensional obstruction to three scalar functions P, J_θ, J_z of (Z, T). It also shows the weighted moments carry an explicit factor ε∂_Z, a free gain of one order that Section 9 uses as (9.12).",
"backward_question": "After every radial divergence integrates to zero by compact support, which scalar obstructions survive in the weighted integrals of the mean equations, and do they carry any extra small factor?",
"mechanism": "The weights are exactly those that turn the cylindrical divergences into exact derivatives: R^2(∂_R + 2/R)F = ∂_R(R^2 F) and R(∂_R + 1/R)F = ∂_R(RF). Hence every radial flux, including W and the base stress Σ, integrates to zero by compact support. Radial viscosity integrates to zero by two integrations by parts: for θ the coefficient is (2 − 1 − 1) = 0, for z it is −∫γ_R + ∫γ_R = 0. Auxiliary averaging turns t_* into −ε∂_T and D_r into ∂_R, so the time and axial-viscosity terms are ∂_T and ∂_Z^2 of the constrained moments (8.2), hence zero. Only the axial fluxes D_z(...) = ε∂_Z(...) survive. The pressure moment follows from the compactly supported reconstruction by one more integration by parts, ∫R⟨p_m⟩_Y dR = −(1/2)∫R^2 ∂_R⟨p_m⟩_Y dR = −(1/2)∫R^2⟨g_r⟩_Y dR + c_ρ P, which is why J_z contains the g_r moment. Because ρ is scaled by the moving q, c_ρ depends on (Z, T), so the whole product c_ρ P stays inside ∂_Z.",
"antecedent": "None cited. Internal: the zero-moment conditions with the same weights for the leading stress in Section 3.2 and Lemma A.8.",
"cost": "Three scalar defects that must be corrected at every cycle (M8.11). The (Z, T)-dependent c_ρ couples the P and J_z corrections.",
"checkable": "Symbolic check with Y-independent fields, run while digesting with exact residual 0 for both identities: on R ∈ [1, 2] with φ = (R − 1)^4(2 − R)^4, take the meridional correction from Ψ = φA(Z, T), v = φ(R − c)B(Z, T) with c chosen so ∫R^2 v dR = 0, an arbitrary polynomial base (b, V, G), compactly supported W and Σ, and a unit-mass ρ whose second moment depends on Z; compute g_r, P, p_m, E_θ, E_z, J_θ, J_z, c_ρ from (8.3), (8.12), (8.15), and compare both sides of (8.16).",
"depends_on": [
"M8.2",
"M8.1",
"M8.5",
"M6.3"
],
"constrains": [],
"reasons": {
"M8.2": "Integrates the conservative rows E_θ, E_z of (8.3), whose radial fluxes are cylindrical divergences that vanish under the R² and R weights.",
"M8.1": "The moments M_θ = M_z = 0 of (8.2) remove the time-derivative and axial-viscosity terms from the weighted integrals.",
"M8.5": "The pressure moment comes from the reconstruction (8.12), which puts −½∫R²⟨g_r⟩_Y and c_ρP into J_z.",
"M6.3": "Auxiliary averaging turns t* = −ε∂_T + c_{i0}N_{i0} into −ε∂_T and D_r into ∂_R, since torus derivatives average to zero."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 93-94"
},
{
"id": "M8.8",
"kind": "move",
"name": "ns-m8-8-auxiliary-independent-covariance-targets-for-the-averaged",
"title": "Auxiliary-independent covariance targets for the averaged tangential residual",
"section": "8",
"pages": "94-95",
"refs": [
"pages 94 to 95",
"(8.18)",
"Corollary 8.5",
"Proposition 7.6 and (7.31) on page 84",
"Proposition 9.6, Step 2 on pages 108 to 109."
],
"statement": "Corollary 8.5: with interior bumps σ_{θ,phys} = q^{−3/2} σ̂_θ(r/√q), σ_{z,phys} = q^{−1} σ̂_z(r/√q), ∫ξ^2 σ̂_θ = ∫ξ σ̂_z = 1, chart forms σ_θ = Q^{3/2}σ_{θ,phys}, σ_z = Qσ_{z,phys} (so ∫R^2 σ_θ dR = ∫R σ_z dR = 1), define H_θ = −T_2(⟨E_θ⟩_Y − σ_θ ε∂_Z J_θ) and H_z = −T_1(⟨E_z⟩_Y − σ_z ε∂_Z(J_z + c_ρ P)) (8.18).",
"description": "Corollary 8.5: with interior bumps σ_{θ,phys} = q^{−3/2} σ̂_θ(r/√q), σ_{z,phys} = q^{−1} σ̂_z(r/√q), ∫ξ^2 σ̂_θ = ∫ξ σ̂_z = 1, chart forms σ_θ = Q^{3/2}σ_{θ,phys}, σ_z = Qσ_{z,phys} (so ∫R^2 σ_θ dR = ∫R σ_z dR = 1), define H_θ = −T_2(⟨E_θ⟩_Y − σ_θ ε∂_Z J_θ) and H_z = −T_1(⟨E_z⟩_Y − σ_z ε∂_Z(J_z + c_ρ P)) (8.18). OBLIGATION: Converts the auxiliary-averaged tangential residual into a compactly supported stress target that waves can supply. Since W_rθ, W_rz enter E_θ, E_z through +(D_r + 2/R) and +(D_r + 1/R), a covariance increment equal to (H_θ, H_z) cancels ⟨E_θ⟩_Y, ⟨E_z⟩_Y except for bump terms carrying ε∂_Z J_θ and ε∂_Z(J_z + c_ρ P). Auxiliary independence is exactly the hypothesis of the signed amplitude map of Proposition 7.6. ANTECEDENT: None cited in Section 8. Internal: the stress formulas of Section 3.2 and Proposition 4.2, here with a cutoff and a moment subtraction. The introduction credits Daneri and Székelyhidi [10] with the general use of oscillations to realize a prescribed stress. REFS: pages 94 to 95; (8.18); Corollary 8.5; Proposition 7.6 and (7.31) on page 84; Proposition 9.6, Step 2 on pages 108 to 109.",
"obligation": "Converts the auxiliary-averaged tangential residual into a compactly supported stress target that waves can supply. Since W_rθ, W_rz enter E_θ, E_z through +(D_r + 2/R) and +(D_r + 1/R), a covariance increment equal to (H_θ, H_z) cancels ⟨E_θ⟩_Y, ⟨E_z⟩_Y except for bump terms carrying ε∂_Z J_θ and ε∂_Z(J_z + c_ρ P). Auxiliary independence is exactly the hypothesis of the signed amplitude map of Proposition 7.6.",
"backward_question": "What compactly supported, torus-independent stress pair, added as wave covariance, would cancel the averaged tangential residual, and what minimal remainder must be conceded to make it compactly supported?",
"mechanism": "Subtracting the bump times the weighted moment makes each source Y-independent with zero weighted integral (by (8.16) and the unit moments), so by the last clause of Lemma 8.2 the cutoff remainder vanishes identically and T_2, T_1 invert exactly. The primitives act at fixed (Z, T), so axial support is preserved. The bumps are defined physically, so they agree on chart overlaps. The factors ε∂_Z are retained in the bump terms so the three defects can later be corrected at fixed (Z, T) without losing them.",
"antecedent": "None cited in Section 8. Internal: the stress formulas of Section 3.2 and Proposition 4.2, here with a cutoff and a moment subtraction. The introduction credits Daneri and Székelyhidi [10] with the general use of oscillations to realize a prescribed stress.",
"cost": "Leaves σ_θ ε∂_Z J_θ and σ_z ε∂_Z(J_z + c_ρ P) in the residual, small only once the defects are improved. H_θ, H_z are targets only; realizing them is Section 9's job (Proposition 9.6, Step 2 redoes this construction in physical variables with bumps b_e and moments M_e).",
"checkable": "For Y-independent E_θ(R) with M = ∫R^2 E_θ dR, compute H_θ = −R^{−2}∫_0^R R′^2(E_θ − σ_θ M) dR′ and check that it vanishes beyond the shell and that (∂_R + 2/R)H_θ = −E_θ + σ_θ M; same for z with weight R and T_1.",
"depends_on": [
"M8.7",
"M8.3",
"M8.4",
"M8.2"
],
"constrains": [],
"reasons": {
"M8.7": "By (8.16) the weighted moments of ⟨E_θ⟩_Y, ⟨E_z⟩_Y equal ε∂_Z J_θ and ε∂_Z(J_z + c_ρP), which the unit-moment bumps subtract.",
"M8.3": "H_θ and H_z are built with the compactly supported primitives T_2 and T_1, which act at fixed (Z, T).",
"M8.4": "The sources are Y-independent with zero weighted integral, so the cutoff remainders vanish identically and T_2, T_1 invert exactly.",
"M8.2": "The covariances W_rθ, W_rz enter E_θ, E_z through (D_r + 2/R) and (D_r + 1/R), so covariance targets can cancel them."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 94-95"
},
{
"id": "M8.9",
"kind": "move",
"name": "ns-m8-9-temporal-corrector-inverting-the-fast-auxiliary-time",
"title": "Temporal corrector: inverting the fast auxiliary-time derivative",
"section": "8",
"pages": "95-96",
"refs": [
"pages 95 to 96",
"Lemma 8.6, (8.19) to (8.23)",
"(6.2), (6.6) on page 63, (6.7) on page 64."
],
"statement": "Lemma 8.6: for N = v_t·∂_y on T^2 and zero-mean F, N^{−1}F = Σ_{k ≠ 0} F̂(k) e^{2πik·y}/(2πi v_t·k) is the unique smooth zero-mean solution, with ‖N^{−1}F‖_{C^m_y} ≤ C_m ‖F‖_{C^{m+4}_y} (8.19). The desired increments are ∆v = −c_{i0}^{−1} N_{i0}^{−1} E°_θ and γ_d = −c_{i0}^{−1} N_{i0}^{−1} E°_z, with c_{i0}^{−1} ≤ CS_* (8.20), defined physically as −N_abs^{−1}(E°_{θ,phys}, E°_{z,phys}).",
"description": "Lemma 8.6: for N = v_t·∂_y on T^2 and zero-mean F, N^{−1}F = Σ_{k ≠ 0} F̂(k) e^{2πik·y}/(2πi v_t·k) is the unique smooth zero-mean solution, with ‖N^{−1}F‖_{C^m_y} ≤ C_m ‖F‖_{C^{m+4}_y} (8.19). The desired increments are ∆v = −c_{i0}^{−1} N_{i0}^{−1} E°_θ and γ_d = −c_{i0}^{−1} N_{i0}^{−1} E°_z, with c_{i0}^{−1} ≤ CS_* (8.20), defined physically as −N_abs^{−1}(E°_{θ,phys}, E°_{z,phys}). OBLIGATION: Cancels the zero-auxiliary-mean part E°_θ, E°_z of the tangential mean residual, which cannot be handled by a stress target (Proposition 7.6 requires Y-independent stresses). What remains is the slow time derivative −ε∂_T of the increment (one extra ε) plus transport and viscous changes. MECHANISM: In chart variables t_* = −ε∂_T + c_{i0}N_{i0} with c_{i0} ≍ S_*^{−1}: the fast term is order one, the slow term costs ε. ANTECEDENT: None cited. Internal: (6.7), the covering (6.5), the operators (6.6), Lemma 6.2. Recognizable classical ingredient (not cited): the cohomological equation for a linear flow on T^2 with Diophantine frequency, used here as a temporal corrector. REFS: pages 95 to 96; Lemma 8.6, (8.19) to (8.23); (6.2), (6.6) on page 63, (6.7) on page 64.",
"obligation": "Cancels the zero-auxiliary-mean part E°_θ, E°_z of the tangential mean residual, which cannot be handled by a stress target (Proposition 7.6 requires Y-independent stresses). What remains is the slow time derivative −ε∂_T of the increment (one extra ε) plus transport and viscous changes.",
"backward_question": "Can a mean residual that oscillates on the auxiliary torus with zero average be absorbed by a mean velocity whose fast time derivative equals it, and what do the small divisors of the irrational time direction cost?",
"mechanism": "In chart variables t_* = −ε∂_T + c_{i0}N_{i0} with c_{i0} ≍ S_*^{−1}: the fast term is order one, the slow term costs ε. An increment whose fast time derivative equals −E° cancels E° exactly, and its slow derivative is smaller by ε. N^{−1} is a Fourier multiplier on nonzero frequencies, bounded because |v_t·k|^{−1} ≤ C(1 + |k|) by (6.7); four torus derivatives are lost (one for the divisor, three for summability of (1 + |k|)^{−3} in two dimensions). Both increments have zero auxiliary mean at every point, so they preserve (8.2) and satisfy the flux hypothesis of Proposition 8.3(ii). N commutes with I, J, and I_c (the shifts are torus translations and χ_m is torus independent), so the axial realization error c_{i0}N_{i0}a is flat by (8.8). The velocity factor Q^{A − (2A + 1/2)} T_g^{−i0} = Q^{−1−h} T_g^{−i0} = c_{i0}^{−1}, and (8.23), which follows from J_g v_t = T_g v_t, makes the physical definition agree on chart overlaps.",
"antecedent": "None cited. Internal: (6.7), the covering (6.5), the operators (6.6), Lemma 6.2. Recognizable classical ingredient (not cited): the cohomological equation for a linear flow on T^2 with Diophantine frequency, used here as a temporal corrector.",
"cost": "Loss of four torus derivatives and a factor c_{i0}^{−1} ≤ CS_* (polynomial in S_* = ℓ^2). The inverse need not preserve auxiliary-torus support, so mean fields may occupy the whole torus. The slow term −ε∂_T of the increments and the flat remainder F_ax = c_{i0}N_{i0}(∆γ − γ_d) are carried into the next residual.",
"checkable": "FFT on a 2D torus grid: for random smooth zero-mean F, apply the multiplier 1/(2πi v_t·k), verify N(N^{−1}F) = F and the C^m versus C^{m+4} bound across resolutions. Verify J_g v_t = T_g v_t and J_g v_r = Λ_g v_r for J_g = [[3, 1], [1, 5]], T_g = 4 + √2, Λ_g = 4 − √2, v_t = (√2 − 1, 1), v_r = (1, 1 − √2). Run while digesting: both hold to machine precision and det J_g = 14.",
"depends_on": [
"M6.4",
"M6.3",
"M8.2",
"M8.6"
],
"constrains": [],
"reasons": {
"M6.4": "The multiplier 1/(2πi v_t·k) is bounded by C(1 + |k|) by the Diophantine bound (6.7), which costs four torus derivatives.",
"M6.3": "In t* = −ε∂_T + c_{i0}N_{i0}, c_{i0}^{-1} ≤ CS* makes the fast derivative order one, and N_abs = T_g^i N_i gives chart consistency.",
"M8.2": "The inverted quantities are the zero-auxiliary-mean parts E°_θ, E°_z of the tangential mean residuals of (8.3).",
"M8.6": "The axial increment γ_d is realized by the potential of (8.14), with a flat remainder since γ_d has zero auxiliary mean."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 95-96"
},
{
"id": "M8.10",
"kind": "move",
"name": "ns-m8-10-the-reserved-mean-patch-power-law-swirl-no-axial-base-flow",
"title": "The reserved mean patch: power-law swirl, no axial base flow",
"section": "8",
"pages": "96-97",
"refs": [
"pages 96 to 97",
"(8.24)",
"Theorem 4.6(vi) on page 33 and (4.30) on page 34",
"(5.18) on page 52",
"(5.44) on page 60."
],
"statement": "On x = r/√q ∈ I_m, the image of I_mean (Theorem 4.6(vi)) under X ↦ √(2X), the q-normalized summed base is G_q = 0, V_q = a(η) x^{−1−2λ}, |a(η)| ≥ a_0 > 0, a(η) = 2^{1/2+λ} c_patch (1 + η^2)^{−1}, with the fixed λ > 0 (8.24). The exact summed-base statement is (5.44); higher-order coefficients vanish there by (5.18).",
"description": "On x = r/√q ∈ I_m, the image of I_mean (Theorem 4.6(vi)) under X ↦ √(2X), the q-normalized summed base is G_q = 0, V_q = a(η) x^{−1−2λ}, |a(η)| ≥ a_0 > 0, a(η) = 2^{1/2+λ} c_patch (1 + η^2)^{−1}, with the fixed λ > 0 (8.24). The exact summed-base statement is (5.44); higher-order coefficients vanish there by (5.18). OBLIGATION: Supplies an explicit, torus-independent base on which the five-equation map (M8.11) is exactly block diagonal and explicitly invertible, with the same inverse at every correction stage. MECHANISM: Theorem 4.6(vi) reserves I_mean ⊂ (X_a, X_v), where U = 0 and E = c_patch(1 + η^2)^{−1} X^{−1/2−λ} (4.30). Section 5 keeps every positive-order background coefficient zero there (5.18), so u_B = u^{(0)} on the patch (5.44). Cutoffs in q applied to azimuthal potentials create no axial component there, because q does not depend on r. Substituting X = x^2/2 gives (8.24). ANTECEDENT: None cited. Internal: Theorem 4.6(vi) and (4.30), (5.18), (5.44). The same reserved-patch device is used on I_pos in Lemma 5.2 and in Appendix A. REFS: pages 96 to 97; (8.24); Theorem 4.6(vi) on page 33 and (4.30) on page 34; (5.18) on page 52; (5.44) on page 60.",
"obligation": "Supplies an explicit, torus-independent base on which the five-equation map (M8.11) is exactly block diagonal and explicitly invertible, with the same inverse at every correction stage.",
"backward_question": "On what region is the base simple enough that three defects and two constraints can be corrected by an explicit finite-dimensional linear map, and why must the swirl there differ from a free vortex?",
"mechanism": "Theorem 4.6(vi) reserves I_mean ⊂ (X_a, X_v), where U = 0 and E = c_patch(1 + η^2)^{−1} X^{−1/2−λ} (4.30). Section 5 keeps every positive-order background coefficient zero there (5.18), so u_B = u^{(0)} on the patch (5.44). Cutoffs in q applied to azimuthal potentials create no axial component there, because q does not depend on r. Substituting X = x^2/2 gives (8.24). G = 0 removes the G∆v and 2RGγ_d couplings from (8.25). λ > 0 makes the base angular momentum RV ∝ x^{−2λ} vary with radius; for a free vortex (λ = 0) the J_θ row ∫R^2 Vγ_d dR would be a multiple of the axial-flux row ∫Rγ_d dR, so a zero-flux axial increment could not move J_θ.",
"antecedent": "None cited. Internal: Theorem 4.6(vi) and (4.30), (5.18), (5.44). The same reserved-patch device is used on I_pos in Lemma 5.2 and in Appendix A.",
"cost": "A structural condition that Sections 4 and 5 must preserve (an exact power law with zero axial velocity on I_mean, for every η ∈ [−1, 1]). Constants in the mean correction depend on λ and deteriorate as λ ↓ 0.",
"checkable": "Substitute X = x^2/2 into E_0 = c_patch(1 + η^2)^{−1} X^{−1/2−λ} and confirm V_q = 2^{1/2+λ} c_patch(1 + η^2)^{−1} x^{−1−2λ}. Check that at λ = 0 the vector of moments (∫R γ_d, ∫R^2 V γ_d) is rank one over all γ_d supported in the patch.",
"depends_on": [
"M4.8",
"M5.14",
"M5.8"
],
"constrains": [],
"reasons": {
"M4.8": "Theorem 4.6(vi) reserves I_mean with U = 0 and E = c_patch(1 + η²)^{-1}X^{-1/2−λ} (4.30), which becomes (8.24) under X = x²/2.",
"M5.14": "The summed background equals the leading field on the patch, the exact statement (5.44).",
"M5.8": "Every positive-order background coefficient vanishes on the mean patch by (5.18)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 96-97"
},