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": "M8.11",
"kind": "move",
"name": "ns-m8-11-five-equation-moment-correction-block-vandermonde",
"title": "Five-equation moment correction (block Vandermonde)",
"section": "8",
"pages": "97-98",
"refs": [
"pages 97 to 98",
"Lemma 8.7, (8.25), matrices A_θ and A_z on page 98",
"(8.17) on page 94."
],
"statement": "Lemma 8.7: with three azimuthal bumps η_0, η_1, η_2 and two axial bumps η_0, η_1 in I_m, geometric copies η_j(x) = a_j^{−1} η_0(x/a_j), a_j = e^{jd}, on disjoint subintervals (these η_j are unrelated to the axial similarity variable η), for arbitrary targets (P, J_θ, J_z) at each (Z, T) there is a unique linear combination (∆v, γ_d) with ∫R^2 ∆v dR = 0, ∫R γ_d dR = 0, ∫(2V/R)∆v dR = −P, ∫R^2(G∆v + Vγ_d) dR = −J_θ, ∫(2RGγ_d − RV∆v) dR = −J_z.",
"description": "Lemma 8.7: with three azimuthal bumps η_0, η_1, η_2 and two axial bumps η_0, η_1 in I_m, geometric copies η_j(x) = a_j^{−1} η_0(x/a_j), a_j = e^{jd}, on disjoint subintervals (these η_j are unrelated to the axial similarity variable η), for arbitrary targets (P, J_θ, J_z) at each (Z, T) there is a unique linear combination (∆v, γ_d) with ∫R^2 ∆v dR = 0, ∫R γ_d dR = 0, ∫(2V/R)∆v dR = −P, ∫R^2(G∆v + Vγ_d) dR = −J_θ, ∫(2RGγ_d − RV∆v) dR = −J_z. OBLIGATION: Cancels the linear parts of the three defects P, J_θ, J_z of (8.12) and (8.15), which obstruct the compactly supported pressure (the −ρP in (8.13)) and the compactly supported stresses (the bump. ANTECEDENT: None cited in the proof. Internal parallel: Lemma 4.7 and Lemma A.1 (distinct power weights against ordered disjoint bumps give an invertible moment matrix, proved there by a Rolle-type count of zeros), used for the five-moment corrections on I_pos (Lemma 5.2) and in Appendix A. The five equations (8.25) are not the five cumulative profile integrals (M, I, J, S, C_p) of (4.15), though the design is the same. REFS: pages 97 to 98; Lemma 8.7, (8.25), matrices A_θ and A_z on page 98; (8.17) on page 94.",
"obligation": "Cancels the linear parts of the three defects P, J_θ, J_z of (8.12) and (8.15), which obstruct the compactly supported pressure (the −ρP in (8.13)) and the compactly supported stresses (the bump terms in (8.18)), while preserving the two moments (9.10).",
"backward_question": "With three scalar defects to cancel and two moments to hold fixed, how many free coefficients are needed, which linear functionals of the base do they probe, and when is the resulting 5x5 system nonsingular?",
"mechanism": "Each row is linear in the increments. A swirl increment ∆v enters P through the centrifugal force 2V∆v/R and enters J_z through the pressure moment, −(1/2)∫R^2(2V/R)∆v = −∫RV∆v; an axial increment enters J_θ through axial transport of base angular momentum, ∫R^2 Vγ_d. With G = 0 the system splits into an angular block (unknowns u_j; rows: angular-momentum constraint, P, J_z; powers x^2, x^{−2−2λ}, x^{−2λ}) and an axial block (unknowns s_j; rows: flux constraint, J_θ; powers x^1, x^{1−2λ}). Power moments of geometric copies factor as ∫x^p η_j dx = μ_p e^{jdp} with μ_p = ∫x^p η_0 dx > 0, so after dividing rows by μ_p and the constants 2a, −a, a, each block is an ordinary Vandermonde matrix in the nodes e^{dp}, nonsingular because the powers are distinct for λ > 0. The resulting map is fixed once, independent of the target values; the Y-independent γ_d with zero flux has identically zero cutoff remainder, and its potential and radial velocity stay inside the patch, including between the bump supports.",
"antecedent": "None cited in the proof. Internal parallel: Lemma 4.7 and Lemma A.1 (distinct power weights against ordered disjoint bumps give an invertible moment matrix, proved there by a Rolle-type count of zeros), used for the five-moment corrections on I_pos (Lemma 5.2) and in Appendix A. The five equations (8.25) are not the five cumulative profile integrals (M, I, J, S, C_p) of (4.15), though the design is the same.",
"cost": "Inverse bounds depend on λ, d, and the bump, and degenerate as λ ↓ 0. Only the axial block degenerates: its nodes e^d and e^{d(1−2λ)} coalesce (the free-vortex degeneracy of M8.10), while the angular nodes e^{2d}, e^{−2d(1+λ)}, e^{−2dλ} stay distinct at λ = 0. Requires the patch structure of M8.10 at every stage.",
"checkable": "The natural candidate. Choose λ > 0, a, d, and a bump η_0; build A_θ and A_z as printed on page 98; solve for arbitrary targets; assemble ∆v and γ_d; verify all five integrals of (8.25) by quadrature with G = 0, V = a x^{−1−2λ}; track condition numbers as λ ↓ 0. Run while digesting (λ = 0.2, a = 1.3, d = 0.15, bump of half-width 0.05 at x_0 = 1, targets P = 0.7, J_θ = −0.4, J_z = 0.25): all five rows hold to about 1e−15; cond(A_z) ≈ 69, 278, 1.39e3, 1.39e4 at λ = 0.2, 0.05, 0.01, 0.001 (growth like 1/λ), while cond(A_θ) stays between about 100 and 118.",
"depends_on": [
"M8.10",
"M8.7",
"M8.5",
"M8.1"
],
"constrains": [],
"reasons": {
"M8.10": "On the patch G = 0 and V = a x^{-1−2λ} with λ > 0, so the five weighted integrals split into two Vandermonde blocks with distinct powers.",
"M8.7": "The targets J_θ, J_z are the flux defects of (8.15), and the last rows are their linearizations in the increments.",
"M8.5": "The target P is the radial source integral of (8.12), reached through the centrifugal term ∫(2V/R)∆v.",
"M8.1": "The first two rows keep the moments M_θ = M_z = 0 of (8.2)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 97-98"
},
{
"id": "M8.12",
"kind": "move",
"name": "ns-m8-12-exact-nonlinear-defect-update-and-its-gain",
"title": "Exact nonlinear defect update and its gain",
"section": "8",
"pages": "98-99",
"refs": [
"pages 98 to 99",
"Lemma 8.8, (8.26), (8.27), class table on page 99",
"consumer Proposition 9.6, Step 4 on page 111."
],
"statement": "Lemma 8.8: with base and w fixed, apply Lemma 8.7 to the current defects and realize γ_d by (8.14). Then R_g := g_{r,new} − g_r − (2V/R)∆v and the recomputed defects are exactly R_g = −t_*∆β − (D_r + 1/R)(2b∆β + 2β∆β + (∆β)^2) − D_z(b∆γ + G∆β + β∆γ + γ∆β + ∆β∆γ) + (2v∆v + (∆v)^2)/R + ε(∆_0 − R^{−2})∆β, (8.26) P_new = ∫⟨R_g⟩_Y dR, (J_θ)_new = ∫R^2⟨γ∆v + v∆γ + ∆γ∆v⟩_Y dR, (J_z)_new = ∫R⟨2γ∆γ + (∆γ)^2⟩_Y dR − (1/2)∫R^2⟨R_g⟩_Y dR.",
"description": "Lemma 8.8: with base and w fixed, apply Lemma 8.7 to the current defects and realize γ_d by (8.14). Then R_g := g_{r,new} − g_r − (2V/R)∆v and the recomputed defects are exactly R_g = −t_*∆β − (D_r + 1/R)(2b∆β + 2β∆β + (∆β)^2) − D_z(b∆γ + G∆β + β∆γ + γ∆β + ∆β∆γ) + (2v∆v + (∆v)^2)/R + ε(∆_0 − R^{−2})∆β, (8.26) P_new = ∫⟨R_g⟩_Y dR, (J_θ)_new = ∫R^2⟨γ∆v + v∆γ + ∆γ∆v⟩_Y dR, (J_z)_new = ∫R⟨2γ∆γ + (∆γ)^2⟩_Y dR − (1/2)∫R^2⟨R_g⟩_Y dR. OBLIGATION: Proves the five-equation correction improves the defects by a fixed power ε^{0.9−2κ_s}, which is Step 4 of Proposition 9.6 (defects in S^{H+0.9−2κ_s}), closing the defect part of the cycle. MECHANISM: Since W and the base are fixed, subtracting the two versions of the g_r row of (8.3) and expanding each quadratic product gives (8.26). The third row of (8.25) cancels the old P against ∫(2V/R)∆v; the fourth and fifth rows cancel the old J_θ, J_z against the terms linear in the base, ∫R^2(G∆v + V∆γ) and ∫(2RG∆γ − RV∆v), the latter's second part coming from −(1/2)∫R^2(2V/R)∆v. ANTECEDENT: None cited. REFS: pages 98 to 99; Lemma 8.8, (8.26), (8.27), class table on page 99; consumer Proposition 9.6, Step 4 on page 111.",
"obligation": "Proves the five-equation correction improves the defects by a fixed power ε^{0.9−2κ_s}, which is Step 4 of Proposition 9.6 (defects in S^{H+0.9−2κ_s}), closing the defect part of the cycle.",
"backward_question": "Once a fixed linear map cancels the linear parts of the defects, what exactly is left, and is it smaller by a fixed power of ε so that repeating the cycle raises the exponent?",
"mechanism": "Since W and the base are fixed, subtracting the two versions of the g_r row of (8.3) and expanding each quadratic product gives (8.26). The third row of (8.25) cancels the old P against ∫(2V/R)∆v; the fourth and fifth rows cancel the old J_θ, J_z against the terms linear in the base, ∫R^2(G∆v + V∆γ) and ∫(2RG∆γ − RV∆v), the latter's second part coming from −(1/2)∫R^2(2V/R)∆v. What remains is quadratic in small quantities or carries an extra ε: the slow time derivative of ∆β (t_*∆β = −ε∂_T ∆β since ∆β is Y-independent), radial fluxes with b = O(ε) or with radial means, axial fluxes (D_z = ε∂_Z), viscosity on ∆β, and products of ∆v, ∆γ with the current means v, γ. Class table (page 99): −t_*∆β in M^{α+2}; (D_r + 1/R)(2b∆β) in M^{α+2−κ_s}; D_z(b∆γ + G∆β) in M^{α+2}; 2v∆v/R in M^{α+0.9}; (∆v)^2/R in M^{2α}; ε(∆_0 − R^{−2})∆β in M^{α+2−2κ_s}; remaining transport in M^{α+2−κ_s}. With α ≥ 0.9 every entry is at least α + 0.9 − 2κ_s.",
"antecedent": "None cited.",
"cost": "The gain depends on the cumulative bounds v, γ ∈ M^{0.9}, β ∈ M^{1.9}, which Section 9 must maintain as (9.9), on b = O(ε) near the patch, and on α ≥ 0.9. The limiting term is 2v∆v/R, the interaction of the new swirl increment with the accumulated swirl correction.",
"checkable": "Symbolic check, run while digesting with exact residual 0: for arbitrary compactly supported increments with ∆β = −ε∂_Z Ψ, ∆γ = (∂_R + 1/R)Ψ, verify that g_{r,new} − g_r − (2V/R)∆v equals (8.26), and that P_new = P + ∫(2V/R)∆v + ∫R_g, (J_θ)_new = J_θ + ∫R^2(G∆v + V∆γ) + ∫R^2(γ∆v + v∆γ + ∆γ∆v), and (J_z)_new = J_z + ∫(2RG∆γ − RV∆v) + ∫R(2γ∆γ + (∆γ)^2) − (1/2)∫R^2 R_g; substituting rows three to five of (8.25) gives (8.27). A scaling check: set v, γ ∝ ε^{0.9}, β ∝ ε^{1.9}, targets ∝ ε^α, and fit the log-log slope of the new defects in ε (expect at least α + 0.9).",
"depends_on": [
"M8.11",
"M8.6",
"M8.2",
"M8.7"
],
"constrains": [],
"reasons": {
"M8.11": "Applies the five-equation map of Lemma 8.7, whose last three rows cancel the parts of the defect changes that are linear in the base.",
"M8.6": "γ_d is realized by (8.14), giving the induced radial velocity ∆β = −ε∂_ZΨ* that enters R_g.",
"M8.2": "R_g is the exact difference of the g_r row of (8.3) before and after the update.",
"M8.7": "The new defects are recomputed from the definitions (8.15) of J_θ, J_z and the pressure integral P."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 98-99"
},
{
"id": "M8.13",
"kind": "move",
"name": "ns-m8-13-recomputation-order-and-chart-compatibility",
"title": "Recomputation order and chart compatibility",
"section": "8",
"pages": "99-100",
"refs": [
"pages 99 to 100",
"Section 8.7."
],
"statement": "Section 8.7: for fixed base coefficients and stress, an actual tuple (β, v, γ, w) determines, in order: (1) W_ab = ⟨w_a w_b⟩_θ from the full wave velocities, and g_r from the third row of (8.3); (2) P = ∫⟨g_r⟩_Y dR and p_m = T_0(g_r − ρP); (3) E_θ, E_z from the first two rows of (8.3) with this pressure; (4) J_θ, J_z from (8.15). After either mean update the new tuple is (β + ∆β, v + ∆v, γ + ∆γ, w), with ∆γ the actual increment from (8.14), cutoff remainder included;",
"description": "Section 8.7: for fixed base coefficients and stress, an actual tuple (β, v, γ, w) determines, in order: (1) W_ab = ⟨w_a w_b⟩_θ from the full wave velocities, and g_r from the third row of (8.3); (2) P = ∫⟨g_r⟩_Y dR and p_m = T_0(g_r − ρP); (3) E_θ, E_z from the first two rows of (8.3) with this pressure; (4) J_θ, J_z from (8.15). After either mean update the new tuple is (β + ∆β, v + ∆v, γ + ∆γ, w), with ∆γ the actual increment from (8.14), cutoff remainder included; OBLIGATION: Guarantees that each correction acts on the residual of the actual current divergence-free field, so all newly created products enter the next step; that a zero-mean cutoff remainder which acquires a nonzero auxiliary mean after multiplication is retained in the pressure and compatibility integrals; and that the constructions are globally well defined (no new dyadic bands, chart independence, one-sided derivatives at η = ±1), as needed by Proposition 9.3 and Theorem 3.1(ii). MECHANISM: Radial integrals hold (z, t) fixed and q = q(z, t), so they introduce no new band, and one common covering index can be. ANTECEDENT: None cited. Internal: Lemma 6.2, (6.20), (8.4), (8.23). REFS: pages 99 to 100; Section 8.7.",
"obligation": "Guarantees that each correction acts on the residual of the actual current divergence-free field, so all newly created products enter the next step; that a zero-mean cutoff remainder which acquires a nonzero auxiliary mean after multiplication is retained in the pressure and compatibility integrals; and that the constructions are globally well defined (no new dyadic bands, chart independence, one-sided derivatives at η = ±1), as needed by Proposition 9.3 and Theorem 3.1(ii).",
"backward_question": "In what order must pressure, mean residuals, and defects be recomputed so that every correction sees the actual updated field, and are the resulting constructions independent of the chart in which they were built?",
"mechanism": "Radial integrals hold (z, t) fixed and q = q(z, t), so they introduce no new band, and one common covering index can be fixed on a neighborhood of all relevant support closures. The Fourier covariance (8.23) and bounded differences of the integer covering indices give agreement on overlaps; the radial formulas agree by their physical definition. On closed regions q ≥ c > 0, including η = ±1, only finitely many bands occur, so the fixed-shift integrals, the Fourier inverse, and the finite-dimensional correction preserve all one-sided source derivatives there.",
"antecedent": "None cited. Internal: Lemma 6.2, (6.20), (8.4), (8.23).",
"cost": "Every cutoff remainder must be kept and recomputed; one common torus index must be fixed per neighborhood; all estimates live on the single domain 0 < q < q_* fixed before the iteration.",
"checkable": "None: bookkeeping. (Its one computable ingredient, the intertwining (8.23), is covered under M8.9.)",
"depends_on": [
"M8.2",
"M8.5",
"M8.7",
"M6.8"
],
"constrains": [],
"reasons": {
"M8.2": "The order starts from W and g_r in the third row of (8.3) and ends with E_θ, E_z from its first two rows.",
"M8.5": "Step (2) reconstructs P and p_m = T_0(g_r − ρP) by (8.12) before E_z is formed.",
"M8.7": "Step (4) computes the defects J_θ, J_z from (8.15).",
"M6.8": "Chart independence uses the common torus and compatibility identity (6.20), and radial integrals at fixed (z, t) add no new band."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 99-100"
},
{
"id": "M9.1",
"kind": "move",
"name": "ns-m9-1-principal-remainder-split-and-the-linear-residual-of-a",
"title": "Principal/remainder split and the linear residual of a curl-generated pulse",
"section": "9",
"pages": "101-102",
"refs": [
"pp. 101 to 102",
"(9.1), (9.2), Proposition 9.1",
"uses (7.5), (7.9), (7.38), (7.39), (7.40), Proposition 7.2, Lemma 7.7, (6.32)."
],
"statement": "Proposition 9.1. Fix a label, a harmonic m ≠ 0, and α ∈ R. Let f_m ∈ W_α satisfy the support and smooth-extension hypotheses of Proposition 7.2, with f_m e^{ikmΦ} extending smoothly by zero outside the local rectangle including its pulse endpoints, and let (t_m, π_m) solve L_m(t_m, π_m) = -f_m, where L_m(a, π) = Q^{1+h} N_abs a + K a + ε k^2 m^2 |n_Φ|^2 a + ikm n_Φ π is the principal amplitude-pressure operator (9.1).",
"description": "Proposition 9.1. Fix a label, a harmonic m ≠ 0, and α ∈ R. Let f_m ∈ W_α satisfy the support and smooth-extension hypotheses of Proposition 7.2, with f_m e^{ikmΦ} extending smoothly by zero outside the local rectangle including its pulse endpoints, and let (t_m, π_m) solve L_m(t_m, π_m) = -f_m, where L_m(a, π) = Q^{1+h} N_abs a + K a + ε k^2 m^2 |n_Φ|^2 a + ikm n_Φ π is the principal amplitude-pressure operator (9.1). OBLIGATION: The pulse inverse only solves the ODE (7.5) along the pulse. Without this proposition nothing controls the rest of the exact linearized operator (slow transport, phase-transport defect, base derivatives and cylindrical connections, pressure-amplitude gradient, viscous amplitude derivatives, the curl. ANTECEDENT: None cited in Section 9. Internal: Proposition 7.2, Lemma 7.7, (7.40). The amplitude equation being completed is the transport of wavevector and polarization along a background flow, which the introduction (p. 2) attributes to Lifschitz and Hameiri [17] and Friedlander and Vishik [14]. REFS: pp. 101 to 102; (9.1), (9.2), Proposition 9.1; uses (7.5), (7.9), (7.38), (7.39), (7.40), Proposition 7.2, Lemma 7.7, (6.32).",
"obligation": "The pulse inverse only solves the ODE (7.5) along the pulse. Without this proposition nothing controls the rest of the exact linearized operator (slow transport, phase-transport defect, base derivatives and cylindrical connections, pressure-amplitude gradient, viscous amplitude derivatives, the curl remainder r_m, the temporal cutoff), so a correction could create an error as large as the source it removes.",
"backward_question": "Once my amplitude ODE cancels the principal part of the linearized operator on a harmonic, is every leftover term uniformly smaller by a fixed power of ε, including the curl remainder and the temporal-cutoff error?",
"mechanism": "Write the harmonic velocity as a e^{ikmΦ} with a = t_m + r_m, where Lemma 7.7 gives r_m ∈ W_{α+1/2-κ_s}. Expanding the linearized residual about the slow base (b, V, G), the terms in which the fast time derivative hits the amplitude, both viscous derivatives hit the exponential, the base shear and rotation act through the matrix K, or the pressure gradient hits the exponential make up exactly L_m, which (7.5) cancels. Everything else is (9.2), and each term carries an explicit gain from the class calculus (6.32): slow time -ε∂_T and D_z = ε∂_Z gain 1, D_r loses κ_s, (km)^{-1} = O(ε^{1/2}), b = O(ε), εk^2 = O(1), and the phase-transport defect E_ik = O(ε S_*^C) of (7.9) times km = O(ε^{-1/2}) gains 1/2. The gains table on p. 102 has minimum 1/2 - κ_s; the potential formula and chain-rule operators bring the common bound to α + 1/2 - 3κ_s, and the principal operator applied to r_m keeps r_m's exponent. Because ψ multiplies the potential and pressure before the curl, incompressibility stays exact. The leftover pieces (1 - ψ)f and ψ' t_m live where the Gaussian envelope P_v ≤ e^{-cS_*}; since S_* = ℓ^2 while Q = 2^{-ℓ}, the bound C Q^{-M} S_*^P e^{-cS_*} is O(q^N) for every N. These tails are retained additively and never fed to later forward solves.",
"antecedent": "None cited in Section 9. Internal: Proposition 7.2, Lemma 7.7, (7.40). The amplitude equation being completed is the transport of wavevector and polarization along a background flow, which the introduction (p. 2) attributes to Lifschitz and Hameiri [17] and Friedlander and Vishik [14].",
"cost": "An exponent loss of 3κ_s per application (gain 1/2 - 3κ_s rather than 1/2). Flat pulse-cutoff tails must be carried separately for the rest of the construction. Sources must extend smoothly by zero across the pulse endpoints.",
"checkable": "(a) Symbolic (sympy): in normalized cylindrical variables with D_r = ∂_R, D_z = ε∂_Z, and t_* = -ε∂_T + ∂_v on the amplitude, apply the linearized normalized Navier-Stokes operator about a general axisymmetric slow base (b, V, G)(R, Z, T) to (a(R, Z, T, v) e^{ikmΦ}, π e^{ikmΦ}) with Φ = pθ + φ(R, Z, T, v); verify that the result equals e^{ikmΦ}[L_m(a, π) + L^rem_m(a, π)] from (9.1) and (9.2) identically, with E_ik = (t_* + bD_r + (V/R)∂_θ + GD_z)Φ. (b) Numeric: evaluate exp(-cℓ^2 + (M + N)ℓ log 2 + 2C log ℓ) for ℓ up to 500 and several (c, M, N, C), and confirm it tends to 0 (flatness of the cutoff tails).",
"depends_on": [
"M7.6",
"M7.12",
"M7.13",
"M6.12"
],
"constrains": [],
"reasons": {
"M7.6": "The amplitude (t_m, π_m) solves the principal equation by Proposition 7.2, whose support and extension hypotheses the source must meet.",
"M7.12": "The velocity is the curl of the potential (7.38), with remainder r_m ∈ W_{α+1/2−κ_s} and the divergence identity (7.39).",
"M7.13": "Cutting potential and pressure by ψ leaves the flat tails of (7.40), which are retained additively.",
"M6.12": "Each non-principal term's gain is read from the cost table (6.32): −ε∂_T and D_z gain 1, D_r loses κ_s, and (km)^{-1} gains 1/2."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 101-102"
},
{
"id": "M9.2",
"kind": "move",
"name": "ns-m9-2-interaction-estimates-and-the-transversality-cancellation",
"title": "Interaction estimates and the transversality cancellation",
"section": "9",
"pages": "102-103",
"refs": [
"pp. 102 to 103",
"Lemma 9.2",
"uses (7.37), (7.39), Lemma 6.1, (6.30), (6.31)."
],
"statement": "Lemma 9.2. If w ∈ W_α is a wave and v is a mean field with tangential components in M_µ and radial component in M_{µ+1}, the nonzero harmonics of (w·∇_*)v + (v·∇_*)w lie in W_{α+µ-1/2}. For two curl-generated waves w, w' with the same label and exponents α, α', the nonzero harmonics of (w·∇_*)w' + (w'·∇_*)w lie in W_{α+α'-κ_s} and the zero harmonic in M_{α+α'-κ_s}. Distinct labels have zero products on their closed supports.",
"description": "Lemma 9.2. If w ∈ W_α is a wave and v is a mean field with tangential components in M_µ and radial component in M_{µ+1}, the nonzero harmonics of (w·∇_*)v + (v·∇_*)w lie in W_{α+µ-1/2}. For two curl-generated waves w, w' with the same label and exponents α, α', the nonzero harmonics of (w·∇_*)w' + (w'·∇_*)w lie in W_{α+α'-κ_s} and the zero harmonic in M_{α+α'-κ_s}. Distinct labels have zero products on their closed supports. OBLIGATION: Every correction produces the quadratic term ∇·(δu ⊗ δu) and cross terms with all earlier fields; the cycle gains only if these are of higher order than the source they accompany. A naive count loses a factor k ≈ ε^{-1/2} in wave self-advection, which would erase the gain of the whole cycle. MECHANISM: Mean advection of a wave differentiates the phase and costs k = O(ε^{-1/2}); ANTECEDENT: None cited in Section 9. Internal: (7.39), Lemma 6.1, Proposition 6.6. The introduction (p. 2) cites Craik and Criminale [9] for exact waves on affine flows that exploit the cancellation of the wave's quadratic self-interaction, the same transversality mechanism. REFS: pp. 102 to 103; Lemma 9.2; uses (7.37), (7.39), Lemma 6.1, (6.30), (6.31).",
"obligation": "Every correction produces the quadratic term ∇·(δu ⊗ δu) and cross terms with all earlier fields; the cycle gains only if these are of higher order than the source they accompany. A naive count loses a factor k ≈ ε^{-1/2} in wave self-advection, which would erase the gain of the whole cycle.",
"backward_question": "Wave self-advection naively costs one power of k ≈ ε^{-1/2}; is there an exact identity, valid for the complete divergence-free amplitude, that removes this loss for every pair of harmonics of one label?",
"mechanism": "Mean advection of a wave differentiates the phase and costs k = O(ε^{-1/2}); that is the -1/2 in the mean-wave bound (radial transport of the amplitude is offset by the extra order of the radial mean, axial transport gains through D_z, and wave transport of a mean costs at most κ_s). For two harmonics of one label, the phase-derivative term in the transport of a' e^{ikm'Φ} by a e^{ikmΦ} is ikm'(a·n_Φ)a'. The exact divergence identity (7.39), ikm n_Φ·a_m = -((D_r + R^{-1})(a_m)_r + D_z(a_m)_z), puts a·n_Φ in W_{α+1/2-κ_s} for the complete curl-generated amplitude, so the factor k is removed up to κ_s. This is why the advecting factor must be the full divergence-free amplitude t_m + r_m and not the transverse part t_m alone. Products of weights obey P_v^2 ≤ P_v and ζ ≤ √ζ, so a nonzero output keeps the wave weight; Lemma 6.1 separates distinct labels by disjoint auxiliary supports; Leibniz' rule extends all bounds to every fixed amplitude derivative.",
"antecedent": "None cited in Section 9. Internal: (7.39), Lemma 6.1, Proposition 6.6. The introduction (p. 2) cites Craik and Criminale [9] for exact waves on affine flows that exploit the cancellation of the wave's quadratic self-interaction, the same transversality mechanism.",
"cost": "A κ_s loss per wave-wave product. The mean-wave product loses 1/2, so the cumulative mean correction must stay small: with µ = 0.9 from (9.9) the mean-wave error sits at B + 0.4. Curl remainders must be kept in every advecting factor.",
"checkable": "Symbolic: for a θ-independent potential coefficient C(R, Z) and phase Φ = pθ + φ(R, Z), form a e^{ikmΦ} = curl_*(C e^{ikmΦ}) with curl_* from (7.37); verify div_*(a e^{ikmΦ}) = 0 and hence (7.39); then expand (a e^{ikmΦ}·∇_*)(a' e^{ikm'Φ}) in cylindrical components and check that its only term proportional to k is ikm'(a·n_Φ)a' = -(m'/m)((D_r + R^{-1})a_r + D_z a_z)a', which contains no factor k.",
"depends_on": [
"M7.12",
"M6.12",
"M6.7",
"M7.2"
],
"constrains": [],
"reasons": {
"M7.12": "The divergence identity (7.39) puts a·n_Φ in W_{α+1/2−κ_s}, which removes the factor k from wave self-advection.",
"M6.12": "The product and zero-harmonic rules (6.30), (6.31) give the classes of the wave-mean and wave-wave products.",
"M6.7": "Products of waves with distinct labels vanish by the disjoint auxiliary supports.",
"M7.2": "Mean advection differentiates the phase and costs k = ⌈ε^{-1/2}⌉, the −1/2 in the wave-mean bound."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 102-103"
},
{
"id": "M9.3",
"kind": "move",
"name": "ns-m9-3-residual-decomposition-with-a-quarantined-flat-part",
"title": "Residual decomposition with a quarantined flat part",
"section": "9",
"pages": "103-105",
"refs": [
"pp. 103 to 105",
"Proposition 9.3, (9.3), (9.4), (9.5), (9.6)",
"uses (6.23), (6.28), (7.25), (7.31), (7.33), Lemma 8.2, Proposition 8.1, (8.12)."
],
"statement": "Proposition 9.3. For any state built from the slow base and primary waves by finitely many pulse inverses and curls, signed amplitude maps for auxiliary-independent stresses, and Section 8 mean maps, with pressure reconstructed by (8.12) after each update and every product formed from the complete fields: R(u^[j], p^[j]) = G^[j] + F^[j] (9.3), where (i) the nonzero angular harmonics of G_*^[j] are a locally finite sum over labels γ and a finite, band-independent harmonic set H_j ⊂ Z \\ {0} of.",
"description": "Proposition 9.3. For any state built from the slow base and primary waves by finitely many pulse inverses and curls, signed amplitude maps for auxiliary-independent stresses, and Section 8 mean maps, with pressure reconstructed by (8.12) after each update and every product formed from the complete fields: R(u^[j], p^[j]) = G^[j] + F^[j] (9.3), where (i) the nonzero angular harmonics of G_*^[j] are a locally finite sum over labels γ and a finite, band-independent harmonic set H_j ⊂ Z \\ {0} of. OBLIGATION: The pulse inverse (Proposition 7.2) accepts only sources with prescribed slow, transverse, shell, and enlarged-rectangle supports and envelope bounds, and mean operations enlarge auxiliary support, so these hypotheses must be re-verified after every cycle. ANTECEDENT: None cited. Internal: Proposition 7.2, Proposition 7.6, (7.33), Lemma 8.2, Proposition 8.1, (8.12). REFS: pp. 103 to 105; Proposition 9.3, (9.3), (9.4), (9.5), (9.6); uses (6.23), (6.28), (7.25), (7.31), (7.33), Lemma 8.2, Proposition 8.1, (8.12).",
"obligation": "The pulse inverse (Proposition 7.2) accepts only sources with prescribed slow, transverse, shell, and enlarged-rectangle supports and envelope bounds, and mean operations enlarge auxiliary support, so these hypotheses must be re-verified after every cycle. The base error E_B, the pulse-cutoff tails, and the cutoff remainders of the compactly supported primitives do not satisfy those hypotheses but are already flat, so they must be kept out of the sources. Part (iii) guarantees that the Section 8 inverses act on the exact conservative mean balance of the full field.",
"backward_question": "Which parts of the residual must the next inverse see, and which are already flat, so that they can be set aside without ever having to satisfy that inverse's support hypotheses?",
"mechanism": "A nonzero harmonic can only come from a product containing a wave factor, and such a product inherits that wave's slow, transverse, and rectangle support and its envelope (P_v^2 ≤ P_v); mean operations never create nonzero harmonics; curls, pressure coefficients, and pulse propagation preserve the phase integer; a quadratic product at most doubles the harmonic range. The pulse inverse propagates along paths with fixed slow and transverse variables, so zero data on a whole path give a zero solution and support containment needs no divisibility by the original cutoffs. For the stress correction fed to Proposition 7.6, a supported interior profile with the same weighted radial moment is subtracted; the zero-moment remainder can be integrated forward from the left edge or backward from the right edge. Near an edge, where ζ ≈ e^{-a/s^2} with s the logarithmic distance, the weight survives integration through ∫_0^δ s^{-M} e^{-a/s^2} ds ≤ C_{M,a} δ^{3-M} e^{-a/δ^2} and |d^k/ds^k e^{-a/s^2}| ≤ C_{k,a} s^{-3k} e^{-a/s^2}. Division by the fixed amplitude a_σ, whose inverse has a ζ^{-1/2} bound, recovers (7.33) and the W_{α-1/2} estimate. The flat term F collects E_B, the Gaussian tails, and the cutoff remainders (Lemma 8.2 makes each O(q^N) at the cost of finitely many extra derivatives); summing polynomially many labels in S_* keeps these bounds; any flat term that a later mean inverse cancels is removed from F.",
"antecedent": "None cited. Internal: Proposition 7.2, Proposition 7.6, (7.33), Lemma 8.2, Proposition 8.1, (8.12).",
"cost": "The flat parts F^[j] are never summed over stages, so the final flatness has to come from comparison with one finite stage (M9.13). Constants and powers of S_* grow with j; H_j grows with j but stays finite at each stage; support containment must be re-checked after every step.",
"checkable": "Numeric check of the edge-weight integral: for a ∈ {0.5, 1, 2} and M ∈ {0, 2, 5, 10}, compute I(δ) = ∫_0^δ s^{-M} e^{-a/s^2} ds by quadrature or by the closed form (1/2) a^{(1-M)/2} Γ((M-1)/2, a/δ^2), and confirm that I(δ)/(δ^{3-M} e^{-a/δ^2}) stays bounded as δ ↓ 0 (it tends to 1/(2a)); also confirm that the supremum over 0 < s ≤ 1 of s^{3k} |∂_s^k e^{-a/s^2}| / e^{-a/s^2} is finite for k ≤ 6.",
"depends_on": [
"M7.6",
"M8.4",
"M7.11",
"M8.2"
],
"constrains": [],
"reasons": {
"M7.6": "The supported part must meet Proposition 7.2's support, extension and envelope hypotheses, which propagation along fixed paths preserves.",
"M8.4": "Cutoff remainders of the compactly supported primitives are flat by Lemma 8.2 and go into F^[j].",
"M7.11": "Stress corrections for the signed amplitude map keep the √ζ-weighted bound (7.33) after division by the fixed amplitudes.",
"M8.2": "Part (iii) is the exact conservative mean balance of Proposition 8.1 for the complete current tuple."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 103-105"
},
{
"id": "M9.4",
"kind": "move",
"name": "ns-m9-4-the-finite-correction-state-and-the-j-schedule",
"title": "The finite correction state and the σ_j schedule",
"section": "9",
"pages": "106",
"refs": [
"p. 106",
"(9.7), Definition 9.4, (9.8), (9.9), (9.10)."
],
"statement": "Definition 9.4. A stage-j state is a real field of the form (9.7): u_* = (b + β, V + v, G + γ) + w and p_* = p_{B,*} + p_m + p_w with ⟨w⟩_θ = ⟨p_w⟩_θ = 0, where w is a sum of curls of supported wave potentials with the fixed label phases and (β, v, γ) is the curl of an azimuthal potential plus a direct azimuthal field, so both corrections are exactly divergence-free. It has the structure of Proposition 9.3;",
"description": "Definition 9.4. A stage-j state is a real field of the form (9.7): u_* = (b + β, V + v, G + γ) + w and p_* = p_{B,*} + p_m + p_w with ⟨w⟩_θ = ⟨p_w⟩_θ = 0, where w is a sum of curls of supported wave potentials with the fixed label phases and (β, v, γ) is the curl of an azimuthal potential plus a direct azimuthal field, so both corrections are exactly divergence-free. It has the structure of Proposition 9.3; OBLIGATION: It is the induction hypothesis: it must hold after initialization and be reproduced with a gain by one cycle. The cumulative bounds are needed because new increments interact with the total existing correction, not only with the last increment. The moment constraints are needed for the integrated identities (8.16), which make the tangential mean residual absorbable by compactly supported stresses. ANTECEDENT: None cited. The introduction (p. 2) cites Córdoba and Martínez-Zoroa [7] for approximations of increasing order that keep every derivative of the source bounded, the nearest cited precedent for order-by-order residual improvement. REFS: p. 106; (9.7), Definition 9.4, (9.8), (9.9), (9.10).",
"obligation": "It is the induction hypothesis: it must hold after initialization and be reproduced with a gain by one cycle. The cumulative bounds are needed because new increments interact with the total existing correction, not only with the last increment. The moment constraints are needed for the integrated identities (8.16), which make the tangential mean residual absorbable by compactly supported stresses.",
"backward_question": "What is the smallest list of residual orders and cumulative field sizes that holds after initialization and is reproduced, with a uniform gain, by one cycle of corrections?",
"mechanism": "Three residual components are tracked separately: nonzero harmonics at order B_j, tangential means at C*_j, and three scalar defects at C*_j. The offset of exactly 1/2 between wave and mean orders matches the proof of Proposition 9.6: a wave increment of order B changes the mean covariance, through its product with the order-1/2 primary wave, at order B + 1/2 = C*. The cumulative bounds pin the total correction: the wave stays at the primary size 1/2, its deviation from the primary transverse field w_0^tan has order at least 0.68, tangential means and the mean pressure have order at least 0.9, and the radial mean at least 1.9 (one better, because radial mean velocity is induced as -ε∂_Z of an azimuthal potential, (8.14)). Every residual and defect is recomputed from the updated complete field after each operation.",
"antecedent": "None cited. The introduction (p. 2) cites Córdoba and Martínez-Zoroa [7] for approximations of increasing order that keep every derivative of the source bounded, the nearest cited precedent for order-by-order residual improvement.",
"cost": "Every later increment must respect the thresholds 0.68, 0.9, and 1.9; the two moments must be preserved exactly at every step; pressure must be reconstructed after every update.",
"checkable": "None: this is the definition of the induction hypothesis; its arithmetic is checked in M9.5 and M9.10.",
"depends_on": [
"M9.3",
"M8.1",
"M8.5",
"M7.12"
],
"constrains": [],
"reasons": {
"M9.3": "A stage-j state has the residual structure of Proposition 9.3: supported harmonic sources plus a quarantined flat part.",
"M8.1": "The form (9.7) is the mean decomposition (8.1), and the exact moments (9.10) are the preserved functionals (8.2).",
"M8.5": "Pressure is reconstructed by (8.12), so the radial residual is −ρP plus a flat cutoff remainder.",
"M7.12": "w is a sum of curls of supported wave potentials with the fixed label phases, hence exactly divergence-free."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 106"
},
{
"id": "M9.5",
"kind": "move",
"name": "ns-m9-5-initialization-at-stage-0",
"title": "Initialization at stage 0",
"section": "9",
"pages": "106-107",
"refs": [
"pp. 106 to 107",
"Proposition 9.5, (9.11)",
"uses (7.24), (7.25), (7.26), (7.35), (8.12), (8.20), (8.25)."
],
"statement": "Proposition 9.5. Starting from the fixed base and the curls of the primary potentials, apply the temporal mean update (8.20) and then the five-equation correction (8.25), reconstructing pressure by (8.12) before and after each update. The result is a stage-0 state with B_0 = 0.7 and C*_0 = 1.2.",
"description": "Proposition 9.5. Starting from the fixed base and the curls of the primary potentials, apply the temporal mean update (8.20) and then the five-equation correction (8.25), reconstructing pressure by (8.12) before and after each update. The result is a stage-0 state with B_0 = 0.7 and C*_0 = 1.2. OBLIGATION: Seeds the induction. The raw primary field has linear residual of order 1 - 3κ_s, nonlinear wave residual 1 - κ_s, and mean balances and defects of order only 1 - κ_s, below the required C*_0 = 1.2. MECHANISM: The decisive fact is exact: the primary covariance of Proposition 7.5, assembled by (7.35), cancels the order-zero auxiliary radial-tangential stress Σ^(0) exactly, including the derivatives of the slow partition, because the squared partition functions sum to one. Written as (9.11), the auxiliary averages of E_θ and E_z are built from differences ⟨W_rθ⟩_Y - Σ^(0)_θ and ⟨W_rz⟩_Y - Σ^(0)_z that contain at least one curl remainder (order 1 - κ_s against the order-1/2 primary. ANTECEDENT: None cited. Internal: Proposition 7.5 and (7.26), (7.35), Lemma 8.6, Lemma 8.7. REFS: pp. 106 to 107; Proposition 9.5, (9.11); uses (7.24), (7.25), (7.26), (7.35), (8.12), (8.20), (8.25).",
"obligation": "Seeds the induction. The raw primary field has linear residual of order 1 - 3κ_s, nonlinear wave residual 1 - κ_s, and mean balances and defects of order only 1 - κ_s, below the required C*_0 = 1.2.",
"backward_question": "Does the leading covariance cancel the background stress exactly, partition derivatives included, so that after the primary pulses the auxiliary-averaged residual is controlled by curl-remainder cross terms rather than by the raw quadratic products?",
"mechanism": "The decisive fact is exact: the primary covariance of Proposition 7.5, assembled by (7.35), cancels the order-zero auxiliary radial-tangential stress Σ^(0) exactly, including the derivatives of the slow partition, because the squared partition functions sum to one. Written as (9.11), the auxiliary averages of E_θ and E_z are built from differences ⟨W_rθ⟩_Y - Σ^(0)_θ and ⟨W_rz⟩_Y - Σ^(0)_z that contain at least one curl remainder (order 1 - κ_s against the order-1/2 primary, hence M_{3/2-κ_s} before the divergence), plus axial fluxes, the axial pressure term, and higher-order stress at order at least 2 - κ_s; so ⟨E_θ⟩_Y, ⟨E_z⟩_Y ∈ M_{1.49} already. The torus-dependent part of the mean residual, of order H_0 = 1 - κ_s, is removed by the temporal inverse, whose leftovers have order at least H_0 + 1 - 2κ_s, with wave interactions at H_0. The five-equation map then cancels the linear parts of the defects, and every other term gains more than 0.8, so the defects end above 1.8 - κ_s. Hence waves ≥ 1 - 3κ_s ≥ 0.7, tangential means ≥ 1.49 ≥ 1.2, defects > 1.8 - κ_s ≥ 1.2. The primary curl correction 1 - κ_s > 0.68 and the mean increments H_0 > 0.9, H_0 + 1 > 1.9 give (9.9); the temporal increments have zero auxiliary mean, and the first two rows of (8.25) enforce (9.10).",
"antecedent": "None cited. Internal: Proposition 7.5 and (7.26), (7.35), Lemma 8.6, Lemma 8.7.",
"cost": "B_0 = 0.7 is set well below the available 1 - 3κ_s; this fixes the lower bound B ≥ 0.7 used in every later cycle and the thresholds of (9.9).",
"checkable": "(a) Exponent arithmetic with κ_s = 10^{-5}: 1 - 3κ_s ≥ 0.7; 3/2 - 2κ_s ≥ 1.49 ≥ 1.2; H_0 + 1 - 2κ_s ≥ 1.2; 1.8 - κ_s ≥ 1.2; 1 - κ_s > 0.68; H_0 > 0.9; H_0 + 1 > 1.9. (b) Quadrature check of the covariance identity behind (9.11): build two model real waves b_± = χ_g(ξ)ψ(v) t_± cos(kΦ_±) on disjoint rectangles of T^2, compute H = [C(b_+) | C(b_-)] by angular and Haar quadrature, set a = sqrt(H^{-1}T) componentwise for a target T inside the cone, and confirm C(√ε(a_+ b_+ + a_- b_-)) = εT to quadrature precision.",
"depends_on": [
"M7.10",
"M8.9",
"M8.11",
"M9.4"
],
"constrains": [],
"reasons": {
"M7.10": "The primary covariance, assembled over boxes and bands, cancels the order-zero stress exactly, slow-partition derivatives included.",
"M8.9": "The temporal mean update (8.20) removes the torus-dependent part of the mean residual, of order 1 − κ_s.",
"M8.11": "The five-equation correction (8.25) cancels the linear parts of the defects and enforces the moments (9.10).",
"M9.4": "The outcome must meet Definition 9.4 with B_0 = 0.7, C*_0 = 1.2 and the cumulative bounds (9.9)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 106-107"
},
{
"id": "M9.6",
"kind": "move",
"name": "ns-m9-6-cycle-step-1-cancel-the-supported-harmonics",
"title": "Cycle step 1, cancel the supported harmonics",
"section": "9",
"pages": "108",
"refs": [
"p. 108",
"Proposition 9.6 Step 1, (9.12)",
"uses (7.13), Proposition 7.2, Proposition 9.1, Lemma 9.2, (8.15), (8.16)."
],
"statement": "Proposition 9.6(i). For each grouped supported source f_m of (9.4), solve L_m(t_m, π_m) = -f_m by Proposition 7.2 with zero initial data at the entrance of the prescribed path on the common torus, and add ∆w_m = curl_*((i n_Φ × (ψ t_m))/(km|n_Φ|^2) e^{ikmΦ}) and ∆p_{w,m} = ψ π_m e^{ikmΦ}, summed over labels and harmonics with conjugate pairs. With B = 1/2 + σ_j and C* = B + 1/2 = 1 + σ_j, the increment is in W_B and its pressure in W_{B+1/2}. New nonzero-harmonic errors: linear B + 1/2 - 3κ_s;",
"description": "Proposition 9.6(i). For each grouped supported source f_m of (9.4), solve L_m(t_m, π_m) = -f_m by Proposition 7.2 with zero initial data at the entrance of the prescribed path on the common torus, and add ∆w_m = curl_*((i n_Φ × (ψ t_m))/(km|n_Φ|^2) e^{ikmΦ}) and ∆p_{w,m} = ψ π_m e^{ikmΦ}, summed over labels and harmonics with conjugate pairs. With B = 1/2 + σ_j and C* = B + 1/2 = 1 + σ_j, the increment is in W_B and its pressure in W_{B+1/2}. New nonzero-harmonic errors: linear B + 1/2 - 3κ_s; OBLIGATION: Removes the entire nonzero-harmonic residual of order B, which no mean operation can reach, and produces the moment gain (9.12) that Step 2 needs. MECHANISM: The zero-data Duhamel inverse of Proposition 7.2 solves the principal ODE along each pulse; the cutoff and curl make the increment divergence-free; Proposition 9.1 bounds the linear error and Lemma 9.2 the interactions (old exact waves in W_{1/2}, mean correction in. ANTECEDENT: None cited. Internal: Proposition 7.2 (Duhamel formula along the pulse), Proposition 9.1, Lemma 9.2, Proposition 8.4 and (8.16). REFS: p. 108; Proposition 9.6 Step 1, (9.12); uses (7.13), Proposition 7.2, Proposition 9.1, Lemma 9.2, (8.15), (8.16).",
"obligation": "Removes the entire nonzero-harmonic residual of order B, which no mean operation can reach, and produces the moment gain (9.12) that Step 2 needs.",
"backward_question": "After the harmonics are removed, how much does the angular mean degrade, and can the conservation constraints make the weighted radial moments of the mean residual better than the residual itself?",
"mechanism": "The zero-data Duhamel inverse of Proposition 7.2 solves the principal ODE along each pulse; the cutoff and curl make the increment divergence-free; Proposition 9.1 bounds the linear error and Lemma 9.2 the interactions (old exact waves in W_{1/2}, mean correction in M_{0.9}). The new waves change the angular mean only through covariance products with existing waves, at order B + 1/2 = C*, and a radial divergence costs κ_s. The moment gain uses conservation: with (9.10) preserved, the exact integrated identities (8.16), ∫R^2 ⟨E_θ⟩_Y dR = ε∂_Z J_θ and ∫R ⟨E_z⟩_Y dR = ε∂_Z(J_z + c_ρ P), express the weighted moments as axial derivatives carrying a factor ε, one full order better than the residual itself. The term c_ρ P inside ∂_Z accounts for the -ρP left in the radial equation by pressure reconstruction.",
"antecedent": "None cited. Internal: Proposition 7.2 (Duhamel formula along the pulse), Proposition 9.1, Lemma 9.2, Proposition 8.4 and (8.16).",
"cost": "The mean residual and defects degrade by κ_s (to C* - κ_s); new flat cutoff tails join F; the new products create auxiliary-dependent means that Steps 2 and 3 must remove.",
"checkable": "Numeric check of the identity (8.16) behind (9.12): on a grid in (R, Z, T), take smooth compactly supported, Y-independent mean fields with (β, γ) = (-ε∂_Z Ψ, (∂_R + R^{-1})Ψ) from a compactly supported Ψ (so ∫R γ dR = 0 automatically) and v with ∫R^2 v dR = 0 at every (Z, T); take a smooth symmetric covariance W, a base (b, V, G), and compactly supported base stresses Σ_θ, Σ_z; compute g_r, P, p_m = T_0(g_r - ρP), E_θ, E_z from (8.3) and (8.12) with t_* = -ε∂_T and D_r = ∂_R; compare ∫R^2 E_θ dR with ε∂_Z J_θ and ∫R E_z dR with ε∂_Z(J_z + c_ρ P) from (8.15). Agreement to discretization error is expected.",
"depends_on": [
"M7.6",
"M9.1",
"M9.2",
"M8.7"
],
"constrains": [],
"reasons": {
"M7.6": "Solves L_m(t_m, π_m) = −f_m for each supported source by Proposition 7.2 with zero data along the pulse path.",
"M9.1": "Proposition 9.1 bounds the new linear residual at B + 1/2 − 3κ_s.",
"M9.2": "Lemma 9.2 bounds the new interactions with old waves, with the mean correction (B + 0.4), and the self-interaction.",
"M8.7": "The integrated identities (8.16) turn the weighted moments into ε∂_Z of defects, giving the extra order of (9.12)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 108"
},
{
"id": "M9.7",
"kind": "move",
"name": "ns-m9-7-cycle-step-2-signed-stress-correction-of-the-auxiliary",
"title": "Cycle step 2, signed stress correction of the auxiliary-averaged residual",
"section": "9",
"pages": "108-110",
"refs": [
"pp. 108 to 110",
"Proposition 9.6 Step 2, (9.13), (9.14)",
"uses (7.31), (7.34), (7.35), (7.36), (7.41), (7.42), (9.12)."
],
"statement": "Proposition 9.6(ii). In physical variables set F_2 = Q^{-2A-1/2}⟨E_θ⟩_Y and F_1 = Q^{-2A-1/2}⟨E_z⟩_Y, which agree between charts. For e ∈ {1, 2} fix an interior profile b̂_e with ∫x^e b̂_e(x) dx = 1, put b_e = q^{-(e+1)/2} b̂_e(r/√q), M_e = ∫_0^∞ r^e F_e dr, and σ_e(r) = -r^{-e} ∫_0^r (r')^e (F_e - b_e M_e) dr' at fixed (z, t). Then σ_e is compactly supported, (∂_r + e/r)σ_e = -F_e + b_e M_e, and Σ = Q^{2A}(σ_2, σ_1) ∈ M_{C*-κ_s} is auxiliary-independent.",
"description": "Proposition 9.6(ii). In physical variables set F_2 = Q^{-2A-1/2}⟨E_θ⟩_Y and F_1 = Q^{-2A-1/2}⟨E_z⟩_Y, which agree between charts. For e ∈ {1, 2} fix an interior profile b̂_e with ∫x^e b̂_e(x) dx = 1, put b_e = q^{-(e+1)/2} b̂_e(r/√q), M_e = ∫_0^∞ r^e F_e dr, and σ_e(r) = -r^{-e} ∫_0^r (r')^e (F_e - b_e M_e) dr' at fixed (z, t). Then σ_e is compactly supported, (∂_r + e/r)σ_e = -F_e + b_e M_e, and Σ = Q^{2A}(σ_2, σ_1) ∈ M_{C*-κ_s} is auxiliary-independent. OBLIGATION: The auxiliary-averaged tangential residual cannot be inverted by the fast-time derivative, which needs zero auxiliary mean, and would otherwise stay at order C*. It must be absorbed by changing the waves' radial fluxes of azimuthal and axial momentum through a compactly supported, chart-consistent stress. ANTECEDENT: None cited in Section 9. Internal: Proposition 7.6, (7.35), (7.36), Corollary 7.8. The introduction (p. 2) credits Daneri and Székelyhidi [10] with the use of oscillations to realize a prescribed stress. REFS: pp. 108 to 110; Proposition 9.6 Step 2, (9.13), (9.14); uses (7.31), (7.34), (7.35), (7.36), (7.41), (7.42), (9.12).",
"obligation": "The auxiliary-averaged tangential residual cannot be inverted by the fast-time derivative, which needs zero auxiliary mean, and would otherwise stay at order C*. It must be absorbed by changing the waves' radial fluxes of azimuthal and axial momentum through a compactly supported, chart-consistent stress.",
"backward_question": "The stress is realized as a positive combination of squared amplitudes; how can I make corrections of either sign without re-solving the positivity problem, and how can the correcting stress be compactly supported in the annulus?",
"mechanism": "Subtracting b_e M_e removes the weighted radial moment, so the primitive σ_e vanishes beyond the source support and no cutoff remainder appears; the subtracted bump term is harmless because M_e has order C* + 1 - κ_s by (9.12). The stress is realized by linearizing the covariance map at the fixed primary amplitudes: dΣ = H^{-1}(Σ/ε) and δa_σ = (dΣ)_σ/(2a_σ), so the symmetrized cross covariance with the primary wave is exactly Σ (L is a right inverse of DC(W_0), Proposition 7.6). Dividing by the fixed positive 2√y_σ allows increments of either sign, and no square root of the current covariance or of y + dΣ is ever taken. The exact expansion (9.13), ⟨∆W⟩_Y = B(w_0^tan, t_s) + B(w - w_0^tan, t_s) + B(w, r_s) + ⟨⟨s ⊗ s⟩_θ⟩_Y, isolates the term whose radial-tangential components equal Σ, whose divergence cancels F_e - b_e M_e, from three remainders: transverse correction times old-wave remainder (C* + 0.18 - κ_s, from w - w_0^tan ∈ W_{0.68}), signed curl remainder times old wave (C* + 1/2 - 2κ_s), and self-interaction (C* + σ_j - 2κ_s); the divergence costs one more κ_s. Since 0.18 - 2κ_s > 0.17 and σ_j - 3κ_s > 0.17, the auxiliary average improves by 0.17. The auxiliary-dependent part of the new products has order only H = C* - 2κ_s and is left for Step 3.",
"antecedent": "None cited in Section 9. Internal: Proposition 7.6, (7.35), (7.36), Corollary 7.8. The introduction (p. 2) credits Daneri and Székelyhidi [10] with the use of oscillations to realize a prescribed stress.",
"cost": "New wave errors of orders B + 1/2 - 4κ_s (linear), B + 0.4 - κ_s (mean interaction), B + 1/2 - 2κ_s (cross with old waves), 2B - 3κ_s (self-interaction); the full mean residual worsens to H = C* - 2κ_s; the averaged gain is capped at 0.17 by the 0.68 bound in (9.9); the primary amplitudes a_σ must stay fixed forever; the stress must be auxiliary-independent.",
"checkable": "(a) Numeric radial primitive: for a random smooth F supported in [r_1, r_2] and a bump b̂_e supported inside with ∫x^e b̂_e dx = 1, compute σ_e by cumulative quadrature and verify (∂_r + e/r)σ_e + F_e - b_e M_e = 0 on the grid and σ_e = 0 for r > r_2, for e = 1, 2. (b) Linear algebra: for a random invertible 2×2 H with y = H^{-1}T > 0, a = √y, and a random Σ, form δa = (H^{-1}Σ/ε)/(2a) componentwise; confirm εH(2a ⊙ δa) = Σ and εH((a + δa) ⊙ (a + δa)) - εH(a ⊙ a) - Σ = εH(δa ⊙ δa), the quadratic remainder kept in the residual.",
"depends_on": [
"M7.11",
"M7.14",
"M9.6",
"M9.4"
],
"constrains": [],
"reasons": {
"M7.11": "The stress Σ is realized by the signed amplitude map L^as, with B(w_0^tan, L^asΣ) = Σ by (7.36).",
"M7.14": "Corollary 7.8 gives the exact covariance change (9.13) and the orders of its three remainders.",
"M9.6": "By (9.12) the weighted moments M_e have order C* + 1 − κ_s, so the subtracted bump term b_eM_e is harmless.",
"M9.4": "The cumulative bound w − w_0^tan ∈ W_{0.68} of (9.9) sets the leading remainder order C* + 0.18 − κ_s."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 108-110"
},
{
"id": "M9.8",
"kind": "move",
"name": "ns-m9-8-cycle-step-3-fast-time-inverse-on-the-auxiliary-dependent",
"title": "Cycle step 3, fast-time inverse on the auxiliary-dependent means",
"section": "9",
"pages": "110",
"refs": [
"p. 110",
"Proposition 9.6 Step 3",
"uses (8.3), (8.14), (8.20), (8.22), Lemma 8.6, (6.7)."
],
"statement": "Proposition 9.6(iii). For E°_a = E_a - ⟨E_a⟩_Y ∈ M_H (a = θ, z), set ∆v = -c_{i0}^{-1} N_{i0}^{-1} E°_θ, γ_d = -c_{i0}^{-1} N_{i0}^{-1} E°_z, Ψ_* = T_1 γ_d, ∆β = -ε∂_Z Ψ_*, ∆γ = (D_r + R^{-1})Ψ_*, with N_{i0}^{-1} the zero-average inverse of Lemma 8.6. Then c_{i0}N_{i0}∆v = -E°_θ and c_{i0}N_{i0}∆γ = -E°_z + F_ax with F_ax flat.",
"description": "Proposition 9.6(iii). For E°_a = E_a - ⟨E_a⟩_Y ∈ M_H (a = θ, z), set ∆v = -c_{i0}^{-1} N_{i0}^{-1} E°_θ, γ_d = -c_{i0}^{-1} N_{i0}^{-1} E°_z, Ψ_* = T_1 γ_d, ∆β = -ε∂_Z Ψ_*, ∆γ = (D_r + R^{-1})Ψ_*, with N_{i0}^{-1} the zero-average inverse of Lemma 8.6. Then c_{i0}N_{i0}∆v = -E°_θ and c_{i0}N_{i0}∆γ = -E°_z + F_ax with F_ax flat. OBLIGATION: Removes the auxiliary-dependent part of the mean residual, which Step 2 does not see and which a compactly supported radial primitive cannot absorb. MECHANISM: The normalized physical time derivative splits as t_* = -ε∂_T + c_{i0}N_{i0}, where N = v_t·∂_y differentiates along the irrational direction v_t = (√2 - 1, 1) of T^2. On zero-mean functions N is inverted by Fourier division, and the divisor bound |v_t·k| ≥ c/(1 + |k|) of (6.7) costs four torus derivatives and no power of ε (c_{i0}^{-1} ≤ C S_*). ANTECEDENT: None cited in Section 9. Internal: Lemma 8.6, Proposition 8.3(ii), (6.7). (Not named by the manuscript: (6.7) is proved in Section 6 by the algebraic-conjugate argument for √2, a Liouville-type bound for a quadratic irrational.) REFS: p. 110; Proposition 9.6 Step 3; uses (8.3), (8.14), (8.20), (8.22), Lemma 8.6, (6.7).",
"obligation": "Removes the auxiliary-dependent part of the mean residual, which Step 2 does not see and which a compactly supported radial primitive cannot absorb.",
"backward_question": "The auxiliary-dependent mean residual oscillates on the torus; since the physical time derivative contains a fast derivative along an irrational torus direction, can I invert that fast derivative instead of the slow evolution?",
"mechanism": "The normalized physical time derivative splits as t_* = -ε∂_T + c_{i0}N_{i0}, where N = v_t·∂_y differentiates along the irrational direction v_t = (√2 - 1, 1) of T^2. On zero-mean functions N is inverted by Fourier division, and the divisor bound |v_t·k| ≥ c/(1 + |k|) of (6.7) costs four torus derivatives and no power of ε (c_{i0}^{-1} ≤ C S_*). The azimuthal increment is added directly. The axial increment is realized through an azimuthal vector potential built with the compactly supported primitive of (8.14), so the increment is exactly divergence-free; because γ_d has zero auxiliary mean, the axial reconstruction error F_ax is flat (Lemma 8.2) and goes to F. What remains of the operator is slow: slow time (gain 1), radial fluxes containing b = O(ε) or a radial mean (gain 1 - κ_s), axial fluxes through D_z = ε∂_Z (gain 1), and viscosity with its factor ε and two D_r (gain 1 - 2κ_s). The pressure change 2V∆v/R has order H in ∆g_r but enters E_z only through D_z.",
"antecedent": "None cited in Section 9. Internal: Lemma 8.6, Proposition 8.3(ii), (6.7). (Not named by the manuscript: (6.7) is proved in Section 6 by the algebraic-conjugate argument for √2, a Liouville-type bound for a quadratic irrational.)",
"cost": "A polynomial loss c_{i0}^{-1} ≤ C S_*; four extra torus derivatives per application; a flat term F_ax added to F; the inverse preserves slow and radial supports but not auxiliary-torus support.",
"checkable": "FFT on T^2: take a smooth zero-mean trigonometric polynomial F(y), compute φ = N^{-1}F by dividing each Fourier coefficient by 2πi v_t·k with v_t = (√2 - 1, 1), and confirm v_t·∇φ = F to spectral precision; compute the minimum over 0 < |k|_∞ ≤ K of (1 + |k|)|v_t·k| for K up to 10^4 and confirm it stays bounded below (the constant in (6.7)).",
"depends_on": [
"M8.9",
"M8.6",
"M8.4",
"M9.7"
],
"constrains": [],
"reasons": {
"M8.9": "∆v and γ_d are the fast-time inverses (8.20) of Lemma 8.6 applied to the zero-auxiliary-mean parts E°_θ, E°_z.",
"M8.6": "The axial increment is realized through the azimuthal potential of (8.14), so it is exactly divergence-free.",
"M8.4": "Because γ_d has zero auxiliary mean, the axial reconstruction error F_ax is flat by Lemma 8.2.",
"M9.7": "Starts from the state after Step 2, where E_θ, E_z ∈ M_H and their auxiliary averages lie in M_{C*+0.17}."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 110"
},
{
"id": "M9.9",
"kind": "move",
"name": "ns-m9-9-cycle-step-4-five-equation-correction-of-the-defects",
"title": "Cycle step 4, five-equation correction of the defects",
"section": "9",
"pages": "111",
"refs": [
"p. 111",
"Proposition 9.6 Step 4",
"uses (8.24), (8.25), (8.26), (8.27), Lemma 8.7, Lemma 8.8."
],
"statement": "Proposition 9.6(iv). Apply the linear map (8.25) of Lemma 8.7 to the current defects (P, J_θ, J_z) at order H. The slow increments ∆v, γ_d ∈ M_H are supported on the fixed test-function profiles inside the reserved mean patch, the induced radial velocity is in M_{H+1}, the first two rows preserve (9.10), and the last three cancel the linear contributions to the changes of (P, J_θ, J_z). After pressure recomputation, (P, J_θ, J_z) ∈ S_{H+0.9-2κ_s} = S_{C*+0.9-4κ_s}.",
"description": "Proposition 9.6(iv). Apply the linear map (8.25) of Lemma 8.7 to the current defects (P, J_θ, J_z) at order H. The slow increments ∆v, γ_d ∈ M_H are supported on the fixed test-function profiles inside the reserved mean patch, the induced radial velocity is in M_{H+1}, the first two rows preserve (9.10), and the last three cancel the linear contributions to the changes of (P, J_θ, J_z). After pressure recomputation, (P, J_θ, J_z) ∈ S_{H+0.9-2κ_s} = S_{C*+0.9-4κ_s}. OBLIGATION: Pressure and stress corrections can be compactly supported in the annulus only if three scalar integrals vanish: the radial source integral P and the axial flux defects J_θ, J_z. Left alone, they would block the next pressure reconstruction and the next Step 2. The two exact moments (9.10) must also survive. MECHANISM: On the reserved mean patch the base is exactly G_q = 0, V_q = a(η)x^{-1-2λ} (8.24), so the five weighted integrals of three azimuthal bumps and two. ANTECEDENT: None cited in Section 9. Internal: Lemma 8.7 (invertibility via the ordinary Vandermonde determinant, named in Section 8) and Lemma 8.8. REFS: p. 111; Proposition 9.6 Step 4; uses (8.24), (8.25), (8.26), (8.27), Lemma 8.7, Lemma 8.8.",
"obligation": "Pressure and stress corrections can be compactly supported in the annulus only if three scalar integrals vanish: the radial source integral P and the axial flux defects J_θ, J_z. Left alone, they would block the next pressure reconstruction and the next Step 2. The two exact moments (9.10) must also survive.",
"backward_question": "Compact support of the pressure and stress corrections fails only through three scalar integrals at each (Z, T); which finite family of slow velocity bumps can zero them while keeping the two conserved moments at zero?",
"mechanism": "On the reserved mean patch the base is exactly G_q = 0, V_q = a(η)x^{-1-2λ} (8.24), so the five weighted integrals of three azimuthal bumps and two axial bumps reduce to power moments with distinct exponents: 2, -2-2λ, -2λ in the angular block and 1, 1-2λ in the axial block. With geometric copies η_j(x) = a_j^{-1}η_0(x/a_j), a_j = e^{jd}, the moment matrices are Vandermonde matrices in the numbers e^{dp}, hence invertible, and the map is fixed and linear. It cancels exactly the terms linear in the base. The exact recomputed defects (8.27) contain only products of tangential means (order at least H + 0.9, since the existing v, γ are in M_{0.9}) and moments of the slow radial remainder R_g of (8.26) (slow time of the induced radial velocity, radial fluxes with b or radial means, axial derivatives, radial viscosity), all of order at least H + 0.9 - 2κ_s by Lemma 8.8. Slow increments have no fast-time term to cancel, and their effect on the tangential residuals has order at least H + 1 - 2κ_s.",
"antecedent": "None cited in Section 9. Internal: Lemma 8.7 (invertibility via the ordinary Vandermonde determinant, named in Section 8) and Lemma 8.8.",
"cost": "Needs the reserved interval I_mean with the exact power law (8.24) and λ > 0; the inverse may deteriorate as λ ↓ 0 (no uniformity is required); the defect gain 0.9 - 4κ_s relies on the cumulative bound v, γ ∈ M_{0.9}.",
"checkable": "Numeric: choose λ = 0.1, a(η) = 1, d = 0.2, and a smooth normalized bump η_0; compute μ_p = ∫x^p η_0 dx, assemble A_θ (3×3) and A_z (2×2) as displayed on p. 98, and confirm nonzero determinants; for random targets (P, J_θ, J_z) solve for (u_0, u_1, u_2) and (s_0, s_1), form ∆v and γ_d, and verify the five equations (8.25) by quadrature. Then apply the increments to a model mean correction and covariance, recompute (P, J_θ, J_z) directly from (8.3), (8.12), (8.15), and confirm they equal the right sides of (8.27) with R_g from (8.26).",
"depends_on": [
"M8.11",
"M8.12",
"M9.4",
"M8.10"
],
"constrains": [],
"reasons": {
"M8.11": "Applies the five-equation map (8.25) of Lemma 8.7 to the current defects, preserving (9.10) with its first two rows.",
"M8.12": "Lemma 8.8 gives the exact recomputed defects (8.27) and their gain to order H + 0.9 − 2κ_s.",
"M9.4": "The gain uses the cumulative bounds v, γ ∈ M_{0.9} and β ∈ M_{1.9} of (9.9), and the moments (9.10) must survive.",
"M8.10": "The increments sit on fixed profiles in the reserved mean patch, where the base is the explicit power law (8.24)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 111"
},
{
"id": "M9.10",
"kind": "move",
"name": "ns-m9-10-closing-the-cycle-with-a-uniform-1-10-gain",
"title": "Closing the cycle with a uniform 1/10 gain",
"section": "9",
"pages": "111",
"refs": [
"p. 111",
"closing display of the proof of Proposition 9.6",
"(9.8), (9.9)."
],
"statement": "End of the proof of Proposition 9.6. With B ≥ 0.7 and κ_s = 10^{-5}: min{1/2 - 3κ_s, 1/2 - κ_s, B - κ_s, 0.4} ≥ 0.4; min{1/2 - 4κ_s, 0.4 - κ_s, 1/2 - 2κ_s, B - 3κ_s} ≥ 0.4 - κ_s; H - B = 1/2 - 2κ_s > 0.1; min{0.17, 1 - 4κ_s} = 0.17 > 0.1; 0.9 - 4κ_s > 0.1. Hence B_{j+1} = B_j + 1/10 and C*_{j+1} = C*_j + 1/10.",
"description": "End of the proof of Proposition 9.6. With B ≥ 0.7 and κ_s = 10^{-5}: min{1/2 - 3κ_s, 1/2 - κ_s, B - κ_s, 0.4} ≥ 0.4; min{1/2 - 4κ_s, 0.4 - κ_s, 1/2 - 2κ_s, B - 3κ_s} ≥ 0.4 - κ_s; H - B = 1/2 - 2κ_s > 0.1; min{0.17, 1 - 4κ_s} = 0.17 > 0.1; 0.9 - 4κ_s > 0.1. Hence B_{j+1} = B_j + 1/10 and C*_{j+1} = C*_j + 1/10. OBLIGATION: Closes the induction with a gain independent of j, so σ_j → ∞. Without a uniform positive gain the residual would not become flat and the summation could not begin. MECHANISM: Each inequality is the margin of one error family over its new target: Step 1 wave errors (at least 0.4 above B), Step 2 wave errors (at least 0.4 - κ_s), wave changes caused by mean increments of order H (the margin H - B), tangential means (0.17 from Step 2 and 1 - 4κ_s from Step 3), and defects (0.9 - 4κ_s from Step 4). The weakest margin is 0.18 - 2κ_s, recorded as 0.17, set by the product of the transverse signed correction with the old-wave remainder w - w_0^tan ∈ W_{0.68}; the schedule claims only 0.1 for all three components. ANTECEDENT: None cited. REFS: p. 111; closing display of the proof of Proposition 9.6; (9.8), (9.9).",
"obligation": "Closes the induction with a gain independent of j, so σ_j → ∞. Without a uniform positive gain the residual would not become flat and the summation could not begin.",
"backward_question": "Which error family is the bottleneck of the cycle, and is the smallest margin positive and independent of the stage?",
"mechanism": "Each inequality is the margin of one error family over its new target: Step 1 wave errors (at least 0.4 above B), Step 2 wave errors (at least 0.4 - κ_s), wave changes caused by mean increments of order H (the margin H - B), tangential means (0.17 from Step 2 and 1 - 4κ_s from Step 3), and defects (0.9 - 4κ_s from Step 4). The weakest margin is 0.18 - 2κ_s, recorded as 0.17, set by the product of the transverse signed correction with the old-wave remainder w - w_0^tan ∈ W_{0.68}; the schedule claims only 0.1 for all three components. New increments are no larger than the cumulative thresholds allow, so finite sums keep (9.9) and the next cycle faces the same cumulative bounds.",
"antecedent": "None cited.",
"cost": "The gain is additive, 1/10 per cycle, not multiplicative. Apart from the self-interaction rows (2B - κ_s and 2B - 3κ_s), every error row has a fixed margin over B or C* that does not grow with B, because the inverses act about the fixed slow base and leave cross terms with the fixed order-1/2 primary wave in the residual. In powers of q the gain is h/10 per cycle, below 10^{-3} since h < 1/100. κ_s must be small enough for every margin; 10^{-5} is used.",
"checkable": "Exponent arithmetic: verify the five displayed inequalities for κ_s = 10^{-5} and B = 0.7 + j/10, j = 0, ..., 1000 (and symbolically for all B ≥ 0.7); tabulate the margin of every error row in Steps 1 to 4 and confirm the minimum is 0.18 - 2κ_s, coming from the w - w_0^tan row.",
"depends_on": [
"M9.7",
"M9.6",
"M9.9",
"M9.8",
"ME.9"
],
"constrains": [],
"reasons": {
"M9.7": "Step 2's averaged gain of 0.17, set by the w − w_0^tan remainder, is the weakest margin of the cycle.",
"M9.6": "Step 1's wave errors sit at least 0.4 above B, using B ≥ 0.7.",
"M9.9": "Step 4 leaves the defects at order C* + 0.9 − 4κ_s.",
"M9.8": "Step 3 puts the tangential means 1 − 4κ_s above H and its wave changes H − B = 1/2 − 2κ_s above B.",
"ME.9": "Its correction cycle cancels the residual step by step, like ME.9's order-by-order cancellation, gaining 1/10 per cycle; the flat remainder becomes the force instead."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 111"
},
{
"id": "M9.11",
"kind": "move",
"name": "ns-m9-11-a-common-domain-and-finite-derivative-counts",
"title": "A common domain and finite derivative counts",
"section": "9",
"pages": "111-112",
"refs": [
"pp. 111 to 112",
"Lemma 9.7",
"uses (7.18), Corollary 7.3, (7.31), Lemma 8.7."
],
"statement": "Lemma 9.7. There is q_big > 0, independent of the correction stage and of the derivative order, such that every finite partial sum, before the summation cutoffs, is well defined on 0 < q < q_big. For each fixed stage and output amplitude derivative, finitely many input amplitude derivatives suffice. Constants may depend on the stage.",
"description": "Lemma 9.7. There is q_big > 0, independent of the correction stage and of the derivative order, such that every finite partial sum, before the summation cutoffs, is well defined on 0 < q < q_big. For each fixed stage and output amplitude derivative, finitely many input amplitude derivatives suffice. Constants may depend on the stage. OBLIGATION: Lemma 5.4 needs every increment on one domain with 0 < q < q_0. An iteration whose inverses required a smaller domain at every stage would leave no common neighborhood of the singular point on which to sum. MECHANISM: Choose 0 < q_big ≤ q_* once, so that the pulse estimates hold with the fixed background, the positive lower bound for |n_Φ|, the primary covariance, and the fixed supports of the mean-correction profiles. Every later step is a linear problem with coefficients frozen by the primary construction. ANTECEDENT: None cited. Internal: (7.18), Corollary 7.3, (7.31), Lemma 8.7. REFS: pp. 111 to 112; Lemma 9.7; uses (7.18), Corollary 7.3, (7.31), Lemma 8.7.",
"obligation": "Lemma 5.4 needs every increment on one domain with 0 < q < q_0. An iteration whose inverses required a smaller domain at every stage would leave no common neighborhood of the singular point on which to sum.",
"backward_question": "Do the inverses depend on the current iterate? If all of them are frozen at the primary construction, does the domain of definition stay the same at every stage?",
"mechanism": "Choose 0 < q_big ≤ q_* once, so that the pulse estimates hold with the fixed background, the positive lower bound for |n_Φ|, the primary covariance, and the fixed supports of the mean-correction profiles. Every later step is a linear problem with coefficients frozen by the primary construction. For the pulse inverse, the propagator of harmonic m is the fundamental one times the damping factor exp(-(m^2 - 1)∫d), of modulus at most 1, by (7.18), so higher harmonics need no smaller threshold (Corollary 7.3). Signed updates divide by the original 2√y_σ; the five-equation map is the fixed matrix of Lemma 8.7; pressure, temporal inverses, and the modified radial integrals are fixed linear maps. Linear maps with frozen coefficients accept sources of any size, so no smallness of the current iterate is ever used. For derivative counts, the finite construction is a directed acyclic graph of sums, products, derivatives, and inverses, with D_{v,a}(m) = max_{w→v} D_{w,a}(m + d_{v,w}), D_{b,a}(m) = m if b = a and 0 otherwise; finitely many vertices per stage give finite counts. Explicit ε losses (one κ_s per D_r) are tracked separately from derivative counts.",
"antecedent": "None cited. Internal: (7.18), Corollary 7.3, (7.31), Lemma 8.7.",
"cost": "The constants C_{j,m} and the derivative counts may grow without bound in j; linearizing every inverse about the fixed base is also why the gain per cycle is additive (M9.10).",
"checkable": "Numeric check of the factorization (7.18) behind the m-uniform threshold: for a model system z' = (A(v) - m^2 d(v) I)z on [0, L] with a random smooth 2×2 matrix A(v) and scalar d(v) > 0, integrate the fundamental matrix V_m(v, w), compare it with exp(-(m^2 - 1)∫_w^v d) V_1(v, w) for m = 1, ..., 10, and confirm ‖V_m‖ ≤ ‖V_1‖. The derivative-count recursion is bookkeeping and needs no computation.",
"depends_on": [
"M7.6",
"M7.11",
"M8.11"
],
"constrains": [],
"reasons": {
"M7.6": "The pulse inverse lives on one domain at every stage (Corollary 7.3), since by (7.18) higher harmonics are only more damped.",
"M7.11": "Signed updates divide by the fixed primary amplitudes 2√y_σ, a linear map defined on the same domain at every stage.",
"M8.11": "The five-equation map is one fixed matrix, so it accepts sources of any size without shrinking the domain."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 111-112"
},
{
"id": "M9.12",
"kind": "move",
"name": "ns-m9-12-stage-uniform-physical-derivative-losses",
"title": "Stage-uniform physical derivative losses",
"section": "9",
"pages": "112-114",
"refs": [
"pp. 112 to 114",
"(9.15), (9.16), Lemma 9.8, (9.17), (9.18), (9.19)",
"uses (5.29), (6.12), (7.3), (9.5), (9.8), (9.9)."
],
"statement": "(9.15), (9.16), Lemma 9.8. The cycle from stage j - 1 to j is grouped as Z_j = (A_j, B_j, p_j), with A_j = A^w_j + Ψ_j e_θ (wave potentials plus the azimuthal mean potential), B_j = b_j e_θ (direct azimuthal increment), p_j = p^[j] - p^[j-1], and ∆u_j = curl A_j + B_j (9.15); the pressure increment is explicit, Q^{2A} p_j = p_w^[j] - p_w^[j-1] + T_0(g_r^[j] - g_r^[j-1] - ρ(P^[j] - P^[j-1])) (9.16).",
"description": "(9.15), (9.16), Lemma 9.8. The cycle from stage j - 1 to j is grouped as Z_j = (A_j, B_j, p_j), with A_j = A^w_j + Ψ_j e_θ (wave potentials plus the azimuthal mean potential), B_j = b_j e_θ (direct azimuthal increment), p_j = p^[j] - p^[j-1], and ∆u_j = curl A_j + B_j (9.15); the pressure increment is explicit, Q^{2A} p_j = p_w^[j] - p_w^[j-1] + T_0(g_r^[j] - g_r^[j-1] - ρ(P^[j] - P^[j-1])) (9.16). OBLIGATION: Lemma 5.4 needs the stage gains as powers of q with a derivative loss independent of the stage, (5.30) and (5.33); the class estimates are chart-local statements in powers of ε. MECHANISM: On perturbation supports r ≍ √Q and q ≍ Q, and Q is frozen in each chart while differentiating. Each physical derivative of an amplitude coefficient costs a fixed power of Q (9.19): radial 1/2 + hκ_s, axial D = 1/2 - h, time 1 + h, frame 1/2. ANTECEDENT: None cited. Internal: (5.26), (6.6), (6.12), (7.3), and hypotheses (5.28) to (5.33) of Lemma 5.4. REFS: pp. 112 to 114; (9.15), (9.16), Lemma 9.8, (9.17), (9.18), (9.19); uses (5.29), (6.12), (7.3), (9.5), (9.8), (9.9).",
"obligation": "Lemma 5.4 needs the stage gains as powers of q with a derivative loss independent of the stage, (5.30) and (5.33); the class estimates are chart-local statements in powers of ε.",
"backward_question": "When ε-exponents are converted to powers of q, is the loss per physical derivative the same at every stage, or do later stages, with more harmonics and phases, cost more per derivative?",
"mechanism": "On perturbation supports r ≍ √Q and q ≍ Q, and Q is frozen in each chart while differentiating. Each physical derivative of an amplitude coefficient costs a fixed power of Q (9.19): radial 1/2 + hκ_s, axial D = 1/2 - h, time 1 + h, frame 1/2. The phase costs more: |∇_x^a ∂_t^b Φ_γ| ≤ C Q^{-a/2-b(1+h)} S_*^P and k ≤ 2Q^{-h/2}, so each derivative of e^{ikmΦ} costs Q^{-s_x} in space or Q^{-s_t} in time, with s_x = 1/2 + h/2 and s_t = 1 + 3h/2, which dominate (9.19). The finitely many harmonic integers at a fixed stage change only constants. A class exponent α becomes Q^{hα - a s_x - b s_t} S_*^P; the edge weights √ζ δ^{-M} and ζ δ^{-M} are bounded on the closed shell; the physical rescalings Q^{-A}, Q^{-2A}, Q^{1/2-A}, Q^{1/2-A} are all at most Q^{-2A}; one extra derivative recovers a velocity from a potential. Hence ℓ_m = 2A + (m + 1)(1 + 3h/2) suffices. Every stage-j increment has normalized exponent at least j/10, which gives g_j = hj/10. Powers of S_* = ℓ^2 become powers of 1 + |log q|. The residual bound follows from (9.8) with a fixed conversion power, the radial residual -ρP, and the flat part (9.5).",
"antecedent": "None cited. Internal: (5.26), (6.6), (6.12), (7.3), and hypotheses (5.28) to (5.33) of Lemma 5.4.",
"cost": "A gain of only h/10 per stage in powers of q; logarithmic factors; a loss ℓ_m that grows linearly in m.",
"checkable": "Exponent arithmetic only: for 0 < h < 1/100 and κ_s = 10^{-5}, verify s_x = 1/2 + h/2 ≥ max{1/2 + hκ_s, 1/2 - h, 1/2}, s_t = 1 + 3h/2 ≥ 1 + h, ⌈Q^{-h/2}⌉ ≤ 2Q^{-h/2} for 0 < Q ≤ 1, and that ℓ_m = 2A + (m + 1)s_t bounds the rescaling Q^{-2A} times m + 1 derivatives at the largest per-derivative cost. The bounds themselves are pure estimates.",
"depends_on": [
"M9.10",
"M5.13",
"M7.2",
"M6.3"
],
"constrains": [],
"reasons": {
"M9.10": "Stage-j increments have normalized order at least j/10 and the residual order σ_j, which become g_j = hj/10 and hσ_j.",
"M5.13": "Lemma 5.4 needs increments bounded by q^{g_j − ℓ_m} with a loss ℓ_m independent of the stage, as in (5.29), (5.30), (5.33).",
"M7.2": "The phase costs Q^{-s_x} or Q^{-s_t} per derivative, with k ≤ 2Q^{-h/2}, which dominates the other losses (9.19).",
"M6.3": "Chart derivatives convert to physical ones at fixed powers of Q through the chart operators and the chain-rule coefficients of the covering."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 112-114"
},
{
"id": "M9.13",
"kind": "move",
"name": "ns-m9-13-summation-of-the-potentials-with-shrinking-cutoffs",
"title": "Summation of the potentials with shrinking cutoffs",
"section": "9",
"pages": "114-115",
"refs": [
"pp. 114 to 115",
"Proposition 9.9 Steps 1 and 2, (9.20), (9.21)",
"uses Lemma 5.4, (5.27), (5.28), (5.30), (5.33), (5.35), (9.15), (9.17), (9.18)."
],
"statement": "Proposition 9.9, Steps 1 and 2. Lemma 5.4 applies with F = R, q_* = q_big, U_0 the slow base plus the initialization block (cut once inside q < q_big), Z_j from (9.15), g_j = hj/10, and ρ_j = hσ_j → ∞. It gives A = A_0 + sum_{j≥1} χ(a_j q)A_j, B e_θ = B_0 e_θ + sum_{j≥1} χ(a_j q)B_j, p_loc = p_0 + sum_{j≥1} χ(a_j q)p_j, u_loc = curl A + B e_θ (9.21), with div u_loc = 0 and |R(u_loc, p_loc)|_m = O(q^N) as q ↓ 0 for all m, N (9.20).",
"description": "Proposition 9.9, Steps 1 and 2. Lemma 5.4 applies with F = R, q_* = q_big, U_0 the slow base plus the initialization block (cut once inside q < q_big), Z_j from (9.15), g_j = hj/10, and ρ_j = hσ_j → ∞. It gives A = A_0 + sum_{j≥1} χ(a_j q)A_j, B e_θ = B_0 e_θ + sum_{j≥1} χ(a_j q)B_j, p_loc = p_0 + sum_{j≥1} χ(a_j q)p_j, u_loc = curl A + B e_θ (9.21), with div u_loc = 0 and |R(u_loc, p_loc)|_m = O(q^N) as q ↓ 0 for all m, N (9.20). OBLIGATION: The constants of the stage increments may grow arbitrarily in j, so the formal sum need not converge. An actual smooth, exactly divergence-free field with flat residual is required, in the vector-potential form that Section 10 uses for localization. MECHANISM: The jth potential, azimuthal field, and pressure are multiplied by χ(a_j q) with a_{j+1} ≥ 2a_j, which removes them except. ANTECEDENT: None cited. Internal: Lemma 5.4, already used for the background in Proposition 5.5. (Not named by the manuscript: the shrinking-cutoff summation has the form of the classical Borel-lemma construction.) REFS: pp. 114 to 115; Proposition 9.9 Steps 1 and 2, (9.20), (9.21); uses Lemma 5.4, (5.27), (5.28), (5.30), (5.33), (5.35), (9.15), (9.17), (9.18).",
"obligation": "The constants of the stage increments may grow arbitrarily in j, so the formal sum need not converge. An actual smooth, exactly divergence-free field with flat residual is required, in the vector-potential form that Section 10 uses for localization.",
"backward_question": "The corrections improve the residual order at every stage but their constants may grow arbitrarily fast; how do I obtain an actual smooth divergence-free field whose residual is flat to all orders without proving convergence?",
"mechanism": "The jth potential, azimuthal field, and pressure are multiplied by χ(a_j q) with a_{j+1} ≥ 2a_j, which removes them except where q < 1/a_j. Because q = q(z, t) with |∂_z^a ∂_t^b q| ≤ C q^{1-aD-b} (5.28), derivatives of χ(aq) cost fixed powers of q independent of a. Choosing a_j so that the jth term is at most 2^{-j} q^{g_j/2} in every derivative of order at most j makes the sum locally finite for q > 0, with the tail beyond J at most 2^{-J} q^{g_{J+1}/2 - ℓ'_m} (5.35). The cutoff acts on potentials before the curl (curl(χA) includes the ∇χ × A term), and on B_j = b_j e_θ, which stays divergence-free because ∂_θ b_j = 0; curl(Ψ_j e_θ) = (-∂_zΨ_j, 0, (∂_r + r^{-1})Ψ_j). Flatness comes from comparing R(u_loc, p_loc) with R(u^[J], p^[J]) at one fixed stage J with ρ_J large: the difference is controlled by |u_loc - u^[J]|_{m+s}, which (5.35) makes smaller than any power of q; the flat parts F^[j] are never summed. Outside a bounded X-interval every finite state equals the exact heat exterior, whose residual is zero, so the estimate holds on the whole local domain. At the axis the base Stokes streamfunction is r^2 times a smooth function of (r^2, z, t), and all annular representatives vanish near the axis.",
"antecedent": "None cited. Internal: Lemma 5.4, already used for the background in Proposition 5.5. (Not named by the manuscript: the shrinking-cutoff summation has the form of the classical Borel-lemma construction.)",
"cost": "A cutoff-scale sequence a_j; the local field exists only as a locally finite sum on Ω_* = {τ > 0, q < q_*}; no convergence of the full series and no quantitative flatness constants.",
"checkable": "Symbolic, in cylindrical coordinates: verify div[χ(q(z, t)) b(r, z, t) e_θ] = 0, curl(Ψ e_θ) = (-∂_zΨ, 0, (∂_r + 1/r)Ψ), and that S = r^2 a(r^2, z, t) gives (S/r)e_θ = a(r^2, z, t)(-x_2, x_1, 0), smooth in Cartesian variables. The flatness (9.20) is a pure estimate.",
"depends_on": [
"M5.13",
"M9.12",
"M9.11",
"M5.12"
],
"constrains": [],
"reasons": {
"M5.13": "Lemma 5.4 sums the increments with shrinking cutoffs χ(a_jq), producing a smooth divergence-free field with flat residual.",
"M9.12": "The stage bounds (9.17), (9.18) with g_j = hj/10 and a stage-independent loss are exactly Lemma 5.4's hypotheses.",
"M9.11": "All finite stages are defined on the common domain 0 < q < q_big, which serves as Lemma 5.4's q*.",
"M5.12": "The base enters in potential form through its Stokes streamfunctions (5.27), so the cutoffs act on potentials before the curl."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 114-115"
},
{
"id": "M9.14",
"kind": "move",
"name": "ns-m9-14-one-sided-regularity-up-to-0-away-from-the-singular-point",
"title": "One-sided regularity up to τ = 0 away from the singular point",
"section": "9",
"pages": "115-116",
"refs": [
"pp. 115 to 116",
"Proposition 9.9 Step 3",
"Theorem 3.1(ii)",
"uses Theorem 4.6, Proposition 5.5, (7.33)."
],
"statement": "Proposition 9.9, Step 3. For every compact spatial set and 0 < c < c' < q_*, every Cartesian space-time derivative of A, B e_θ, and p_loc is uniformly bounded on c ≤ q ≤ c' up to τ = 0, and the one-sided limits are compatible under spatial and time differentiation: Theorem 3.1(ii).",
"description": "Proposition 9.9, Step 3. For every compact spatial set and 0 < c < c' < q_*, every Cartesian space-time derivative of A, B e_θ, and p_loc is uniformly bounded on c ≤ q ≤ c' up to τ = 0, and the one-sided limits are compatible under spatial and time differentiation: Theorem 3.1(ii). OBLIGATION: Section 10 must show that every derivative of the force f = R(u, p) has a limit as t ↑ 1 in the cutoff transition regions, where q stays positive. This needs the fields themselves, not only their residual, to extend smoothly to τ = 0 away from q = 0. MECHANISM: On c ≤ q ≤ c' only finitely many expansion orders and correction stages have nonzero cutoff factors, because both cutoff sequences tend to infinity, and only finitely many bands and slow labels occur. The base profiles and their Stokes streamfunctions have bounds on the closed range -1 ≤ η ≤ 1 (η = ±1 is t = 1 away from the origin). ANTECEDENT: None cited (the fundamental theorem of calculus is named). Internal: Theorem 4.6, Proposition 5.5, Proposition 7.2 (one-sided endpoint derivatives), (7.33). REFS: pp. 115 to 116; Proposition 9.9 Step 3; Theorem 3.1(ii); uses Theorem 4.6, Proposition 5.5, (7.33).",
"obligation": "Section 10 must show that every derivative of the force f = R(u, p) has a limit as t ↑ 1 in the cutoff transition regions, where q stays positive. This needs the fields themselves, not only their residual, to extend smoothly to τ = 0 away from q = 0.",
"backward_question": "At t = 1 but away from the origin, where q ≥ c > 0, do only finitely many terms of the construction survive, and is each of them smooth up to τ = 0?",
"mechanism": "On c ≤ q ≤ c' only finitely many expansion orders and correction stages have nonzero cutoff factors, because both cutoff sequences tend to infinity, and only finitely many bands and slow labels occur. The base profiles and their Stokes streamfunctions have bounds on the closed range -1 ≤ η ≤ 1 (η = ±1 is t = 1 away from the origin). All discrete geometric choices (labels, representatives, rounded frequencies, enlarged rectangles) are made on the closed range τ ≥ 0 and held fixed as τ → 0. The pulse inverse is a fixed linear ODE along paths with fixed physical slow variables inside τ ≥ 0, so differentiating it bounds every derivative; the quotient bound (7.33) uses the fixed positive primary amplitudes; the radial and temporal mean maps preserve bounds. The coordinate conversion has denominator L = 1 - 2hη^2 ≥ 1 - 2h > 0. Bounding one extra time derivative and applying the fundamental theorem of calculus gives uniform one-sided limits; integration gives compatibility with spatial derivatives and between consecutive time derivatives.",
"antecedent": "None cited (the fundamental theorem of calculus is named). Internal: Theorem 4.6, Proposition 5.5, Proposition 7.2 (one-sided endpoint derivatives), (7.33).",
"cost": "All discrete choices must be made on τ ≥ 0 and held fixed; only one-sided limits at τ = 0 are obtained.",
"checkable": "None: pure estimate.",
"depends_on": [
"M9.13",
"M5.14",
"M7.6",
"M7.11"
],
"constrains": [],
"reasons": {
"M9.13": "On c ≤ q ≤ c′ only finitely many cutoff terms of the summed A, Be_θ, p_loc are nonzero.",
"M5.14": "The background and its potentials extend smoothly to t = 1 away from the origin, with bounds on the closed range −1 ≤ η ≤ 1.",
"M7.6": "The pulse inverse is a fixed linear ODE along paths inside τ ≥ 0, so its outputs have one-sided derivatives up to τ = 0.",
"M7.11": "The signed-amplitude quotient bound (7.33) uses the fixed positive primary amplitudes, uniformly up to τ = 0."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 115-116"
},
{
"id": "M9.15",
"kind": "move",
"name": "ns-m9-15-the-heat-exterior-and-the-inner-growth-survive-the",
"title": "The heat exterior and the inner growth survive the summation",
"section": "9",
"pages": "116",
"refs": [
"p. 116",
"Proposition 9.9 Steps 4 and 5",
"(3.5), (3.6)",
"uses (4.29), (A.34), (A.35), Lemma A.6, (5.1), (5.41), (5.42), (9.20)."
],
"statement": "Proposition 9.9, Steps 4 and 5. For a fixed X_ext beyond all slow supports: A = 0, B = K(r, τ) = r^{-1-2h} H_ext(τ/r^2) with H_ext(s) = 2^A c_∞ H(4s), p = -∫_r^∞ K(ρ, τ)^2 dρ/ρ, and the residual vanishes identically (3.5); sup_{s≥0} |H_ext^{(m)}(s)| ≤ 2^A c_∞ 4^m (h)_m (1 + h)_m for every m ≥ 0. For a fixed X_in ∈ (0, X_a) with e_0 = E_0(X_in, 0) > 0: u_{θ,loc}(√(2X_in τ), 0, 0, 1 - τ) = τ^{-A}(e_0 + O(τ^{2h})) (3.6). With (9.20) and (5.41) this proves Theorem 3.1(iii) and (iv).",
"description": "Proposition 9.9, Steps 4 and 5. For a fixed X_ext beyond all slow supports: A = 0, B = K(r, τ) = r^{-1-2h} H_ext(τ/r^2) with H_ext(s) = 2^A c_∞ H(4s), p = -∫_r^∞ K(ρ, τ)^2 dρ/ρ, and the residual vanishes identically (3.5); sup_{s≥0} |H_ext^{(m)}(s)| ≤ 2^A c_∞ 4^m (h)_m (1 + h)_m for every m ≥ 0. For a fixed X_in ∈ (0, X_a) with e_0 = E_0(X_in, 0) > 0: u_{θ,loc}(√(2X_in τ), 0, 0, 1 - τ) = τ^{-A}(e_0 + O(τ^{2h})) (3.6). With (9.20) and (5.41) this proves Theorem 3.1(iii) and (iv). OBLIGATION: Section 10 needs an exterior that is an exact Navier-Stokes solution with explicit derivative bounds, so that the force vanishes there and has limits at fixed r > 0 as t → 1, and it needs a path along which the velocity provably blows up. MECHANISM: Compact support is built into every Section 7 and 8 construction (supported wave potentials, compactly supported radial primitives, bump subtractions whose defects Step 4 drives to higher order), so every wave and mean correction potential. ANTECEDENT: None cited. Internal: (4.29), Lemma A.6, (A.34), (5.1), (5.42). REFS: p. 116; Proposition 9.9 Steps 4 and 5; (3.5), (3.6); uses (4.29), (A.34), (A.35), Lemma A.6, (5.1), (5.41), (5.42), (9.20).",
"obligation": "Section 10 needs an exterior that is an exact Navier-Stokes solution with explicit derivative bounds, so that the force vanishes there and has limits at fixed r > 0 as t → 1, and it needs a path along which the velocity provably blows up.",
"backward_question": "Does any correction ever reach the heat exterior or the inner growth point? If every correction is annular and every background streamfunction carries zero total axial flux, neither is touched.",
"mechanism": "Compact support is built into every Section 7 and 8 construction (supported wave potentials, compactly supported radial primitives, bump subtractions whose defects Step 4 drives to higher order), so every wave and mean correction potential, azimuthal mean component, and pressure correction vanishes beyond X_b. Beyond X_b the positive-order background Stokes streamfunctions also vanish, because each axial coefficient in the expansion in powers of q^{2h} has zero total axial moment. So beyond X_ext the field is the leading heat exterior (4.29), which solves the radial swirl heat equation exactly (Lemma A.6) and, with its centrifugal pressure normalized at radial infinity, has zero residual. The derivative bound follows from the integral formula (A.34), since (1 + Zv)^{-h-m} ≤ 1 for Z, v ≥ 0. Inside, at X_in < X_a, all annular corrections vanish, so the swirl is that of the realized background expansion (5.1), whose normalized value is E_0 + O(q^{2h}) by (5.42); at z = 0 one has η = 0 and q = τ.",
"antecedent": "None cited. Internal: (4.29), Lemma A.6, (A.34), (5.1), (5.42).",
"cost": "The exterior formula holds only for X ≥ X_ext; the growth statement holds only along X = X_in < X_a, z = 0, with error O(τ^{2h}); the argument relies on the zero total axial moment of every background coefficient.",
"checkable": "(a) Compute H(Z) = Γ(1 + h)^{-1} ∫_0^∞ e^{-v} v^h (1 + Zv)^{-h} dv by quadrature for h = 0.005; set K(r, τ) = r^{-1-2h} 2^A c_∞ H(4τ/r^2) with c_∞ = 1 and A = 1/2 + h; verify -∂_τ K = ∂_r^2 K + r^{-1}∂_r K - r^{-2}K by high-order finite differences on r ∈ [0.5, 2], τ ∈ [0, 1]. (b) Evaluate H^{(m)} from (A.34) for m = 0, ..., 6 and confirm that sup_{s≥0} |H_ext^{(m)}(s)| equals 2^A c_∞ 4^m (h)_m (1 + h)_m, attained at s = 0 by (A.35). (c) The inner asymptotic reduces to (5.42) and needs the constructed base profile E_0; no separate computation belongs to Section 9.",
"depends_on": [
"M9.13",
"MA.10",
"M5.14",
"M4.8"
],
"constrains": [],
"reasons": {
"M9.13": "Examines the summed fields and their flat residual (9.20), every correction potential being compactly supported inside X_b.",
"MA.10": "Beyond X_ext the field is the heat exterior K of Lemma A.6, an exact solution, with derivative bounds from its integral formula (A.34).",
"M5.14": "The swirl at X_in is the realized background's, within O(q^{2h}) of E_0 by (5.42), and (5.41) gives the residual behind Theorem 3.1(iii).",
"M4.8": "The heat exterior (4.29) and the value E_0(X_in, 0) > 0 come from the leading profile of Theorem 4.6."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 116"
},
{
"id": "M10.1",
"kind": "move",
"name": "ns-m10-1-smooth-cartesian-potential-that-vanishes-in-the-heat",
"title": "Smooth Cartesian potential that vanishes in the heat exterior",
"section": "10",
"pages": "116",
"refs": [
"p. 116 (Section 10 opening",
"Step 4 of the proof of Theorem 3.1, A = 0 and B = K beyond X_ext)",
"p. 117 ((10.1), with (4.28), (5.10), (8.4), (9.21) cited there)",
"(9.21) on p. 115",
"Theorem 3.1(i) and (3.5), pp. 15 to 16."
],
"statement": "The local velocity is u_loc = curl A + B e_θ with the representatives of (9.21), B independent of θ. The base potential is A_base = (S/r) e_θ with the Stokes streamfunctions of (10.1), S_n = q^{1−A+2nh} ∫_0^X U_n(X′, η) dX′ and S = S_0 + Σ_{n≥1} χ(c_n q) S_n, the cutoffs being those of Proposition 5.5. By (4.28) and (5.10), ∫_0^∞ U_n(X, η) dX = 0 for every n ≥ 0, so each radial integral in (10.1) vanishes beyond the common support of the axial coefficients.",
"description": "The local velocity is u_loc = curl A + B e_θ with the representatives of (9.21), B independent of θ. The base potential is A_base = (S/r) e_θ with the Stokes streamfunctions of (10.1), S_n = q^{1−A+2nh} ∫_0^X U_n(X′, η) dX′ and S = S_0 + Σ_{n≥1} χ(c_n q) S_n, the cutoffs being those of Proposition 5.5. By (4.28) and (5.10), ∫_0^∞ U_n(X, η) dX = 0 for every n ≥ 0, so each radial integral in (10.1) vanishes beyond the common support of the axial coefficients. OBLIGATION: Localization must act on a potential to keep div u = 0 (M10.2), so the potential must be globally defined, smooth at the axis in Cartesian coordinates, and under control in the exterior X ≥ X_ext. ANTECEDENT: None cited. The Stokes streamfunction is named without citation; the zero-moment identities are the manuscript's own (4.28) and (5.10), and the representation is (9.21) of Proposition 9.9. REFS: p. 116 (Section 10 opening; Step 4 of the proof of Theorem 3.1, A = 0 and B = K beyond X_ext); p. 117 ((10.1), with (4.28), (5.10), (8.4), (9.21) cited there); (9.21) on p. 115; Theorem 3.1(i) and (3.5), pp. 15 to 16.",
"obligation": "Localization must act on a potential to keep div u = 0 (M10.2), so the potential must be globally defined, smooth at the axis in Cartesian coordinates, and under control in the exterior X ≥ X_ext. That exterior contains the plane z = 0 at positive radius as t ↑ 1, where q → 0 and Theorem 3.1(ii) gives no bounds. With A = 0 there, the cutoff term ∇c × A disappears and the localized fields are built only from K and its centrifugal pressure, which Lemma 10.2 handles explicitly (M10.3).",
"backward_question": "Is there a vector potential for the local field that is smooth at the axis and identically zero in the heat exterior, so that a cutoff applied to it creates no error where the concentration scale degenerates away from the singular point?",
"mechanism": "For the axisymmetric meridional flow generated by (S/r) e_θ, one has u_z = r^{−1} ∂_r S and u_r = −r^{−1} ∂_z S. Since X = r²/(2q) with q depending only on (z, t), r dr = q dX, so integrating u_z = q^{−A} U outward from the axis gives S_0 = q^{1−A} ∫_0^X U dX′, and each order q^{2nh} contributes S_n the same way. The zero total axial flux ∫_0^∞ U_n dX = 0 (the moment M(∞, η) = 0 of (4.28) for n = 0 and the moment m_{n,1} of (5.10) for n ≥ 1, both imposed back in Sections 4 and 5) makes S_n constant, hence zero, beyond the support of U_n: no net axial flux crosses large discs, so the potential dies. At the axis S vanishes to second order and is even in r, so (S/r) e_θ is the smooth Cartesian field a (−x_2, x_1, 0). Wave potentials are supported with the waves, and the mean potential uses the compactly supported primitive I_c, which subtracts the full integral J once χ_m = 1. So A has compact support in X, and the swirl B alone carries the exterior flow K e_θ.",
"antecedent": "None cited. The Stokes streamfunction is named without citation; the zero-moment identities are the manuscript's own (4.28) and (5.10), and the representation is (9.21) of Proposition 9.9.",
"cost": "Depends on the vanishing total axial moment of the leading profile and of every expansion coefficient (constraints carried from Sections 4 and 5) and on the specific representative of (9.21); the localization is not representation-free.",
"checkable": "Symbolically, with S_0 = q^{1−A} ∫_0^X U dX′, X = r²/(2q) and q = q(z, t), confirm that curl((S_0/r) e_θ) has axial component q^{−A} U(X, η) and radial component −r^{−1} ∂_z S_0. Numerically, for a compactly supported test profile U with ∫_0^∞ U dX = 0, confirm S_0 ≡ 0 beyond supp U. Confirm (S/r) e_θ = a (−x_2, x_1, 0) when S = r² a.",
"depends_on": [
"M9.13",
"M5.12",
"M4.8",
"M5.8"
],
"constrains": [],
"reasons": {
"M9.13": "Starts from the local representation u_loc = curl A + Be_θ of (9.21).",
"M5.12": "The base potential is (S/r)e_θ built from the Stokes streamfunctions of (5.27), smooth at the axis.",
"M4.8": "The vanishing total axial moment M(∞) = 0 in (4.28) makes S_0 vanish beyond the axial support.",
"M5.8": "Each positive order has F_n = m_{n,1} = 0 beyond X_+, so S_n vanishes there."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 116"
},
{
"id": "M10.2",
"kind": "move",
"name": "ns-m10-2-r-uniform-bound-on-q-and-localization-by-cutting",
"title": "r-uniform bound on q and localization by cutting potentials",
"section": "10",
"pages": "117-118",
"refs": [
"pp. 117 to 118, Proposition 10.1, (10.2), (10.3), (10.4), (10.5)",
"Section 3.5, p. 16",
"(3.2), p. 7."
],
"statement": "Proposition 10.1: there are a compact K ⊂ R³ and smooth u, p on R³ × [0, 1) with supp u(·, t) ∪ supp p(·, t) ⊂ K for every 0 ≤ t < 1, div u = 0, and u(·, t) = p(·, t) = 0 for all sufficiently small t ≥ 0 (10.2), agreeing with u_loc, p_loc on a spatial neighborhood of the origin for all t close to 1. The proof rests on (10.3), q ≤ C_0(τ + |z|^{1/D}), uniform in r. One picks 0 < τ_0 < 1/2 and z_0 > 0 with C_0(τ_0 + z_0^{1/D}) < q∗/2;",
"description": "Proposition 10.1: there are a compact K ⊂ R³ and smooth u, p on R³ × [0, 1) with supp u(·, t) ∪ supp p(·, t) ⊂ K for every 0 ≤ t < 1, div u = 0, and u(·, t) = p(·, t) = 0 for all sufficiently small t ≥ 0 (10.2), agreeing with u_loc, p_loc on a spatial neighborhood of the origin for all t close to 1. The proof rests on (10.3), q ≤ C_0(τ + |z|^{1/D}), uniform in r. One picks 0 < τ_0 < 1/2 and z_0 > 0 with C_0(τ_0 + z_0^{1/D}) < q∗/2; OBLIGATION: Theorem 1.1 needs a smooth, exactly divergence-free field on all of R³ × [0, 1) with zero initial datum and a fixed compact support. The local fields exist only on Ω∗, which contains only times with τ < q∗ (because q ≥ τ) and only heights with |z| < q∗^D (because q ≥ |z|^{1/D}). Multiplying the velocity itself by a cutoff would destroy incompressibility. MECHANISM: From τ = q(1 − η²) and z = q^D η: if 1 − η² ≥ 1/2 then q ≤ 2τ; otherwise |η| > 2^{−1/2} and q ≤ (√2 |z|)^{1/D}. ANTECEDENT: None cited. It reuses the manuscript's own device of cutting potentials before taking curls (Lemma 5.4, (9.21)). REFS: pp. 117 to 118, Proposition 10.1, (10.2), (10.3), (10.4), (10.5); Section 3.5, p. 16; (3.2), p. 7.",
"obligation": "Theorem 1.1 needs a smooth, exactly divergence-free field on all of R³ × [0, 1) with zero initial datum and a fixed compact support. The local fields exist only on Ω∗, which contains only times with τ < q∗ (because q ≥ τ) and only heights with |z| < q∗^D (because q ≥ |z|^{1/D}). Multiplying the velocity itself by a cutoff would destroy incompressibility.",
"backward_question": "Can fields that exist only where q < q∗ be cut to a compactly supported, exactly divergence-free field that starts from rest, using a cutoff that stays a fixed distance from q = q∗ at every radius and leaves the concentrating core unchanged?",
"mechanism": "From τ = q(1 − η²) and z = q^D η: if 1 − η² ≥ 1/2 then q ≤ 2τ; otherwise |η| > 2^{−1/2} and q ≤ (√2 |z|)^{1/D}. This bounds q by τ and |z| alone, with no reference to r, so any cutoff supported in |z| < z_0 and 1 − t < τ_0 lives in q < q∗/2, a fixed margin from the edge of Ω∗, whatever its radial extent. Cutting A and then taking the curl gives an exactly divergence-free field, and cB e_θ is divergence-free because cB does not depend on θ (this is why χ_x must be axisymmetric). The Cartesian representatives of M10.1 keep the product smooth at the axis, and the q-margin makes the zero extension smooth elsewhere. The time cutoff makes everything vanish for t ≤ 1 − τ_0, which gives the zero datum and a force vanishing near t = 0. Both cutoffs equal one near (0, 1), so the concentrating core is untouched. The force is simply the residual, so the equation holds by construction; the terms created by the cutoffs ((∂_t c − ∆c) u_loc, p_loc ∇c, the derivatives and advection products of ∇c × A, and (c² − c)(u_loc · ∇) u_loc, as listed in Section 3.5) sit in the transition regions, away from (0, 1).",
"antecedent": "None cited. It reuses the manuscript's own device of cutting potentials before taking curls (Lemma 5.4, (9.21)).",
"cost": "f acquires cutoff terms whose smoothness through t = 1 must be proved (M10.3, M10.4). The pressure is cut off together with the velocity, so f is not divergence-free in general: the paper says \"the force may have nonzero divergence\", and div f absorbs the mismatch in the Poisson equation. The flow is identically zero until t = 1 − τ_0 and is driven from rest entirely by f. The spatial cutoff must be axisymmetric; r_0 is free, while τ_0 and z_0 are constrained by q∗.",
"checkable": "Solve q − z² q^{2h} = τ (the equation defining q, uniquely solvable by Lemma 4.1) on a grid and verify (10.3) with C_0 = max{2, 2^{1/(2D)}} = 2^{1/(1−2h)}, which the case split above yields. A sanity run during digestion at h = 0.005 on a logarithmic grid with τ and |z| in (10^{−6}, 1), plus z = 0, gave a largest ratio q/(τ + |z|^{1/D}) of about 1.004, against C_0 ≈ 2.014. Symbolically verify div(curl(cA) + cB e_θ) = 0 for axisymmetric c and B, and the product rule u = c u_loc + ∇c × A.",
"depends_on": [
"M10.1",
"M4.1",
"M9.13"
],
"constrains": [],
"reasons": {
"M10.1": "Cuts the Cartesian-smooth potential that vanishes in the heat exterior, taking the curl after multiplication.",
"M4.1": "The bound (10.3), q ≤ C_0(τ + |z|^{1/D}) uniformly in r, follows from τ = q(1 − η²) and z = q^Dη.",
"M9.13": "The local fields exist only on Ω* = {τ > 0, q < q*}, and the localized pair agrees with them near (0, 1)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 117-118"
},
{
"id": "M10.3",
"kind": "move",
"name": "ns-m10-3-endpoint-limits-of-the-force-away-from-the-origin",
"title": "Endpoint limits of the force away from the origin",
"section": "10",
"pages": "118-119",
"refs": [
"pp. 118 to 119 (Lemma 10.2 and its proof), (10.7), (10.8)",
"p. 116 (the H_ext derivative bound, Step 4 of the proof of Theorem 3.1)",
"Theorem 3.1(ii) and (3.5), pp. 15 to 16",
"Lemma A.6 and (A.32) to (A.37), p. 138",
"(4.29), p. 33."
],
"statement": "First part of the proof of Lemma 10.2. (a) On a compact spatial set K_0 where q is bounded below and away from q∗, for G = A, B e_θ, p_loc and t < t′ < 1: sup_{K_0} |∂^α_x ∂^j_t G(·, t′) − ∂^α_x ∂^j_t G(·, t)| ≤ |t′ − t| sup_{K_0 × [t, t′]} |∂^α_x ∂^{j+1}_t G|, the last supremum being bounded by Theorem 3.1(ii) (through the finitely many nonzero cutoff terms of Proposition 9.9, on the closed range −1 ≤ η ≤ 1).",
"description": "First part of the proof of Lemma 10.2. (a) On a compact spatial set K_0 where q is bounded below and away from q∗, for G = A, B e_θ, p_loc and t < t′ < 1: sup_{K_0} |∂^α_x ∂^j_t G(·, t′) − ∂^α_x ∂^j_t G(·, t)| ≤ |t′ − t| sup_{K_0 × [t, t′]} |∂^α_x ∂^{j+1}_t G|, the last supremum being bounded by Theorem 3.1(ii) (through the finitely many nonzero cutoff terms of Proposition 9.9, on the closed range −1 ≤ η ≤ 1). OBLIGATION: The cutoff terms of M10.2 avoid (0, 1) but still reach the terminal slice t = 1, and the flatness (3.4) only controls bounded X near the singular point. The delicate set is the plane z = 0 at positive radius: there q = τ → 0 although nothing is singular, and the constants of Theorem 3.1(ii) depend on a. ANTECEDENT: None cited (fundamental theorem of calculus, dominated convergence). The heat profile, its equation and its derivative formula are the manuscript's Lemma A.6, (A.32) to (A.35), and (4.29). REFS: pp. 118 to 119 (Lemma 10.2 and its proof), (10.7), (10.8); p. 116 (the H_ext derivative bound, Step 4 of the proof of Theorem 3.1); Theorem 3.1(ii) and (3.5), pp. 15 to 16; Lemma A.6 and (A.32) to (A.37), p. 138; (4.29), p. 33.",
"obligation": "The cutoff terms of M10.2 avoid (0, 1) but still reach the terminal slice t = 1, and the flatness (3.4) only controls bounded X near the singular point. The delicate set is the plane z = 0 at positive radius: there q = τ → 0 although nothing is singular, and the constants of Theorem 3.1(ii) depend on a positive lower bound for q. Without the exact heat exterior, terms such as (∂_t c − ∆c) u_loc and p_loc ∇c on that plane would have no proven limit.",
"backward_question": "The flatness estimate controls the residual only near the singular point; what controls the cutoff terms on the part of the terminal slice where q tends to zero without any singularity, namely the plane z = 0 at positive radius?",
"mechanism": "Where q stays positive, a bounded (j+1)-st time derivative makes the j-th one uniformly Cauchy by the fundamental theorem of calculus; points with z ≠ 0 reach t = 1 at η = ±1 with q = |z|^{1/D} > 0, which is why those bounds are needed on the closed range −1 ≤ η ≤ 1. On the plane z = 0 at radius r > 0, η = 0 and q = τ, so X = r²/(2τ) → ∞ and the point enters the exterior, where A = 0 and the flow is the explicit heat swirl K e_θ = r^{−1−2h} H_ext(τ/r²) e_θ. The heat factor (A.32) is a Laplace-type integral whose derivatives are dominated for all Z ≥ 0, so each τ-derivative of K is bounded by a power of r uniformly up to τ = 0, and the formula itself makes sense for τ ≥ 0, which gives the one-sided extension. The pressure is the centrifugal integral from r to infinity, and ρ^{−3−4h−2j} is integrable there, so derivatives pass under the integral. Because the uncut exterior is an exact Navier-Stokes solution (the swirl heat equation plus centrifugal balance), only cutoff terms built from K and p_loc survive there, and these have limits.",
"antecedent": "None cited (fundamental theorem of calculus, dominated convergence). The heat profile, its equation and its derivative formula are the manuscript's Lemma A.6, (A.32) to (A.35), and (4.29).",
"cost": "Constants depend on the lower bound for q and on the distance to the origin; uniformity holds only on compact sets avoiding the origin. The step requires the exact heat exterior (3.5), that is, the Appendix A replacement of the power-law tail by an exact heat flow.",
"checkable": "(1) By quadrature, verify that H of (A.32) satisfies (A.37), Z² H″ + (1 + 2 a_K Z) H′ + a_K(a_K − 1) H = 0 with a_K = 1 + h; by the computation in Lemma A.6 this is equivalent to ∂_t K = (∂_rr + r^{−1} ∂_r − r^{−2}) K, and then u = K e_θ, p = −∫_r^∞ K²/ρ dρ has zero residual because (u · ∇)u = −(K²/r) e_r. (2) Verify H^{(m)}(0) = (−1)^m (h)_m (1 + h)_m (A.35) and the page-116 bound sup_{s≥0} |H_ext^{(m)}(s)| ≤ 2^A c∞ 4^m (h)_m (1 + h)_m. (3) Check that r^{1+2h+2j} |∂_τ^j K(r, τ)| stays bounded for τ ≥ 0. Sanity run during digestion at h = 0.005: the (A.37) residual was about 10^{−16} at Z = 0.1, 1 and 5, and H^{(m)}(0) matched (−1)^m (h)_m (1 + h)_m for m = 1, 2, 3.",
"depends_on": [
"M9.14",
"M9.15",
"MA.10",
"M10.2"
],
"constrains": [],
"reasons": {
"M9.14": "Where q is bounded below, Theorem 3.1(ii) bounds one more time derivative, so each derivative converges uniformly.",
"M9.15": "On the plane z = 0 at positive radius the field is the heat exterior K, with A = 0 and centrifugal pressure.",
"MA.10": "Derivatives of the heat factor (A.32) are dominated uniformly for Z ≥ 0, giving the bounds (10.8).",
"M10.2": "The limits are taken for the force (10.5) of the localized fields, whose cutoff terms reach t = 1 away from the origin."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 118-119"
},