Other material · A dividing-plane barrier in the OpenAI forced Navier-Stokes blow-up construction
The ledger as data, version 1.0, September 30, 2026
The first version of the ledger (see ledger.md) in machine-readable form, generated on September 30, 2026, and kept frozen as exactly what the three small open models of Hypnos, the research harness this site describes (Gemma 4 31B, Gemma 4 26B and Qwen3 32B), were shown in a one-time test on the manuscript's moves with the reasons withheld: in 16,018 lines of their output, graded blind by Claude Opus 5.5 sessions, they never recovered the reason for a move. It is shown here in pages of whole records.
- Written by
- Claude Opus sessions and Claude Fable 5.1 (Anthropic)
- Size
- 897,753 bytes
- SHA-256
f2f7a98d815175f32ec70f1d694bf138920b250608d0376a13191fe89b8120a2
The note's pageEvery file published with itThis file on GitHub
{
"id": "M10.4",
"kind": "move",
"name": "ns-m10-4-flatness-at-the-origin-and-the-taylor-data-f-j",
"title": "Flatness at the origin and the Taylor data F_j",
"section": "10",
"pages": "118-120",
"refs": [
"pp. 118 to 120, (10.6), (10.9), (10.10)",
"(3.4), p. 15",
"(10.3), p. 118."
],
"statement": "Lemma 10.2: for every spatial multi-index α and integer j ≥ 0, ∂^α_x ∂^j_t f converges uniformly on R³ as t ↑ 1, and there are F_j ∈ C_c^∞(R³; R³), all supported in K, with lim_{t↑1} ∂^α_x ∂^j_t f(x, t) = ∂^α_x F_j(x) and ∂^α_x F_j(0) = 0 (10.6). Near the origin, on a fixed neighborhood of (0, 1), (10.9): |∂^α_x ∂^j_t f(x, t)| ≤ C_{α,j,N} (τ + |z|^{1/D})^N for every α, j, N. Compatibility (10.10): ∂^α_x ∂^j_t f(x, t) = ∂^α_x F_j(x) − ∫_t^1 ∂^α_x ∂^{j+1}_t f(x, s) ds.",
"description": "Lemma 10.2: for every spatial multi-index α and integer j ≥ 0, ∂^α_x ∂^j_t f converges uniformly on R³ as t ↑ 1, and there are F_j ∈ C_c^∞(R³; R³), all supported in K, with lim_{t↑1} ∂^α_x ∂^j_t f(x, t) = ∂^α_x F_j(x) and ∂^α_x F_j(0) = 0 (10.6). Near the origin, on a fixed neighborhood of (0, 1), (10.9): |∂^α_x ∂^j_t f(x, t)| ≤ C_{α,j,N} (τ + |z|^{1/D})^N for every α, j, N. Compatibility (10.10): ∂^α_x ∂^j_t f(x, t) = ∂^α_x F_j(x) − ∫_t^1 ∂^α_x ∂^{j+1}_t f(x, s) ds. OBLIGATION: At the singular point the individual terms of the residual diverge, and a smooth force needs every derivative of their sum to have a limit there. This is where the flat-residual output of Sections 5 to 9, (3.4), is spent. (10.10) is the compatibility that Lemma 10.3 needs to produce a C^∞ extension rather than a merely continuous one. ANTECEDENT: None cited (uniform convergence of derivatives, fundamental theorem of calculus). The input (3.4) is Theorem 3.1(iii), proved in Proposition 9.9 from (5.41) and (9.20). REFS: pp. 118 to 120, (10.6), (10.9), (10.10); (3.4), p. 15; (10.3), p. 118.",
"obligation": "At the singular point the individual terms of the residual diverge, and a smooth force needs every derivative of their sum to have a limit there. This is where the flat-residual output of Sections 5 to 9, (3.4), is spent. (10.10) is the compatibility that Lemma 10.3 needs to produce a C^∞ extension rather than a merely continuous one.",
"backward_question": "Does the residual, whose individual terms blow up at the singular point, have limits for all of its derivatives at t = 1, and do those limits fit together as the time-Taylor data of a smooth function?",
"mechanism": "Near (0, 1) both cutoffs equal one, so f = R(u_loc, p_loc). On X ≤ X_ext, (3.4) bounds every derivative by C q^N, and (10.3) turns q^N into (τ + |z|^{1/D})^N; on X > X_ext the residual vanishes identically. For a given tolerance, one first picks a small ball about the origin and then a late time so that (10.9) is below the tolerance there; M10.3 and a finite cover handle the rest of K; everything vanishes off K. Each derivative is therefore uniformly Cauchy on R³, with limit zero at the origin. The limit F_j of ∂_t^j f is smooth because limits of spatial derivatives pass through the fundamental theorem of calculus along coordinate segments, and passing to the limit in the same theorem in time gives (10.10), which says that the limits are the one-sided time-Taylor data of f at t = 1.",
"antecedent": "None cited (uniform convergence of derivatives, fundamental theorem of calculus). The input (3.4) is Theorem 3.1(iii), proved in Proposition 9.9 from (5.41) and (9.20).",
"cost": "None new. The data vanish to infinite order at the origin (∂^α_x F_j(0) = 0). Letting t ↑ 1 in (10.9) also bounds |∂^α_x F_j(x)| by C_{α,j,N} |z|^{N/D} on the neighborhood where (10.9) holds, although the lemma records only the vanishing at the origin.",
"checkable": "None: pure estimate. Its one computable ingredient, (10.3), is checked under M10.2, and the flatness input (3.4) is proved in Sections 5 to 9.",
"depends_on": [
"M9.13",
"M10.3",
"M10.2",
"M9.15"
],
"constrains": [],
"reasons": {
"M9.13": "Near (0, 1) the force is the local residual, flat by (9.20), which is (3.4).",
"M10.3": "Away from the origin the uniform limits come from the first part of Lemma 10.2.",
"M10.2": "Near (0, 1) both cutoffs equal one, and (10.3) turns q^N into (τ + |z|^{1/D})^N.",
"M9.15": "For X > X_ext the residual vanishes identically."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 118-120"
},
{
"id": "M10.5",
"kind": "move",
"name": "ns-m10-5-continuation-of-the-force-through-t-1-by-shrinking-time",
"title": "Continuation of the force through t = 1 by shrinking time cutoffs",
"section": "10",
"pages": "120",
"refs": [
"p. 120, Lemma 10.3, (10.10), (10.11), (10.12), the display defining b_j, and the decay display",
"[13, (5)] cited on p. 120."
],
"statement": "Lemma 10.3: the force in (10.5) extends to f ∈ C_c^∞(R³ × (0, ∞); R³) with support contained in K × [0, 2]. With χ_0 ∈ C_c^∞(R) equal to one near zero and zero for arguments at least one, and σ = t − 1 ≥ 0, (10.11): f(x, 1 + σ) = Σ_{j≥0} χ_0(b_j σ) (σ^j/j!) F_j(x) for increasing integers b_j ≥ 1. The product rule and 0 ≤ σ ≤ b_j^{−1} on each support give (10.12): ‖∂^α_x ∂^m_σ (χ_0(b_j σ) σ^j F_j / j!)‖_∞ ≤ C_{j,m} b_j^{m−j} ‖F_j‖_{C^{|α|}}.",
"description": "Lemma 10.3: the force in (10.5) extends to f ∈ C_c^∞(R³ × (0, ∞); R³) with support contained in K × [0, 2]. With χ_0 ∈ C_c^∞(R) equal to one near zero and zero for arguments at least one, and σ = t − 1 ≥ 0, (10.11): f(x, 1 + σ) = Σ_{j≥0} χ_0(b_j σ) (σ^j/j!) F_j(x) for increasing integers b_j ≥ 1. The product rule and 0 ≤ σ ≤ b_j^{−1} on each support give (10.12): ‖∂^α_x ∂^m_σ (χ_0(b_j σ) σ^j F_j / j!)‖_∞ ≤ C_{j,m} b_j^{m−j} ‖F_j‖_{C^{|α|}}. OBLIGATION: Theorem 1.1 requires f ∈ C_c^∞(R³ × (0, ∞); R³), smooth for all t > 0 and compactly supported in time, together with the decay conditions of [13, (5)]; Lemma 10.2 supplies only one-sided limits at t = 1. MECHANISM: The series realizes the prescribed Taylor data at σ = 0 from the right. Since each cutoff is constant near zero, the m-th σ-derivative of the j-th summand at σ = 0 is F_j when m = j and zero otherwise, so the series. ANTECEDENT: None cited. (This is the classical Borel-lemma construction; the identification is mine, the manuscript does not name it.) The decay conditions are those of [13, (5)]. REFS: p. 120, Lemma 10.3, (10.10), (10.11), (10.12), the display defining b_j, and the decay display; [13, (5)] cited on p. 120.",
"obligation": "Theorem 1.1 requires f ∈ C_c^∞(R³ × (0, ∞); R³), smooth for all t > 0 and compactly supported in time, together with the decay conditions of [13, (5)]; Lemma 10.2 supplies only one-sided limits at t = 1.",
"backward_question": "Given compatible one-sided limits of every derivative at t = 1, can a single smooth force realize all of them from t > 1 and still vanish after a fixed time?",
"mechanism": "The series realizes the prescribed Taylor data at σ = 0 from the right. Since each cutoff is constant near zero, the m-th σ-derivative of the j-th summand at σ = 0 is F_j when m = j and zero otherwise, so the series reproduces the limits F_m and, by (10.10), all mixed space-time derivative limits from t < 1. On the support of χ_0(b_j σ) one has σ ≤ 1/b_j, so each derivative, whether it falls on the cutoff (a factor b_j) or on the monomial (one power of σ lost), costs a factor b_j, which yields b_j^{m−j}. Because m − j < 0 in each of the finitely many constraints with a + m ≤ ⌊j/2⌋, a large enough b_j makes the j-th term at most 2^{−j} in C^{⌊j/2⌋}. Every fixed derivative of the tail therefore converges uniformly, which gives smoothness across σ = 0 and at the support boundaries. Every summand vanishes for σ ≥ 1, so f = 0 for t ≥ 2, and f = 0 near t = 0 by (10.2) and the construction of p. Compact support makes the polynomial decay bounds automatic.",
"antecedent": "None cited. (This is the classical Borel-lemma construction; the identification is mine, the manuscript does not name it.) The decay conditions are those of [13, (5)].",
"cost": "For t ≥ 1 the force is not the residual of any constructed flow; it is one of many smooth continuations and carries no dynamical meaning. No new condition on the construction.",
"checkable": "For a fixed χ_0, compute sup_σ |∂_σ^m (χ_0(bσ) σ^j / j!)| for several b, j, m and confirm the scaling b^{m−j} of (10.12). For model data F_j (for example the Taylor data of a known smooth function times a fixed bump), compute b_j by the rule and check numerically that the truncated series (10.11) has σ-derivatives F_m at σ = 0 and vanishes for σ ≥ 1.",
"depends_on": [
"M10.4",
"M10.2"
],
"constrains": [],
"reasons": {
"M10.4": "The series realizes the Taylor data F_j of Lemma 10.2, and the compatibility (10.10) makes the continuation smooth across t = 1.",
"M10.2": "The force vanishes near t = 0 by (10.2) and is supported in K."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 120"
},
{
"id": "M10.6",
"kind": "move",
"name": "ns-m10-6-energy-bound-derived-from-the-equation",
"title": "Energy bound derived from the equation",
"section": "10",
"pages": "121",
"refs": [
"p. 121, Lemma 10.4, (10.13), (10.14)",
"Section 3.5, pp. 16 to 17."
],
"statement": "Lemma 10.4: with F(t) = ∫_0^t ‖f(s)‖_2 ds for 0 ≤ t ≤ 1, F(1) < ∞ and ‖u(t)‖_2² + 2 ∫_0^t ‖∇u(s)‖_2² ds ≤ F(t)² for 0 ≤ t < 1 (10.13); the kinetic energy is uniformly bounded and the total dissipation on [0, 1) is finite. It rests on the energy identity (10.14), (1/2) d/dt ‖u(t)‖_2² + ‖∇u(t)‖_2² = ⟨f(t), u(t)⟩.",
"description": "Lemma 10.4: with F(t) = ∫_0^t ‖f(s)‖_2 ds for 0 ≤ t ≤ 1, F(1) < ∞ and ‖u(t)‖_2² + 2 ∫_0^t ‖∇u(s)‖_2² ds ≤ F(t)² for 0 ≤ t < 1 (10.13); the kinetic energy is uniformly bounded and the total dissipation on [0, 1) is finite. It rests on the energy identity (10.14), (1/2) d/dt ‖u(t)‖_2² + ‖∇u(t)‖_2² = ⟨f(t), u(t)⟩. OBLIGATION: Theorem 1.1 asserts sup_{0≤t<1} ‖u(t)‖_{L²} < ∞ for the whole localized field, pulses, corrections and cutoff regions included; the heuristic core scale E_core ≍ τ^{1/2−3h} of Section 3.5 concerns only the leading core. MECHANISM: For t < 1 the localized fields are smooth with fixed compact support, so pairing the equation with u gives (10.14) exactly, with no boundary terms: transport and pressure integrate to zero by incompressibility. Dividing by (‖u‖_2² + δ²)^{1/2}, discarding dissipation and using Cauchy-Schwarz gives d/dt (‖u‖_2² + δ²)^{1/2} ≤ ‖f‖_2; integrating from the zero datum and letting δ ↓ 0 gives ‖u(t)‖_2 ≤ F(t). ANTECEDENT: None cited at the lemma. It is the classical energy identity; Section 1.1 cites Leray [16] for the energy inequality of weak solutions. REFS: p. 121, Lemma 10.4, (10.13), (10.14); Section 3.5, pp. 16 to 17.",
"obligation": "Theorem 1.1 asserts sup_{0≤t<1} ‖u(t)‖_{L²} < ∞ for the whole localized field, pulses, corrections and cutoff regions included; the heuristic core scale E_core ≍ τ^{1/2−3h} of Section 3.5 concerns only the leading core.",
"backward_question": "Is the kinetic energy of the whole localized field bounded up to the blowup time, and can that be read off from the force alone instead of tracking the energy of every pulse and correction?",
"mechanism": "For t < 1 the localized fields are smooth with fixed compact support, so pairing the equation with u gives (10.14) exactly, with no boundary terms: transport and pressure integrate to zero by incompressibility. Dividing by (‖u‖_2² + δ²)^{1/2}, discarding dissipation and using Cauchy-Schwarz gives d/dt (‖u‖_2² + δ²)^{1/2} ≤ ‖f‖_2; integrating from the zero datum and letting δ ↓ 0 gives ‖u(t)‖_2 ≤ F(t). Feeding this back into (10.14) bounds the left side of (10.13) by 2 ∫_0^t F′(s) F(s) ds = F(t)². Because Lemma 10.3 makes f smooth and compactly supported through t = 1, F(1) < ∞, and monotone convergence gives finite dissipation on [0, 1). The energy bound is thus a consequence of the smooth extension of the force, not a bookkeeping of the construction's pieces.",
"antecedent": "None cited at the lemma. It is the classical energy identity; Section 1.1 cites Leray [16] for the energy inequality of weak solutions.",
"cost": "None beyond Lemma 10.3, which must come first.",
"checkable": "None: pure estimate. (The outline's heuristic scales on p. 16, E_core ≍ τ^{1/2−3h}, D_core ≍ τ^{−1/2−3h} and ∫_0^{τ_0} τ^{−1/2−3h} dτ = τ_0^{1/2−3h}/(1/2 − 3h) for h < 1/6, are arithmetic but are not what the lemma uses.)",
"depends_on": [
"M10.5",
"M10.2"
],
"constrains": [],
"reasons": {
"M10.5": "F(1) < ∞ because the force is smooth and compactly supported through t = 1.",
"M10.2": "The localized u is smooth, compactly supported and divergence-free, starts from rest, and solves the equation with f = R(u, p)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 121"
},
{
"id": "M10.7",
"kind": "move",
"name": "ns-m10-7-pressure-gradient-identification-with-unrestricted",
"title": "Pressure-gradient identification with unrestricted pressure growth",
"section": "10",
"pages": "121-122",
"refs": [
"pp. 121 to 122, Lemma 10.5 statement, (10.15), (10.16)."
],
"statement": "First step of Lemma 10.5 (fix T < 1; a smooth solution v, P of (1.1) at viscosity one on R³ × [0, T], with the force of Lemma 10.3, zero initial velocity and v ∈ L^∞([0, T]; L²(R³)), equals u there). Set w = v − u, π = P − p, g_ij = v_i v_j − u_i u_j = w_i w_j + w_i u_j + u_i w_j; then ‖w(t)‖_2 ≤ C_T, Σ_{i,j} ‖g_ij(t)‖_1 ≤ C_T, and (10.15): ∂_t w + (v · ∇)w + (w · ∇)u = ∆w − ∇π, div w = 0. Define (10.16), π∗ = Σ_{i,j} R_i R_j g_ij, with R_i the Riesz transform of multiplier i ξ_i/|ξ|;",
"description": "First step of Lemma 10.5 (fix T < 1; a smooth solution v, P of (1.1) at viscosity one on R³ × [0, T], with the force of Lemma 10.3, zero initial velocity and v ∈ L^∞([0, T]; L²(R³)), equals u there). Set w = v − u, π = P − p, g_ij = v_i v_j − u_i u_j = w_i w_j + w_i u_j + u_i w_j; then ‖w(t)‖_2 ≤ C_T, Σ_{i,j} ‖g_ij(t)‖_1 ≤ C_T, and (10.15): ∂_t w + (v · ∇)w + (w · ∇)u = ∆w − ∇π, div w = 0. Define (10.16), π∗ = Σ_{i,j} R_i R_j g_ij, with R_i the Riesz transform of multiplier i ξ_i/|ξ|; OBLIGATION: The competitor's pressure is only assumed smooth, with no growth or integrability condition at spatial infinity (\"no spatial growth condition has been imposed on P\"), so the pressure difference could a priori carry an arbitrary harmonic part. The pressure flux in the localized energy estimate (M10.8) cannot be bounded until ∇π is known. MECHANISM: The common force cancels, so (10.15) contains no force, and its divergence gives ∆π = −Σ ∂_i ∂_j g_ij = ∆π∗, even though f itself is not. ANTECEDENT: None cited for the argument. Riesz transforms are standard; Stein [20] is cited in the next step for their L^p boundedness. REFS: pp. 121 to 122, Lemma 10.5 statement, (10.15), (10.16).",
"obligation": "The competitor's pressure is only assumed smooth, with no growth or integrability condition at spatial infinity (\"no spatial growth condition has been imposed on P\"), so the pressure difference could a priori carry an arbitrary harmonic part. The pressure flux in the localized energy estimate (M10.8) cannot be bounded until ∇π is known.",
"backward_question": "With no growth condition on the competitor's pressure, is its pressure gradient still the one the velocity determines through Riesz transforms, or could a harmonic pressure gradient drive a different flow with the same force and datum?",
"mechanism": "The common force cancels, so (10.15) contains no force, and its divergence gives ∆π = −Σ ∂_i ∂_j g_ij = ∆π∗, even though f itself is not divergence-free. For a ∈ C_c^∞(0, T), integrating the conservative form ∂_t w + div g = ∆w − ∇π against a(t) gives ∫ a ∇π dt = ∆ ∫ a w dt + ∫ a′ w dt − div ∫ a g dt, whose three terms lie in H^{−2}, L² and H^{−3} because w ∈ L^∞_t L²_x and g ∈ L^∞_t L¹_x (Fourier estimate with s = 2). With π∗ ∈ L^∞_t H^{−2}_x, the difference H_a = ∫ a (∇π − ∇π∗) dt lies in H^{−3} and satisfies ∆H_a = 0. A harmonic tempered distribution has Fourier transform supported at the origin, while the Fourier transform of an element of H^{−3} is a weighted L² function, which cannot concentrate on a point; so H_a = 0, and testing in space as well gives ∇π = ∇π∗. This is where the energy hypothesis on v enters: it places the difference in a Sobolev space, which excludes, for instance, a spatially constant pressure gradient, whose Fourier transform is a point mass.",
"antecedent": "None cited for the argument. Riesz transforms are standard; Stein [20] is cited in the next step for their L^p boundedness.",
"cost": "Uses v ∈ L^∞([0, T]; L²(R³)) essentially, to put w in L² and g in L¹. The identification holds in the open interval (0, T), for almost every t.",
"checkable": "None: pure estimate.",
"depends_on": [
"M10.2",
"M10.5"
],
"constrains": [],
"reasons": {
"M10.2": "u, p are the localized fields, smooth with compact support on [0, T], so w = v − u ∈ L² and g_ij ∈ L¹.",
"M10.5": "The competitor carries the same force, which cancels in the difference equation (10.15)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 121-122"
},
{
"id": "M10.8",
"kind": "move",
"name": "ns-m10-8-pressure-flux-through-expanding-balls-by-a-riesz",
"title": "Pressure flux through expanding balls by a Riesz commutator",
"section": "10",
"pages": "122-123",
"refs": [
"pp. 122 to 123, (10.17), (10.18), (10.19)",
"[20] cited on p. 122."
],
"statement": "With 0 ≤ φ ≤ 1 smooth, compactly supported and equal to one on the unit ball, φ_R(x) = φ(x/R) for R ≥ 1, χ_R = φ_R^8, E_R = ∫ χ_R |w|², A_R = (∫ χ_R |∇w|²)^{1/2} and B_R = ‖φ_R^4 w‖_6: (10.17), B_R ≤ C ‖∇(φ_R^4 w)‖_2 ≤ C (A_R + R^{−1} ‖w‖_2); (10.18), φ_R^4 π∗ = Σ R_i R_j (φ_R^4 g_ij) + Σ [φ_R^4, R_i R_j] g_ij. The first sum has L^{3/2} norm at most C_T (B_R + 1).",
"description": "With 0 ≤ φ ≤ 1 smooth, compactly supported and equal to one on the unit ball, φ_R(x) = φ(x/R) for R ≥ 1, χ_R = φ_R^8, E_R = ∫ χ_R |w|², A_R = (∫ χ_R |∇w|²)^{1/2} and B_R = ‖φ_R^4 w‖_6: (10.17), B_R ≤ C ‖∇(φ_R^4 w)‖_2 ≤ C (A_R + R^{−1} ‖w‖_2); (10.18), φ_R^4 π∗ = Σ R_i R_j (φ_R^4 g_ij) + Σ [φ_R^4, R_i R_j] g_ij. The first sum has L^{3/2} norm at most C_T (B_R + 1). OBLIGATION: The pressure flux is the only nonlocal term in the localized difference energy (M10.9). It must be bounded by powers of the local dissipation A_R strictly below 2, with a factor that decays in R, or the limit R → ∞ fails. MECHANISM: After M10.7, π may be replaced by π∗ in the flux. Commuting the cutoff φ_R^4 through the double Riesz transform splits φ_R^4 π∗ into a localized part, bounded in L^{3/2} by the L^p boundedness of Riesz transforms together with ‖φ_R^4 w_i w_j‖_{3/2} ≤ B_R ‖w‖_2 and ‖φ_R^4 w_i u_j‖_{3/2} ≤ ‖w‖_2 ‖u‖_6, and a commutator. ANTECEDENT: Stein [20] for the L^p boundedness of Riesz transforms, 1 < p < ∞. The commutator-kernel bound, the Sobolev inequality and Young's convolution inequality are used without citation. REFS: pp. 122 to 123, (10.17), (10.18), (10.19); [20] cited on p. 122.",
"obligation": "The pressure flux is the only nonlocal term in the localized difference energy (M10.9). It must be bounded by powers of the local dissipation A_R strictly below 2, with a factor that decays in R, or the limit R → ∞ fails.",
"backward_question": "In a localized energy estimate for the difference of two solutions, how can the pressure flux through the boundary of a large ball be controlled when the pressure is a nonlocal function of the velocity and nothing is known about it at infinity?",
"mechanism": "After M10.7, π may be replaced by π∗ in the flux. Commuting the cutoff φ_R^4 through the double Riesz transform splits φ_R^4 π∗ into a localized part, bounded in L^{3/2} by the L^p boundedness of Riesz transforms together with ‖φ_R^4 w_i w_j‖_{3/2} ≤ B_R ‖w‖_2 and ‖φ_R^4 w_i u_j‖_{3/2} ≤ ‖w‖_2 ‖u‖_6, and a commutator whose kernel (φ_R^4(x) − φ_R^4(y)) k(x − y) gains the factor min{|x − y|/R, 1} over the singular kernel |x − y|^{−3} (the multiple of the identity in R_i R_j cancels). Radial integration gives ‖K_R‖_{4/3} ≲ R^{−3/4}, and Young's inequality with g ∈ L¹ gives an L^{4/3} bound that decays in R. The eighth power in χ_R leaves cutoff factors to spare: |∇χ_R| ≤ C R^{−1} φ_R^7, so each piece pairs with R^{−1} φ_R^3 |w|, which interpolates between ‖w‖_2 and B_R: ‖φ_R^3 w‖_3 ≤ ‖φ_R^2 w‖_3 ≤ B_R^{1/2} ‖w‖_2^{1/2} and ‖φ_R^3 w‖_4 ≤ B_R^{3/4} ‖w‖_2^{1/4}. The Sobolev inequality (10.17) controls B_R by local dissipation plus R^{−1}. The identities are proved first for compactly supported smooth truncations of g and then passed to the limit (L¹ convergence, the uniform commutator bound, and H^{−s} convergence of the Riesz transforms); in particular π∗ is locally integrable in space and time.",
"antecedent": "Stein [20] for the L^p boundedness of Riesz transforms, 1 < p < ∞. The commutator-kernel bound, the Sobolev inequality and Young's convolution inequality are used without citation.",
"cost": "Constants C_T depend on T, on sup_{[0,T]} ‖v‖_2, and on ‖u‖_6 over [0, T]. The cutoff power 8 and the weight φ_R^4 in B_R are tuned so that every pairing closes.",
"checkable": "The radial integral behind ‖K_R‖_{4/3}^{4/3} ≤ C R^{−1}: with C = 1, ∫_{R³} (|x|^{−3} min{|x|/R, 1})^{4/3} dx = 4π(3 R^{−1} + R^{−1}) = 16π/R exactly; a sanity run during digestion by quadrature gave 50.2655 at R = 1 and 5.02655 at R = 10, matching 16π/R. The interpolation exponents follow from Hölder: ∫ φ_R^6 |w|³ ≤ B_R^{3/2} ‖w‖_2^{3/2} and ∫ φ_R^{12} |w|⁴ ≤ B_R³ ‖w‖_2. Otherwise a pure estimate.",
"depends_on": [
"M10.7",
"M10.2"
],
"constrains": [],
"reasons": {
"M10.7": "After ∇π = ∇π*, the flux uses π* = ΣR_iR_j g_ij, with ‖w‖_2 ≤ C_T and g_ij ∈ L¹.",
"M10.2": "The localized u is smooth with compact support, so ‖u‖_6 is bounded on [0, T]."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 122-123"
},
{
"id": "M10.9",
"kind": "move",
"name": "ns-m10-9-localized-difference-energy-gronwall-and-r",
"title": "Localized difference energy, Gronwall, and R → ∞",
"section": "10",
"pages": "123",
"refs": [
"p. 123 (difference energy and Gronwall), (10.15), (10.17), (10.19)",
"p. 121 (remark before Lemma 10.5)."
],
"statement": "Pairing (10.15) with χ_R w gives (1/2) E_R′ + A_R² = −∫ χ_R (w · ∇)u · w + (1/2) ∫ |w|² ∆χ_R + (1/2) ∫ |w|² v · ∇χ_R + ∫ π w · ∇χ_R. For R so large that χ_R = 1 on a neighborhood of supp u, one has v = w on supp ∇χ_R, the transport flux is at most C R^{−1} ∫ φ_R^6 |w|³ ≤ C_T R^{−1} B_R^{3/2}, and the Laplacian term is at most C_T R^{−2}.",
"description": "Pairing (10.15) with χ_R w gives (1/2) E_R′ + A_R² = −∫ χ_R (w · ∇)u · w + (1/2) ∫ |w|² ∆χ_R + (1/2) ∫ |w|² v · ∇χ_R + ∫ π w · ∇χ_R. For R so large that χ_R = 1 on a neighborhood of supp u, one has v = w on supp ∇χ_R, the transport flux is at most C R^{−1} ∫ φ_R^6 |w|³ ≤ C_T R^{−1} B_R^{3/2}, and the Laplacian term is at most C_T R^{−2}. OBLIGATION: Closes Lemma 10.5. A global energy identity for w would need decay of the competitor's derivatives and pressure at infinity, which the hypotheses do not provide (\"These hypotheses leave the growth of spatial derivatives at infinity unrestricted\"). MECHANISM: Since u has compact support, outside supp u the difference w is the competitor v itself, so the cubic transport flux and the pressure flux live on the annulus where ∇χ_R is supported and involve only w. ANTECEDENT: None cited. (Structurally it is the classical energy-plus-Gronwall uniqueness argument in which the known smooth solution supplies the Lipschitz norm; the identification is mine.) REFS: p. 123 (difference energy and Gronwall), (10.15), (10.17), (10.19); p. 121 (remark before Lemma 10.5).",
"obligation": "Closes Lemma 10.5. A global energy identity for w would need decay of the competitor's derivatives and pressure at infinity, which the hypotheses do not provide (\"These hypotheses leave the growth of spatial derivatives at infinity unrestricted\").",
"backward_question": "Why does uniqueness hold for smooth bounded-energy solutions with this force and zero datum on each [0, T], T < 1, when nothing is assumed about the competitor's derivatives or pressure at spatial infinity?",
"mechanism": "Since u has compact support, outside supp u the difference w is the competitor v itself, so the cubic transport flux and the pressure flux live on the annulus where ∇χ_R is supported and involve only w. Both are R^{−1} times powers of B_R, hence by (10.17) powers of A_R no larger than 3/2, and Young's inequality absorbs them into half the local dissipation with remainders of order R^{−1} or smaller for R ≥ 1. The only term that is not small is the stretching term, bounded by ‖∇u‖_∞ E_R, and ‖∇u‖_∞ is bounded on [0, T] because T < 1 and u is smooth with compact support there. Gronwall from E_R(0) = 0 gives E_R(t) ≤ C′_T/R, and since χ_R = 1 on any fixed ball once R is large, w vanishes identically.",
"antecedent": "None cited. (Structurally it is the classical energy-plus-Gronwall uniqueness argument in which the known smooth solution supplies the Lipschitz norm; the identification is mine.)",
"cost": "Uniqueness is proved only on [0, T] for each T < 1, because the argument uses ‖∇u‖_∞ on [0, T], which is unbounded as T ↑ 1 (u has fixed compact support and unbounded L^∞ norm). The competitor must be smooth on R³ × [0, T] and lie in L^∞([0, T]; L²(R³)). This step fixes the class in which Theorem 1.1's non-existence is proved.",
"checkable": "None: pure estimate. (The exponent bookkeeping is arithmetic: the fluxes carry A_R to the powers 3/2, 1/2 and 3/4, each below 2, and the corresponding Young remainders are of order R^{−4}, R^{−4/3} and R^{−14/5}, all at most of order R^{−1} for R ≥ 1.)",
"depends_on": [
"M10.8",
"M10.7",
"M10.2"
],
"constrains": [],
"reasons": {
"M10.8": "The pressure-flux bound (10.19) and the Sobolev inequality (10.17) keep every power of A_R below 2.",
"M10.7": "Pairs the difference equation (10.15) with χ_R w.",
"M10.2": "u has compact support, so v = w near supp ∇χ_R for large R, and ‖∇u‖_∞ is bounded on [0, T]."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 123"
},
{
"id": "M10.10",
"kind": "move",
"name": "ns-m10-10-growth-path-classical-lifespan-and-exclusion-of-a-global",
"title": "Growth path, classical lifespan, and exclusion of a global bounded-energy solution",
"section": "10",
"pages": "116",
"refs": [
"p. 116 (Step 5 of the proof of Theorem 3.1, e_0 = E_0(X_in, 0))",
"p. 124, (10.20), (10.21)",
"Theorem 3.1(iv) and (3.6), p. 16",
"Theorem 1.1 and alternative (C), p. 1."
],
"statement": "Proof of Theorem 1.1. The localized field solves the equation exactly on [0, 1) by (10.5), and u ∈ C([0, T]; H³) for each T < 1. Along (10.20), x_τ = (√(2 X_in τ), 0, 0), t = 1 − τ, one has z = 0 and q = τ, the cutoffs of (10.4) equal one for all small τ > 0, and (3.6) gives (10.21): u_θ(x_τ, 1 − τ) = τ^{−A}(e_0 + O(τ^{2h})) → +∞, with x_τ → 0.",
"description": "Proof of Theorem 1.1. The localized field solves the equation exactly on [0, 1) by (10.5), and u ∈ C([0, T]; H³) for each T < 1. Along (10.20), x_τ = (√(2 X_in τ), 0, 0), t = 1 − τ, one has z = 0 and q = τ, the cutoffs of (10.4) equal one for all small τ > 0, and (3.6) gives (10.21): u_θ(x_τ, 1 − τ) = τ^{−A}(e_0 + O(τ^{2h})) → +∞, with x_τ → 0. OBLIGATION: Converts the construction into the non-existence statement of Theorem 1.1 and supplies the blowup lim sup_{t↑1} ‖u(t)‖_{L^∞} = ∞. MECHANISM: On the plane z = 0 the similarity relations give η = 0 and q = τ, so x_τ sits at the fixed similarity point (X, η) = (X_in, 0) inside the inner region, where all annular corrections vanish and the swirl equals q^{−A} times the leading profile value e_0 = E_0(X_in, 0) > 0, up to a relative O(q^{2h}) from the higher-order background terms (Step 5 on p. 116). ANTECEDENT: Fefferman [13], alternative (C), as stated in Section 1; nothing else is cited in the argument. REFS: p. 116 (Step 5 of the proof of Theorem 3.1, e_0 = E_0(X_in, 0)); p. 124, (10.20), (10.21); Theorem 3.1(iv) and (3.6), p. 16; Theorem 1.1 and alternative (C), p. 1.",
"obligation": "Converts the construction into the non-existence statement of Theorem 1.1 and supplies the blowup lim sup_{t↑1} ‖u(t)‖_{L^∞} = ∞.",
"backward_question": "Along which space-time path does the localized velocity provably diverge, does that path stay inside the region where the cutoffs equal one and the inner asymptotics (3.6) hold, and what then forbids a smooth bounded-energy global solution with the same data?",
"mechanism": "On the plane z = 0 the similarity relations give η = 0 and q = τ, so x_τ sits at the fixed similarity point (X, η) = (X_in, 0) inside the inner region, where all annular corrections vanish and the swirl equals q^{−A} times the leading profile value e_0 = E_0(X_in, 0) > 0, up to a relative O(q^{2h}) from the higher-order background terms (Step 5 on p. 116). Since x_τ → 0 and t → 1, the path eventually lies where c = 1, so the localized field inherits (3.6). A global smooth solution is bounded on a compact neighborhood of (0, 1); by Lemma 10.5 on every [0, T] it agrees with u before t = 1, and u is unbounded along x_τ. Contradiction.",
"antecedent": "Fefferman [13], alternative (C), as stated in Section 1; nothing else is cited in the argument.",
"cost": "The conclusion covers only smooth competitors with uniformly bounded kinetic energy (the hypothesis Lemma 10.5 needs on each [0, T]); the maximal-lifespan statement is in the classical H³ class. The rate τ^{−A}, A = 1/2 + h, is proved at the points x_τ; Theorem 1.1 states the blowup as a lim sup, while (10.21) gives the lower bound ‖u(1 − τ)‖_{L^∞} ≥ τ^{−A}(e_0 + O(τ^{2h})) at every small τ.",
"checkable": "From τ = q(1 − η²) and z = q^D η, verify that z = 0 forces η = 0 and q = τ, that X = r²/(2q) = X_in along x_τ, and that |x_τ| = √(2 X_in τ) → 0. Given the realized profiles of (5.1), evaluate τ^A u_θ(x_τ, 1 − τ) − e_0 and check that it is O(τ^{2h}).",
"depends_on": [
"M9.15",
"M10.2",
"M10.9",
"M10.5"
],
"constrains": [],
"reasons": {
"M9.15": "The inner growth (3.6) gives u_θ = τ^{-A}(e_0 + O(τ^{2h})) along X = X_in, z = 0.",
"M10.2": "The cutoffs equal one along the growth path for small τ, so the localized field inherits (3.6).",
"M10.9": "Lemma 10.5 makes any smooth bounded-energy solution with the same data equal u on every [0, T], T < 1.",
"M10.5": "The global competitor is posed with the extended force f ∈ C_c^∞(R³ × (0, ∞)) of Lemma 10.3."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 116"
},
{
"id": "M10.11",
"kind": "move",
"name": "ns-m10-11-viscosity-rescaling",
"title": "Viscosity rescaling",
"section": "10",
"pages": "124",
"refs": [
"p. 124, (10.22), (10.23)",
"p. 7."
],
"statement": "(10.22): u_ν(x, t) = √ν u(x/√ν, t), p_ν(x, t) = ν p(x/√ν, t), f_ν(x, t) = √ν f(x/√ν, t). With y = x/√ν, ∂_t u_ν + (u_ν · ∇_x)u_ν − ν ∆_x u_ν + ∇_x p_ν = √ν [∂_t u + (u · ∇_y)u − ∆_y u + ∇_y p](y, t) = f_ν(x, t) and ∇_x · u_ν = 0. The datum stays zero, the support becomes K_ν = √ν K, time is unchanged, and ∂^α_x ∂^m_t f_ν(x, t) = ν^{(1−|α|)/2} (∂^α_y ∂^m_t f)(x/√ν, t), so f_ν is smooth, supported in K_ν × [0, 2], and satisfies the decay bounds.",
"description": "(10.22): u_ν(x, t) = √ν u(x/√ν, t), p_ν(x, t) = ν p(x/√ν, t), f_ν(x, t) = √ν f(x/√ν, t). With y = x/√ν, ∂_t u_ν + (u_ν · ∇_x)u_ν − ν ∆_x u_ν + ∇_x p_ν = √ν [∂_t u + (u · ∇_y)u − ∆_y u + ∇_y p](y, t) = f_ν(x, t) and ∇_x · u_ν = 0. The datum stays zero, the support becomes K_ν = √ν K, time is unchanged, and ∂^α_x ∂^m_t f_ν(x, t) = ν^{(1−|α|)/2} (∂^α_y ∂^m_t f)(x/√ν, t), so f_ν is smooth, supported in K_ν × [0, 2], and satisfies the decay bounds. OBLIGATION: Everything above is at viscosity one, while Theorem 1.1 is claimed for every ν > 0. MECHANISM: The Navier-Stokes system is invariant under spatial dilation by √ν with velocity multiplied by √ν, pressure by ν and force by √ν at fixed time, which carries viscosity one to viscosity ν. Since time is not rescaled, the singular time stays t = 1; incompressibility, the zero datum, compact support, smoothness and bounded energy all transfer, and the inverse map sends any smooth bounded-energy competitor at viscosity ν to one at viscosity one. ANTECEDENT: None cited (the scaling is announced in Section 3 on p. 7). REFS: p. 124, (10.22), (10.23); p. 7.",
"obligation": "Everything above is at viscosity one, while Theorem 1.1 is claimed for every ν > 0.",
"backward_question": "Does the viscosity-one construction give every positive viscosity without moving the singular time?",
"mechanism": "The Navier-Stokes system is invariant under spatial dilation by √ν with velocity multiplied by √ν, pressure by ν and force by √ν at fixed time, which carries viscosity one to viscosity ν. Since time is not rescaled, the singular time stays t = 1; incompressibility, the zero datum, compact support, smoothness and bounded energy all transfer, and the inverse map sends any smooth bounded-energy competitor at viscosity ν to one at viscosity one.",
"antecedent": "None cited (the scaling is announced in Section 3 on p. 7).",
"cost": "None; the force and the support depend on ν (f_ν, K_ν = √ν K).",
"checkable": "Symbolic chain-rule verification of the identity after (10.22), of the derivative factor ν^{(1−|α|)/2}, and of the factor ν^{5/2} in (10.23) (the Jacobian ν^{3/2} of x = √ν y times the squared amplitude ν).",
"depends_on": [
"M10.5",
"M10.2",
"M10.10"
],
"constrains": [],
"reasons": {
"M10.5": "Rescales the smooth force supported in K × [0, 2], keeping its decay bounds.",
"M10.2": "Rescales the localized u, p, keeping the zero datum, divergence-freeness and compact support K_ν = √νK.",
"M10.10": "Transfers the viscosity-one blowup and exclusion, since a competitor at viscosity ν maps back to viscosity one."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 124"
},
{
"id": "M10.12",
"kind": "move",
"name": "ns-m10-12-periodization-onto-t-corollary-10-6",
"title": "Periodization onto T³ (Corollary 10.6)",
"section": "10",
"pages": "125-126",
"refs": [
"pp. 125 to 126, Corollary 10.6 and its proof",
"[13] cited on p. 125."
],
"statement": "Corollary 10.6 (quoted below). Proof: choose λ > 1 with λ^{−1} K_ν ⋐ Q_0 = (−1/2, 1/2)³ and set t_0 = 1 − λ^{−2}; for t ≥ t_0 put ũ(x, t) = λ u(λx, λ²(t − t_0)), p̃(x, t) = λ² p(λx, λ²(t − t_0)), f̃(x, t) = λ³ f(λx, λ²(t − t_0)), extended by zero for t < t_0 (smooth across t_0 because the original fields and force vanish on an initial interval). Each term of the momentum equation is λ³ times its original value, so the viscosity stays ν, and the original time one is reached exactly at t = 1.",
"description": "Corollary 10.6 (quoted below). Proof: choose λ > 1 with λ^{−1} K_ν ⋐ Q_0 = (−1/2, 1/2)³ and set t_0 = 1 − λ^{−2}; for t ≥ t_0 put ũ(x, t) = λ u(λx, λ²(t − t_0)), p̃(x, t) = λ² p(λx, λ²(t − t_0)), f̃(x, t) = λ³ f(λx, λ²(t − t_0)), extended by zero for t < t_0 (smooth across t_0 because the original fields and force vanish on an initial interval). Each term of the momentum equation is λ³ times its original value, so the viscosity stays ν, and the original time one is reached exactly at t = 1. OBLIGATION: The periodic breakdown alternative (D) in [13], with a periodic pressure \"as required in the erratum to the problem statement [13]\". MECHANISM: Parabolic scaling by λ shrinks the support into the open unit cube and compresses time by λ², and the shift t_0 = 1 − λ^{−2} keeps the singular time at t = 1. Integer translates of fields with disjoint, positively separated supports do not interact, since at every point at most one translate is nonzero, so the periodic sum solves the equation exactly. ANTECEDENT: Fefferman [13] (alternative (D), and the erratum requiring a periodic pressure); otherwise none cited. REFS: pp. 125 to 126, Corollary 10.6 and its proof; [13] cited on p. 125.",
"obligation": "The periodic breakdown alternative (D) in [13], with a periodic pressure \"as required in the erratum to the problem statement [13]\".",
"backward_question": "Can a compactly supported whole-space blowup be transplanted to the torus without the translates interacting through the nonlinearity or the pressure, and with the singular time and viscosity unchanged?",
"mechanism": "Parabolic scaling by λ shrinks the support into the open unit cube and compresses time by λ², and the shift t_0 = 1 − λ^{−2} keeps the singular time at t = 1. Integer translates of fields with disjoint, positively separated supports do not interact, since at every point at most one translate is nonzero, so the periodic sum solves the equation exactly, nonlinear term and pressure included, and the pressure is automatically periodic. On T³ uniqueness is simpler than on R³: periodic integration removes the transport and pressure terms, so Gronwall with ‖∇U‖_∞ closes on each [0, T], T < 1, with no energy or pressure-growth hypothesis.",
"antecedent": "Fefferman [13] (alternative (D), and the erratum requiring a periodic pressure); otherwise none cited.",
"cost": "The force now has time support in [t_0, 1 + λ^{−2}], the solution vanishes for t < t_0, and λ depends on ν through K_ν = √ν K. The non-existence is stated for global smooth periodic solutions with the same datum and force.",
"checkable": "Symbolically confirm that ũ, p̃, f̃ scale every term of the momentum equation by λ³ and that λ²(t − t_0) = 1 exactly at t = 1. For a given K_ν and λ with λ^{−1} K_ν ⋐ Q_0, confirm numerically that the translates λ^{−1} K_ν + k are pairwise disjoint with a positive gap. Confirm (λ x̃_τ, λ²(t̃_τ − t_0)) = (√ν x_τ, 1 − τ), which together with (10.21) and (10.22) gives the stated growth of U_θ.",
"depends_on": [
"M10.11",
"M10.2",
"M10.5",
"M10.10"
],
"constrains": [],
"reasons": {
"M10.11": "Periodizes the viscosity-ν fields supported in K_ν, choosing λ with λ^{-1}K_ν inside the open unit cube Q_0.",
"M10.2": "The fields vanish on an initial time interval and have fixed compact support, so zero extension and disjoint translates work.",
"M10.5": "The force vanishes near t = 0 and has compact time support, so the rescaled periodic force is smooth.",
"M10.10": "The growth (10.21) transfers to U_θ along the rescaled path."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 125-126"
},
{
"id": "MA.1",
"kind": "move",
"name": "ns-ma-1-distinct-power-weights-give-independent-moment-changes",
"title": "Distinct power weights give independent moment changes (Lemma A.1)",
"section": "A",
"pages": "126-127",
"refs": [
"pp. 126 to 127, Lemma A.1, (A.1)",
"restated p. 34 (Lemma 4.7)."
],
"statement": "For distinct real α_1, ..., α_m and nonnegative nonzero smooth bumps β_j supported in the interiors of compact intervals I_1 < ... < I_m in (0, ∞), the matrix B_ij = ∫_0^∞ x^{α_i} β_j(x) dx is invertible; the same holds for exponential weights in a logarithmic coordinate, and the inverse and each fixed parameter derivative stay bounded over a smooth compact family that keeps the separations.",
"description": "For distinct real α_1, ..., α_m and nonnegative nonzero smooth bumps β_j supported in the interiors of compact intervals I_1 < ... < I_m in (0, ∞), the matrix B_ij = ∫_0^∞ x^{α_i} β_j(x) dx is invertible; the same holds for exponential weights in a logarithmic coordinate, and the inverse and each fixed parameter derivative stay bounded over a smooth compact family that keeps the separations. OBLIGATION: Every exact moment restoration in the paper needs the linear map from bump coefficients to moment changes to be invertible with a controlled inverse: Theorem 4.6 Step 3 (4.42), Proposition A.7, Proposition B.8, Proposition C.2, and the order-n solve (5.16) in Lemma 5.2. Without it a local edit could leave a moment discrepancy that propagates to the exterior, and Lemma 4.4(i) could not be invoked. MECHANISM: Multilinearity in the columns gives det B = ∫_{I_1 × ... × I_m} det[x_j^{α_i}] Π_j β_j(x_j) dx. The generalized Vandermonde determinant cannot vanish on 0 < x_1 < ... ANTECEDENT: None cited. The proof names Rolle's theorem (zero counting for sums of distinct powers) and multilinearity of the determinant. REFS: pp. 126 to 127, Lemma A.1, (A.1); restated p. 34 (Lemma 4.7).",
"obligation": "Every exact moment restoration in the paper needs the linear map from bump coefficients to moment changes to be invertible with a controlled inverse: Theorem 4.6 Step 3 (4.42), Proposition A.7, Proposition B.8, Proposition C.2, and the order-n solve (5.16) in Lemma 5.2. Without it a local edit could leave a moment discrepancy that propagates to the exterior, and Lemma 4.4(i) could not be invoked.",
"backward_question": "If I add finitely many fixed bumps to a profile, when do the resulting changes in finitely many power-weighted integrals span every prescribed discrepancy, and how fast does this fail as two weights coalesce?",
"mechanism": "Multilinearity in the columns gives det B = ∫_{I_1 × ... × I_m} det[x_j^{α_i}] Π_j β_j(x_j) dx. The generalized Vandermonde determinant cannot vanish on 0 < x_1 < ... < x_m: otherwise some nonzero combination of the m distinct powers would have m distinct positive zeros, whereas dividing by the lowest power and applying Rolle's theorem inductively shows it has at most m - 1. The ordered cone is connected, so the integrand has one sign and is nonzero on a set of positive measure. The substitution x = e^y gives the logarithmic version; compactness plus differentiation of B^{-1}B = Id gives the uniform bounds. The explicit 2 × 2 determinant (A.1) is proportional to the exponent gap, which quantifies the loss.",
"antecedent": "None cited. The proof names Rolle's theorem (zero counting for sums of distinct powers) and multilinearity of the determinant.",
"cost": "Bumps must have ordered disjoint supports and the exponents within each block must be distinct. A gap of size λ costs λ^{-1} in the inverse, so λ must be fixed before any later large parameter (the radial frequency N of Proposition C.2), or the loss must be absorbed by an exponentially small discrepancy, as in (A.15).",
"checkable": "Compute B for random distinct exponents and rescaled σ' bumps on ordered intervals and check that det B is nonzero with the sign of det[x_j^{α_i}] on the ordered cone; verify (A.1) symbolically; tabulate ‖B^{-1}‖ against λ for the weights (1, x^{-λ}) and (e^{(1/2-λ)y}, e^{(1/2-2λ)y}) to see the λ^{-1} growth.",
"depends_on": [],
"constrains": [],
"reasons": {},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 126-127"
},
{
"id": "MA.2",
"kind": "move",
"name": "ns-ma-2-quadratic-moment-equations-solved-by-contraction-with-c-k",
"title": "Quadratic moment equations solved by contraction with C^k control (Lemma A.2)",
"section": "A",
"pages": "127-128",
"refs": [
"pp. 127 to 128, Lemma A.2, (A.2), (A.3), scaling bound p. 128",
"restated pp. 34 to 35 (Lemma 4.7)."
],
"statement": "Suppose correction coefficients c ∈ R^m change the required moments (after fixed linear combinations and division by fixed nonzero factors) by exactly F_η(c) = B(η)c + Q_η(c, c) (A.2) on K = [-1, 1], with B smooth and invertible and Q smooth bilinear. Put β_0 = sup_K ‖B^{-1}‖, κ_0 = sup_K ‖Q‖, d_0 = ‖d‖_{C^0(K)}. If 8 β_0^2 κ_0 d_0 ≤ 1, then F_η(c) = d(η) has a unique solution in ‖c‖_{C^0} ≤ 2 β_0 d_0, smooth in η and selected by iterating c ↦ B^{-1}(d - Q(c, c)) from zero;",
"description": "Suppose correction coefficients c ∈ R^m change the required moments (after fixed linear combinations and division by fixed nonzero factors) by exactly F_η(c) = B(η)c + Q_η(c, c) (A.2) on K = [-1, 1], with B smooth and invertible and Q smooth bilinear. Put β_0 = sup_K ‖B^{-1}‖, κ_0 = sup_K ‖Q‖, d_0 = ‖d‖_{C^0(K)}. If 8 β_0^2 κ_0 d_0 ≤ 1, then F_η(c) = d(η) has a unique solution in ‖c‖_{C^0} ≤ 2 β_0 d_0, smooth in η and selected by iterating c ↦ B^{-1}(d - Q(c, c)) from zero; OBLIGATION: The moments J, S, C_p are quadratic in (U, E), so an invertible linearization alone does not restore them exactly. The lemma gives exact solutions whose finitely many prescribed η-derivatives are small, and the scaling bound turns this into small field derivatives on the patch, which is what keeps the strict cone inequalities (which involve finitely many field derivatives) intact at every correction. ANTECEDENT: None cited. The proof names the contraction argument in C^0 and in the Banach algebra C^k and the pointwise implicit function theorem. REFS: pp. 127 to 128, Lemma A.2, (A.2), (A.3), scaling bound p. 128; restated pp. 34 to 35 (Lemma 4.7).",
"obligation": "The moments J, S, C_p are quadratic in (U, E), so an invertible linearization alone does not restore them exactly. The lemma gives exact solutions whose finitely many prescribed η-derivatives are small, and the scaling bound turns this into small field derivatives on the patch, which is what keeps the strict cone inequalities (which involve finitely many field derivatives) intact at every correction.",
"backward_question": "The moment functionals are quadratic in the profile; can the finite system be solved exactly, smoothly in η, with bounds on a prescribed finite number of η-derivatives, without demanding smallness at every derivative order at once?",
"mechanism": "On the C^0 ball of radius r = 2 β_0 d_0, the map sends c to a vector of norm at most r/2 + β_0 κ_0 r^2 ≤ r and has Lipschitz constant at most 2 β_0 κ_0 r ≤ 1/2, so it is a contraction. The same argument in the Banach algebra C^k(K) yields (A.3), and because the iterates are identical, the two limits coincide. The same smallness makes B + D_c Q invertible, so the pointwise implicit function theorem gives smoothness in η, including one-sided derivatives at η = ±1; all other fixed derivatives are finite by implicit differentiation, with no simultaneous smallness over all orders. An extra compact parameter (the pulse amplitude) is carried the same way.",
"antecedent": "None cited. The proof names the contraction argument in C^0 and in the Banach algebra C^k and the pointwise implicit function theorem.",
"cost": "The smallness conditions 8 β_0^2 κ_0 d_0 ≤ 1 and 8 β_k^2 κ_k ‖d‖_{C^k} ≤ 1, imposed only for finitely many k; each discrepancy must therefore be made small first (by a large radius, a large frequency, or exponential decay).",
"checkable": "None: pure estimate. Its concrete instances are the finite solves listed under MA.3, MA.5, MA.6 and MA.11, which are checkable there.",
"depends_on": [
"M4.5",
"MA.1"
],
"constrains": [],
"reasons": {
"M4.5": "the equations it solves are exact changes of the cumulative integrals (4.15), in which J, S, Cp are quadratic in (U, E).",
"MA.1": "its invertible linear part B, with bounded η-derivatives of B^{-1}, is the power-weight moment matrix of Lemma A.1."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 127-128"
},
{
"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": "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}; the moment changes have the exact quadratic form (A.2);",
"description": "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}; the moment changes have the exact quadratic form (A.2); 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. ANTECEDENT: None cited beyond Lemma A.1. REFS: p. 128, Corollary A.3, (A.4); used p. 42 (4.42), pp. 139 to 140, pp. 156 to 157, p. 162.",
"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"
},
{
"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": "Fix the smooth step σ of (A.5) and the parameter order (A.6): M_d, then T_d = e^{M_d} + 10, then P∗ > e^{T_d}, then 0 < λ ≪ 1, then 0 < h ≪ min{λ, e^{-T_d}}, and only afterward the large radius X_R. Each stage is written in a local logarithmic coordinate y (d/dy = X∂_X) by prescribing l = X∂_X log H, using (log E)' = l - 1/2: (1) the inner reference (A.7), U = 4η, E = P∗ f(η) e^{y/10}, f = (1 + η^2)^{-1} = e^{-J_0}, J_0 = log(1 + η^2), for y ≤ 0;",
"description": "Fix the smooth step σ of (A.5) and the parameter order (A.6): M_d, then T_d = e^{M_d} + 10, then P∗ > e^{T_d}, then 0 < λ ≪ 1, then 0 < h ≪ min{λ, e^{-T_d}}, and only afterward the large radius X_R. Each stage is written in a local logarithmic coordinate y (d/dy = X∂_X) by prescribing l = X∂_X log H, using (log E)' = l - 1/2: (1) the inner reference (A.7), U = 4η, E = P∗ f(η) e^{y/10}, f = (1 + η^2)^{-1} = e^{-J_0}, J_0 = log(1 + η^2), for y ≤ 0; 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). ANTECEDENT: None cited. The step (A.5) is the standard e^{-1/y^2} gluing function, used without citation. 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"
},
{
"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": "On the pulse 0 ≤ y ≤ 13/λ, l = -λ and U = E R_b with ξ_b = λy, φ_b(ξ_b) = ∫_0^{ξ_b} σ(v/.02) dv, R_0 = φ_b [1 - σ(ξ_b - 10)], R_b = Amp(η) R_0(ξ_b) + c_1 β_1(y) + c_2 β_2(y), the β_i identical translates of width .3 centered at 13/λ - 3 and 13/λ - 1. At pulse start (A.14): e_b ≤ C_pre λ^{30}, ‖A_X(U)/E‖_{C^1_η} ≤ C_pre λ^{29}, ‖S(X_p)/(X_p e_b^2 f^2)‖_{C^1_η} ≤ C_pre(1 + log(1/λ)).",
"description": "On the pulse 0 ≤ y ≤ 13/λ, l = -λ and U = E R_b with ξ_b = λy, φ_b(ξ_b) = ∫_0^{ξ_b} σ(v/.02) dv, R_0 = φ_b [1 - σ(ξ_b - 10)], R_b = Amp(η) R_0(ξ_b) + c_1 β_1(y) + c_2 β_2(y), the β_i identical translates of width .3 centered at 13/λ - 3 and 13/λ - 1. At pulse start (A.14): e_b ≤ C_pre λ^{30}, ‖A_X(U)/E‖_{C^1_η} ≤ C_pre λ^{29}, ‖S(X_p)/(X_p e_b^2 f^2)‖_{C^1_η} ≤ C_pre(1 + log(1/λ)). 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. 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/λ -. ANTECEDENT: None cited. REFS: pp. 130 to 131, (A.14), (A.15).",
"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"
},
{
"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",
"refs": [
"p. 130, (A.10) to (A.13)",
"pp. 131 to 132, (A.16) to (A.18)."
],
"statement": "After the pulse U = 0. The interpolation (A.10), log E = log e_end - (1/2 + λ)y - ϑ_f(y) J_0 - (1 - ϑ_f(y)) log 2, ϑ_f(y) = 1 - σ(y/T_f), makes E η-independent; on the following 30 log(1/λ) hold, two relative E bumps impose (A.11): I = XH/(1 - λ) at the end and ∫_{two bumps} (E^2 - E^2_unedited) dy = 0, with coefficients O_{C^1_η}(C_pre λ^{28}). At the start of the exterior transition, U = M = J = 0 and (4.16) gives Q_s = (λ - h)/(1 - λ) exactly.",
"description": "After the pulse U = 0. The interpolation (A.10), log E = log e_end - (1/2 + λ)y - ϑ_f(y) J_0 - (1 - ϑ_f(y)) log 2, ϑ_f(y) = 1 - σ(y/T_f), makes E η-independent; on the following 30 log(1/λ) hold, two relative E bumps impose (A.11): I = XH/(1 - λ) at the end and ∫_{two bumps} (E^2 - E^2_unedited) dy = 0, with coefficients O_{C^1_η}(C_pre λ^{28}). At the start of the exterior transition, U = M = J = 0 and (4.16) gives Q_s = (λ - h)/(1 - λ) exactly. 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; ANTECEDENT: None cited (integrating-factor solution of a linear first-order ODE). REFS: p. 130, (A.10) to (A.13); pp. 131 to 132, (A.16) to (A.18).",
"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"
},
{
"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"
},
{
"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"
},
{
"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": "With w = N_s/(E Q_s) where Q_s > 0, the sufficient test of Lemma 4.5 is (A.24): a - b_s w > 0 and 2 b_s w + b_s^2/a + (a - 2) w^2 < 2, established with uniform margins on compact ranges, after which p_{s,1} = X Q_s/L is made large by increasing X_R (where v_s ≤ 2 only P_c = p_{s,1}(1 - b_s w/a) > 2 is needed). Stage results: reference, (A.25) Q_s = [(3/5)(4L - 1) - h(1 - 8η^2) + (D + 4d)η J_0']/(8/5) ≥ c > 0, b_s = 0, a = 4/5;",
"description": "With w = N_s/(E Q_s) where Q_s > 0, the sufficient test of Lemma 4.5 is (A.24): a - b_s w > 0 and 2 b_s w + b_s^2/a + (a - 2) w^2 < 2, established with uniform margins on compact ranges, after which p_{s,1} = X Q_s/L is made large by increasing X_R (where v_s ≤ 2 only P_c = p_{s,1}(1 - b_s w/a) > 2 is needed). Stage results: reference, (A.25) Q_s = [(3/5)(4L - 1) - h(1 - 8η^2) + (D + 4d)η J_0']/(8/5) ≥ c > 0, b_s = 0, a = 4/5; 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). ANTECEDENT: None cited (variation of constants; Taylor's formula for the convolution remainder). 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"
},
{
"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"
},
{
"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"
},
{
"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"
},
{
"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"
},
{
"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": "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_θ)^2 has a uniform positive lower bound; for δ = 3 - y small, T_{0,θ} = e^{-4/δ^2} δ^{-3} b_θ(δ, η) with b_θ(0, η) > 0 (A.48), T_{0,z} = e^{-4/δ^2} δ^3 b_z(δ, η) (A.49), T_{0,z}/T_{0,θ} = δ^6 b_z/b_θ → 0 (A.50), and |∂^I T_0| ≤ C_I e^{-4/δ^2} δ^{-N_I}, |T_0| ≥ c e^{-4/δ^2} δ^{-3} (A.51), with constants independent.",
"description": "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_θ)^2 has a uniform positive lower bound; for δ = 3 - y small, T_{0,θ} = e^{-4/δ^2} δ^{-3} b_θ(δ, η) with b_θ(0, η) > 0 (A.48), T_{0,z} = e^{-4/δ^2} δ^3 b_z(δ, η) (A.49), T_{0,z}/T_{0,θ} = δ^6 b_z/b_θ → 0 (A.50), and |∂^I T_0| ≤ C_I e^{-4/δ^2} δ^{-N_I}, |T_0| ≥ c e^{-4/δ^2} δ^{-3} (A.51), with constants independent. 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. ANTECEDENT: None cited. 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"
},