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": "MA.3",
"kind": "move",
"name": "ns-ma-3-the-five-moment-jacobian-on-a-power-law-patch-corollary-a",
"title": "The five-moment Jacobian on a power-law patch (Corollary A.3)",
"section": "A",
"pages": "128",
"refs": [
"p. 128, Corollary A.3, (A.4)",
"used p. 42 (4.42), pp. 139 to 140, pp. 156 to 157, p. 162."
],
"statement": "Corollary A.3 (p. 128): for the five cumulative integrals (M, I, J, S, C_p) of (4.15), under X = ρx the normalizing factors are (ρ, ρ^{3/2}, ρ^{3/2}, ρ, 1), with H = ρ^{1/2}√(2x) E (A.4). On a correction interval with U_0 = u_c(η) and E_0 = e∗ f∗(η) x^α (e∗ > 0, f∗ > 0 smooth), two additive U bumps and three additive E bumps give an invertible Jacobian of the normalized five-moment map provided α ∉ {−1/2, 1/2, 3/2}, and the moment changes have the exact quadratic form (A.2); at U_0 = 0 the three E bumps prescribe changes in (I, S, C_p) while preserving M and J.",
"description": "Corollary A.3 (p. 128): for the five cumulative integrals (M, I, J, S, C_p) of (4.15), under X = ρx the normalizing factors are (ρ, ρ^{3/2}, ρ^{3/2}, ρ, 1), with H = ρ^{1/2}√(2x) E (A.4). On a correction interval with U_0 = u_c(η) and E_0 = e∗ f∗(η) x^α (e∗ > 0, f∗ > 0 smooth), two additive U bumps and three additive E bumps give an invertible Jacobian of the normalized five-moment map provided α ∉ {−1/2, 1/2, 3/2}, and the moment changes have the exact quadratic form (A.2); at U_0 = 0 the three E bumps prescribe changes in (I, S, C_p) while preserving M and J. OBLIGATION: Lemma 4.4(i) preserves the exterior pressure, radial velocity, Q_s, N_s, p_s and T_0 only when all five integrals agree at the joining radius. The corollary says exactly which patches let five local bumps reset all five integrals, so that each join (Proposition B.8 at α = 1/10; Theorem 4.6 Step 3, Proposition A.7 and Proposition C.2 at α = -1/2 - λ) is solvable. MECHANISM: With u_c frozen at its base value, the row operations J → J - u_c I and S → S - 2 u_c M make the linearization block diagonal: the U block (rows M and J - u_c I, the latter with differential ∫ √(2x) E_0 δU dx) has weights.",
"obligation": "Lemma 4.4(i) preserves the exterior pressure, radial velocity, Q_s, N_s, p_s and T_0 only when all five integrals agree at the joining radius. The corollary says exactly which patches let five local bumps reset all five integrals, so that each join (Proposition B.8 at α = 1/10; Theorem 4.6 Step 3, Proposition A.7 and Proposition C.2 at α = -1/2 - λ) is solvable.",
"backward_question": "On which explicit profile patches can two axial and three azimuthal bumps reset all five cumulative integrals independently, and which exponent coincidences must be avoided?",
"mechanism": "With u_c frozen at its base value, the row operations J → J - u_c I and S → S - 2 u_c M make the linearization block diagonal: the U block (rows M and J - u_c I, the latter with differential ∫ √(2x) E_0 δU dx) has weights 1, x^{α+1/2}, and the E block (rows I, S - 2 u_c M with differential -∫ E_0 δE dx, and C_p) has weights x^{1/2}, x^α, x^{α-1}. Distinct exponents within each block is exactly α ∉ {-1/2, 1/2, 3/2}, so Lemma A.1 applies; the original functionals have degree at most two in (U, E), so the remainder is exactly quadratic and Lemma A.2 applies (the row operations do not assume the corrected U stays constant). The two instances used: α = 1/10 (axis moment correction) with blocks (0, 3/5) and (1/2, 1/10, -9/10); α = -1/2 - λ (intermediate patches) with blocks (0, -λ) and (1/2, -1/2 - λ, -3/2 - λ), where the first block has inverse bound λ^{-1}.",
"antecedent": "None cited beyond Lemma A.1.",
"cost": "Correction patches must carry an exact power law with U_0 constant in X, which is why Section A.2 reserves untouched patches. On the intermediate patches the λ^{-1} inverse forces λ to be fixed before the radial frequency N.",
"checkable": "Assemble the 5 × 5 Jacobian of (M, I, J, S, C_p) at U_0 = u_c, E_0 = e∗ f∗ x^α with fixed bumps; check invertibility for α outside {-1/2, 1/2, 3/2} and singularity at those three values (two rows then carry the same weight); confirm the block exponents for α = 1/10 and α = -1/2 - λ and the λ^{-1} growth of the U-block inverse as λ → 0.",
"depends_on": [
"M4.5",
"MA.1",
"MA.2"
],
"constrains": [],
"reasons": {
"M4.5": "the map it linearizes is the five cumulative integrals (4.15), rescaled under X = ρx by the factors (A.4).",
"MA.1": "after row operations each block has distinct power weights against ordered disjoint bumps, so Lemma A.1 inverts it when α ∉ {-1/2, 1/2, 3/2}.",
"MA.2": "the full moment change is exactly quadratic, the form (A.2) that Lemma A.2 solves by contraction."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 128",
"analogous_to": [],
"relations": {
"M4.5": "prerequisite",
"MA.1": "prerequisite",
"MA.2": "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": "MA.4",
"kind": "move",
"name": "ns-ma-4-the-staged-outer-reference-profile-with-four-reserved",
"title": "The staged outer reference profile with four reserved patches (Section A.2, Proposition A.4)",
"section": "A",
"pages": "129-131",
"refs": [
"pp. 129 to 131, (A.5) to (A.13), Proposition A.4",
"used by Lemma 4.8, pp. 35 to 36."
],
"statement": "Proposition A.4 (pp. 129 to 131): with σ of (A.5) and finite choices in the order (A.6) (M_d, T_d = e^{M_d} + 10, P∗ > e^{T_d}, 0 < λ ≪ 1, 0 < h ≪ min{λ, e^{−T_d}}, then X_R), the staged profile (reference (A.7), axial reduction, l = −λ over T_w (A.9), pulse, η-flattening, exterior transition) has U, E smooth for X > 0, E > 0, (A.8); U = M = J = 0 after the pulse, E = c∞X^{−A} after the terminal interval; the four patches keep U = 0, E ∝ f X^{−1/2−λ}; for x_− ∈ (0, 1], X_R large, the strict relaxed cone holds from x_−, the admissible cone from the first l < 0, through tail coordinate 1/2.",
"description": "Proposition A.4 (pp. 129 to 131): with σ of (A.5) and finite choices in the order (A.6) (M_d, T_d = e^{M_d} + 10, P∗ > e^{T_d}, 0 < λ ≪ 1, 0 < h ≪ min{λ, e^{−T_d}}, then X_R), the staged profile (reference (A.7), axial reduction, l = −λ over T_w (A.9), pulse, η-flattening, exterior transition) has U, E smooth for X > 0, E > 0, (A.8); U = M = J = 0 after the pulse, E = c∞X^{−A} after the terminal interval; the four patches keep U = 0, E ∝ f X^{−1/2−λ}; for x_− ∈ (0, 1], X_R large, the strict relaxed cone holds from x_−, the admissible cone from the first l < 0, through tail coordinate 1/2. OBLIGATION: Lemma 4.8 needs one outer family that (a) fixes the axis pressure datum (MA.8), (b) ends in an η-independent power law that can be heat-replaced (MA.10, MA.11), (c) satisfies the total identities that remove stress tails (MA.12), (d) keeps the cone (MA.9), and (e) leaves untouched power-law patches for Proposition C.2 and Theorem 4.6 Step 3 (I_1), Proposition A.7 (I_2), Lemma 5.2 (I_pos = I_3) and Lemma 8.7 (I_mean = I_4). Theorem 4.6(vi) is the statement that I_3, I_4 survive with the form (4.30). REFS: pp. 129 to 131, (A.5) to (A.13), Proposition A.4; used by Lemma 4.8, pp. 35 to 36.",
"obligation": "Lemma 4.8 needs one outer family that (a) fixes the axis pressure datum (MA.8), (b) ends in an η-independent power law that can be heat-replaced (MA.10, MA.11), (c) satisfies the total identities that remove stress tails (MA.12), (d) keeps the cone (MA.9), and (e) leaves untouched power-law patches for Proposition C.2 and Theorem 4.6 Step 3 (I_1), Proposition A.7 (I_2), Lemma 5.2 (I_pos = I_3) and Lemma 8.7 (I_mean = I_4). Theorem 4.6(vi) is the statement that I_3, I_4 survive with the form (4.30).",
"backward_question": "Can I write down, explicitly and stage by stage in log X, an outer profile that starts at the reference inner power law, ends at an η-independent power law c∞ X^{-A}, has enough independent scalar knobs to meet every total moment identity, stays inside the stress cone, and still leaves room for four later corrections?",
"mechanism": "Prescribing the log slope l instead of E makes every stage an explicit exponential in y, so the moment integrals and the linear equations for Q_s, N_s become explicit. The reference stage (l = 3/5, a = 4/5) is where the axis profile will later be attached. The axial reduction first flattens H (a potential vortex, a = 2) and then removes the axial velocity so slowly that |k'| ≤ e_d/(1 + y) with e_d = 4‖σ'‖_∞/M_d, keeping the axial shear b_s small. The intermediate stage l = -λ gives a = 2 + 2λ > 2 (admissible) and exact power-law patches. The pulse is the one adjustable source of positive S-moment. The interpolation (A.10) replaces the η shape f by its value 1/2 at η = ±1 without letting E increase, so the tail is η-independent, as a z-independent heat exterior requires. The steep stage (l = -1) cuts the amplitude by h^6 and resets Q_s, and the terminal factor f_o is what later produces a positive angular stress at the outer edge. Since the schedule depends only on x = X/X_R, normalized fields are X_R-independent and X_R remains a free final scale.",
"antecedent": "None cited. The step (A.5) is the standard e^{-1/y^2} gluing function, used without citation.",
"cost": "The ordering (A.6); auxiliary constants T_f (large), c_o (small), bump width .3; λ small enough that the four patches fit in (0, T_w); a very long logarithmic profile (roughly e^{M_d} + 13/λ + 90 log(1/λ) + O(log(1/h)) units) whose amplitude is exponentially small in 1/λ after the pulse. The inner reference branch (A.7) is not regular at the axis and must be replaced (Appendix B).",
"checkable": "Integrate (log E)' = l(y) - 1/2 along the schedule for sample parameters (work in log variables to avoid underflow) and compute the five cumulative integrals by quadrature in y. Check that k = 0 exactly on the last eleven units of [0, T_d] (since σ(log(1 + y)/M_d) = 1 iff y ≥ e^{M_d} - 1 = T_d - 11); that the patches lie in (0, T_w) iff T_w > 25; that E = c_patch f X^{-1/2-λ}, U = 0 on each patch. Digest-pass computation: ‖σ'‖_∞ = σ'(1/2) = 8, so e_d = 32/M_d, and T_f ≥ 10 (log 2) ‖σ'‖_∞ ≈ 55.5 suffices for -λ - .1 ≤ l ≤ -λ in (A.10) (there l = -λ + ϑ_f'(y)(log 2 - J_0) with ϑ_f' ≤ 0 and 0 ≤ log 2 - J_0 ≤ log 2).",
"depends_on": [
"M4.5",
"M4.7",
"M4.4"
],
"constrains": [],
"reasons": {
"M4.5": "its tuning targets the total cumulative integrals: U = M = J = 0 after the pulse and the identities (A.8) for S and the renormalized I.",
"M4.7": "it asserts the strict relaxed cone from x_- and the admissible cone from the intermediate power law onward, in Lemma 4.5's terms.",
"M4.4": "each stage prescribes l = D_X log H of (4.8), which fixes the shear a = 2 - 2l and makes Q_s, N_s of (4.9) explicit."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 129-131",
"analogous_to": [],
"relations": {
"M4.5": "prerequisite",
"M4.7": "prerequisite",
"M4.4": "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": "MA.5",
"kind": "move",
"name": "ns-ma-5-closing-m-j-0-after-the-axial-pulse-section-a-3-first-part",
"title": "Closing M = J = 0 after the axial pulse (Section A.3, first part)",
"section": "A",
"pages": "130-131",
"refs": [
"pp. 130 to 131, (A.14), (A.15)."
],
"statement": "Section A.3, closing M = J = 0 (pp. 130 to 131): on the pulse 0 ≤ y ≤ 13/λ, with l = −λ and U = E R_b, R_b = Amp(η) R_0(λy) + c_1β_1(y) + c_2β_2(y), R_0 the ramp φ_b[1 − σ(ξ_b − 10)], ξ_b = λy, and β_i identical width-.3 bumps centered at 13/λ − 3 and 13/λ − 1: given the pre-pulse bounds (A.14), e_b ≤ C_pre λ^{30} and ‖A_X(U)/E‖_{C^1_η} ≤ C_pre λ^{29}, there are end coefficients c_i, affine in Amp with ‖c_i‖_{C^1_η} ≤ C_pre e^{−c/λ}(1 + |Amp|), that give M = J = 0 after the pulse (A.15); every fixed y-derivative obeys the same bound.",
"description": "Section A.3, closing M = J = 0 (pp. 130 to 131): on the pulse 0 ≤ y ≤ 13/λ, with l = −λ and U = E R_b, R_b = Amp(η) R_0(λy) + c_1β_1(y) + c_2β_2(y), R_0 the ramp φ_b[1 − σ(ξ_b − 10)], ξ_b = λy, and β_i identical width-.3 bumps centered at 13/λ − 3 and 13/λ − 1: given the pre-pulse bounds (A.14), e_b ≤ C_pre λ^{30} and ‖A_X(U)/E‖_{C^1_η} ≤ C_pre λ^{29}, there are end coefficients c_i, affine in Amp with ‖c_i‖_{C^1_η} ≤ C_pre e^{−c/λ}(1 + |Amp|), that give M = J = 0 after the pulse (A.15); every fixed y-derivative obeys the same bound. OBLIGATION: M(∞) = J(∞) = 0 are two of the four identities (4.28). U = M = 0 beyond X_v gives V_0 = 0 by (4.7), so the exterior is purely azimuthal; M(∞) = 0 also makes the Stokes streamfunction vanish in the exterior (A = 0 for X ≥ X_ext in Theorem 3.1(iii), via (10.1)); J(∞) = 0 removes the angular-momentum transport integral in Lemma A.8. REFS: pp. 130 to 131, (A.14), (A.15). ANTECEDENT: None cited.",
"obligation": "M(∞) = J(∞) = 0 are two of the four identities (4.28). U = M = 0 beyond X_v gives V_0 = 0 by (4.7), so the exterior is purely azimuthal; M(∞) = 0 also makes the Stokes streamfunction vanish in the exterior (A = 0 for X ≥ X_ext in Theorem 3.1(iii), via (10.1)); J(∞) = 0 removes the angular-momentum transport integral in Lemma A.8.",
"backward_question": "After an axial pulse, how do I cancel the axial mass flux M and the axial transport of angular momentum J exactly when the only available weights are nearly degenerate (exponents differing by λ)?",
"mechanism": "The pre-pulse debts are tiny in natural units: M is frozen after the axial reduction while XE grows like e^{(1/2-λ)y} and XHE like e^{(1/2-2λ)y} over T_w = 60 log(1/λ), and E itself drops by e^{-(1/2+λ)T_w} ≤ λ^{30}. The main pulse is cut off at ξ_b = 11 (y = 11/λ), at least 2/λ - 3 before the first bump center, so, normalized at that center, its contributions carry factors like e^{-s_i(2/λ - 3)} with s_1 = 1/2 - λ, s_2 = 1/2 - 2λ, both above .4. With E fixed, M and J are linear in U, so the correction is a linear 2 × 2 solve with weights e^{s_1 y}, e^{s_2 y}; its inverse is O(λ^{-1}) by (A.1), which the factor e^{-c/λ} absorbs.",
"antecedent": "None cited.",
"cost": "The gap of order 2/λ between the pulse cutoff and the end bumps; the end coefficients depend affinely on the still unknown Amp, which is fixed in MA.7.",
"checkable": "For sample λ, form the 2 × 2 matrix of the weights e^{(1/2-λ)y}, e^{(1/2-2λ)y} against the two width-.3 bumps, check ‖B^{-1}‖ ≈ C λ^{-1}, compute the normalized contributions of the main pulse to M and J and confirm their e^{-c/λ} decay, and check e^{-(1/2+λ)·60 log(1/λ)} = λ^{30 + 60λ} ≤ λ^{30}.",
"depends_on": [
"MA.4",
"MA.1",
"M4.5"
],
"constrains": [],
"reasons": {
"MA.4": "works on the axial-pulse stage of the Section A.2 schedule, after the intermediate power law of length T_w = 60 log(1/λ).",
"MA.1": "the two end bumps solve a 2×2 system with weights e^{(1/2-λ)y}, e^{(1/2-2λ)y}, whose inverse is O(λ^{-1}) by (A.1).",
"M4.5": "the targets are the cumulative integrals M = ∫U and J = ∫UH of (4.15), linear in U once E is fixed."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 130-131",
"analogous_to": [],
"relations": {
"MA.4": "prerequisite",
"MA.1": "prerequisite",
"M4.5": "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.6",
"kind": "move",
"name": "ns-ma-6-the-renormalized-angular-moment-identity-through-the",
"title": "The renormalized angular-moment identity through the exact Q_s equation (Section A.3, second part)",
"section": "A",
"pages": "130-132",
"refs": [
"p. 130, (A.10) to (A.13)",
"pp. 131 to 132, (A.16) to (A.18)."
],
"statement": "Section A.3, angular identity (pp. 130 to 132): after the pulse U = 0; the interpolation (A.10) makes E η-independent, and two relative E bumps on the following 30 log(1/λ) hold impose (A.11), I = XH/(1 − λ) with ∫(E² − E²_unedited) dy = 0, coefficients O_{C^1_η}(C_pre λ^{28}). At the exterior transition Q_s = (λ − h)/(1 − λ) by (4.16); the l = −h hold runs until Q_s reaches Q_p of (A.13), and the terminal solution (A.16) vanishes from y = 3 on, so I = XH/(1 − h) beyond the tail, i.e. ∫_0^∞ (H − H_pow) dX = 0. The steep interval gives E ratio h^6 (A.17), and (A.18) bounds the release.",
"description": "Section A.3, angular identity (pp. 130 to 132): after the pulse U = 0; the interpolation (A.10) makes E η-independent, and two relative E bumps on the following 30 log(1/λ) hold impose (A.11), I = XH/(1 − λ) with ∫(E² − E²_unedited) dy = 0, coefficients O_{C^1_η}(C_pre λ^{28}). At the exterior transition Q_s = (λ − h)/(1 − λ) by (4.16); the l = −h hold runs until Q_s reaches Q_p of (A.13), and the terminal solution (A.16) vanishes from y = 3 on, so I = XH/(1 − h) beyond the tail, i.e. ∫_0^∞ (H − H_pow) dX = 0. The steep interval gives E ratio h^6 (A.17), and (A.18) bounds the release. OBLIGATION: The renormalized angular identity in (A.8) and (4.28). Without it the integrated angular residual need not vanish and T_θ keeps an r^{-2} tail in the exterior, so Lemma A.8 fails. The same computation makes the reference inviscid angular stress vanish beyond the tail, and the h^6 reduction is what later makes w and T_z/T_θ small near the outer edge. MECHANISM: The ratio r_I = I/(XH) obeys r_I' + (1 + l) r_I = 1, so on the η-independent hold it relaxes to 1/(1 - λ) at rate 1 - λ, leaving an O(λ^{28}) discrepancy after 30 log(1/λ) units;",
"obligation": "The renormalized angular identity in (A.8) and (4.28). Without it the integrated angular residual need not vanish and T_θ keeps an r^{-2} tail in the exterior, so Lemma A.8 fails. The same computation makes the reference inviscid angular stress vanish beyond the tail, and the h^6 reduction is what later makes w and T_z/T_θ small near the outer edge.",
"backward_question": "How can the renormalized total angular momentum be made to vanish exactly and uniformly in η, when the moment is coupled to Q_s through an ODE in log X and the exterior must be η-independent?",
"mechanism": "The ratio r_I = I/(XH) obeys r_I' + (1 + l) r_I = 1, so on the η-independent hold it relaxes to 1/(1 - λ) at rate 1 - λ, leaving an O(λ^{28}) discrepancy after 30 log(1/λ) units; two relative bumps (I row slope 1 - λ, linearized pressure row slope -1 - 2λ, bounded inverse by (A.1)) cancel it exactly by Lemma A.2 while keeping ∫E^2 dy, hence Π_0, unchanged. Because E is now η-independent, Q_s follows an explicit scalar ODE: during l = -1 it grows linearly (Q_s' = 1 - h) to size about log(1/h), and during l = -h it decays at rate 1 - h. Since Q_p ≍ ρ_o ≍ h is smaller, the hold has a positive finite length, used as a shooting parameter so that Q_s hits Q_p exactly; the terminal source -f_o'/f_o ≤ 0 then drives Q_s to zero at y = 3. Beyond the tail H = H_pow ∝ X^{-h}, integrable at 0 since h < 1, so ∫_0^X H_pow = X H_pow/(1 - h) and I = XH/(1 - h) is the same as ∫_0^∞ (H - H_pow) dX = 0. This part uses E only and is independent of Amp.",
"antecedent": "None cited (integrating-factor solution of a linear first-order ODE).",
"cost": "A steep interval of length 4 log(1/h) and an h-dependent hold length; the constant c_o must make 0 ≤ f_o'/f_o < h/4.",
"checkable": "Integrate Q' + (1 + l)Q = -l - h along the exterior schedule from Q = (λ - h)/(1 - λ), find the hold length at which Q = Q_p, verify Q_s(3) = 0 from (A.16), and confirm I(X) = XH/(1 - h) beyond the tail by direct quadrature of I. Check (A.17) as e^{2(-1)·4 log(1/h)} = h^8 and e^{(-3/2)·4 log(1/h)} = h^6. Digest-pass computation: with c_o = 0.05625 (so max f_o'/f_o = 0.225 h < h/4), Q_p/ρ_o = 7.415 for h = 10^{-3} and 7.430 for h = 10^{-6}, confirming Q_p ≍ ρ_o ≍ h.",
"depends_on": [
"MA.4",
"M4.5",
"MA.5",
"MA.2"
],
"constrains": [],
"reasons": {
"MA.4": "tunes the interpolation (A.10), the hold with two bumps (A.11), and the l = -h hold length in the Section A.2 schedule.",
"M4.5": "with U = M = J = 0 and E η-independent, (4.16) gives Q_s = -1 + (1 - h)I/(XH), so Q_s = 0 beyond the tail means I = XH/(1 - h).",
"MA.5": "starts from U = M = J = 0 after the pulse, which turns Q_s into the solution of a scalar ODE in log X.",
"MA.2": "the two relative E bumps meet (A.11) exactly while keeping ∫E²dy, hence Π0, by Lemma A.2's contraction."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 130",
"analogous_to": [],
"relations": {
"MA.4": "prerequisite",
"M4.5": "prerequisite",
"MA.5": "prerequisite",
"MA.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": "astra-spot-check-2026-10-01",
"computation_checked": false,
"astra_spot_check": "locator-corrected"
}
},
{
"id": "MA.7",
"kind": "move",
"name": "ns-ma-7-s-0-by-a-scalar-root-in-the-pulse-amplitude-section-a-3",
"title": "S(∞) = 0 by a scalar root in the pulse amplitude (Section A.3, third part)",
"section": "A",
"pages": "132-133",
"refs": [
"pp. 132 to 133, (A.19), (A.20)."
],
"statement": "With M, J, I fixed independently of Amp, (A.19) holds: λ S(∞)/(X_p e_b^2 f^2) = Amp^2 K_b - (1 - e^{-26})/4 + E(Amp, η), K_b = ∫_0^{13} e^{-2ξ_b} R_0(ξ_b)^2 dξ_b, with ‖E‖_{C^1} ≤ C_pre λ(1 + log(1/λ)) on [.9, 1.2] × [-1, 1]. Since .20 < K_b ≤ 1/4, the principal expression is below -.047 at .9, above .038 at 1.2, and has amplitude derivative at least .36, so for small λ there is a unique smooth root with |∂_η Amp| ≤ C_pre λ(1 + log(1/λ)) (A.20). Both equalities of (A.8) then hold.",
"description": "With M, J, I fixed independently of Amp, (A.19) holds: λ S(∞)/(X_p e_b^2 f^2) = Amp^2 K_b - (1 - e^{-26})/4 + E(Amp, η), K_b = ∫_0^{13} e^{-2ξ_b} R_0(ξ_b)^2 dξ_b, with ‖E‖_{C^1} ≤ C_pre λ(1 + log(1/λ)) on [.9, 1.2] × [-1, 1]. Since .20 < K_b ≤ 1/4, the principal expression is below -.047 at .9, above .038 at 1.2, and has amplitude derivative at least .36, so for small λ there is a unique smooth root with |∂_η Amp| ≤ C_pre λ(1 + log(1/λ)) (A.20). Both equalities of (A.8) then hold. OBLIGATION: S(∞) = 0 in (A.8) and (4.28). Without it the axial momentum flux including pressure does not integrate to zero and T_z keeps an r^{-1} tail in the exterior (Lemma A.8 fails). The small η-derivative (A.20) is reused in the cone check on the pulse, where it makes the η m_η term negligible. MECHANISM: On the pulse U^2 - E^2/2 = E^2(R_b^2 - 1/2) and XE^2 = X_p e_b^2 f^2 e^{-2λy}, so in ξ_b = λy the pulse contributes (X_p e_b^2 f^2/λ)[Amp^2 K_b - (1 - e^{-26})/4] up to exponentially small end-bump terms. ANTECEDENT: None cited (a monotone scalar root with implicit differentiation). REFS: pp. 132 to 133, (A.19), (A.20).",
"obligation": "S(∞) = 0 in (A.8) and (4.28). Without it the axial momentum flux including pressure does not integrate to zero and T_z keeps an r^{-1} tail in the exterior (Lemma A.8 fails). The small η-derivative (A.20) is reused in the cone check on the pulse, where it makes the η m_η term negligible.",
"backward_question": "After M, J and I are fixed, which single scalar knob controls the last total moment S(∞), and is its equation monotone enough to solve uniquely with small η-derivatives?",
"mechanism": "On the pulse U^2 - E^2/2 = E^2(R_b^2 - 1/2) and XE^2 = X_p e_b^2 f^2 e^{-2λy}, so in ξ_b = λy the pulse contributes (X_p e_b^2 f^2/λ)[Amp^2 K_b - (1 - e^{-26})/4] up to exponentially small end-bump terms. Everything else (the pre-pulse debt (A.14), the interpolation and hold stages, and the release integral (A.18), all either carrying the factor e^{-26} or lacking the 1/λ length) is of relative size λ(1 + log(1/λ)). So at leading order the pulse's axial term must balance its own azimuthal term, a monotone scalar equation in Amp. The bounds on K_b follow from R_0 ≤ ξ_b (giving ∫_0^∞ ξ^2 e^{-2ξ} dξ = 1/4) and R_0 ≥ ξ_b - .02 on [.02, 9].",
"antecedent": "None cited (a monotone scalar root with implicit differentiation).",
"cost": "λ small enough that E(Amp, η) stays within the bracket margins; the pulse makes U/E as large as about 10·Amp, which the cone check (MA.9) must tolerate.",
"checkable": "Evaluate K_b by quadrature, using φ_b(ξ) = ξ - .01 for ξ ≥ .02 (because ∫_0^1 σ = 1/2). Digest-pass computation: K_b = 0.245050; principal expression -0.0515 at .9 and 0.1029 at 1.2; root Amp_0 = ((1 - e^{-26})/(4 K_b))^{1/2} = 1.01005; worst-case bracket values .81/4 - 1/4 = -.0475, 1.44(.20) - .25 = .038, slope 2(.9)(.20) = .36, matching the paper.",
"depends_on": [
"MA.5",
"MA.6",
"M4.5"
],
"constrains": [],
"reasons": {
"MA.5": "Amp scales the axial pulse R_b of Section A.3, whose end bumps already give M = J = 0 affinely in Amp.",
"MA.6": "the angular identity uses E only, so I is fixed independently of Amp and S(∞) is the one remaining moment.",
"M4.5": "S = ∫(U² - E²/2) of (4.15) is the moment set to zero; on the pulse U² - E²/2 = E²(R_b² - 1/2)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 132-133",
"analogous_to": [],
"relations": {
"MA.5": "prerequisite",
"MA.6": "prerequisite",
"M4.5": "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": "MA.8",
"kind": "move",
"name": "ns-ma-8-the-analytic-axis-pressure-datum-fixed-from-the-outer",
"title": "The analytic axis pressure datum fixed from the outer schedule (Lemma A.5)",
"section": "A",
"pages": "133-134",
"refs": [
"pp. 133 to 134, Lemma A.5, (A.21) to (A.23)",
"used p. 35 ((4.31)), p. 37, p. 144, p. 150."
],
"statement": "Let E_{id,sched} be the inner reference (A.7) followed by the Section A.2 outer profile with the pressure-preserving angular bumps omitted. Then Π_0(η) = -(1/2) ∫_{-∞}^{∞} E_{id,sched}(y, η)^2 dy (A.21) is independent of X_R, analytic on a complex neighborhood of [-1, 1], even, has Π_0' with the sign of η, and satisfies Π_0 ≤ -(5/2) P∗^2 f(η)^2 (A.22); for the complete reference profile, Π(X, η) = -(1/2) ∫_{log(X/X_R)}^∞ E(v, η)^2 dv (A.23).",
"description": "Let E_{id,sched} be the inner reference (A.7) followed by the Section A.2 outer profile with the pressure-preserving angular bumps omitted. Then Π_0(η) = -(1/2) ∫_{-∞}^{∞} E_{id,sched}(y, η)^2 dy (A.21) is independent of X_R, analytic on a complex neighborhood of [-1, 1], even, has Π_0' with the sign of η, and satisfies Π_0 ≤ -(5/2) P∗^2 f(η)^2 (A.22); for the complete reference profile, Π(X, η) = -(1/2) ∫_{log(X/X_R)}^∞ E(v, η)^2 dv (A.23). OBLIGATION: The regular axis construction (Proposition B.2) needs its pressure value at X = 0 before the axis profile exists, analytic near [-1, 1] and with the sign and size properties used on p. 144 to make Z∗(η_0) ≥ c j_0 P∗^2 > 0 at the zero η_0 of H∗. The final profile must also satisfy the normalization (4.25). The lemma breaks this circularity: the datum depends only on the outer schedule, and later edits are required to preserve it. MECHANISM: Since Π = Π_0 + C_p with C_p = (1/2)∫E^2 dy, pressure vanishing at infinity forces Π_0 = -C_p(∞). ANTECEDENT: None cited (uniform integration of holomorphic functions). REFS: pp. 133 to 134, Lemma A.5, (A.21) to (A.23); used p. 35 ((4.31)), p. 37, p. 144, p. 150.",
"obligation": "The regular axis construction (Proposition B.2) needs its pressure value at X = 0 before the axis profile exists, analytic near [-1, 1] and with the sign and size properties used on p. 144 to make Z∗(η_0) ≥ c j_0 P∗^2 > 0 at the zero η_0 of H∗. The final profile must also satisfy the normalization (4.25). The lemma breaks this circularity: the datum depends only on the outer schedule, and later edits are required to preserve it.",
"backward_question": "The axis problem needs its pressure value at X = 0 before the inner profile exists; can that datum be fixed from the outer profile alone, analytic in η, and kept invariant under every later edit?",
"mechanism": "Since Π = Π_0 + C_p with C_p = (1/2)∫E^2 dy, pressure vanishing at infinity forces Π_0 = -C_p(∞). Without the angular bumps every piece of E has the form c(y) f(η)^{ϑ(y)}, 0 ≤ ϑ ≤ 1, with c and all transition lengths independent of η (ϑ = 1 through the pulse, decreasing to 0 in the interpolation, 0 beyond). On a simply connected complex neighborhood avoiding the poles and zeros of f, f^ϑ = exp(ϑ log f) is holomorphic uniformly in ϑ, and the integral converges uniformly (bounded by C e^{y/5} as y → -∞ and C e^{-(1+2h)y} as y → +∞), so Π_0 is analytic. Evenness is inherited from f. From ∂_η f^{2ϑ} = -2ϑ J_0' f^{2ϑ} with J_0' = 2η/(1 + η^2), every contribution to Π_0' has the sign of η, strictly so from the reference part, which contributes exactly -(5/2) P∗^2 f^2. No X_R enters the log-coordinate schedule, and the angular bumps change ∫E^2 dy by zero, which gives (A.23). More generally, an edit with zero total ∫(E_new^2 - E_old^2)/(2X) dX leaves the forward pressure unchanged before and after its support (not inside it), which is why pressure-neutral edits may be omitted in the backward integral (A.23).",
"antecedent": "None cited (uniform integration of holomorphic functions).",
"cost": "A standing constraint on every later edit of E: its total pressure increment must be zero or be restored by a five-moment match. Non-analytic edits (the heat factor) are allowed only under that constraint.",
"checkable": "Compute Π_0(η) by quadrature of the schedule; check evenness, the sign of Π_0', the bound (A.22), and that the reference piece equals -(1/2) P∗^2 f^2 ∫_{-∞}^0 e^{y/5} dy = -(5/2) P∗^2 f^2 (consistent with C_{p,0} = (5/2) P∗^2 f^2 x^{1/5} in (4.34)); evaluate at complex η near [-1, 1] to confirm analyticity.",
"depends_on": [
"MA.4",
"M4.5",
"MA.6"
],
"constrains": [],
"reasons": {
"MA.4": "the datum integrates E² along the Section A.2 schedule, whose pieces c(y)f(η)^{ϑ(y)} have η-independent transition lengths.",
"M4.5": "Π = Π(0, η) + Cp with Cp = ∫E²/(2x), so pressure vanishing at infinity forces Π0 = -Cp(∞).",
"MA.6": "the angular bumps of (A.11) leave ∫E²dy unchanged, so omitting them gives the same datum and (A.23) for the full profile."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 133-134",
"analogous_to": [],
"relations": {
"MA.4": "prerequisite",
"M4.5": "prerequisite",
"MA.6": "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": "MA.9",
"kind": "move",
"name": "ns-ma-9-stage-by-stage-cone-verification-and-the-large-x-r",
"title": "Stage-by-stage cone verification and the large-X_R scaling (Section A.5, completing Proposition A.4)",
"section": "A",
"pages": "134-137",
"refs": [
"pp. 134 to 137, (A.24) to (A.31)",
"Proposition A.4 pp. 130 to 131",
"Lemma 4.5 pp. 31 to 32."
],
"statement": "Section A.5, completing Proposition A.4 (pp. 134 to 137): with w = N_s/(E Q_s) where Q_s > 0, the sufficient test (A.24) of Lemma 4.5, a − b_s w > 0 and 2b_s w + b_s²/a + (a − 2)w² < 2, holds with uniform margins at each stage, while p_{s,1} = XQ_s/L grows with X_R. Reference (A.25): Q_s ≥ c > 0, b_s = 0, a = 4/5; axial reduction (A.26): |b_s w| ≤ C e_d, a = 2; intermediate (A.27): √λ|w| = o(1), a = 2 + 2λ; pulse (A.28) to (A.30): b_s w < .74, the quadratic < 1.68, v_s ≥ a > 2; then (A.31): |w| ≪ 1, b_s = 0, 2 < a ≤ 4. Where a ≤ 2 only the relaxed cone results.",
"description": "Section A.5, completing Proposition A.4 (pp. 134 to 137): with w = N_s/(E Q_s) where Q_s > 0, the sufficient test (A.24) of Lemma 4.5, a − b_s w > 0 and 2b_s w + b_s²/a + (a − 2)w² < 2, holds with uniform margins at each stage, while p_{s,1} = XQ_s/L grows with X_R. Reference (A.25): Q_s ≥ c > 0, b_s = 0, a = 4/5; axial reduction (A.26): |b_s w| ≤ C e_d, a = 2; intermediate (A.27): √λ|w| = o(1), a = 2 + 2λ; pulse (A.28) to (A.30): b_s w < .74, the quadratic < 1.68, v_s ≥ a > 2; then (A.31): |w| ≪ 1, b_s = 0, 2 < a ≤ 4. Where a ≤ 2 only the relaxed cone results. OBLIGATION: The cone assertions of Proposition A.4, which become Lemma 4.8(iii) (relaxed on [e^{-5} X_R, e^{1/2} X_tail], admissible on [X_good, e^{1/2} X_tail]); Proposition 7.5 needs the admissible cone to realize the stress with positive squared wave amplitudes. MECHANISM: Under (A.4) the shears a, b_s (logarithmic derivatives), the ratio w and Q_s are X_R-invariant, while p_{s,1} = X Q_s/L grows linearly in X_R; Lemma 4.5 then reduces the admissible cone at large p_{s,1} to (A.24) on a compact set of (a, b_s, w). REFS: pp. 134 to 137, (A.24) to (A.31); Proposition A.4 pp. 130 to 131; Lemma 4.5 pp. 31 to 32.",
"obligation": "The cone assertions of Proposition A.4, which become Lemma 4.8(iii) (relaxed on [e^{-5} X_R, e^{1/2} X_tail], admissible on [X_good, e^{1/2} X_tail]); Proposition 7.5 needs the admissible cone to realize the stress with positive squared wave amplitudes.",
"backward_question": "Along each stage of the outer profile, does the integrated inviscid stress p_s stay inside the admissible cone around the shear direction once the radial scale X_R is large, and which stages can only give the relaxed cone?",
"mechanism": "Under (A.4) the shears a, b_s (logarithmic derivatives), the ratio w and Q_s are X_R-invariant, while p_{s,1} = X Q_s/L grows linearly in X_R; Lemma 4.5 then reduces the admissible cone at large p_{s,1} to (A.24) on a compact set of (a, b_s, w). Each stage is handled by solving the linear equations (4.9) for Q_s, N_s explicitly or by (4.16): on the axial reduction the slow decay of k makes b_s w small (M_d large) and P∗ > e^{T_d} makes b_s^2 small; on the intermediate interval a = 2 + 2λ > 2 and (a - 2) w^2 = 2λ w^2 = o(1); on the pulse m = A_X(U)/E solves m' + βm = R_b with β = 1/2 - λ, and a two-term expansion of the exponential convolution (A.28) together with (A.29), (A.30) gives w ≈ 2R_b - C_d ∂_{ξ_b} R_b, so, with R_b ≥ 0 and ∂_{ξ_b} R_b ≤ 1.2, both cone quantities are bounded by explicit quadratics in R = R_b; after the pulse E is exponentially small in 1/λ, and after the steep interval it is further cut by h^6, while Q_s ≥ cλ or ch, so w is negligible. Where a ≤ 2 (the reference and the first transition), only the relaxed condition results.",
"antecedent": "None cited (variation of constants; Taylor's formula for the convolution remainder).",
"cost": "The orderings M_d large (e_d small), P∗ > e^{T_d}, h ≪ e^{-T_d} (used in (A.26)), h/λ → 0 (used for C_d ≤ 2 + o(1)), and one final increase of X_R. The admissible condition is not obtained where a ≤ 2; that gap is left to Appendix C.",
"checkable": "Verify (A.25) symbolically from (4.9) with U = 4η, E ∝ f x^{1/10} (so l = 3/5, W = -(4L - 1), Q_s = S_q/(1 + l)); check C_d → 2 at c_η = 0 as λ, h/λ → 0 and that C_d decreases in c_η. Digest-pass computation: sup_{R≥0}(-2R^2 + 2.41R) = 0.72601 < .74, sup_{R≥0}(-3.5R^2 + 4.82R) = 1.65946 < 1.68, and max ∂_ξ R_0 = 1.0, so ∂_{ξ_b} R_b ≤ 1.2 for Amp ≤ 1.2. A full check integrates (4.9) along the numerically built schedule and evaluates the gap map Ψ of (4.35) with p_{s,1} scaled by X_R.",
"depends_on": [
"M4.7",
"MA.4",
"M4.4",
"MA.7"
],
"constrains": [],
"reasons": {
"M4.7": "applies Lemma 4.5's sufficient test (A.24) on compact (a, b_s, w) ranges, then makes p_s,1 = XQ_s/L large through X_R.",
"MA.4": "checks each stage of the schedule: reference, axial reduction, intermediate power law, pulse, interpolation, exterior transition.",
"M4.4": "solves (4.9) for Q_s, N_s stage by stage and uses the shear a = 2 - 2l, b_s = 2D_XU/E of (4.11).",
"MA.7": "on the pulse, the small η-derivative (A.20) of the amplitude makes the ηm_η term negligible in N_s/E."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 134-137",
"analogous_to": [],
"relations": {
"M4.7": "prerequisite",
"MA.4": "prerequisite",
"M4.4": "prerequisite",
"MA.7": "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": "MA.10",
"kind": "move",
"name": "ns-ma-10-the-self-similar-swirl-heat-exterior-lemma-a-6",
"title": "The self-similar swirl heat exterior (Lemma A.6)",
"section": "A",
"pages": "137-138",
"refs": [
"pp. 137 to 138, (A.32) to (A.38)",
"used p. 33 (4.29), p. 35 (Lemma 4.8(iii)), p. 116 ((3.5)), p. 119 ((10.7), (10.8))."
],
"statement": "With a_K = 1 + h, the heat factor H(Z) = Γ(a_K)^{-1} ∫_0^∞ e^{-v} v^{a_K - 1} (1 + Zv)^{-h} dv, Z ≥ 0 (A.32), has H(0) = 1, is positive and smooth up to Z = 0 with every fixed derivative bounded on bounded intervals, and K(r, t) = c∞ s^{-A} H(2τ/s), s = r^2/2 (A.33), is independent of z, satisfies ∂_t K = (∂_rr + r^{-1}∂_r - r^{-2})K, and has K_r < 0; its profile E_pow(X) H(2d/X) is smooth with all η-derivatives continuous up to η = ±1.",
"description": "With a_K = 1 + h, the heat factor H(Z) = Γ(a_K)^{-1} ∫_0^∞ e^{-v} v^{a_K - 1} (1 + Zv)^{-h} dv, Z ≥ 0 (A.32), has H(0) = 1, is positive and smooth up to Z = 0 with every fixed derivative bounded on bounded intervals, and K(r, t) = c∞ s^{-A} H(2τ/s), s = r^2/2 (A.33), is independent of z, satisfies ∂_t K = (∂_rr + r^{-1}∂_r - r^{-2})K, and has K_r < 0; its profile E_pow(X) H(2d/X) is smooth with all η-derivatives continuous up to η = ±1. OBLIGATION: The exterior must have identically zero Navier-Stokes residual (so that T_0 = 0 there and no force is needed outside the annulus) and smooth limits of every derivative as t ↑ 1 at each fixed r > 0: Theorem 3.1(iii), formula (3.5), proved on p. 116 with (A.34), and Lemma 10.2, (10.7) and (10.8). The pure power law c∞ s^{-A} is not a steady swirl solution and leaves a viscous residual outside the annulus. ANTECEDENT: None cited. The proof names the gamma integral, dominated differentiation and the finite Taylor formula. REFS: pp. 137 to 138, (A.32) to (A.38); used p. 33 (4.29), p. 35 (Lemma 4.8(iii)), p. 116 ((3.5)), p. 119 ((10.7), (10.8)).",
"obligation": "The exterior must have identically zero Navier-Stokes residual (so that T_0 = 0 there and no force is needed outside the annulus) and smooth limits of every derivative as t ↑ 1 at each fixed r > 0: Theorem 3.1(iii), formula (3.5), proved on p. 116 with (A.34), and Lemma 10.2, (10.7) and (10.8). The pure power law c∞ s^{-A} is not a steady swirl solution and leaves a viscous residual outside the annulus.",
"backward_question": "Is there an exact, z-independent swirl heat solution that equals the power law c∞ s^{-A} at t = 1, is smooth in time up to t = 1 at every fixed r > 0, decreases in r, and matches the profile power law to O(X^{-1}) at large X?",
"mechanism": "Inserting the self-similar ansatz with Z = 2τ/s into the swirl heat equation gives ∂_t K = -2c∞ s^{-A-1} H' and (∂_rr + r^{-1}∂_r - r^{-2})K = 2c∞ s^{-A-1}[Z^2 H'' + (2A + 1) Z H' + (A^2 - 1/4) H], which reduces to (A.37) because 2A + 1 = 2a_K and A^2 - 1/4 = a_K(a_K - 1). The Laplace-type integral solves (A.37): integrating the total derivative h ∂_v[e^{-v} v^{a_K} (1 + Zv)^{-a_K}] produces the equation with vanishing boundary terms. H(0) = 1 means the flow arrives exactly at the prescribed power law at t = 1. Differentiation under the integral, with majorant e^{-v} v^{h+m} (since (1 + Zv)^{-h-m} ≤ 1), bounds all derivatives uniformly on Z ≥ 0, which is the source of the smooth one-sided limits at τ = 0. Writing -Z H'/H as an average of hZv/(1 + Zv) against a positive density gives the monotonicity. In profile variables Z = 2(1 - η^2)/X, so η-derivatives produce only polynomials in d' = -2η, d'' = -2 times H^{(k)}(2d/X)(2/X)^k, with no division by d. By (A.35) the Taylor coefficients (h)_m (1 + h)_m/m! grow factorially, so the Taylor series at Z = 0 diverges; the paper uses only finite Taylor formulas (\"no convergent Taylor series is needed\"), treats the heat factor as merely smooth in η, and keeps it out of the analytic axis datum (MA.8, MA.11).",
"antecedent": "None cited. The proof names the gamma integral, dominated differentiation and the finite Taylor formula.",
"cost": "h > 0 ties the exterior decay X^{-A}, A = 1/2 + h, to the heat solution; the exterior profile depends on η through d = 1 - η^2 and is smooth but not analytic at η = ±1; the replacement disturbs three moments that must be restored (MA.11).",
"checkable": "Evaluate H by quadrature and check (A.35), (A.36), (A.37), 0 ≤ -ZH'/H < h, and the swirl heat equation for K by finite differences. Digest-pass computation (mpmath, h = 0.005, 0.01, 0.2): (A.35) matches for m ≤ 3; the (A.37) residual is below 10^{-31} at Z = 10^{-3}, 0.1, 1, 10; -ZH'/H < h at all those points; (|H - 1| + |ZH'|)/(hZ) lies between 1.28 and 2.36 at Z = .01, .1, .5; the swirl heat residual of K is below 10^{-38} relative at four (r, t) points, with r K_r/(2K) in (-A, -1/2). An independent evaluation route, not stated in the manuscript and confirmed here to 12 digits: H(Z) = Z^{-1-h} U(1 + h, 2, 1/Z), with U the Tricomi confluent hypergeometric function.",
"depends_on": [
"MA.4",
"M4.1"
],
"constrains": [],
"reasons": {
"MA.4": "replaces the schedule's η-independent exterior power law E_pow = c∞X^{-A} by a heat solution that reaches the same power at t = 1.",
"M4.1": "in similarity variables Z = 2τ/s = 2d/X, so the physical swirl K is the profile E_pow(X)H(2d/X), smooth up to η = ±1."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 137-138",
"analogous_to": [],
"relations": {
"MA.4": "prerequisite",
"M4.1": "prerequisite"
},
"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": "correct"
}
},
{
"id": "MA.11",
"kind": "move",
"name": "ns-ma-11-heat-replacement-and-three-moment-compensation-on-the",
"title": "Heat replacement and three-moment compensation on the second patch (Proposition A.7)",
"section": "A",
"pages": "137",
"refs": [
"p. 137, pp. 139 to 140, (A.39) to (A.43)."
],
"statement": "With X_K = e^{.2} X_tail and a smooth step 0 ≤ χ_K(y) ≤ 1 equal to 0 for y ≤ .2 and 1 for y ≥ .5, the replacement E_cl ↦ E_cl[1 + χ_K(y)(H(2d/X) - 1)] (A.39) can be compensated by three additive E bumps on the second reserved patch; the complete edit preserves M, J, S(∞), C_p(∞) and ∫_0^∞ (H - H_pow) dX pointwise in η, and, for large X_R, preserves E > 0 and the strict admissible cone from the patch through y = .5; the axis datum Π_0 and the profile before the patch are unchanged.",
"description": "With X_K = e^{.2} X_tail and a smooth step 0 ≤ χ_K(y) ≤ 1 equal to 0 for y ≤ .2 and 1 for y ≥ .5, the replacement E_cl ↦ E_cl[1 + χ_K(y)(H(2d/X) - 1)] (A.39) can be compensated by three additive E bumps on the second reserved patch; the complete edit preserves M, J, S(∞), C_p(∞) and ∫_0^∞ (H - H_pow) dX pointwise in η, and, for large X_R, preserves E > 0 and the strict admissible cone from the patch through y = .5; the axis datum Π_0 and the profile before the patch are unchanged. OBLIGATION: Lemma 4.8(iii) (the heat exterior) together with parts (i) and (ii) (the unchanged datum and exact moments). Without compensation the heat factor would shift C_p(∞) (hence Π_0, destroying the analytic datum of Appendix B and the normalization (4.25)), S(∞) and the angular moment (reintroducing stress tails). MECHANISM: By (A.34) to (A.36), |(X∂_X)^j ∂_η^m (E - E_cl)| ≤ C e_K X_K^{-1} x^{-A-1} for x = X/X_K ≥ 1, bounded even at d = 0. Both edited regions have U = 0, so M and J are untouched; the other three discrepancies obey (A.40), (A.41), (A.42), the last using ∫_1^∞ x^{-A-1/2} dx = 1/h, finite because h is fixed. ANTECEDENT: None cited. REFS: p. 137, pp. 139 to 140, (A.39) to (A.43).",
"obligation": "Lemma 4.8(iii) (the heat exterior) together with parts (i) and (ii) (the unchanged datum and exact moments). Without compensation the heat factor would shift C_p(∞) (hence Π_0, destroying the analytic datum of Appendix B and the normalization (4.25)), S(∞) and the angular moment (reintroducing stress tails).",
"backward_question": "If I swap the power-law tail for the exact heat flow, which cumulative moments change, by how much in natural units, and can I restore them upstream without touching the axis pressure datum or the cone?",
"mechanism": "By (A.34) to (A.36), |(X∂_X)^j ∂_η^m (E - E_cl)| ≤ C e_K X_K^{-1} x^{-A-1} for x = X/X_K ≥ 1, bounded even at d = 0. Both edited regions have U = 0, so M and J are untouched; the other three discrepancies obey (A.40), (A.41), (A.42), the last using ∫_1^∞ x^{-A-1/2} dx = 1/h, finite because h is fixed before X_R. Normalized by (A.43) (e∗^2, X∗ e∗^2, X∗^{3/2} e∗) each is O_m(X_K^{-1}). On the patch E = e∗ f x∗^{-1/2-λ}, so the pressure, S and angular rows have weights f x∗^{-3/2-λ}, -f x∗^{-1/2-λ}, √2 x∗^{1/2}, with distinct exponents; Lemma A.1 gives an inverse uniform in η and Lemma A.2 gives ‖∂_η^m c‖_∞ ≤ C_m X_K^{-1} (the first two rows carry quadratic remainders, the last is linear). The normalized formulas (4.16) contain no X_R, so Q_s, N_s change by O(X_K^{-1}) at the cost of one η-derivative, and the cone margins of Proposition A.4 survive for large X_R. Zero net pressure change means forward integration from the unchanged Π_0 still gives pressure vanishing at infinity.",
"antecedent": "None cited.",
"cost": "A further largeness requirement on X_R. The compensation coefficients depend on η through the heat factor, which is only smooth in η; this is harmless because analyticity is required only on the axis rectangle [0, X_an] and Π_0 is unchanged.",
"checkable": "Compute the three discrepancies of (A.39) by quadrature for sample (h, X_K), divide by (A.43), solve the 3 × 3 system with weights f x∗^{-3/2-λ}, -f x∗^{-1/2-λ}, √2 x∗^{1/2} plus the quadratic terms, and confirm that c = O(X_K^{-1}) and that the totals C_p(∞), S(∞), ∫(H - H_pow) dX agree with the reference profile afterward.",
"depends_on": [
"MA.10",
"MA.3",
"MA.4",
"MA.9"
],
"constrains": [],
"reasons": {
"MA.10": "the heat-factor bounds (A.34) to (A.36) make the replacement's changes to Cp(∞), S(∞), and the angular moment O(X_K^{-1}).",
"MA.3": "three E bumps on a power-law patch with U = 0 reset (I, S, Cp) while preserving M and J, by Corollary A.3.",
"MA.4": "the compensation sits on the schedule's second reserved patch; the replacement acts on the tail beyond X_K = e^{.2}X_tail.",
"MA.9": "the stage cone margins of Proposition A.4 absorb the O(X_K^{-1}) changes in Q_s, N_s for large X_R."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 137",
"analogous_to": [],
"relations": {
"MA.10": "prerequisite",
"MA.3": "prerequisite",
"MA.4": "prerequisite",
"MA.9": "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": "MA.12",
"kind": "move",
"name": "ns-ma-12-zero-total-residual-integrals-and-the-backward-stress",
"title": "Zero total residual integrals and the backward stress formula (Lemma A.8)",
"section": "A",
"pages": "140-141",
"refs": [
"pp. 140 to 141, Lemma A.8, (A.44) to (A.46)",
"conservative forms p. 53",
"restated p. 36 (Lemma 4.9)."
],
"statement": "Suppose the leading axisymmetric field is smooth at the axis, has U = 0 and E = E_pow f_o[1 + χ_K(H(2d/X) - 1)] for y ≥ 0, and satisfies M(∞) = J(∞) = S(∞) = 0, ∫_0^∞ (H - H_pow) dX = 0 and Π(X) = -(1/2) ∫_X^∞ E(x)^2/x dx. Then ∫_0^∞ r^2 R^{(0)}_θ dr = ∫_0^∞ r R^{(0)}_z dr = 0, the stress is given by the backward integrals T_θ(r) = r^{-2} ∫_r^∞ r'^2 R^{(0)}_θ(r') dr', T_z(r) = r^{-1} ∫_r^∞ r' R^{(0)}_z(r') dr' (A.46), and it vanishes for X ≥ X_b. Restated as Lemma 4.9.",
"description": "Suppose the leading axisymmetric field is smooth at the axis, has U = 0 and E = E_pow f_o[1 + χ_K(H(2d/X) - 1)] for y ≥ 0, and satisfies M(∞) = J(∞) = S(∞) = 0, ∫_0^∞ (H - H_pow) dX = 0 and Π(X) = -(1/2) ∫_X^∞ E(x)^2/x dx. Then ∫_0^∞ r^2 R^{(0)}_θ dr = ∫_0^∞ r R^{(0)}_z dr = 0, the stress is given by the backward integrals T_θ(r) = r^{-2} ∫_r^∞ r'^2 R^{(0)}_θ(r') dr', T_z(r) = r^{-1} ∫_r^∞ r' R^{(0)}_z(r') dr' (A.46), and it vanishes for X ≥ X_b. Restated as Lemma 4.9. OBLIGATION: Theorem 4.6(ii): T_0 = 0 for X ≥ X_b. The stress is defined by integration from the axis (Proposition 4.2), so a zero exterior residual alone would still leave stresses proportional to r^{-2} (angular) and r^{-1} (axial) whenever the total weighted residual integrals are nonzero (p. 30). MECHANISM: Integrate the conservative forms of the leading tangential residuals (those displayed in Lemma 5.2, Step 4, without the axial viscosity terms) over 0 < r < ∞. By p. ANTECEDENT: None cited (integration of conservation forms; Fubini). REFS: pp. 140 to 141, Lemma A.8, (A.44) to (A.46); conservative forms p. 53; restated p. 36 (Lemma 4.9).",
"obligation": "Theorem 4.6(ii): T_0 = 0 for X ≥ X_b. The stress is defined by integration from the axis (Proposition 4.2), so a zero exterior residual alone would still leave stresses proportional to r^{-2} (angular) and r^{-1} (axial) whenever the total weighted residual integrals are nonzero (p. 30).",
"backward_question": "Once the exterior residual is zero, why should a stress defined by integrating from the axis vanish there, and which conserved totals must vanish to exclude r^{-2} and r^{-1} tails?",
"mechanism": "Integrate the conservative forms of the leading tangential residuals (those displayed in Lemma 5.2, Step 4, without the axial viscosity terms) over 0 < r < ∞. By p. 30, M, J, S are the radially integrated axial momentum, the axial transport of angular momentum, and the axial momentum flux including pressure. The time and axial derivatives fall on q^{3/2-A} ∫(H - H_pow) dX (A.45), q^{3/2-2A} J(∞), q^{1-A} M(∞) and q^{1-2A} S(∞), the last via ∫_0^∞ r p dr = -(1/2) ∫_0^∞ r' u_θ^2 dr' (Fubini), and all vanish by hypothesis. The radial boundary terms vanish by axis regularity and the exterior decay (A.44), K - K_pow = O_h(τ r^{-3-2h}), ∂_t K = O_h(r^{-3-2h}), r^2 K_r - rK = O_h(r^{-2h}): the viscous flux [r^2 ∂_r u_θ - r u_θ] tends to zero at infinity and the subtracted angular moment converges (majorant r^{-1-2h}) precisely because h > 0; the axial pressure moment converges since p = O(r^{-2-4h}). So forward and backward primitives coincide, and beyond X_b the field (0, K, 0) with centrifugal pressure has zero residual by Lemma A.6, giving T = 0 there. Once the regular axis and the moments are supplied, the stress depends only on the exterior profile.",
"antecedent": "None cited (integration of conservation forms; Fubini).",
"cost": "It is conditional on a regular axis and exact moment identities, which the outer profile alone cannot supply because the reference branch (A.7) is not regular; they come from Proposition B.2 and Corollary B.10 (with Proposition B.8). It also needs h > 0.",
"checkable": "For a sample profile satisfying the hypotheses, compute R^{(0)}_θ and R^{(0)}_z (on the terminal collar they are (A.52) and p_z of (A.53)) and check numerically that the forward and backward formulas in (A.46) agree; check the scalings (A.44) from (A.36) and the tail integral ∫_{R∗}^∞ r^{-1-2h} dr = R∗^{-2h}/(2h).",
"depends_on": [
"M4.4",
"M4.5",
"MA.11",
"MA.10"
],
"constrains": [],
"reasons": {
"M4.4": "the stress is Proposition 4.2's forward primitive from the axis; the lemma shows it equals the backward primitive (A.46).",
"M4.5": "the derivatives of the weighted residual integrals fall on M, J, S and the renormalized I, which vanish by hypothesis.",
"MA.11": "its hypothesis profile E = E_pow f_o[1 + χ_K(H(2d/X) - 1)] for y ≥ 0 is the heat-replaced terminal profile of Proposition A.7.",
"MA.10": "beyond X_b the field (0, K, 0) of Lemma A.6 has zero residual, and its heat-factor bounds give the decay (A.44) at infinity."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 140-141",
"analogous_to": [],
"relations": {
"M4.4": "prerequisite",
"M4.5": "prerequisite",
"MA.11": "prerequisite",
"MA.10": "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": "MA.13",
"kind": "move",
"name": "ns-ma-13-factoring-a-flat-edge-weight-out-of-a-backward-integral",
"title": "Factoring a flat edge weight out of a backward integral (Lemma A.9)",
"section": "A",
"pages": "141-142",
"refs": [
"pp. 141 to 142, Lemma A.9, (A.47)",
"used p. 54 ((5.22)), p. 143, p. 152."
],
"statement": "For c > 0, a fixed integer j ≥ 0 and smooth b(u, η) on [0, δ_0] × K, ∫_0^δ e^{-c/u^2} u^{-j} b(u, η) du = (1/2) e^{-c/δ^2} δ^{3-j} B(δ, η) (A.47), with B smooth on [0, δ_0] × K, B(0, η) = b(0, η)/c, and bounded mixed derivatives of every fixed order; the same holds with any finite set of smooth compact parameters.",
"description": "For c > 0, a fixed integer j ≥ 0 and smooth b(u, η) on [0, δ_0] × K, ∫_0^δ e^{-c/u^2} u^{-j} b(u, η) du = (1/2) e^{-c/δ^2} δ^{3-j} B(δ, η) (A.47), with B smooth on [0, δ_0] × K, B(0, η) = b(0, η)/c, and bounded mixed derivatives of every fixed order; the same holds with any finite set of smooth compact parameters. OBLIGATION: The stress vanishes to infinite order at both edges, so its direction and the weighted bounds (4.27) require factoring out the flat weight with a smooth nonvanishing remainder. Used at the outer edge (Proposition A.10, c = 4, j = 3 and j = 0), at the inner collar (p. 152, c = t_1^2, j = 0) and for the order-one outer term (5.22) in Lemma 5.2 (c = 4, j = 3, 6). MECHANISM: The substitution u = δ/(1 + δ^2 v)^{1/2} maps (0, δ] onto v ∈ [0, ∞), turns c/u^2 into c/δ^2 + cv, and has Jacobian -(1/2) δ^3 (1 + δ^2 v)^{-3/2}, so B(δ, η) = ∫_0^∞ e^{-cv} (1 + δ^2 v)^{(j-3)/2} b(δ/(1 + δ^2 v)^{1/2}, η) dv, a Laplace-type integral whose derivatives are dominated by e^{-cv} times polynomials in v. ANTECEDENT: None cited (change of variables and dominated differentiation). REFS: pp. 141 to 142, Lemma A.9, (A.47); used p. 54 ((5.22)), p. 143, p. 152.",
"obligation": "The stress vanishes to infinite order at both edges, so its direction and the weighted bounds (4.27) require factoring out the flat weight with a smooth nonvanishing remainder. Used at the outer edge (Proposition A.10, c = 4, j = 3 and j = 0), at the inner collar (p. 152, c = t_1^2, j = 0) and for the order-one outer term (5.22) in Lemma 5.2 (c = 4, j = 3, 6).",
"backward_question": "The stress and its sources vanish to infinite order at the outer edge; how can the relative rates of the two stress components, and hence the limiting direction, still be computed?",
"mechanism": "The substitution u = δ/(1 + δ^2 v)^{1/2} maps (0, δ] onto v ∈ [0, ∞), turns c/u^2 into c/δ^2 + cv, and has Jacobian -(1/2) δ^3 (1 + δ^2 v)^{-3/2}, so B(δ, η) = ∫_0^∞ e^{-cv} (1 + δ^2 v)^{(j-3)/2} b(δ/(1 + δ^2 v)^{1/2}, η) dv, a Laplace-type integral whose derivatives are dominated by e^{-cv} times polynomials in v. Integrating a flat factor from the edge thus returns the same flat factor with three more powers of δ.",
"antecedent": "None cited (change of variables and dominated differentiation).",
"cost": "None beyond smoothness of b.",
"checkable": "Digest-pass computation: (A.47) with b(u) = 1 + 3u + sin^2 u, c = 4, j ∈ {0, 3, 6}, δ ∈ {.05, .2} agrees to 50 digits when the left side is integrated in the variable w = c/u^2 - c/δ^2 (plain quadrature in u loses accuracy for δ ≤ .2 because the integrand is concentrated at u = δ), and B(δ) → b(0)/c as δ → 0.",
"depends_on": [],
"constrains": [],
"reasons": {},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 141-142",
"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.14",
"kind": "move",
"name": "ns-ma-14-outer-edge-stress-factorization-and-limiting-direction",
"title": "Outer-edge stress factorization and limiting direction (Proposition A.10)",
"section": "A",
"pages": "142-144",
"refs": [
"pp. 142 to 144, Proposition A.10, (A.48) to (A.56)",
"restated p. 36 ((4.32))",
"used p. 44, pp. 163 to 164."
],
"statement": "Proposition A.10 (pp. 142 to 144): under the hypotheses of Lemma A.8, the terminal profile satisfies the admissible cone on .5 ≤ y < 3; its stress direction extends smoothly to the outer endpoint and 2 − (a − 2)(T_z/T_θ)² has a uniform positive lower bound; for δ = 3 − y small, T_{0,θ} = e^{−4/δ²} δ^{−3} b_θ(δ, η), b_θ(0, η) > 0 (A.48), T_{0,z} = e^{−4/δ²} δ³ b_z(δ, η) (A.49), T_{0,z}/T_{0,θ} = δ^6 b_z/b_θ → 0 (A.50), and |∂^I T_0| ≤ C_I e^{−4/δ²} δ^{−N_I}, |T_0| ≥ c e^{−4/δ²} δ^{−3} (A.51), constants independent of q.",
"description": "Proposition A.10 (pp. 142 to 144): under the hypotheses of Lemma A.8, the terminal profile satisfies the admissible cone on .5 ≤ y < 3; its stress direction extends smoothly to the outer endpoint and 2 − (a − 2)(T_z/T_θ)² has a uniform positive lower bound; for δ = 3 − y small, T_{0,θ} = e^{−4/δ²} δ^{−3} b_θ(δ, η), b_θ(0, η) > 0 (A.48), T_{0,z} = e^{−4/δ²} δ³ b_z(δ, η) (A.49), T_{0,z}/T_{0,θ} = δ^6 b_z/b_θ → 0 (A.50), and |∂^I T_0| ≤ C_I e^{−4/δ²} δ^{−N_I}, |T_0| ≥ c e^{−4/δ²} δ^{−3} (A.51), constants independent of q. OBLIGATION: Theorem 4.6(iii) at X = X_b (n(X_b, η) = (1, 0), b_s(X_b, η) = 0, strict margin κ in (4.26)) and the outer half of Theorem 4.6(iv) (the factor e^{-4/y_b^2} in ζ, finalized as (C.18), and the bounds (4.27)). The wave construction needs a smooth stress direction strictly inside the cone up to the edge where the stress itself tends to zero (p. 32). MECHANISM: On y ≥ 1/2 one has u_θ = K f with f = f_o(y) and u_r = u_z = 0. Since K solves the swirl heat equation, the residual (A.52) R^{(0)}_θ = K f'/(qL) - K(f_rr + r^{-1} f_r) - 2 K_r f_r and the. REFS: pp. 142 to 144, Proposition A.10, (A.48) to (A.56); restated p. 36 ((4.32)); used p. 44, pp. 163 to 164.",
"obligation": "Theorem 4.6(iii) at X = X_b (n(X_b, η) = (1, 0), b_s(X_b, η) = 0, strict margin κ in (4.26)) and the outer half of Theorem 4.6(iv) (the factor e^{-4/y_b^2} in ζ, finalized as (C.18), and the bounds (4.27)). The wave construction needs a smooth stress direction strictly inside the cone up to the edge where the stress itself tends to zero (p. 32).",
"backward_question": "At the outer edge, where the stress vanishes to infinite order, what is its limiting direction, and can the terminal amplitude factor be designed so that this direction sits strictly inside the admissible cone with a positive angular component?",
"mechanism": "On y ≥ 1/2 one has u_θ = K f with f = f_o(y) and u_r = u_z = 0. Since K solves the swirl heat equation, the residual (A.52) R^{(0)}_θ = K f'/(qL) - K(f_rr + r^{-1} f_r) - 2 K_r f_r and the axial pressure gradient (A.53) come only from derivatives of f, whose argument depends on (z, t) through q (y_t = (qL)^{-1}, y_z = -2η/(q^D L)). Integrating the viscous terms by parts in (A.46) gives (A.54), a sum of three nonnegative terms because K > 0, K_r < 0, f' ≥ 0; the last yields T_θ ≥ c r K ρ_o ψ_o(y)/(qL) > 0. The axial stress comes from the pressure, quadratic in the small amplitude, so |T_z/T_θ| ≤ C q^{1-D} K = C E_pow H(2d/X) (A.55), small by the h^6 reduction; with b_s = 0 and 2 + h < a ≤ 2 + 2h (A.56), the cone reduces to (a - 2)(T_z/T_θ)^2 < 2 with fixed slack. At the endpoint ψ_o = e^{-4/δ^2} g(δ), g(δ) = 1/(e^{-(1-δ/2)^{-2}} + e^{-4/δ^2}), g(0) = e, so f' = ρ_o e^{-4/δ^2} δ^{-3}[8g(δ) + δ^3 g'(δ)]. The boundary term of (A.54), rescaled as q^{A+1/2} K f_r = 2 E_pow(X) H(2d/X) f'/√(2X), has exactly the rate e^{-4/δ^2} δ^{-3} with b_θ(0, η) = 16 ρ_o E_pow(X_b) H(2d/X_b) g(0)/√(2X_b) > 0; the two integral terms gain δ^3 by Lemma A.9 (c = 4, j = 3). For the axial component, p_z is itself an integral of K^2 f f', which the same identity turns into e^{-4/δ^2} times a smooth coefficient, and the backward integral for T_z (Lemma A.9 with j = 0) then gives e^{-4/δ^2} δ^3; the powers of q cancel as q^{A+1/2} q^{1/2-D-2A} = q^{1-D-A} = 1. The limiting direction (1, 0) is the cone axis when b_s = 0, where the normalized quadratic expression equals 2.",
"antecedent": "None cited.",
"cost": "Requires c_o small (f_o'/f_o < h/4), X_R large (-ZH'/H < h/4 on the collar), h small, and a positive minimum of H on [0, 2/X_b]. It fixes the exponent 4 in the outer factor of the weight ζ = exp(-t_1^2/y_a^2 - 4/y_b^2) of (C.18).",
"checkable": "Digest-pass computation: ψ_o(3 - δ) = e^{-4/δ^2} g(δ) and -∂_y ψ_o = e^{-4/δ^2} δ^{-3}[8g + δ^3 g'] agree to 15 digits at δ = .3, .6, and g(δ) → e. A fuller check evaluates T_θ from (A.54) and T_z from (A.53) and (A.46) for sample (h, c_o, X_R, q) and fits the rates δ^{-3} and δ^3 after dividing by e^{-4/δ^2}, comparing the leading coefficient with 16 ρ_o E_pow(X_b) H(2d/X_b) e/√(2X_b) and checking that the ratio is independent of q.",
"depends_on": [
"MA.12",
"MA.13",
"MA.10",
"MA.4"
],
"constrains": [],
"reasons": {
"MA.12": "evaluates on the terminal collar the backward stress integrals (A.46) that Lemma A.8 makes valid.",
"MA.13": "Lemma A.9 with c = 4 and j = 3, 0 factors e^{-4/δ²} out of the integral terms, giving the rates δ^{-3} and δ³.",
"MA.10": "K solves the swirl heat equation, so the residual comes only from derivatives of f_o; K > 0 and K_r < 0 make the angular stress positive.",
"MA.4": "the terminal factor f_o = 1 - ρ_o ψ_o of (A.12), with 0 ≤ f_o'/f_o < h/4, fixes the flat rate e^{-4/δ²} at the endpoint."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 142-144",
"analogous_to": [],
"relations": {
"MA.12": "prerequisite",
"MA.13": "prerequisite",
"MA.10": "prerequisite",
"MA.4": "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": "MB.1",
"kind": "move",
"name": "ns-mb-1-symmetry-breaking-axis-velocity-and-the-two-region-split",
"title": "Symmetry-breaking axis velocity and the two-region split of the parameter interval",
"section": "B",
"pages": "144",
"refs": [
"p. 144, (B.1), (B.2)",
"Lemma A.5, (A.21) to (A.22), p. 133",
"Proposition 4.10 proof, p. 37",
"Section 2.1, pp. 3 to 5",
"p. 8."
],
"statement": "With Π0 from Lemma A.5 (real analytic near [−1, 1], even, Π0 ≤ −cP∗²f², ηΠ0η > 0 for η ≠ 0, f = (1 + η²)^{−1}) and h ≤ 10^{−2} fixed, choose 0 < j0 ≤ .05 and set U∗ = 4η + j0, H∗ = Dη + dU∗, W∗ = 1 − dU∗η − 2DηU∗, Z∗ = −A(1 − 2ηU∗)U∗ − H∗U∗η − dΠ0η + 4AηΠ0 (B.1). Then H∗ has exactly one zero η0 ∈ (−1, 0), |η0| ≍ j0; −W∗ > 2.8; Z∗(η0) ≥ cj0P∗² > 0. So on a compact I ⊃ [−1, 1] choose δ∗ > 0 with {|Z∗| ≤ δ∗} avoiding a neighborhood of η0, then σ∗ > 0 with χ = H∗²/(H∗² + σ∗²) > .99 wherever |Z∗| ≤ δ∗ (B.2): every η has χ > .99 or |Z∗| > δ∗.",
"description": "With Π0 from Lemma A.5 (real analytic near [−1, 1], even, Π0 ≤ −cP∗²f², ηΠ0η > 0 for η ≠ 0, f = (1 + η²)^{−1}) and h ≤ 10^{−2} fixed, choose 0 < j0 ≤ .05 and set U∗ = 4η + j0, H∗ = Dη + dU∗, W∗ = 1 − dU∗η − 2DηU∗, Z∗ = −A(1 − 2ηU∗)U∗ − H∗U∗η − dΠ0η + 4AηΠ0 (B.1). Then H∗ has exactly one zero η0 ∈ (−1, 0), |η0| ≍ j0; −W∗ > 2.8; Z∗(η0) ≥ cj0P∗² > 0. So on a compact I ⊃ [−1, 1] choose δ∗ > 0 with {|Z∗| ≤ δ∗} avoiding a neighborhood of η0, then σ∗ > 0 with χ = H∗²/(H∗² + σ∗²) > .99 wherever |Z∗| ≤ δ∗ (B.2): every η has χ > .99 or |Z∗| > δ∗. OBLIGATION: The inner-edge inequality (B.19), which is vs > 2 + cex at X0 = 4/Λ (the viscous part of the admissible stress cone at the edge where the stress is born parallel to the shear; Proposition 4.10(ii), Theorem 4.6(iii)), must hold for every η. H∗ is the axis value of the coefficient Hc of the η-derivative in the transport terms, so the rotational mechanism dies at its zero; Z∗ is the axis value of the axial source Sn (so ns ≈ Z∗/L), so the axial-shear mechanism dies at its zeros. REFS: p. 144, (B.1), (B.2); Lemma A.5, (A.21) to (A.22), p. 133; Proposition 4.10 proof, p. 37; Section 2.1, pp. 3 to 5; p. 8.",
"obligation": "The inner-edge inequality (B.19), which is vs > 2 + cex at X0 = 4/Λ (the viscous part of the admissible stress cone at the edge where the stress is born parallel to the shear; Proposition 4.10(ii), Theorem 4.6(iii)), must hold for every η. H∗ is the axis value of the coefficient Hc of the η-derivative in the transport terms, so the rotational mechanism dies at its zero; Z∗ is the axis value of the axial source Sn (so ns ≈ Z∗/L), so the axial-shear mechanism dies at its zeros. With j0 = 0 both vanish at η = 0 (U∗(0) = 0, H∗(0) = 0, and Π0η(0) = 0 by evenness), leaving the midplane uncovered; this is the upward-biased, mildly asymmetric axial profile motivated physically in Section 2.1. The constant −W∗ > 2.8 also supplies the order-one part of the angular source in (B.17), and the nonzero axis datum U∗ gives the axial velocity lower bound ‖uz(0)‖ ≍ τ^{−1/2−h} on the core (page 8).",
"backward_question": "At which values of η does each available amplification mechanism (axial transport of angular momentum versus radial shear of axial velocity) degenerate, and can a single small symmetry-breaking parameter keep those degeneracy sets disjoint?",
"mechanism": "H∗/d = Dη/d + 4η + j0 increases strictly from −∞ to +∞ on (−1, 1) and equals j0 > 0 at η = 0, so its zero η0 is unique, negative, and about −j0/(D + 4). At η0 the H∗U∗η term of Z∗ drops out, 4Aη0Π0(η0) is positive (η0 < 0 and Π0 < 0) and at least cj0P∗², −dΠ0η(η0) ≥ 0 by the sign of ηΠ0η, and the remaining terms are O(j0), which the already large P∗ absorbs. So the zero set of Z∗ is separated from η0; δ∗ quantifies the separation, and σ∗ is then chosen so small that away from a neighborhood of η0 the regularized indicator χ of H∗ ≠ 0 exceeds .99. Every η then lies either in {χ > .99}, where the rotational branch of (B.19) will work, or in {|Z∗| > δ∗}, where the axial-shear branch will work. The formula for −W∗ is direct algebra from W∗ = 1 − 4d − 2Dη(4η + j0) with D = 1/2 − h.",
"antecedent": "None cited. The physical motivation is Section 2.1 (pages 3 to 5).",
"cost": "Parameters j0, δ∗, σ∗, the enlarged interval I and the complex domain Ω; the order j0 → δ∗, σ∗ → Λ in (B.40); dependence on the sign and size properties of the outer datum Π0 and on P∗ being already large. The offset also enters the final axial matching error (‖Gi − 4η‖ contains a Ckj0 term in the proof of Proposition 4.10), so j0 ≪ εm in the hierarchy of section 4.6.",
"checkable": "With the actual Π0 of (A.21) (or, as a smoke test, the reference inner contribution −(5/2)P∗²f², which has the same parity and sign properties), tabulate H∗, W∗, Z∗ on I for fixed h and several j0 ≤ .05; root-find η0 and compare with −j0/(D + 4); confirm min(−W∗) > 2.8 (digest check: at h = .01, j0 = .05 the minimum over [−1, 1] is 2.871 and η0 = −0.01114); confirm Z∗(η0) > 0; then compute the largest admissible δ∗ and the largest σ∗ giving χ > .99 on {|Z∗| ≤ δ∗}.",
"depends_on": [
"MA.8",
"M4.4"
],
"constrains": [],
"reasons": {
"MA.8": "the sign of Z*(η0) comes from Lemma A.5's datum: analytic, even, Π0 ≤ -(5/2)P*²f², and ηΠ0' > 0.",
"M4.4": "H*, W*, Z* are the axis values of the transport coefficient H_c, the factor W, and the axial source S_n of (4.8), (4.9)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 144",
"analogous_to": [],
"relations": {
"MA.8": "prerequisite",
"M4.4": "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": "MB.2",
"kind": "move",
"name": "ns-mb-2-steep-holomorphic-swirl-datum-on-the-axis",
"title": "Steep, holomorphic swirl datum on the axis",
"section": "B",
"pages": "144-145",
"refs": [
"pp. 144 to 145, (B.3)",
"p. 147, (B.16)",
"p. 37 (proof of Proposition 4.10)",
"(4.9), p. 26."
],
"statement": "For Λ ≥ 1 define ζ∗ = −LH∗/(H∗² + σ∗²), ξ0 = Λζ∗, ϕ∗ = exp(Λ ∫0^η ζ∗(w) dw) (B.3). The integral is well defined on Ω, ϕ∗ > 0 on the real interval, and ϕ(0, η) = ϕ∗. Consequently ∂η log ϕ∗ = ξ0 and −H∗ξ0 = ΛLχ exactly (the manuscript writes H∗ξ0/(ΛL) = −χ). The amplitude C is chosen after Λ.",
"description": "For Λ ≥ 1 define ζ∗ = −LH∗/(H∗² + σ∗²), ξ0 = Λζ∗, ϕ∗ = exp(Λ ∫0^η ζ∗(w) dw) (B.3). The integral is well defined on Ω, ϕ∗ > 0 on the real interval, and ϕ(0, η) = ϕ∗. Consequently ∂η log ϕ∗ = ξ0 and −H∗ξ0 = ΛLχ exactly (the manuscript writes H∗ξ0/(ΛL) = −χ). The amplitude C is chosen after Λ. OBLIGATION: Makes the angular source Sq = −Wl − h(1 − 2ηU) − Hc(log E)η of (4.9) large and positive where H∗ is not small. This gives p1 = a > 0 on the stress-free region, the bound (B.17), and the rotational branch of (B.19), while keeping ϕ > 0 and analytic in η, as Theorem 4.6(i) and Lemma 5.1 require. It is the axis value ϕ(0, η) specified in the proof of Proposition 4.10, and its Λ fixes the radial scale Y = ΛX and hence Xa = 4/Λ. MECHANISM: The term −Hc(log E)η in Sq is axial transport of angular momentum between η-layers. Prescribing (log ϕ)η ≈ −ΛL/H∗ would make it ≈ ΛL, a large positive source. The regularization H∗/(H∗² + σ∗²) in place of 1/H∗ keeps ϕ∗ holomorphic across the zero of H∗, at the price that the large source becomes ΛLχ and switches off near η0, which is. ANTECEDENT: None cited. REFS: pp. 144 to 145, (B.3); p. 147, (B.16); p. 37 (proof of Proposition 4.10); (4.9), p. 26.",
"obligation": "Makes the angular source Sq = −Wl − h(1 − 2ηU) − Hc(log E)η of (4.9) large and positive where H∗ is not small. This gives p1 = a > 0 on the stress-free region, the bound (B.17), and the rotational branch of (B.19), while keeping ϕ > 0 and analytic in η, as Theorem 4.6(i) and Lemma 5.1 require. It is the axis value ϕ(0, η) specified in the proof of Proposition 4.10, and its Λ fixes the radial scale Y = ΛX and hence Xa = 4/Λ.",
"backward_question": "Can the sign of the angular-momentum source be forced by prescribing the η-dependence of the swirl on the axis alone, and how can the natural prescription (log ϕ)η ∝ −1/H∗, singular where H∗ vanishes, be made holomorphic without losing positivity?",
"mechanism": "The term −Hc(log E)η in Sq is axial transport of angular momentum between η-layers. Prescribing (log ϕ)η ≈ −ΛL/H∗ would make it ≈ ΛL, a large positive source. The regularization H∗/(H∗² + σ∗²) in place of 1/H∗ keeps ϕ∗ holomorphic across the zero of H∗, at the price that the large source becomes ΛLχ and switches off near η0, which is exactly where the axial branch of MB.1 takes over. Physically, the swirl amplitude decreases in the direction of the axial characteristic speed H∗, so axial flow carries fluid from more rapidly rotating layers (Section 2.1). Because the leading source is proportional to Λ, balancing it against radial diffusion forces the radial scale X ~ 1/Λ, which is why the axis problem is posed in Y = ΛX.",
"antecedent": "None cited.",
"cost": "The large parameter Λ (Λ ≥ Λ0, chosen after σ∗). The manuscript notes that ϕ∗ can grow exponentially with Λ, which forces the amplitude condition C ≥ sup over Ω of |ϕ∗| in (B.16) and hence the Λ-dependent threshold C0(Λ). The stress-free region shrinks to X ≤ 4.1/Λ, X-derivative bounds carry factors Λ^{r−1}, and the O(Λ) slope of log ϕ∗ inflates ℓi = log(CE(Xi, ·)), which is why Tsh in (B.33) depends on Λ through Bk.",
"checkable": "Compute ζ∗ and ϕ∗ by quadrature on I for given j0, σ∗, Λ; verify the identity −H∗ξ0 = ΛLχ to rounding error; evaluate |ϕ∗| on a complex strip around I to size the threshold C0(Λ) ≥ sup|ϕ∗| and observe its growth in Λ.",
"depends_on": [
"MB.1",
"M4.4"
],
"constrains": [],
"reasons": {
"MB.1": "uses H* and the regularization σ* chosen there, so χ = H*²/(H*² + σ*²) > .99 where |Z*| ≤ δ*, on the complex domain Ω.",
"M4.4": "the datum targets the term -H_c(log E)_η of the angular source S_q in (4.9), making it ≈ ΛLχ on the axis."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 144-145",
"analogous_to": [],
"relations": {
"MB.1": "prerequisite",
"M4.4": "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": "MB.3",
"kind": "move",
"name": "ns-mb-3-weighted-analytic-coefficient-space-b-and-the-radial",
"title": "Weighted analytic coefficient space Bρ and the radial inverses (Lemma B.1)",
"section": "B",
"pages": "145-146",
"refs": [
"pp. 145 to 146, (B.4) to (B.10), Lemma B.1."
],
"statement": "In Y = ΛX, for F = Σα Fα(η)Y^α let aαβ = 20^{−α}ρ^{−β}β! C(α + β, β)/((α + 1)²(β + 1)²) and ‖F‖ρ = sup over α, β ≥ 0, η ∈ I of |∂η^β Fα(η)|/aαβ (B.4); Bρ is complete. Lemma B.1: multiplication is bounded on Bρ; for ν = 1, 2 the inverse Jν of YGYY + νGY = F regular at 0 with G(0) = 0, (JνF)α+1 = Fα/((α + 1)(α + ν)) (B.5), is bounded, as are AX(F) = Y^{−1}IF, multiplication by Y, IF = ∫0^Y F dY' and ∂ηI; and ‖Jν[(∂ηF)(DXG)]‖ρ ≤ Cρ‖F‖ρ‖G‖ρ (B.6), also with either derivative omitted, with AX(F) for F, or with extra undifferentiated factors.",
"description": "In Y = ΛX, for F = Σα Fα(η)Y^α let aαβ = 20^{−α}ρ^{−β}β! C(α + β, β)/((α + 1)²(β + 1)²) and ‖F‖ρ = sup over α, β ≥ 0, η ∈ I of |∂η^β Fα(η)|/aαβ (B.4); Bρ is complete. Lemma B.1: multiplication is bounded on Bρ; for ν = 1, 2 the inverse Jν of YGYY + νGY = F regular at 0 with G(0) = 0, (JνF)α+1 = Fα/((α + 1)(α + ν)) (B.5), is bounded, as are AX(F) = Y^{−1}IF, multiplication by Y, IF = ∫0^Y F dY' and ∂ηI; and ‖Jν[(∂ηF)(DXG)]‖ρ ≤ Cρ‖F‖ρ‖G‖ρ (B.6), also with either derivative omitted, with AX(F) for F, or with extra undifferentiated factors. OBLIGATION: The stress-free equations (4.13) have a regular singular point at X = 0 and contain first-order η-derivatives (Hc∂η in the transport, ∂ηAX(U) inside W, η-derivatives of the pressure). An iteration in functions of Y alone loses one η-derivative per step. REFS: pp. 145 to 146, (B.4) to (B.10), Lemma B.1.",
"obligation": "The stress-free equations (4.13) have a regular singular point at X = 0 and contain first-order η-derivatives (Hc∂η in the transport, ∂ηAX(U) inside W, η-derivatives of the pressure). An iteration in functions of Y alone loses one η-derivative per step. Without a space in which \"increasing the radial degree compensates for a parameter derivative\" (Section B.2, p. 145), the contraction for Proposition B.2 does not close, and neither analyticity in η nor regularity at the axis (a power series in X = r²/(2q)) would come out.",
"backward_question": "In which Banach space does inverting the regular singular radial operator gain exactly the one η-derivative that the transport terms cost, so that a fixed-point iteration closes without shrinking the domain?",
"mechanism": "The factor ρ^{−β}β! measures analyticity in η with radius about ρ, the factor 20^{−α} measures analyticity in Y with radius 20, and the binomial C(α + β, β) ties them: by (B.10), moving one unit from radial degree to η-derivative count costs (80/ρ)(i + 1), and the divisor i + 1 produced by one radial integration (or the divisor (α + 1)(α + ν) of Jν) pays for it. The quadratic denominators make Bρ a Banach algebra: in the Leibniz formula the derivative binomials cancel the factorials of the weights, (B.8) (a count of β-element subsets of a set split into two blocks) bounds the remaining binomial ratio by one, and (B.7), proved by splitting the sum at N/2, bounds the convolution of the (α + 1)^{−2} weights. In a mixed product (∂ηF)(DXG), the extra radial degree supplied by Jν is assigned to the factor carrying the η-derivative, while DX = Y∂Y multiplies a coefficient by its degree, which the (α + ν) divisor absorbs.",
"antecedent": "Named ingredients only: the Leibniz formula, an elementary convolution estimate (B.7), and completeness via uniform convergence of coefficients and derivatives. No classical theorem is cited. (Digest's identification, not the manuscript's: a majorant-series norm of Cauchy-Kovalevskaya type adapted to a regular singular, Fuchsian-type, radial operator.)",
"cost": "A fixed small η-radius ρ, later taken strictly below the distance from the working neighborhood to the boundary of Ω so that Cauchy's inequality absorbs the (β + 1)² factor; the fixed Y-radius 20, which must exceed 4.1; algebra constants Csq² and Cρ.",
"checkable": "Exact-arithmetic checks: (B.5) by substitution into YG'' + νG' = F; (B.8) by brute force over small indices; (B.9) and (B.10) as rational identities in the weights (digest check: both identities and bounds hold for all α, β < 40, and the supremum in (B.9) is 80, attained at α = β = 0); (B.7) numerically (digest check: the left side stays below 3.52 for N < 200, against the bound 8Σ i^{−2} = 4π²/3 ≈ 13.16).",
"depends_on": [
"M4.4",
"M4.3"
],
"constrains": [],
"reasons": {
"M4.4": "J_1, J_2 invert the radial viscous operators of the zero-stress equations (4.13), regular at Y = 0, for U and for ϕ.",
"M4.3": "it bounds the radial average A_X of (4.6), which enters (4.13) through V0 and W, together with ∂_η I."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 145-146",
"analogous_to": [],
"relations": {
"M4.4": "prerequisite",
"M4.3": "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": "MB.4",
"kind": "move",
"name": "ns-mb-4-explicit-leading-swirl-profile-f0-and-its-positivity",
"title": "Explicit leading swirl profile f0 and its positivity window",
"section": "B",
"pages": "146",
"refs": [
"p. 146, (B.11)",
"p. 148 (Φ0 = f0(Yχ))",
"pp. 149 to 150 (use at the endpoint)."
],
"statement": "f0(z) = Σα≥0 (−z/2)^α/(α!(α + 1)!). For 0 ≤ z ≤ 4.1 and t = z/2: f0(z) ≥ 1 − t/2 + t²/12 − t³/144 ≥ 305719/1152000 > .265 and f0(z) ≤ 1 (B.11); the cubic is decreasing on [0, 2.05]. It is the unperturbed angular profile: Φ0 = (1 + T)^{−1}1 = f0(Yχ), the solution regular at Y = 0 with value 1 of 2(YΦYY + 2ΦY) = −χΦ. The companion quantity f0 + zf0' enters (B.19) through the bound f0 + zf0' ≤ 1 − t + t²/4 − t³/36 + t⁴/576.",
"description": "f0(z) = Σα≥0 (−z/2)^α/(α!(α + 1)!). For 0 ≤ z ≤ 4.1 and t = z/2: f0(z) ≥ 1 − t/2 + t²/12 − t³/144 ≥ 305719/1152000 > .265 and f0(z) ≤ 1 (B.11); the cubic is decreasing on [0, 2.05]. It is the unperturbed angular profile: Φ0 = (1 + T)^{−1}1 = f0(Yχ), the solution regular at Y = 0 with value 1 of 2(YΦYY + 2ΦY) = −χΦ. The companion quantity f0 + zf0' enters (B.19) through the bound f0 + zf0' ≤ 1 − t + t²/4 − t³/36 + t⁴/576. OBLIGATION: Division by ϕ in the first equation of (B.15), and the use of log Φ in l and (log E)η, are legitimate only if Φ > 0 on the whole stress-free interval; (B.11) with (B.13) gives Φ ≥ c0 > 0 on 0 ≤ Y ≤ 4.1 for large Λ. f0 also fixes the rotational shear at the edge, a = −2YΦY/Φ ≈ −2zf0'(z)/f0(z) at Y = 4. MECHANISM: When the large source ΛLχ dominates, the angular equation in Y becomes a linear regular singular ODE whose coefficient χ(η) does not depend on Y; ANTECEDENT: None cited; alternating-series bounds are used directly. (Digest's identification, not the manuscript's: f0(z) = J1(2√t)/√t and f0 + zf0' = J0(2√t) with t = z/2, Bessel functions of the first kind.) REFS: p. 146, (B.11); p. 148 (Φ0 = f0(Yχ)); pp. 149 to 150 (use at the endpoint).",
"obligation": "Division by ϕ in the first equation of (B.15), and the use of log Φ in l and (log E)η, are legitimate only if Φ > 0 on the whole stress-free interval; (B.11) with (B.13) gives Φ ≥ c0 > 0 on 0 ≤ Y ≤ 4.1 for large Λ. f0 also fixes the rotational shear at the edge, a = −2YΦY/Φ ≈ −2zf0'(z)/f0(z) at Y = 4.",
"backward_question": "When axial transport of angular momentum dominates the source, what linear equation does the swirl obey near the axis, and on what radial interval is its explicit solution still positive while its logarithmic slope already exceeds the viscous threshold 2?",
"mechanism": "When the large source ΛLχ dominates, the angular equation in Y becomes a linear regular singular ODE whose coefficient χ(η) does not depend on Y; its regular solution is a power series with alternating coefficients of decreasing magnitude on the relevant range, so partial sums bound it from both sides. The cubic partial sum equals 305719/1152000 at t = 2.05, and since 0 ≤ χ ≤ 1 the argument z = Yχ stays in [0, 4.1]. The edge Y = 4 lies beyond the point where −2zf0'/f0 first reaches 2 (digest computation: z ≈ 2.8916, the first zero of f0 + zf0') and well before f0 vanishes (digest computation: first zero at z ≈ 7.341).",
"antecedent": "None cited; alternating-series bounds are used directly. (Digest's identification, not the manuscript's: f0(z) = J1(2√t)/√t and f0 + zf0' = J0(2√t) with t = z/2, Bessel functions of the first kind.)",
"cost": "Caps the stress-free analytic region at Y ≤ 4.1 and places the stress activation at Y = 4 (X0 = 4/Λ, which is Xa of Proposition 4.10); forces t̄ with 4e^{2t̄} < 4.1 and tc with 4e^{tc} < 4.1 so that later cutoffs stay inside the analytic region.",
"checkable": "Evaluate f0 by its series (or as J1(√(2z))/√(z/2)) on [0, 4.1] and confirm min > .265 (digest check: minimum .27111 at z = 4.1, maximum 1 at z = 0); confirm in exact arithmetic that the cubic partial sum at t = 41/20 equals 305719/1152000; confirm symbolically that f0 solves 2(zf'' + 2f') + f = 0 with f(0) = 1.",
"depends_on": [
"MB.2",
"M4.4",
"MB.3"
],
"constrains": [],
"reasons": {
"MB.2": "the large source ΛLχ from the steep axis datum reduces the angular equation to 2(YΦ_YY + 2Φ_Y) = -χΦ, solved by f0(Yχ).",
"M4.4": "that equation is the leading part of the angular zero-stress equation (4.13) in the variable Y = ΛX.",
"MB.3": "Φ0 = (1 + T)^{-1}1 is written with T = J_2χ/2, the radial inverse of Lemma B.1."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 146",
"analogous_to": [],
"relations": {
"MB.2": "prerequisite",
"M4.4": "prerequisite",
"MB.3": "prerequisite"
},
"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": "correct"
}
},
{
"id": "MB.5",
"kind": "move",
"name": "ns-mb-5-proposition-b-2-the-analytic-stress-free-axis-profile-by",
"title": "Proposition B.2, the analytic stress-free axis profile by contraction",
"section": "B",
"pages": "146-148",
"refs": [
"pp. 146 to 148, Proposition B.2, (B.12) to (B.16)",
"Theorem 4.6(i) to (ii), p. 33",
"Proposition 4.10(i), p. 36",
"(4.4) to (4.5), p. 25",
"Lemma 5.1, p. 47."
],
"statement": "With the axis data of Section B.1 there are Λ0 and, for each Λ ≥ Λ0, a threshold C0(Λ) such that every C ≥ C0(Λ) admits an analytic profile with vanishing leading residual stress on 0 ≤ Y = ΛX ≤ 4.1 of the form ϕ = ϕ∗Φ, U = U∗ + Λ^{−1}u, Π = Π0 + Λ^{−1}I(g²Φ²), g = ϕ∗/C (B.12), with Φ(0, η) = 1, u(0, η) = 0, analytic in Y and η on a common neighborhood of [0, 4.1] × I, and |∂Y^r ∂η^s (Φ − f0(Yχ), u + YZ∗/(2L))| ≤ Cr,s/Λ (B.13), uniformly in large Λ and C ≥ C0(Λ) (for X-derivatives the bound is Cr,sΛ^{r−1}).",
"description": "With the axis data of Section B.1 there are Λ0 and, for each Λ ≥ Λ0, a threshold C0(Λ) such that every C ≥ C0(Λ) admits an analytic profile with vanishing leading residual stress on 0 ≤ Y = ΛX ≤ 4.1 of the form ϕ = ϕ∗Φ, U = U∗ + Λ^{−1}u, Π = Π0 + Λ^{−1}I(g²Φ²), g = ϕ∗/C (B.12), with Φ(0, η) = 1, u(0, η) = 0, analytic in Y and η on a common neighborhood of [0, 4.1] × I, and |∂Y^r ∂η^s (Φ − f0(Yχ), u + YZ∗/(2L))| ≤ Cr,s/Λ (B.13), uniformly in large Λ and C ≥ C0(Λ) (for X-derivatives the bound is Cr,sΛ^{r−1}). OBLIGATION: This is the inner region of Theorem 4.6: (4.13) holds and T0 = 0 on 0 ≤ X ≤ Xa (Theorem 4.6(ii), Proposition 4.10(i)). ANTECEDENT: As cited in the text: a strict contraction and its unique fixed point, Cauchy's inequality, and Cauchy estimates, in the norm of Lemma B.1. The inversion of 1 + T is a Neumann series, not named as such. (Digest's identification, not the manuscript's: the resolvent series has Volterra-type factorial decay.) REFS: pp. 146 to 148, Proposition B.2, (B.12) to (B.16); Theorem 4.6(i) to (ii), p. 33; Proposition 4.10(i), p. 36; (4.4) to (4.5), p. 25; Lemma 5.1, p. 47.",
"obligation": "This is the inner region of Theorem 4.6: (4.13) holds and T0 = 0 on 0 ≤ X ≤ Xa (Theorem 4.6(ii), Proposition 4.10(i)). F = ϕ/C, U, Π and V0/X are analytic in X (power series in r²/(2q)), hence smooth at the axis, and with E = √(2X)ϕ/C and (4.4) to (4.5) the Cartesian field is smooth across r = 0 (Definition 3.2, Theorem 4.6(i)). The profiles are analytic in η on one complex neighborhood (Theorem 4.6(i), used by Lemma 5.1), and ϕ > 0 gives E > 0 for X > 0.",
"backward_question": "Can the same large parameter that steepens the swirl in η also rescale the radius so that the nonlinear stress-free system becomes a 1/Λ perturbation of an explicitly solvable linear problem, and can the pressure's coupling to an exponentially large swirl datum be neutralized by the still-free amplitude C?",
"mechanism": "In Y the stress-free system becomes 2(YΦYY + 2ΦY) = −χΦ + Λ^{−1}R1 and 2(YuYY + uY) = −Z∗/L + Λ^{−1}R2, where R1, R2 are explicit polynomials in Φ, u, their DX and η derivatives, W = W∗ + Λ^{−1}B, Hc = H∗ + Λ^{−1}du, and p = I(g²Φ²). The only products with both an unintegrated η-derivative and a DX derivative are (∂ηAX(u))DXΦ and (∂ηAX(u))DXu, controlled by (B.6); ∂ηp is bounded because ∂ηI is, and DXp = Yg²Φ². So (Φ, u) ↦ JνRi is bounded and locally Lipschitz on balls of Bρ². The angular term −χΦ is of order one, not small, but T = J2χ/2 raises the minimal radial degree by one and divides by (b + 1)(b + 2), so ‖T^k‖ ≤ (40Mχ)^k/(k!(k + 1)!) and Σ(−T)^k inverts 1 + T whatever the size of χ. The map (Φ, u) ↦ (Φ0 + (1 + T)^{−1}J2R1/(2Λ), u0 + J1R2/(2Λ)), with (Φ0, u0) = (f0(Yχ), −YZ∗/(2L)), is then a strict contraction on a fixed ball for large Λ, with fixed point within C/Λ of the center. The pressure couples to ϕ∗, which can be exponentially large in Λ; (B.16) gives |g| ≤ 1 on the complex neighborhood, so Cauchy's inequality bounds all η-derivatives of g uniformly in both large parameters (the manuscript stresses that this bound must hold on a complex neighborhood). Finally Σα C(α + β, β)(R/20)^α = (1 − R/20)^{−β−1} turns the coefficient norm into analyticity on |Y| ≤ R for any 4.1 < R < 20 with η-radius below ρ(1 − R/20); Cauchy estimates give (B.13); real data and uniqueness of the fixed point give a real solution; (B.11) gives Φ > 0.",
"antecedent": "As cited in the text: a strict contraction and its unique fixed point, Cauchy's inequality, and Cauchy estimates, in the norm of Lemma B.1. The inversion of 1 + T is a Neumann series, not named as such. (Digest's identification, not the manuscript's: the resolvent series has Volterra-type factorial decay.)",
"cost": "Λ ≥ Λ0; C ≥ C0(Λ) ≥ sup over Ω of |ϕ∗|, so C is chosen after Λ and may be exponentially large in Λ; ρ strictly below the distance to the boundary of Ω; the solution exists only for Y ≤ 4.1; the smaller common complex neighborhood fixed here is the one Corollary B.6 later preserves.",
"checkable": "Run the fixed-point iteration numerically on truncated Taylor coefficients in Y (coefficient rule (B.5) for J1, J2), with η discretized spectrally (Chebyshev), for several moderately large Λ and C ≥ max over a complex strip of |ϕ∗|. Check that sup|Φ − f0(Yχ)| and sup|u + YZ∗/(2L)| on [0, 4.1] × [−1, 1] scale like 1/Λ as in (B.13), that the Taylor coefficients decay at least like 20^{−α}(α + 1)^{−2} as membership in Bρ requires, and that Φ > 0.",
"depends_on": [
"MB.3",
"MB.4",
"MB.2",
"M4.4"
],
"constrains": [],
"reasons": {
"MB.3": "the fixed point is found in Lemma B.1's space B_ρ, whose radial inverses and product bound (B.6) absorb the η-derivatives of (4.13).",
"MB.4": "the contraction is centered at Φ0 = f0(Yχ), with 1 + T inverted by its factorially decaying series.",
"MB.2": "the axis data are ϕ(0, η) = ϕ*, and C ≥ sup|ϕ*| on Ω (B.16) tames the pressure coupling through g = ϕ*/C.",
"M4.4": "the system solved is the zero-stress equations (4.13), so T0 = 0 on the stress-free region."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 146-148",
"analogous_to": [],
"relations": {
"MB.3": "prerequisite",
"MB.4": "prerequisite",
"MB.2": "prerequisite",
"M4.4": "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": "MB.6",
"kind": "move",
"name": "ns-mb-6-proposition-b-3-positive-angular-source-and-the-two",
"title": "Proposition B.3, positive angular source and the two-branch endpoint inequality",
"section": "B",
"pages": "148-150",
"refs": [
"pp. 148 to 150, Proposition B.3, (B.17) to (B.21)",
"Proposition 4.10(ii), p. 37",
"Theorem 4.6(iii), p. 33",
"Section 2.1, p. 5."
],
"statement": "After increasing Λ and then C0(Λ): Φ ≥ c0 > 0 on [0, 4.1] × [−1, 1]; Sq ≥ 2.5 + .95ΛLχ (B.17); with p1 = ps,1 = XQs/L, p2 = ps,2 = XNs/(LE), ns = Ns/L, one has p1/X ≥ c1 > 0, 0 < p1 ≤ C1, ns = −2UX = Z∗/L + O(Λ^{−1}) on 0 < X ≤ 4.1/Λ (B.18); at X0 = 4/Λ, p1 + p2²/p1 > 2 + cex (B.19), for example with cex = .2; Φ, log Φ, u, p1, ns have η-derivative bounds of every fixed order uniform in C ≥ C0(Λ).",
"description": "After increasing Λ and then C0(Λ): Φ ≥ c0 > 0 on [0, 4.1] × [−1, 1]; Sq ≥ 2.5 + .95ΛLχ (B.17); with p1 = ps,1 = XQs/L, p2 = ps,2 = XNs/(LE), ns = Ns/L, one has p1/X ≥ c1 > 0, 0 < p1 ≤ C1, ns = −2UX = Z∗/L + O(Λ^{−1}) on 0 < X ≤ 4.1/Λ (B.18); at X0 = 4/Λ, p1 + p2²/p1 > 2 + cex (B.19), for example with cex = .2; Φ, log Φ, u, p1, ns have η-derivative bounds of every fixed order uniform in C ≥ C0(Λ). OBLIGATION: In the stress-free region ps = s = (a, −bs), so vs = a + bs²/a = p1 + p2²/p1, and (B.19) is exactly vs > 2 + cex at the inner annulus edge. Since the stress is born parallel to the shear there (Theorem 4.6(iii)), this is the viscous inequality of the admissible stress cone at the edge, stated in Proposition 4.10(ii) as a(Xa) > 0 and vs(Xa) > 2 + cex. The source bound gives p1 = a > 0 (so ts and vs are defined) and the lower bounds that Lemma B.4 propagates. ANTECEDENT: Young's inequality and alternating-series remainder bounds, used directly; nothing classical cited. REFS: pp. 148 to 150, Proposition B.3, (B.17) to (B.21); Proposition 4.10(ii), p. 37; Theorem 4.6(iii), p. 33; Section 2.1, p. 5.",
"obligation": "In the stress-free region ps = s = (a, −bs), so vs = a + bs²/a = p1 + p2²/p1, and (B.19) is exactly vs > 2 + cex at the inner annulus edge. Since the stress is born parallel to the shear there (Theorem 4.6(iii)), this is the viscous inequality of the admissible stress cone at the edge, stated in Proposition 4.10(ii) as a(Xa) > 0 and vs(Xa) > 2 + cex. The source bound gives p1 = a > 0 (so ts and vs are defined) and the lower bounds that Lemma B.4 propagates.",
"backward_question": "At the radius where the stress will be switched on, can vs > 2 be guaranteed for every η, and which free parameter enlarges the rotational part a, and which the axial part bs²/a, of vs?",
"mechanism": "For the source, (B.20) follows from Φ ≈ f0(Yχ) and |H∗χ'| ≤ 2‖H∗'‖∞χ; then −Hc(log ϕ)η ≈ ΛLχ with errors absorbed by Young's inequality (allocating .05ΛLχ), and with l = 1 + DX log Φ, −W∗ > 2.8 and |h(1 − 2ηU)| ≤ 10h ≤ .1 one gets (B.17) without dividing by χ near the zero of H∗. Qs > 0 follows from the positive representation Qs = ∫0^X X'Φ(ΛX')Sq dX'/(X²Φ(ΛX)). Integrating the stress-free equations from the axis gives p1 = a = −2YΦY/Φ and ns = −2uY. At Y = 4 there are two branches. If χ > .99, then t = 2χ ∈ (1.98, 2] and f0 + zf0' ≤ 1 − t + t²/4 − t³/36 + t⁴/576 < −.18 (the quartic equals −75535511/400000000 < −.188 at t = 1.98 and decreases on [1.98, 2]), so a = −2zf0'/f0 = 2 − 2(f0 + zf0')/f0 > 2.36 and p1 > 2.3 for large Λ: the rotational shear alone clears the threshold. If χ ≤ .99, then |Z∗| > δ∗ by (B.2), so |ns| ≥ δ∗/2, and at the endpoint |p2| = C(2/Λ)^{1/2}|ns|/(ϕ∗Φ) grows linearly in C for fixed Λ while p1 ≤ C1; enlarging C0(Λ) gives p2²/p1 > 2.3: a small swirl amplitude 1/C lets the axial shear dominate. This is the analytic form of Section 2.1's statement that the radial shear of axial velocity supplies the amplification near the middle plane while the rotational mechanism suffices farther away.",
"antecedent": "Young's inequality and alternating-series remainder bounds, used directly; nothing classical cited.",
"cost": "A further increase of Λ and of C0(Λ) (C must beat a Λ-dependent bound on ϕ∗Φ at the endpoint); the constants c0, c1, C1; the margin cex = .2, which reappears as vs > 2 + cex in Proposition 4.10(ii).",
"checkable": "Exact rational check that the quartic partial sum at t = 99/50 equals −75535511/400000000; evaluate a(z) = −2zf0'(z)/f0(z) on [3.96, 4] (digest check: 3.326 to 3.389, well above the proved 2.36); symbolic check that p2 = XNs/(LE) with E = √(2X)ϕ∗Φ/C equals C(X/2)^{1/2}ns/(ϕ∗Φ), which is C(2/Λ)^{1/2}ns/(ϕ∗Φ) at X = 4/Λ; with the numerical profile of MB.5, evaluate p1 + p2²/p1 at Y = 4 over η ∈ [−1, 1] for increasing C.",
"depends_on": [
"MB.5",
"MB.1",
"MB.4",
"M4.7"
],
"constrains": [],
"reasons": {
"MB.5": "reads all bounds off Proposition B.2's stress-free profile and its closeness (B.13) to f0(Yχ) and -YZ*/(2L).",
"MB.1": "the two branches at Y = 4 are the split χ > .99 (rotational) or |Z*| > δ* (axial shear), with -W* > 2.8 in the source.",
"MB.4": "on χ > .99 the bound on f0 + zf0' gives a = -2zf0'/f0 > 2.36 at Y = 4, and (B.11) gives Φ ≥ c0 > 0.",
"M4.7": "with p_s = s in the stress-free region, p1 + p2²/p1 is v_s of (4.20), so (B.19) is v_s > 2 + c_ex at the edge."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 148-150",
"analogous_to": [],
"relations": {
"MB.5": "prerequisite",
"MB.1": "prerequisite",
"MB.4": "prerequisite",
"M4.7": "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": "MB.7",
"kind": "move",
"name": "ns-mb-7-lemma-b-4-reference-continuation-with-frozen-logarithmic",
"title": "Lemma B.4, reference continuation with frozen logarithmic slopes",
"section": "B",
"pages": "150-151",
"refs": [
"pp. 150 to 151, Lemma B.4, (B.22) to (B.25)",
"(A.5), p. 129."
],
"statement": "Lemma B.4. Let X0 = 4/Λ, Xi = 110, y = log(X/X0), 0 < t1 ≤ t̄ with 4e^{2t̄} < 4.1. The reference (ϕr, Ur) is the analytic profile for y ≤ t1, has its slopes ∂y log ϕr, ∂yUr cut to zero by the step σ of (A.5) on t1 < y < 2t1 (B.22), and is constant in log X after; pressure, Qs, Ns are integrated from the axis with datum Π0. For Λ, then C, large and then t1 small, on [X0, Xi] × [−1, 1]: Sq,r ≥ .94LΛχ + 2.4, lr ≤ 1, vr = p1,r + p2,r²/p1,r > 2 + c (B.23), p1,r > 0, p1,r > 3 on [100, 110]; η-norms of CEr, 1/(CEr), p1,r, ns,r are bounded uniformly in C, t1; ‖Πr − Π0‖ ≤ CkC^{−2} (B.24).",
"description": "Lemma B.4. Let X0 = 4/Λ, Xi = 110, y = log(X/X0), 0 < t1 ≤ t̄ with 4e^{2t̄} < 4.1. The reference (ϕr, Ur) is the analytic profile for y ≤ t1, has its slopes ∂y log ϕr, ∂yUr cut to zero by the step σ of (A.5) on t1 < y < 2t1 (B.22), and is constant in log X after; pressure, Qs, Ns are integrated from the axis with datum Π0. For Λ, then C, large and then t1 small, on [X0, Xi] × [−1, 1]: Sq,r ≥ .94LΛχ + 2.4, lr ≤ 1, vr = p1,r + p2,r²/p1,r > 2 + c (B.23), p1,r > 0, p1,r > 3 on [100, 110]; η-norms of CEr, 1/(CEr), p1,r, ns,r are bounded uniformly in C, t1; ‖Πr − Π0‖ ≤ CkC^{−2} (B.24). OBLIGATION: The analytic solution exists only for Y ≤ 4.1, but the profile must reach X ≈ XRe^{−5}, a radius growing like C^{10}. The shear reduction of Proposition B.5 needs a comparison profile on the whole interval whose integrated coefficients ps,r are uniformly bounded and signed, with vr > 2 + c, so that the stress created by lowering the shear lies in the admissible cone. MECHANISM: Cutting the logarithmic slopes of ϕ and U to zero and then holding the fields constant in log X means nothing grows, however long the interval: Ur stays within O(Λ^{−1}) + o(1) of U∗ (radial averaging is a.",
"obligation": "The analytic solution exists only for Y ≤ 4.1, but the profile must reach X ≈ XRe^{−5}, a radius growing like C^{10}. The shear reduction of Proposition B.5 needs a comparison profile on the whole interval whose integrated coefficients ps,r are uniformly bounded and signed, with vr > 2 + c, so that the stress created by lowering the shear lies in the admissible cone.",
"backward_question": "How can a profile known only on a short analytic interval be carried out to arbitrarily large radius with every quantity in the cone test bounded uniformly in the length of the interval and in the amplitude?",
"mechanism": "Cutting the logarithmic slopes of ϕ and U to zero and then holding the fields constant in log X means nothing grows, however long the interval: Ur stays within O(Λ^{−1}) + o(1) of U∗ (radial averaging is a contraction in sup norm, so AX(Ur) does too, independently of the interval length), log ϕr stays a bounded distance from log ϕ∗, and the pressure moves only by O(C^{−2}) because E ∝ 1/C. The source keeps its large gradient part LΛχ (replacing H∗ by Hc,r costs Cσ∗√χ + o(1), absorbed) and its constant part from −W∗ > 2.8. Because the analytic profile has p1 = a > 0, its ϕ slope is nonpositive, so freezing it gives lr ≤ 1. The equations (B.25) are linear with regular initial values; with lr ≤ 1 and either Sq,r ≥ .94LΛχ or Sq,r ≥ 2.4, integrating factors give the exponential and the linear lower bounds for p1,r, keeping p1,r above 2.3 on χ > .99 and above 3 from X = 100. On χ ≤ .99 the axial source keeps |ns,r| bounded below and p2,r = Xns,r/Er grows with C, so vr > 2 + c everywhere.",
"antecedent": "None cited; the smooth step (A.5) is the manuscript's own.",
"cost": "The width t1 (0 < t1 ≤ t̄) and t̄ with 4e^{2t̄} < 4.1; the fixed local radii X0, 100, 110; the order Λ, then C, then t1; the constant c in vr > 2 + c.",
"checkable": "From the numerical axis profile of MB.5, integrate (B.22) and then (B.25) in y up to log(110/X0); check Sq,r ≥ .94LΛχ + 2.4, lr ≤ 1, vr > 2 + c, and p1,r > 3 on [100, 110]; check the two comparison inequalities pointwise.",
"depends_on": [
"MB.6",
"MB.5",
"M4.4"
],
"constrains": [],
"reasons": {
"MB.6": "propagates Proposition B.3's source bound, p1 > 0, and the endpoint inequality v > 2 + c from X0 out to X_i = 110.",
"MB.5": "the reference equals the analytic profile for y ≤ t1 and then freezes its logarithmic slopes.",
"M4.4": "Q_s, N_s are integrated from the axis by (4.9), giving the linear equations (B.25) for p1,r and n_s,r."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 150-151",
"analogous_to": [],
"relations": {
"MB.6": "prerequisite",
"MB.5": "prerequisite",
"M4.4": "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
}
},