Other material · A dividing-plane barrier in the OpenAI forced Navier-Stokes blow-up construction
The ledger as data, version 1.1, October 1, 2026
The revised ledger in machine-readable form, the version ledger.md shows: GPT-6 Astra's review of the material folded in, and 113 statements replaced after a completeness audit on October 1, 2026, each replacement written by one Claude Opus 5.5 session and checked by a second against the same digest. It is shown here in pages of whole records.
- Written by
- Claude Opus sessions and Claude Fable 5.1 (Anthropic); version 1.1 folds in a review by GPT-6 Astra (OpenAI)
- Size
- 1,021,722 bytes
- SHA-256
73908ae5c651d11684c8a670d84a81bf53cb0cb0e67cb9f29d63dd7dfbfc2aa3
The note's pageEvery file published with itThis file on GitHub
{
"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"
],
"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",
"analogous_to": [
"ME.9"
],
"relations": {
"M9.7": "prerequisite",
"M9.6": "prerequisite",
"M9.9": "prerequisite",
"M9.8": "prerequisite",
"ME.9": "analogy"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "astra-spot-check-2026-10-01",
"hypotheses_checked": "astra-spot-check-2026-10-01",
"computation_checked": false,
"astra_spot_check": "relation-retyped"
}
},
{
"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",
"analogous_to": [],
"relations": {
"M7.6": "prerequisite",
"M7.11": "prerequisite",
"M8.11": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "digest-only",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"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": "Lemma 9.8 (9.15)-(9.18): group the cycle from stage j − 1 to j as Z_j = (A_j, B_j, p_j), A_j = A^w_j + Ψ_je_θ, B_j = b_je_θ, p_j = p^[j] − p^[j−1], ∆u_j = curl A_j + B_j (9.15), with explicit pressure increment (9.16). Then |Z_j|_m + |∆u_j|_m ≤ C_{j,m}q^{g_j−ℓ_m}(1 + |log q|)^{P_{j,m}}, g_j = hj/10, ℓ_m independent of j (9.17); |(u^[j], p^[j])|_m ≤ C_{j,m}q^{−K_m}(1 + |log q|)^{P_{j,m}}; and |R(u^[j], p^[j])|_m ≤ C_{j,m}q^{hσ_j−K_m}(1 + |log q|)^{P_{j,m}} + E_{j,m}, E_{j,m} ≤ C_{j,m,N}q^N for all N, K_m independent of j (9.18).",
"description": "Lemma 9.8 (9.15)-(9.18): group the cycle from stage j − 1 to j as Z_j = (A_j, B_j, p_j), A_j = A^w_j + Ψ_je_θ, B_j = b_je_θ, p_j = p^[j] − p^[j−1], ∆u_j = curl A_j + B_j (9.15), with explicit pressure increment (9.16). Then |Z_j|_m + |∆u_j|_m ≤ C_{j,m}q^{g_j−ℓ_m}(1 + |log q|)^{P_{j,m}}, g_j = hj/10, ℓ_m independent of j (9.17); |(u^[j], p^[j])|_m ≤ C_{j,m}q^{−K_m}(1 + |log q|)^{P_{j,m}}; and |R(u^[j], p^[j])|_m ≤ C_{j,m}q^{hσ_j−K_m}(1 + |log q|)^{P_{j,m}} + E_{j,m}, E_{j,m} ≤ C_{j,m,N}q^N for all N, K_m independent of j (9.18). 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. 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",
"analogous_to": [],
"relations": {
"M9.10": "prerequisite",
"M5.13": "prerequisite",
"M7.2": "prerequisite",
"M6.3": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: FRAGMENT; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"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",
"analogous_to": [],
"relations": {
"M5.13": "prerequisite",
"M9.12": "prerequisite",
"M9.11": "prerequisite",
"M5.12": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "digest-only",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"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",
"analogous_to": [],
"relations": {
"M9.13": "prerequisite",
"M5.14": "prerequisite",
"M7.6": "prerequisite",
"M7.11": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "digest-only",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"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",
"analogous_to": [],
"relations": {
"M9.13": "prerequisite",
"MA.10": "prerequisite",
"M5.14": "prerequisite",
"M4.8": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "digest-only",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"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": "Section 10 (pp. 116 to 117): write u_loc = curl A + B e_θ with the representatives of (9.21), B independent of θ. The base potential A_base = (S/r) e_θ uses the Stokes streamfunctions (10.1), S_n = q^{1−A+2nh} ∫_0^X U_n(X′, η) dX′, S = S_0 + Σ_{n≥1} χ(c_n q) S_n; since ∫_0^∞ U_n dX = 0 by (4.28) and (5.10), each S_n vanishes beyond the support of U_n. Near the axis S = r² a and (S/r) e_θ = a(r², z, t)(−x_2, x_1, 0) is smooth, and the mean potential of (8.4) vanishes beyond its source. Hence A = 0 on X ≥ X_ext, where B = K (Step 4 of the proof of Theorem 3.1).",
"description": "Section 10 (pp. 116 to 117): write u_loc = curl A + B e_θ with the representatives of (9.21), B independent of θ. The base potential A_base = (S/r) e_θ uses the Stokes streamfunctions (10.1), S_n = q^{1−A+2nh} ∫_0^X U_n(X′, η) dX′, S = S_0 + Σ_{n≥1} χ(c_n q) S_n; since ∫_0^∞ U_n dX = 0 by (4.28) and (5.10), each S_n vanishes beyond the support of U_n. Near the axis S = r² a and (S/r) e_θ = a(r², z, t)(−x_2, x_1, 0) is smooth, and the mean potential of (8.4) vanishes beyond its source. Hence A = 0 on X ≥ X_ext, where B = K (Step 4 of the proof of Theorem 3.1). 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",
"analogous_to": [],
"relations": {
"M9.13": "prerequisite",
"M5.12": "prerequisite",
"M4.8": "prerequisite",
"M5.8": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"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 (pp. 117 to 118): there are a compact K ⊂ R³ and smooth u, p on R³ × [0, 1), supported in K at every time, with div u = 0, u = p = 0 for all small t ≥ 0 (10.2), and agreeing with u_loc, p_loc near the origin for t close to 1. Since q ≤ C_0(τ + |z|^{1/D}) uniformly in r (10.3), choosing C_0(τ_0 + z_0^{1/D}) < q∗/2 puts the cutoff c = χ_x χ_t (χ_x axisymmetric with support in {r < r_0, |z| < z_0}, χ_t = 0 for 1 − t ≥ τ_0) in q < q∗/2. Then u = curl(cA) + cB e_θ, p = c p_loc (10.4), K = supp χ_x, and f = ∂_t u + (u · ∇)u − ∆u + ∇p (10.5).",
"description": "Proposition 10.1 (pp. 117 to 118): there are a compact K ⊂ R³ and smooth u, p on R³ × [0, 1), supported in K at every time, with div u = 0, u = p = 0 for all small t ≥ 0 (10.2), and agreeing with u_loc, p_loc near the origin for t close to 1. Since q ≤ C_0(τ + |z|^{1/D}) uniformly in r (10.3), choosing C_0(τ_0 + z_0^{1/D}) < q∗/2 puts the cutoff c = χ_x χ_t (χ_x axisymmetric with support in {r < r_0, |z| < z_0}, χ_t = 0 for 1 − t ≥ τ_0) in q < q∗/2. Then u = curl(cA) + cB e_θ, p = c p_loc (10.4), K = supp χ_x, and f = ∂_t u + (u · ∇)u − ∆u + ∇p (10.5). 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}. 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",
"analogous_to": [],
"relations": {
"M10.1": "prerequisite",
"M4.1": "prerequisite",
"M9.13": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: TRUNCATED; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"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": "Lemma 10.2, away from the origin (pp. 118 to 119): every Cartesian space-time derivative of the force f converges uniformly as t ↑ 1 on compact spatial sets avoiding the origin. Where z ≠ 0, q ≥ |z|^{1/D} > 0, and Theorem 3.1(ii) bounds the next time derivative of A, B e_θ, p_loc, so each derivative is uniformly Cauchy. On z = 0 at r > 0, X ≥ X_ext, A = 0 and the flow is the heat swirl K e_θ, K = c∞ s^{−A} H(2τ/s), s = r²/2 (10.7), with |∂_τ^j K| ≤ C_j r^{−1−2h−2j} (10.8); K and p_loc have one-sided limits at τ = 0 and the uncut exterior residual is zero.",
"description": "Lemma 10.2, away from the origin (pp. 118 to 119): every Cartesian space-time derivative of the force f converges uniformly as t ↑ 1 on compact spatial sets avoiding the origin. Where z ≠ 0, q ≥ |z|^{1/D} > 0, and Theorem 3.1(ii) bounds the next time derivative of A, B e_θ, p_loc, so each derivative is uniformly Cauchy. On z = 0 at r > 0, X ≥ X_ext, A = 0 and the flow is the heat swirl K e_θ, K = c∞ s^{−A} H(2τ/s), s = r²/2 (10.7), with |∂_τ^j K| ≤ C_j r^{−1−2h−2j} (10.8); K and p_loc have one-sided limits at τ = 0 and the uncut exterior residual is zero. 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. 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",
"analogous_to": [],
"relations": {
"M9.14": "prerequisite",
"M9.15": "prerequisite",
"MA.10": "prerequisite",
"M10.2": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: FRAGMENT; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M10.4",
"kind": "move",
"name": "ns-m10-4-flatness-at-the-origin-and-the-taylor-data-f-j",
"title": "Flatness at the origin and the Taylor data F_j",
"section": "10",
"pages": "118-120",
"refs": [
"pp. 118 to 120, (10.6), (10.9), (10.10)",
"(3.4), p. 15",
"(10.3), p. 118."
],
"statement": "Lemma 10.2: for every spatial multi-index α and integer j ≥ 0, ∂^α_x ∂^j_t f converges uniformly on R³ as t ↑ 1, and there are F_j ∈ C_c^∞(R³; R³), all supported in K, with lim_{t↑1} ∂^α_x ∂^j_t f(x, t) = ∂^α_x F_j(x) and ∂^α_x F_j(0) = 0 (10.6). Near the origin, on a fixed neighborhood of (0, 1), (10.9): |∂^α_x ∂^j_t f(x, t)| ≤ C_{α,j,N} (τ + |z|^{1/D})^N for every α, j, N. Compatibility (10.10): ∂^α_x ∂^j_t f(x, t) = ∂^α_x F_j(x) − ∫_t^1 ∂^α_x ∂^{j+1}_t f(x, s) ds.",
"description": "Lemma 10.2: for every spatial multi-index α and integer j ≥ 0, ∂^α_x ∂^j_t f converges uniformly on R³ as t ↑ 1, and there are F_j ∈ C_c^∞(R³; R³), all supported in K, with lim_{t↑1} ∂^α_x ∂^j_t f(x, t) = ∂^α_x F_j(x) and ∂^α_x F_j(0) = 0 (10.6). Near the origin, on a fixed neighborhood of (0, 1), (10.9): |∂^α_x ∂^j_t f(x, t)| ≤ C_{α,j,N} (τ + |z|^{1/D})^N for every α, j, N. Compatibility (10.10): ∂^α_x ∂^j_t f(x, t) = ∂^α_x F_j(x) − ∫_t^1 ∂^α_x ∂^{j+1}_t f(x, s) ds. OBLIGATION: At the singular point the individual terms of the residual diverge, and a smooth force needs every derivative of their sum to have a limit there. This is where the flat-residual output of Sections 5 to 9, (3.4), is spent. (10.10) is the compatibility that Lemma 10.3 needs to produce a C^∞ extension rather than a merely continuous one. ANTECEDENT: None cited (uniform convergence of derivatives, fundamental theorem of calculus). The input (3.4) is Theorem 3.1(iii), proved in Proposition 9.9 from (5.41) and (9.20). REFS: pp. 118 to 120, (10.6), (10.9), (10.10); (3.4), p. 15; (10.3), p. 118.",
"obligation": "At the singular point the individual terms of the residual diverge, and a smooth force needs every derivative of their sum to have a limit there. This is where the flat-residual output of Sections 5 to 9, (3.4), is spent. (10.10) is the compatibility that Lemma 10.3 needs to produce a C^∞ extension rather than a merely continuous one.",
"backward_question": "Does the residual, whose individual terms blow up at the singular point, have limits for all of its derivatives at t = 1, and do those limits fit together as the time-Taylor data of a smooth function?",
"mechanism": "Near (0, 1) both cutoffs equal one, so f = R(u_loc, p_loc). On X ≤ X_ext, (3.4) bounds every derivative by C q^N, and (10.3) turns q^N into (τ + |z|^{1/D})^N; on X > X_ext the residual vanishes identically. For a given tolerance, one first picks a small ball about the origin and then a late time so that (10.9) is below the tolerance there; M10.3 and a finite cover handle the rest of K; everything vanishes off K. Each derivative is therefore uniformly Cauchy on R³, with limit zero at the origin. The limit F_j of ∂_t^j f is smooth because limits of spatial derivatives pass through the fundamental theorem of calculus along coordinate segments, and passing to the limit in the same theorem in time gives (10.10), which says that the limits are the one-sided time-Taylor data of f at t = 1.",
"antecedent": "None cited (uniform convergence of derivatives, fundamental theorem of calculus). The input (3.4) is Theorem 3.1(iii), proved in Proposition 9.9 from (5.41) and (9.20).",
"cost": "None new. The data vanish to infinite order at the origin (∂^α_x F_j(0) = 0). Letting t ↑ 1 in (10.9) also bounds |∂^α_x F_j(x)| by C_{α,j,N} |z|^{N/D} on the neighborhood where (10.9) holds, although the lemma records only the vanishing at the origin.",
"checkable": "None: pure estimate. Its one computable ingredient, (10.3), is checked under M10.2, and the flatness input (3.4) is proved in Sections 5 to 9.",
"depends_on": [
"M9.13",
"M10.3",
"M10.2",
"M9.15"
],
"constrains": [],
"reasons": {
"M9.13": "Near (0, 1) the force is the local residual, flat by (9.20), which is (3.4).",
"M10.3": "Away from the origin the uniform limits come from the first part of Lemma 10.2.",
"M10.2": "Near (0, 1) both cutoffs equal one, and (10.3) turns q^N into (τ + |z|^{1/D})^N.",
"M9.15": "For X > X_ext the residual vanishes identically."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 118-120",
"analogous_to": [],
"relations": {
"M9.13": "prerequisite",
"M10.3": "prerequisite",
"M10.2": "prerequisite",
"M9.15": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "digest-only",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M10.5",
"kind": "move",
"name": "ns-m10-5-continuation-of-the-force-through-t-1-by-shrinking-time",
"title": "Continuation of the force through t = 1 by shrinking time cutoffs",
"section": "10",
"pages": "120",
"refs": [
"p. 120, Lemma 10.3, (10.10), (10.11), (10.12), the display defining b_j, and the decay display",
"[13, (5)] cited on p. 120."
],
"statement": "Lemma 10.3 (p. 120): the force of (10.5) extends to f ∈ C_c^∞(R³ × (0, ∞); R³) supported in K × [0, 2], with the decay bounds of [13, (5)]. For σ = t − 1 ≥ 0, f(x, 1 + σ) = Σ_{j≥0} χ_0(b_j σ)(σ^j/j!) F_j(x) (10.11), χ_0 equal to one near 0 and zero on [1, ∞). Each term obeys ‖∂^α_x ∂^m_σ(·)‖_∞ ≤ C_{j,m} b_j^{m−j} ‖F_j‖_{C^{|α|}} (10.12); with b_0 = 1 and b_j increasing and chosen so this is at most 2^{−j} whenever |α| + m ≤ ⌊j/2⌋, the series is smooth and matches the limits F_j of (10.10) at t = 1.",
"description": "Lemma 10.3 (p. 120): the force of (10.5) extends to f ∈ C_c^∞(R³ × (0, ∞); R³) supported in K × [0, 2], with the decay bounds of [13, (5)]. For σ = t − 1 ≥ 0, f(x, 1 + σ) = Σ_{j≥0} χ_0(b_j σ)(σ^j/j!) F_j(x) (10.11), χ_0 equal to one near 0 and zero on [1, ∞). Each term obeys ‖∂^α_x ∂^m_σ(·)‖_∞ ≤ C_{j,m} b_j^{m−j} ‖F_j‖_{C^{|α|}} (10.12); with b_0 = 1 and b_j increasing and chosen so this is at most 2^{−j} whenever |α| + m ≤ ⌊j/2⌋, the series is smooth and matches the limits F_j of (10.10) at t = 1. OBLIGATION: Theorem 1.1 requires f ∈ C_c^∞(R³ × (0, ∞); R³), smooth for all t > 0 and compactly supported in time, together with the decay conditions of [13, (5)]; Lemma 10.2 supplies only one-sided limits at t = 1. MECHANISM: The series realizes the prescribed Taylor data at σ = 0 from the right. Since each cutoff is constant near zero, the m-th σ-derivative of the j-th summand at σ = 0 is F_j when m = j and zero otherwise, so the series. REFS: p. 120, Lemma 10.3, (10.10), (10.11), (10.12), the display defining b_j, and the decay display; [13, (5)] cited on p. 120.",
"obligation": "Theorem 1.1 requires f ∈ C_c^∞(R³ × (0, ∞); R³), smooth for all t > 0 and compactly supported in time, together with the decay conditions of [13, (5)]; Lemma 10.2 supplies only one-sided limits at t = 1.",
"backward_question": "Given compatible one-sided limits of every derivative at t = 1, can a single smooth force realize all of them from t > 1 and still vanish after a fixed time?",
"mechanism": "The series realizes the prescribed Taylor data at σ = 0 from the right. Since each cutoff is constant near zero, the m-th σ-derivative of the j-th summand at σ = 0 is F_j when m = j and zero otherwise, so the series reproduces the limits F_m and, by (10.10), all mixed space-time derivative limits from t < 1. On the support of χ_0(b_j σ) one has σ ≤ 1/b_j, so each derivative, whether it falls on the cutoff (a factor b_j) or on the monomial (one power of σ lost), costs a factor b_j, which yields b_j^{m−j}. Because m − j < 0 in each of the finitely many constraints with a + m ≤ ⌊j/2⌋, a large enough b_j makes the j-th term at most 2^{−j} in C^{⌊j/2⌋}. Every fixed derivative of the tail therefore converges uniformly, which gives smoothness across σ = 0 and at the support boundaries. Every summand vanishes for σ ≥ 1, so f = 0 for t ≥ 2, and f = 0 near t = 0 by (10.2) and the construction of p. Compact support makes the polynomial decay bounds automatic.",
"antecedent": "None cited. (This is the classical Borel-lemma construction; the identification is mine, the manuscript does not name it.) The decay conditions are those of [13, (5)].",
"cost": "For t ≥ 1 the force is not the residual of any constructed flow; it is one of many smooth continuations and carries no dynamical meaning. No new condition on the construction.",
"checkable": "For a fixed χ_0, compute sup_σ |∂_σ^m (χ_0(bσ) σ^j / j!)| for several b, j, m and confirm the scaling b^{m−j} of (10.12). For model data F_j (for example the Taylor data of a known smooth function times a fixed bump), compute b_j by the rule and check numerically that the truncated series (10.11) has σ-derivatives F_m at σ = 0 and vanishes for σ ≥ 1.",
"depends_on": [
"M10.4",
"M10.2"
],
"constrains": [],
"reasons": {
"M10.4": "The series realizes the Taylor data F_j of Lemma 10.2, and the compatibility (10.10) makes the continuation smooth across t = 1.",
"M10.2": "The force vanishes near t = 0 by (10.2) and is supported in K."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 120",
"analogous_to": [],
"relations": {
"M10.4": "prerequisite",
"M10.2": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M10.6",
"kind": "move",
"name": "ns-m10-6-energy-bound-derived-from-the-equation",
"title": "Energy bound derived from the equation",
"section": "10",
"pages": "121",
"refs": [
"p. 121, Lemma 10.4, (10.13), (10.14)",
"Section 3.5, pp. 16 to 17."
],
"statement": "Lemma 10.4: with F(t) = ∫_0^t ‖f(s)‖_2 ds for 0 ≤ t ≤ 1, F(1) < ∞ and ‖u(t)‖_2² + 2 ∫_0^t ‖∇u(s)‖_2² ds ≤ F(t)² for 0 ≤ t < 1 (10.13); the kinetic energy is uniformly bounded and the total dissipation on [0, 1) is finite. It rests on the energy identity (10.14), (1/2) d/dt ‖u(t)‖_2² + ‖∇u(t)‖_2² = ⟨f(t), u(t)⟩.",
"description": "Lemma 10.4: with F(t) = ∫_0^t ‖f(s)‖_2 ds for 0 ≤ t ≤ 1, F(1) < ∞ and ‖u(t)‖_2² + 2 ∫_0^t ‖∇u(s)‖_2² ds ≤ F(t)² for 0 ≤ t < 1 (10.13); the kinetic energy is uniformly bounded and the total dissipation on [0, 1) is finite. It rests on the energy identity (10.14), (1/2) d/dt ‖u(t)‖_2² + ‖∇u(t)‖_2² = ⟨f(t), u(t)⟩. OBLIGATION: Theorem 1.1 asserts sup_{0≤t<1} ‖u(t)‖_{L²} < ∞ for the whole localized field, pulses, corrections and cutoff regions included; the heuristic core scale E_core ≍ τ^{1/2−3h} of Section 3.5 concerns only the leading core. MECHANISM: For t < 1 the localized fields are smooth with fixed compact support, so pairing the equation with u gives (10.14) exactly, with no boundary terms: transport and pressure integrate to zero by incompressibility. Dividing by (‖u‖_2² + δ²)^{1/2}, discarding dissipation and using Cauchy-Schwarz gives d/dt (‖u‖_2² + δ²)^{1/2} ≤ ‖f‖_2; integrating from the zero datum and letting δ ↓ 0 gives ‖u(t)‖_2 ≤ F(t). ANTECEDENT: None cited at the lemma. It is the classical energy identity; Section 1.1 cites Leray [16] for the energy inequality of weak solutions. REFS: p. 121, Lemma 10.4, (10.13), (10.14); Section 3.5, pp. 16 to 17.",
"obligation": "Theorem 1.1 asserts sup_{0≤t<1} ‖u(t)‖_{L²} < ∞ for the whole localized field, pulses, corrections and cutoff regions included; the heuristic core scale E_core ≍ τ^{1/2−3h} of Section 3.5 concerns only the leading core.",
"backward_question": "Is the kinetic energy of the whole localized field bounded up to the blowup time, and can that be read off from the force alone instead of tracking the energy of every pulse and correction?",
"mechanism": "For t < 1 the localized fields are smooth with fixed compact support, so pairing the equation with u gives (10.14) exactly, with no boundary terms: transport and pressure integrate to zero by incompressibility. Dividing by (‖u‖_2² + δ²)^{1/2}, discarding dissipation and using Cauchy-Schwarz gives d/dt (‖u‖_2² + δ²)^{1/2} ≤ ‖f‖_2; integrating from the zero datum and letting δ ↓ 0 gives ‖u(t)‖_2 ≤ F(t). Feeding this back into (10.14) bounds the left side of (10.13) by 2 ∫_0^t F′(s) F(s) ds = F(t)². Because Lemma 10.3 makes f smooth and compactly supported through t = 1, F(1) < ∞, and monotone convergence gives finite dissipation on [0, 1). The energy bound is thus a consequence of the smooth extension of the force, not a bookkeeping of the construction's pieces.",
"antecedent": "None cited at the lemma. It is the classical energy identity; Section 1.1 cites Leray [16] for the energy inequality of weak solutions.",
"cost": "None beyond Lemma 10.3, which must come first.",
"checkable": "None: pure estimate. (The outline's heuristic scales on p. 16, E_core ≍ τ^{1/2−3h}, D_core ≍ τ^{−1/2−3h} and ∫_0^{τ_0} τ^{−1/2−3h} dτ = τ_0^{1/2−3h}/(1/2 − 3h) for h < 1/6, are arithmetic but are not what the lemma uses.)",
"depends_on": [
"M10.5",
"M10.2"
],
"constrains": [],
"reasons": {
"M10.5": "F(1) < ∞ because the force is smooth and compactly supported through t = 1.",
"M10.2": "The localized u is smooth, compactly supported and divergence-free, starts from rest, and solves the equation with f = R(u, p)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 121",
"analogous_to": [],
"relations": {
"M10.5": "prerequisite",
"M10.2": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "digest-only",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M10.7",
"kind": "move",
"name": "ns-m10-7-pressure-gradient-identification-with-unrestricted",
"title": "Pressure-gradient identification with unrestricted pressure growth",
"section": "10",
"pages": "121-122",
"refs": [
"pp. 121 to 122, Lemma 10.5 statement, (10.15), (10.16)."
],
"statement": "First step of Lemma 10.5 (pp. 121 to 122). Fix T < 1 and a smooth solution v, P of (1.1) at viscosity one on R³ × [0, T] with the force of Lemma 10.3, zero initial velocity and v ∈ L^∞([0, T]; L²). With w = v − u, π = P − p, g_ij = v_i v_j − u_i u_j, one has ‖w(t)‖_2 ≤ C_T, Σ‖g_ij(t)‖_1 ≤ C_T and (10.15): ∂_t w + (v · ∇)w + (w · ∇)u = ∆w − ∇π, div w = 0. Then π∗ = Σ R_i R_j g_ij (10.16), R_i the Riesz transforms, lies uniformly in H^{−s} for each s > 3/2, ∆π∗ = −Σ ∂_i ∂_j g_ij, and ∇π = ∇π∗ in the space-time interior.",
"description": "First step of Lemma 10.5 (pp. 121 to 122). Fix T < 1 and a smooth solution v, P of (1.1) at viscosity one on R³ × [0, T] with the force of Lemma 10.3, zero initial velocity and v ∈ L^∞([0, T]; L²). With w = v − u, π = P − p, g_ij = v_i v_j − u_i u_j, one has ‖w(t)‖_2 ≤ C_T, Σ‖g_ij(t)‖_1 ≤ C_T and (10.15): ∂_t w + (v · ∇)w + (w · ∇)u = ∆w − ∇π, div w = 0. Then π∗ = Σ R_i R_j g_ij (10.16), R_i the Riesz transforms, lies uniformly in H^{−s} for each s > 3/2, ∆π∗ = −Σ ∂_i ∂_j g_ij, and ∇π = ∇π∗ in the space-time interior. OBLIGATION: The competitor's pressure is only assumed smooth, with no growth or integrability condition at spatial infinity (\"no spatial growth condition has been imposed on P\"), so the pressure difference could a priori carry an arbitrary harmonic part. The pressure flux in the localized energy estimate (M10.8) cannot be bounded until ∇π is known. MECHANISM: The common force cancels, so (10.15) contains no force, and its divergence gives ∆π = −Σ ∂_i ∂_j g_ij = ∆π∗, even though f itself is not. REFS: pp. 121 to 122, Lemma 10.5 statement, (10.15), (10.16).",
"obligation": "The competitor's pressure is only assumed smooth, with no growth or integrability condition at spatial infinity (\"no spatial growth condition has been imposed on P\"), so the pressure difference could a priori carry an arbitrary harmonic part. The pressure flux in the localized energy estimate (M10.8) cannot be bounded until ∇π is known.",
"backward_question": "With no growth condition on the competitor's pressure, is its pressure gradient still the one the velocity determines through Riesz transforms, or could a harmonic pressure gradient drive a different flow with the same force and datum?",
"mechanism": "The common force cancels, so (10.15) contains no force, and its divergence gives ∆π = −Σ ∂_i ∂_j g_ij = ∆π∗, even though f itself is not divergence-free. For a ∈ C_c^∞(0, T), integrating the conservative form ∂_t w + div g = ∆w − ∇π against a(t) gives ∫ a ∇π dt = ∆ ∫ a w dt + ∫ a′ w dt − div ∫ a g dt, whose three terms lie in H^{−2}, L² and H^{−3} because w ∈ L^∞_t L²_x and g ∈ L^∞_t L¹_x (Fourier estimate with s = 2). With π∗ ∈ L^∞_t H^{−2}_x, the difference H_a = ∫ a (∇π − ∇π∗) dt lies in H^{−3} and satisfies ∆H_a = 0. A harmonic tempered distribution has Fourier transform supported at the origin, while the Fourier transform of an element of H^{−3} is a weighted L² function, which cannot concentrate on a point; so H_a = 0, and testing in space as well gives ∇π = ∇π∗. This is where the energy hypothesis on v enters: it places the difference in a Sobolev space, which excludes, for instance, a spatially constant pressure gradient, whose Fourier transform is a point mass.",
"antecedent": "None cited for the argument. Riesz transforms are standard; Stein [20] is cited in the next step for their L^p boundedness.",
"cost": "Uses v ∈ L^∞([0, T]; L²(R³)) essentially, to put w in L² and g in L¹. The identification holds in the open interval (0, T), for almost every t.",
"checkable": "None: pure estimate.",
"depends_on": [
"M10.2",
"M10.5"
],
"constrains": [],
"reasons": {
"M10.2": "u, p are the localized fields, smooth with compact support on [0, T], so w = v − u ∈ L² and g_ij ∈ L¹.",
"M10.5": "The competitor carries the same force, which cancels in the difference equation (10.15)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 121-122",
"analogous_to": [],
"relations": {
"M10.2": "prerequisite",
"M10.5": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: TRUNCATED; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M10.8",
"kind": "move",
"name": "ns-m10-8-pressure-flux-through-expanding-balls-by-a-riesz",
"title": "Pressure flux through expanding balls by a Riesz commutator",
"section": "10",
"pages": "122-123",
"refs": [
"pp. 122 to 123, (10.17), (10.18), (10.19)",
"[20] cited on p. 122."
],
"statement": "Pressure flux in the proof of Lemma 10.5 (pp. 122 to 123), w = v − u, π = P − p: with φ_R = φ(·/R) (φ smooth, 0 ≤ φ ≤ 1, compactly supported, one on the unit ball, R ≥ 1), χ_R = φ_R^8, A_R = (∫ χ_R |∇w|²)^{1/2}, B_R = ‖φ_R^4 w‖_6: B_R ≤ C(A_R + R^{−1}‖w‖_2) (10.17). Splitting φ_R^4 π∗ as in (10.18) into Σ R_i R_j(φ_R^4 g_ij), at most C_T(B_R + 1) in L^{3/2}, and a Riesz commutator, at most C_T R^{−3/4} in L^{4/3}, and using ∇π = ∇π∗ gives, for a.e. t, (10.19): |∫ π w · ∇χ_R| ≤ C_T R^{−1}[(B_R + 1)B_R^{1/2} + R^{−3/4}B_R^{3/4}].",
"description": "Pressure flux in the proof of Lemma 10.5 (pp. 122 to 123), w = v − u, π = P − p: with φ_R = φ(·/R) (φ smooth, 0 ≤ φ ≤ 1, compactly supported, one on the unit ball, R ≥ 1), χ_R = φ_R^8, A_R = (∫ χ_R |∇w|²)^{1/2}, B_R = ‖φ_R^4 w‖_6: B_R ≤ C(A_R + R^{−1}‖w‖_2) (10.17). Splitting φ_R^4 π∗ as in (10.18) into Σ R_i R_j(φ_R^4 g_ij), at most C_T(B_R + 1) in L^{3/2}, and a Riesz commutator, at most C_T R^{−3/4} in L^{4/3}, and using ∇π = ∇π∗ gives, for a.e. t, (10.19): |∫ π w · ∇χ_R| ≤ C_T R^{−1}[(B_R + 1)B_R^{1/2} + R^{−3/4}B_R^{3/4}]. OBLIGATION: The pressure flux is the only nonlocal term in the localized difference energy (M10.9). It must be bounded by powers of the local dissipation A_R strictly below 2, with a factor that decays in R, or the limit R → ∞ fails. MECHANISM: After M10.7, π may be replaced by π∗ in the flux. Commuting the cutoff φ_R^4 through the double Riesz transform splits φ_R^4 π∗ into a localized part, bounded in L^{3/2} by the L^p boundedness of Riesz transforms together with ‖φ_R^4 w_i w_j‖_{3/2} ≤ B_R ‖w‖_2 and ‖φ_R^4 w_i u_j‖_{3/2} ≤ ‖w‖_2 ‖u‖_6, and a commutator. REFS: pp. 122 to 123, (10.17), (10.18), (10.19); [20] cited on p. 122.",
"obligation": "The pressure flux is the only nonlocal term in the localized difference energy (M10.9). It must be bounded by powers of the local dissipation A_R strictly below 2, with a factor that decays in R, or the limit R → ∞ fails.",
"backward_question": "In a localized energy estimate for the difference of two solutions, how can the pressure flux through the boundary of a large ball be controlled when the pressure is a nonlocal function of the velocity and nothing is known about it at infinity?",
"mechanism": "After M10.7, π may be replaced by π∗ in the flux. Commuting the cutoff φ_R^4 through the double Riesz transform splits φ_R^4 π∗ into a localized part, bounded in L^{3/2} by the L^p boundedness of Riesz transforms together with ‖φ_R^4 w_i w_j‖_{3/2} ≤ B_R ‖w‖_2 and ‖φ_R^4 w_i u_j‖_{3/2} ≤ ‖w‖_2 ‖u‖_6, and a commutator whose kernel (φ_R^4(x) − φ_R^4(y)) k(x − y) gains the factor min{|x − y|/R, 1} over the singular kernel |x − y|^{−3} (the multiple of the identity in R_i R_j cancels). Radial integration gives ‖K_R‖_{4/3} ≲ R^{−3/4}, and Young's inequality with g ∈ L¹ gives an L^{4/3} bound that decays in R. The eighth power in χ_R leaves cutoff factors to spare: |∇χ_R| ≤ C R^{−1} φ_R^7, so each piece pairs with R^{−1} φ_R^3 |w|, which interpolates between ‖w‖_2 and B_R: ‖φ_R^3 w‖_3 ≤ ‖φ_R^2 w‖_3 ≤ B_R^{1/2} ‖w‖_2^{1/2} and ‖φ_R^3 w‖_4 ≤ B_R^{3/4} ‖w‖_2^{1/4}. The Sobolev inequality (10.17) controls B_R by local dissipation plus R^{−1}. The identities are proved first for compactly supported smooth truncations of g and then passed to the limit (L¹ convergence, the uniform commutator bound, and H^{−s} convergence of the Riesz transforms); in particular π∗ is locally integrable in space and time.",
"antecedent": "Stein [20] for the L^p boundedness of Riesz transforms, 1 < p < ∞. The commutator-kernel bound, the Sobolev inequality and Young's convolution inequality are used without citation.",
"cost": "Constants C_T depend on T, on sup_{[0,T]} ‖v‖_2, and on ‖u‖_6 over [0, T]. The cutoff power 8 and the weight φ_R^4 in B_R are tuned so that every pairing closes.",
"checkable": "The radial integral behind ‖K_R‖_{4/3}^{4/3} ≤ C R^{−1}: with C = 1, ∫_{R³} (|x|^{−3} min{|x|/R, 1})^{4/3} dx = 4π(3 R^{−1} + R^{−1}) = 16π/R exactly; a sanity run during digestion by quadrature gave 50.2655 at R = 1 and 5.02655 at R = 10, matching 16π/R. The interpolation exponents follow from Hölder: ∫ φ_R^6 |w|³ ≤ B_R^{3/2} ‖w‖_2^{3/2} and ∫ φ_R^{12} |w|⁴ ≤ B_R³ ‖w‖_2. Otherwise a pure estimate.",
"depends_on": [
"M10.7",
"M10.2"
],
"constrains": [],
"reasons": {
"M10.7": "After ∇π = ∇π*, the flux uses π* = ΣR_iR_j g_ij, with ‖w‖_2 ≤ C_T and g_ij ∈ L¹.",
"M10.2": "The localized u is smooth with compact support, so ‖u‖_6 is bounded on [0, T]."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 122-123",
"analogous_to": [],
"relations": {
"M10.7": "prerequisite",
"M10.2": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M10.9",
"kind": "move",
"name": "ns-m10-9-localized-difference-energy-gronwall-and-r",
"title": "Localized difference energy, Gronwall, and R → ∞",
"section": "10",
"pages": "123",
"refs": [
"p. 123 (difference energy and Gronwall), (10.15), (10.17), (10.19)",
"p. 121 (remark before Lemma 10.5)."
],
"statement": "Lemma 10.5, uniqueness: on [0, T] for every T < 1, any smooth competitor v in L^infty([0, T]; L^2) with the same force and zero datum equals the compactly supported blow-up solution u. Pairing (10.15) with chi_R w, w = v - u: the cubic transport and pressure fluxes live on supp grad chi_R, where v = w, and are at most C_T R^{-1} times powers of the local dissipation A_R below 2 ((10.17) in (10.19)); Young absorbs them into A_R^2/2 with O(1/R) remainders; the stretching term is at most ||grad u||_infty E_R; Gronwall from E_R(0) = 0 gives E_R(t) <= C'_T/R, and R -> infinity gives w = 0.",
"description": "Lemma 10.5, uniqueness: on [0, T] for every T < 1, any smooth competitor v in L^infty([0, T]; L^2) with the same force and zero datum equals the compactly supported blow-up solution u. Pairing (10.15) with chi_R w, w = v - u: the cubic transport and pressure fluxes live on supp grad chi_R, where v = w, and are at most C_T R^{-1} times powers of the local dissipation A_R below 2 ((10.17) in (10.19)); Young absorbs them into A_R^2/2 with O(1/R) remainders; the stretching term is at most ||grad u||_infty E_R; Gronwall from E_R(0) = 0 gives E_R(t) <= C'_T/R, and R -> infinity gives w = 0. OBLIGATION: Closes Lemma 10.5. A global energy identity for w would need decay of the competitor's derivatives and pressure at infinity, which the hypotheses do not provide (\"These hypotheses leave the growth of spatial derivatives at infinity unrestricted\"). MECHANISM: Since u has compact support, outside supp u the difference w is the competitor v itself, so the cubic transport flux and the pressure flux live on the annulus where ∇χ_R is supported and involve only w. ANTECEDENT: None cited. REFS: p. 123 (difference energy and Gronwall), (10.15), (10.17), (10.19); p. 121 (remark before Lemma 10.5).",
"obligation": "Closes Lemma 10.5. A global energy identity for w would need decay of the competitor's derivatives and pressure at infinity, which the hypotheses do not provide (\"These hypotheses leave the growth of spatial derivatives at infinity unrestricted\").",
"backward_question": "Why does uniqueness hold for smooth bounded-energy solutions with this force and zero datum on each [0, T], T < 1, when nothing is assumed about the competitor's derivatives or pressure at spatial infinity?",
"mechanism": "Since u has compact support, outside supp u the difference w is the competitor v itself, so the cubic transport flux and the pressure flux live on the annulus where ∇χ_R is supported and involve only w. Both are R^{−1} times powers of B_R, hence by (10.17) powers of A_R no larger than 3/2, and Young's inequality absorbs them into half the local dissipation with remainders of order R^{−1} or smaller for R ≥ 1. The only term that is not small is the stretching term, bounded by ‖∇u‖_∞ E_R, and ‖∇u‖_∞ is bounded on [0, T] because T < 1 and u is smooth with compact support there. Gronwall from E_R(0) = 0 gives E_R(t) ≤ C′_T/R, and since χ_R = 1 on any fixed ball once R is large, w vanishes identically.",
"antecedent": "None cited. (Structurally it is the classical energy-plus-Gronwall uniqueness argument in which the known smooth solution supplies the Lipschitz norm; the identification is mine.)",
"cost": "Uniqueness is proved only on [0, T] for each T < 1, because the argument uses ‖∇u‖_∞ on [0, T], which is unbounded as T ↑ 1 (u has fixed compact support and unbounded L^∞ norm). The competitor must be smooth on R³ × [0, T] and lie in L^∞([0, T]; L²(R³)). This step fixes the class in which Theorem 1.1's non-existence is proved.",
"checkable": "None: pure estimate. (The exponent bookkeeping is arithmetic: the fluxes carry A_R to the powers 3/2, 1/2 and 3/4, each below 2, and the corresponding Young remainders are of order R^{−4}, R^{−4/3} and R^{−14/5}, all at most of order R^{−1} for R ≥ 1.)",
"depends_on": [
"M10.8",
"M10.7",
"M10.2"
],
"constrains": [],
"reasons": {
"M10.8": "The pressure-flux bound (10.19) and the Sobolev inequality (10.17) keep every power of A_R below 2.",
"M10.7": "Pairs the difference equation (10.15) with χ_R w.",
"M10.2": "u has compact support, so v = w near supp ∇χ_R for large R, and ‖∇u‖_∞ is bounded on [0, T]."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 123",
"analogous_to": [],
"relations": {
"M10.8": "prerequisite",
"M10.7": "prerequisite",
"M10.2": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completed 2026-10-01 from the digest after the pull-back graders tagged the v1.0 statement stimulus-defect (truncated or a fragment)",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M10.10",
"kind": "move",
"name": "ns-m10-10-growth-path-classical-lifespan-and-exclusion-of-a-global",
"title": "Growth path, classical lifespan, and exclusion of a global bounded-energy solution",
"section": "10",
"pages": "124",
"refs": [
"p. 116 (Step 5 of the proof of Theorem 3.1, e_0 = E_0(X_in, 0))",
"p. 124, (10.20), (10.21)",
"Theorem 3.1(iv) and (3.6), p. 16",
"Theorem 1.1 and alternative (C), p. 1."
],
"statement": "Proof of Theorem 1.1 (p. 124): the localized field solves the equation exactly on [0, 1) by (10.5), u ∈ C([0, T]; H³) for T < 1, and along (10.20), x_τ = (√(2 X_in τ), 0, 0), t = 1 − τ, where z = 0, q = τ and the cutoffs equal one for small τ > 0, (3.6) gives (10.21): u_θ(x_τ, 1 − τ) = τ^{−A}(e_0 + O(τ^{2h})) → +∞ with x_τ → 0. By H³ ↪ L^∞ and H³ uniqueness the maximal classical existence interval is [0, 1); no global smooth solution with the same force and zero datum has uniformly bounded kinetic energy, since by Lemma 10.5 it would equal u on each [0, T]. The force is nonzero by (10.13).",
"description": "Proof of Theorem 1.1 (p. 124): the localized field solves the equation exactly on [0, 1) by (10.5), u ∈ C([0, T]; H³) for T < 1, and along (10.20), x_τ = (√(2 X_in τ), 0, 0), t = 1 − τ, where z = 0, q = τ and the cutoffs equal one for small τ > 0, (3.6) gives (10.21): u_θ(x_τ, 1 − τ) = τ^{−A}(e_0 + O(τ^{2h})) → +∞ with x_τ → 0. By H³ ↪ L^∞ and H³ uniqueness the maximal classical existence interval is [0, 1); no global smooth solution with the same force and zero datum has uniformly bounded kinetic energy, since by Lemma 10.5 it would equal u on each [0, T]. The force is nonzero by (10.13). OBLIGATION: Converts the construction into the non-existence statement of Theorem 1.1 and supplies the blowup lim sup_{t↑1} ‖u(t)‖_{L^∞} = ∞. MECHANISM: On the plane z = 0 the similarity relations give η = 0 and q = τ, so x_τ sits at the fixed similarity point (X, η) = (X_in, 0) inside the inner region, where all annular corrections vanish and the swirl equals q^{−A} times the leading profile value e_0 = E_0(X_in, 0) > 0, up to a relative O(q^{2h}) from the higher-order background terms (Step 5 on p. 116).",
"obligation": "Converts the construction into the non-existence statement of Theorem 1.1 and supplies the blowup lim sup_{t↑1} ‖u(t)‖_{L^∞} = ∞.",
"backward_question": "Along which space-time path does the localized velocity provably diverge, does that path stay inside the region where the cutoffs equal one and the inner asymptotics (3.6) hold, and what then forbids a smooth bounded-energy global solution with the same data?",
"mechanism": "On the plane z = 0 the similarity relations give η = 0 and q = τ, so x_τ sits at the fixed similarity point (X, η) = (X_in, 0) inside the inner region, where all annular corrections vanish and the swirl equals q^{−A} times the leading profile value e_0 = E_0(X_in, 0) > 0, up to a relative O(q^{2h}) from the higher-order background terms (Step 5 on p. 116). Since x_τ → 0 and t → 1, the path eventually lies where c = 1, so the localized field inherits (3.6). A global smooth solution is bounded on a compact neighborhood of (0, 1); by Lemma 10.5 on every [0, T] it agrees with u before t = 1, and u is unbounded along x_τ. Contradiction.",
"antecedent": "Fefferman [13], alternative (C), as stated in Section 1; nothing else is cited in the argument.",
"cost": "The conclusion covers only smooth competitors with uniformly bounded kinetic energy (the hypothesis Lemma 10.5 needs on each [0, T]); the maximal-lifespan statement is in the classical H³ class. The rate τ^{−A}, A = 1/2 + h, is proved at the points x_τ; Theorem 1.1 states the blowup as a lim sup, while (10.21) gives the lower bound ‖u(1 − τ)‖_{L^∞} ≥ τ^{−A}(e_0 + O(τ^{2h})) at every small τ.",
"checkable": "From τ = q(1 − η²) and z = q^D η, verify that z = 0 forces η = 0 and q = τ, that X = r²/(2q) = X_in along x_τ, and that |x_τ| = √(2 X_in τ) → 0. Given the realized profiles of (5.1), evaluate τ^A u_θ(x_τ, 1 − τ) − e_0 and check that it is O(τ^{2h}).",
"depends_on": [
"M9.15",
"M10.2",
"M10.9",
"M10.5"
],
"constrains": [],
"reasons": {
"M9.15": "The inner growth (3.6) gives u_θ = τ^{-A}(e_0 + O(τ^{2h})) along X = X_in, z = 0.",
"M10.2": "The cutoffs equal one along the growth path for small τ, so the localized field inherits (3.6).",
"M10.9": "Lemma 10.5 makes any smooth bounded-energy solution with the same data equal u on every [0, T], T < 1.",
"M10.5": "The global competitor is posed with the extended force f ∈ C_c^∞(R³ × (0, ∞)) of Lemma 10.3."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 116",
"analogous_to": [],
"relations": {
"M9.15": "prerequisite",
"M10.2": "prerequisite",
"M10.9": "prerequisite",
"M10.5": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "astra-spot-check-2026-10-01",
"computation_checked": false,
"astra_spot_check": "locator-corrected"
}
},
{
"id": "M10.11",
"kind": "move",
"name": "ns-m10-11-viscosity-rescaling",
"title": "Viscosity rescaling",
"section": "10",
"pages": "124",
"refs": [
"p. 124, (10.22), (10.23)",
"p. 7."
],
"statement": "Viscosity rescaling (p. 124): u_ν(x, t) = √ν u(x/√ν, t), p_ν = ν p(x/√ν, t), f_ν = √ν f(x/√ν, t) (10.22) solve the forced Navier-Stokes equations at viscosity ν with div u_ν = 0, zero datum, support K_ν = √ν K and unchanged time; f_ν is smooth, supported in K_ν × [0, 2], with the decay bounds. By (10.23), ‖u_ν(t)‖_2² = ν^{5/2}‖u(t)‖_2² and the dissipation scales likewise; growth occurs along √ν x_τ at t = 1; and a smooth bounded-energy competitor at viscosity ν maps back, v(y, t) = ν^{−1/2} v_ν(√ν y, t), to one at viscosity one, already excluded. So Theorem 1.1 holds for every ν > 0.",
"description": "Viscosity rescaling (p. 124): u_ν(x, t) = √ν u(x/√ν, t), p_ν = ν p(x/√ν, t), f_ν = √ν f(x/√ν, t) (10.22) solve the forced Navier-Stokes equations at viscosity ν with div u_ν = 0, zero datum, support K_ν = √ν K and unchanged time; f_ν is smooth, supported in K_ν × [0, 2], with the decay bounds. By (10.23), ‖u_ν(t)‖_2² = ν^{5/2}‖u(t)‖_2² and the dissipation scales likewise; growth occurs along √ν x_τ at t = 1; and a smooth bounded-energy competitor at viscosity ν maps back, v(y, t) = ν^{−1/2} v_ν(√ν y, t), to one at viscosity one, already excluded. So Theorem 1.1 holds for every ν > 0. OBLIGATION: Everything above is at viscosity one, while Theorem 1.1 is claimed for every ν > 0. MECHANISM: The Navier-Stokes system is invariant under spatial dilation by √ν with velocity multiplied by √ν, pressure by ν and force by √ν at fixed time, which carries viscosity one to viscosity ν. Since time is not rescaled, the singular time stays t = 1; incompressibility, the zero datum, compact support, smoothness and bounded energy all transfer, and the inverse map sends any smooth bounded-energy competitor at viscosity ν to one at viscosity one. REFS: p. 124, (10.22), (10.23); p. 7.",
"obligation": "Everything above is at viscosity one, while Theorem 1.1 is claimed for every ν > 0.",
"backward_question": "Does the viscosity-one construction give every positive viscosity without moving the singular time?",
"mechanism": "The Navier-Stokes system is invariant under spatial dilation by √ν with velocity multiplied by √ν, pressure by ν and force by √ν at fixed time, which carries viscosity one to viscosity ν. Since time is not rescaled, the singular time stays t = 1; incompressibility, the zero datum, compact support, smoothness and bounded energy all transfer, and the inverse map sends any smooth bounded-energy competitor at viscosity ν to one at viscosity one.",
"antecedent": "None cited (the scaling is announced in Section 3 on p. 7).",
"cost": "None; the force and the support depend on ν (f_ν, K_ν = √ν K).",
"checkable": "Symbolic chain-rule verification of the identity after (10.22), of the derivative factor ν^{(1−|α|)/2}, and of the factor ν^{5/2} in (10.23) (the Jacobian ν^{3/2} of x = √ν y times the squared amplitude ν).",
"depends_on": [
"M10.5",
"M10.2",
"M10.10"
],
"constrains": [],
"reasons": {
"M10.5": "Rescales the smooth force supported in K × [0, 2], keeping its decay bounds.",
"M10.2": "Rescales the localized u, p, keeping the zero datum, divergence-freeness and compact support K_ν = √νK.",
"M10.10": "Transfers the viscosity-one blowup and exclusion, since a competitor at viscosity ν maps back to viscosity one."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 124",
"analogous_to": [],
"relations": {
"M10.5": "prerequisite",
"M10.2": "prerequisite",
"M10.10": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M10.12",
"kind": "move",
"name": "ns-m10-12-periodization-onto-t-corollary-10-6",
"title": "Periodization onto T³ (Corollary 10.6)",
"section": "10",
"pages": "125-126",
"refs": [
"pp. 125 to 126, Corollary 10.6 and its proof",
"[13] cited on p. 125."
],
"statement": "Corollary 10.6 (pp. 125 to 126): for every ν > 0 there is a smooth force on T³ × [0, ∞), compactly supported in time, for which the solution (U, P_per) of the periodic Navier-Stokes equations with viscosity ν and zero initial velocity is smooth on [0, 1), has velocity and pressure supported at every earlier time in a fixed compact subset of the interior of Q_0 = (−1/2, 1/2)³, and satisfies lim sup_{t↑1} ‖U(t)‖_{L^∞(T³)} = ∞; there is no global smooth periodic solution for the same datum and force. Proof: rescale by λ with t_0 = 1 − λ^{−2}, then sum the disjoint integer translates.",
"description": "Corollary 10.6 (pp. 125 to 126): for every ν > 0 there is a smooth force on T³ × [0, ∞), compactly supported in time, for which the solution (U, P_per) of the periodic Navier-Stokes equations with viscosity ν and zero initial velocity is smooth on [0, 1), has velocity and pressure supported at every earlier time in a fixed compact subset of the interior of Q_0 = (−1/2, 1/2)³, and satisfies lim sup_{t↑1} ‖U(t)‖_{L^∞(T³)} = ∞; there is no global smooth periodic solution for the same datum and force. Proof: rescale by λ with t_0 = 1 − λ^{−2}, then sum the disjoint integer translates. OBLIGATION: The periodic breakdown alternative (D) in [13], with a periodic pressure \"as required in the erratum to the problem statement [13]\". MECHANISM: Parabolic scaling by λ shrinks the support into the open unit cube and compresses time by λ², and the shift t_0 = 1 − λ^{−2} keeps the singular time at t = 1. Integer translates of fields with disjoint, positively separated supports do not interact, since at every point at most one translate is nonzero, so the periodic sum solves the equation exactly. REFS: pp. 125 to 126, Corollary 10.6 and its proof; [13] cited on p. 125.",
"obligation": "The periodic breakdown alternative (D) in [13], with a periodic pressure \"as required in the erratum to the problem statement [13]\".",
"backward_question": "Can a compactly supported whole-space blowup be transplanted to the torus without the translates interacting through the nonlinearity or the pressure, and with the singular time and viscosity unchanged?",
"mechanism": "Parabolic scaling by λ shrinks the support into the open unit cube and compresses time by λ², and the shift t_0 = 1 − λ^{−2} keeps the singular time at t = 1. Integer translates of fields with disjoint, positively separated supports do not interact, since at every point at most one translate is nonzero, so the periodic sum solves the equation exactly, nonlinear term and pressure included, and the pressure is automatically periodic. On T³ uniqueness is simpler than on R³: periodic integration removes the transport and pressure terms, so Gronwall with ‖∇U‖_∞ closes on each [0, T], T < 1, with no energy or pressure-growth hypothesis.",
"antecedent": "Fefferman [13] (alternative (D), and the erratum requiring a periodic pressure); otherwise none cited.",
"cost": "The force now has time support in [t_0, 1 + λ^{−2}], the solution vanishes for t < t_0, and λ depends on ν through K_ν = √ν K. The non-existence is stated for global smooth periodic solutions with the same datum and force.",
"checkable": "Symbolically confirm that ũ, p̃, f̃ scale every term of the momentum equation by λ³ and that λ²(t − t_0) = 1 exactly at t = 1. For a given K_ν and λ with λ^{−1} K_ν ⋐ Q_0, confirm numerically that the translates λ^{−1} K_ν + k are pairwise disjoint with a positive gap. Confirm (λ x̃_τ, λ²(t̃_τ − t_0)) = (√ν x_τ, 1 − τ), which together with (10.21) and (10.22) gives the stated growth of U_θ.",
"depends_on": [
"M10.11",
"M10.2",
"M10.5",
"M10.10"
],
"constrains": [],
"reasons": {
"M10.11": "Periodizes the viscosity-ν fields supported in K_ν, choosing λ with λ^{-1}K_ν inside the open unit cube Q_0.",
"M10.2": "The fields vanish on an initial time interval and have fixed compact support, so zero extension and disjoint translates work.",
"M10.5": "The force vanishes near t = 0 and has compact time support, so the rescaled periodic force is smooth.",
"M10.10": "The growth (10.21) transfers to U_θ along the rescaled path."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 125-126",
"analogous_to": [],
"relations": {
"M10.11": "prerequisite",
"M10.2": "prerequisite",
"M10.5": "prerequisite",
"M10.10": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: FRAGMENT; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "MA.1",
"kind": "move",
"name": "ns-ma-1-distinct-power-weights-give-independent-moment-changes",
"title": "Distinct power weights give independent moment changes (Lemma A.1)",
"section": "A",
"pages": "126-127",
"refs": [
"pp. 126 to 127, Lemma A.1, (A.1)",
"restated p. 34 (Lemma 4.7)."
],
"statement": "For distinct real α_1, ..., α_m and nonnegative nonzero smooth bumps β_j supported in the interiors of compact intervals I_1 < ... < I_m in (0, ∞), the matrix B_ij = ∫_0^∞ x^{α_i} β_j(x) dx is invertible; the same holds for exponential weights in a logarithmic coordinate, and the inverse and each fixed parameter derivative stay bounded over a smooth compact family that keeps the separations.",
"description": "For distinct real α_1, ..., α_m and nonnegative nonzero smooth bumps β_j supported in the interiors of compact intervals I_1 < ... < I_m in (0, ∞), the matrix B_ij = ∫_0^∞ x^{α_i} β_j(x) dx is invertible; the same holds for exponential weights in a logarithmic coordinate, and the inverse and each fixed parameter derivative stay bounded over a smooth compact family that keeps the separations. OBLIGATION: Every exact moment restoration in the paper needs the linear map from bump coefficients to moment changes to be invertible with a controlled inverse: Theorem 4.6 Step 3 (4.42), Proposition A.7, Proposition B.8, Proposition C.2, and the order-n solve (5.16) in Lemma 5.2. Without it a local edit could leave a moment discrepancy that propagates to the exterior, and Lemma 4.4(i) could not be invoked. MECHANISM: Multilinearity in the columns gives det B = ∫_{I_1 × ... × I_m} det[x_j^{α_i}] Π_j β_j(x_j) dx. The generalized Vandermonde determinant cannot vanish on 0 < x_1 < ... ANTECEDENT: None cited. The proof names Rolle's theorem (zero counting for sums of distinct powers) and multilinearity of the determinant. REFS: pp. 126 to 127, Lemma A.1, (A.1); restated p. 34 (Lemma 4.7).",
"obligation": "Every exact moment restoration in the paper needs the linear map from bump coefficients to moment changes to be invertible with a controlled inverse: Theorem 4.6 Step 3 (4.42), Proposition A.7, Proposition B.8, Proposition C.2, and the order-n solve (5.16) in Lemma 5.2. Without it a local edit could leave a moment discrepancy that propagates to the exterior, and Lemma 4.4(i) could not be invoked.",
"backward_question": "If I add finitely many fixed bumps to a profile, when do the resulting changes in finitely many power-weighted integrals span every prescribed discrepancy, and how fast does this fail as two weights coalesce?",
"mechanism": "Multilinearity in the columns gives det B = ∫_{I_1 × ... × I_m} det[x_j^{α_i}] Π_j β_j(x_j) dx. The generalized Vandermonde determinant cannot vanish on 0 < x_1 < ... < x_m: otherwise some nonzero combination of the m distinct powers would have m distinct positive zeros, whereas dividing by the lowest power and applying Rolle's theorem inductively shows it has at most m - 1. The ordered cone is connected, so the integrand has one sign and is nonzero on a set of positive measure. The substitution x = e^y gives the logarithmic version; compactness plus differentiation of B^{-1}B = Id gives the uniform bounds. The explicit 2 × 2 determinant (A.1) is proportional to the exponent gap, which quantifies the loss.",
"antecedent": "None cited. The proof names Rolle's theorem (zero counting for sums of distinct powers) and multilinearity of the determinant.",
"cost": "Bumps must have ordered disjoint supports and the exponents within each block must be distinct. A gap of size λ costs λ^{-1} in the inverse, so λ must be fixed before any later large parameter (the radial frequency N of Proposition C.2), or the loss must be absorbed by an exponentially small discrepancy, as in (A.15).",
"checkable": "Compute B for random distinct exponents and rescaled σ' bumps on ordered intervals and check that det B is nonzero with the sign of det[x_j^{α_i}] on the ordered cone; verify (A.1) symbolically; tabulate ‖B^{-1}‖ against λ for the weights (1, x^{-λ}) and (e^{(1/2-λ)y}, e^{(1/2-2λ)y}) to see the λ^{-1} growth.",
"depends_on": [],
"constrains": [],
"reasons": {},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 126-127",
"analogous_to": [],
"relations": {},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "digest-only",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "MA.2",
"kind": "move",
"name": "ns-ma-2-quadratic-moment-equations-solved-by-contraction-with-c-k",
"title": "Quadratic moment equations solved by contraction with C^k control (Lemma A.2)",
"section": "A",
"pages": "127-128",
"refs": [
"pp. 127 to 128, Lemma A.2, (A.2), (A.3), scaling bound p. 128",
"restated pp. 34 to 35 (Lemma 4.7)."
],
"statement": "Lemma A.2 (pp. 127 to 128): suppose coefficients c ∈ R^m change the required moments by exactly F_η(c) = B(η)c + Q_η(c, c) (A.2) on K = [−1, 1], with B smooth and invertible and Q smooth bilinear; let β_0 = sup_K ‖B^{−1}‖, κ_0 = sup_K ‖Q‖, d_0 = ‖d‖_{C^0(K)}. If 8β_0²κ_0 d_0 ≤ 1, then F_η(c) = d(η) has a unique solution with ‖c‖_{C^0} ≤ 2β_0 d_0, smooth in η and the limit of c ↦ B^{−1}(d − Q(c, c)) from zero; if Q = 0 no smallness is needed. If also 8β_k²κ_k‖d‖_{C^k} ≤ 1 (β_k, κ_k the C^k analogues) for a preselected k, then ‖c‖_{C^k} ≤ 2β_k‖d‖_{C^k} (A.3).",
"description": "Lemma A.2 (pp. 127 to 128): suppose coefficients c ∈ R^m change the required moments by exactly F_η(c) = B(η)c + Q_η(c, c) (A.2) on K = [−1, 1], with B smooth and invertible and Q smooth bilinear; let β_0 = sup_K ‖B^{−1}‖, κ_0 = sup_K ‖Q‖, d_0 = ‖d‖_{C^0(K)}. If 8β_0²κ_0 d_0 ≤ 1, then F_η(c) = d(η) has a unique solution with ‖c‖_{C^0} ≤ 2β_0 d_0, smooth in η and the limit of c ↦ B^{−1}(d − Q(c, c)) from zero; if Q = 0 no smallness is needed. If also 8β_k²κ_k‖d‖_{C^k} ≤ 1 (β_k, κ_k the C^k analogues) for a preselected k, then ‖c‖_{C^k} ≤ 2β_k‖d‖_{C^k} (A.3). OBLIGATION: The moments J, S, C_p are quadratic in (U, E), so an invertible linearization alone does not restore them exactly. The lemma gives exact solutions whose finitely many prescribed η-derivatives are small, and the scaling bound turns this into small field derivatives on the patch, which is what keeps the strict cone inequalities (which involve finitely many field derivatives) intact at every correction. REFS: pp. 127 to 128, Lemma A.2, (A.2), (A.3), scaling bound p. 128; restated pp. 34 to 35 (Lemma 4.7).",
"obligation": "The moments J, S, C_p are quadratic in (U, E), so an invertible linearization alone does not restore them exactly. The lemma gives exact solutions whose finitely many prescribed η-derivatives are small, and the scaling bound turns this into small field derivatives on the patch, which is what keeps the strict cone inequalities (which involve finitely many field derivatives) intact at every correction.",
"backward_question": "The moment functionals are quadratic in the profile; can the finite system be solved exactly, smoothly in η, with bounds on a prescribed finite number of η-derivatives, without demanding smallness at every derivative order at once?",
"mechanism": "On the C^0 ball of radius r = 2 β_0 d_0, the map sends c to a vector of norm at most r/2 + β_0 κ_0 r^2 ≤ r and has Lipschitz constant at most 2 β_0 κ_0 r ≤ 1/2, so it is a contraction. The same argument in the Banach algebra C^k(K) yields (A.3), and because the iterates are identical, the two limits coincide. The same smallness makes B + D_c Q invertible, so the pointwise implicit function theorem gives smoothness in η, including one-sided derivatives at η = ±1; all other fixed derivatives are finite by implicit differentiation, with no simultaneous smallness over all orders. An extra compact parameter (the pulse amplitude) is carried the same way.",
"antecedent": "None cited. The proof names the contraction argument in C^0 and in the Banach algebra C^k and the pointwise implicit function theorem.",
"cost": "The smallness conditions 8 β_0^2 κ_0 d_0 ≤ 1 and 8 β_k^2 κ_k ‖d‖_{C^k} ≤ 1, imposed only for finitely many k; each discrepancy must therefore be made small first (by a large radius, a large frequency, or exponential decay).",
"checkable": "None: pure estimate. Its concrete instances are the finite solves listed under MA.3, MA.5, MA.6 and MA.11, which are checkable there.",
"depends_on": [
"M4.5",
"MA.1"
],
"constrains": [],
"reasons": {
"M4.5": "the equations it solves are exact changes of the cumulative integrals (4.15), in which J, S, Cp are quadratic in (U, E).",
"MA.1": "its invertible linear part B, with bounded η-derivatives of B^{-1}, is the power-weight moment matrix of Lemma A.1."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 127-128",
"analogous_to": [],
"relations": {
"M4.5": "prerequisite",
"MA.1": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: TRUNCATED; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},