Other material · A dividing-plane barrier in the OpenAI forced Navier-Stokes blow-up construction
The ledger as data, version 1.1, October 1, 2026
The revised ledger in machine-readable form, the version ledger.md shows: GPT-6 Astra's review of the material folded in, and 113 statements replaced after a completeness audit on October 1, 2026, each replacement written by one Claude Opus 5.5 session and checked by a second against the same digest. It is shown here in pages of whole records.
- Written by
- Claude Opus sessions and Claude Fable 5.1 (Anthropic); version 1.1 folds in a review by GPT-6 Astra (OpenAI)
- Size
- 1,021,722 bytes
- SHA-256
73908ae5c651d11684c8a670d84a81bf53cb0cb0e67cb9f29d63dd7dfbfc2aa3
The note's pageEvery file published with itThis file on GitHub
{
"id": "M5.5",
"kind": "move",
"name": "ns-m5-5-lemma-5-1-part-3-smoothness-in-x-at-the-axis-via-volterra",
"title": "Lemma 5.1, part 3: smoothness in X at the axis via Volterra identities and parity",
"section": "5",
"pages": "45-62",
"refs": [
"p48 to p49 (Step 3 of the proof of Lemma 5.1)."
],
"statement": "Step 3 of Lemma 5.1: - (Gg)_i = ξ ∫_0^1 t^{c_i} g_i(tξ) dt; - ∂ξ(Gg)_i = g_i(ξ) - c_i ∫_0^1 t^{c_i} g_i(tξ) dt, which is continuous at ξ = 0. Repeated use gives every radial derivative. The integral equation extends across ξ = 0, and the equations preserve even parity of the first four coordinates and odd parity of the last two. Uniqueness forces these parities. Taylor's formula for an even smooth function of ξ then gives smoothness in X = ξ^2, to every finite order.",
"description": "Step 3 of Lemma 5.1: - (Gg)_i = ξ ∫_0^1 t^{c_i} g_i(tξ) dt; - ∂ξ(Gg)_i = g_i(ξ) - c_i ∫_0^1 t^{c_i} g_i(tξ) dt, which is continuous at ξ = 0. Repeated use gives every radial derivative. The integral equation extends across ξ = 0, and the equations preserve even parity of the first four coordinates and odd parity of the last two. Uniqueness forces these parities. Taylor's formula for an even smooth function of ξ then gives smoothness in X = ξ^2, to every finite order. OBLIGATION: Cartesian smoothness of each coefficient field across the axis for t < 1 (Definition 3.2, via the Cartesian forms (4.4) to (4.5)). It also gives regularity of the next source Ωn/X. MECHANISM: G never differentiates a singular expression. Its derivative identity writes ∂ξ(Gg) through g itself and a smooth average, so regularity in ξ bootstraps (with a smaller η-neighborhood when needed). But smoothness in ξ is not enough. ξ is proportional to r, and smoothness in r does not give smoothness across the axis; ANTECEDENT: None cited. (The even-function fact is classical and often attributed to Whitney; that attribution is mine.) REFS: p48 to p49 (Step 3 of the proof of Lemma 5.1).",
"obligation": "Cartesian smoothness of each coefficient field across the axis for t < 1 (Definition 3.2, via the Cartesian forms (4.4) to (4.5)). It also gives regularity of the next source Ωn/X.",
"backward_question": "The solution is built as a function of ξ = √X, that is, of r. How do I know it is smooth as a function of X ∝ r^2, which is what smoothness across the axis requires?",
"mechanism": "G never differentiates a singular expression. Its derivative identity writes ∂ξ(Gg) through g itself and a smooth average, so regularity in ξ bootstraps (with a smaller η-neighborhood when needed). But smoothness in ξ is not enough. ξ is proportional to r, and smoothness in r does not give smoothness across the axis; what is needed is smoothness in X ∝ r^2. The extended equations are invariant under ξ → -ξ with the stated parities. Uniqueness in the holomorphic class forces the solution to inherit them. An even smooth function of ξ is a smooth function of ξ^2 on the half-interval.",
"antecedent": "None cited. (The even-function fact is classical and often attributed to Whitney; that attribution is mine.)",
"cost": "Nothing new. It relies on the uniqueness class of Lemma 5.1 and may shrink the η-neighborhood per derivative.",
"checkable": "Take test g(ξ) (even or odd polynomials times e^{-ξ^2}) and c ∈ {1, 2, 3}. 1. Compute (Gg)(ξ) = ∫_0^ξ (s/ξ)^c g(s) ds with scipy quad and compare with ξ ∫_0^1 t^c g(tξ) dt. 2. Compare a finite-difference derivative with g(ξ) - c ∫_0^1 t^c g(tξ) dt. 3. Confirm that G maps even g to odd output (the factor ξ), matching the parity split of (5.7).",
"depends_on": [
"M5.4",
"M5.3",
"M4.2"
],
"constrains": [],
"reasons": {
"M5.4": "uniqueness of the Picard solution forces the even and odd parities that the extended equations preserve.",
"M5.3": "differentiates the Volterra operator G of the regular singular system (5.7) in ξ = √X at ξ = 0.",
"M4.2": "its target, smoothness in X rather than ξ ∝ r, is the axis-regularity criterion (4.4) for a smooth Cartesian field."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62",
"analogous_to": [],
"relations": {
"M5.4": "prerequisite",
"M5.3": "prerequisite",
"M4.2": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "digest-only",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M5.6",
"kind": "move",
"name": "ns-m5-6-order-n-stress-primitives-and-the-five-total-moments",
"title": "Order-n stress primitives and the five total moments",
"section": "5",
"pages": "45-62",
"refs": [
"p49 (rθ,n, rz,n, (5.9), (5.10), (5.11), Fn)",
"p50 (mn, Pn)."
],
"statement": "Order-n stress and moments (p. 49-50): rθ,n = (R/C)[right minus left side of (5.3)], rz,n = [right minus left side of (5.4)], R = √(2X), vanish where the inner equations hold; Rj,n = q^{-A-1+λn}rj,n. The stress (5.9), physically q^{-A-1/2+λn}Tn, is Tn,θ = -R^{-2}∫_0^R ϱ²rθ,n dϱ, Tn,z = -R^{-1}∫_0^R ϱrz,n dϱ. The five moments (5.10)-(5.11), functions of η: mn,1 = ∫RUn dR, mn,2 = ∫R²En dR, mn,3 = ∫∂RΠn dR, mn,4 = ∫R²ΣUiEj dR, mn,5 = ∫(RΣUiUj - R²∂RΠn/2)dR; and Pn = (ϕn, Un, Vn/X, Πn, Fn/X), Fn = X AX(Un).",
"description": "Order-n stress and moments (p. 49-50): rθ,n = (R/C)[right minus left side of (5.3)], rz,n = [right minus left side of (5.4)], R = √(2X), vanish where the inner equations hold; Rj,n = q^{-A-1+λn}rj,n. The stress (5.9), physically q^{-A-1/2+λn}Tn, is Tn,θ = -R^{-2}∫_0^R ϱ²rθ,n dϱ, Tn,z = -R^{-1}∫_0^R ϱrz,n dϱ. The five moments (5.10)-(5.11), functions of η: mn,1 = ∫RUn dR, mn,2 = ∫R²En dR, mn,3 = ∫∂RΠn dR, mn,4 = ∫R²ΣUiEj dR, mn,5 = ∫(RΣUiUj - R²∂RΠn/2)dR; and Pn = (ϕn, Un, Vn/X, Πn, Fn/X), Fn = X AX(Un). OBLIGATION: The order-n residual must be written as minus the cylindrical divergence of a stress supported in the annulus, the only place waves can supply it. The forward primitive from the axis vanishes wherever the inner equations hold. But beyond the source support it equals R^{-2} (or R^{-1}) times the total moment. ANTECEDENT: None cited. Internal: - Proposition 4.2, the leading stress by radial integration; - (4.15) and Lemma 4.4; - the remark after (4.19) that, without total moment identities, a zero exterior residual could leave stresses proportional to r^{-2} and r^{-1} (Lemma A.8). REFS: p49 (rθ,n, rz,n, (5.9), (5.10), (5.11), Fn); p50 (mn, Pn).",
"obligation": "The order-n residual must be written as minus the cylindrical divergence of a stress supported in the annulus, the only place waves can supply it. The forward primitive from the axis vanishes wherever the inner equations hold. But beyond the source support it equals R^{-2} (or R^{-1}) times the total moment. A bare radial cutoff also leaves an exterior pressure constant and an exterior streamfunction.",
"backward_question": "Integrating the order-n residual from the axis gives a stress that vanishes near the axis. Which finitely many global integrals of the order-n profile must vanish so that this stress also vanishes past the correction support, and so that pressure and streamfunction leave no exterior constants?",
"mechanism": "R^2 and R are the integrating factors of ∂R + 2/R (flux of angular momentum) and ∂R + 1/R (flux of axial momentum). So (5.9) is the primitive regular at the axis, and it vanishes past the source support exactly when ∫R^2 rθ,n dR = ∫R rz,n dR = 0. The five moments are the order-n analogs of the cumulative integrals (4.15): - mn,1 is the analog of M (radially integrated axial momentum, which is also the streamfunction at infinity); - mn,2 of I (angular momentum); - mn,3 of Cp (pressure increment from the axis to infinity); - mn,4 of J (axial transport of angular momentum); - mn,5 of S (axial momentum flux including pressure). M5.9 proves that these five conditions force both total residual integrals to vanish.",
"antecedent": "None cited. Internal: - Proposition 4.2, the leading stress by radial integration; - (4.15) and Lemma 4.4; - the remark after (4.19) that, without total moment identities, a zero exterior residual could leave stresses proportional to r^{-2} and r^{-1} (Lemma A.8).",
"cost": "Five scalar constraints at every order, each a function of η.",
"checkable": "1. Take a compactly supported test pair (rθ, rz) on 1 ≤ R ≤ 2 and compute T by (5.9) with scipy quad. 2. Verify (∂R + 2/R)Tθ = -rθ and (∂R + 1/R)Tz = -rz by finite differences. 3. Verify that for R > 2, Tθ = -R^{-2} ∫ ϱ^2 rθ dϱ and Tz = -R^{-1} ∫ ϱ rz dϱ. 4. Subtract a bump multiple from the test residual to zero each moment, and confirm the tails then vanish.",
"depends_on": [
"M4.4",
"M5.2",
"M4.5"
],
"constrains": [],
"reasons": {
"M4.4": "the primitives (5.9) repeat Proposition 4.2's radial integration from the axis, with integrating factors R² and R.",
"M5.2": "the residual coefficients r_θ,n and r_z,n are the right minus left sides of (5.3) and (5.4).",
"M4.5": "defines the five total moments m_n on the pattern of the cumulative integrals M, I, Cp, J, S of (4.15), taken at infinity."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62",
"analogous_to": [],
"relations": {
"M4.4": "prerequisite",
"M5.2": "prerequisite",
"M4.5": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M5.7",
"kind": "move",
"name": "ns-m5-7-radial-extension-by-a-cutoff-plus-five-reserved-patch",
"title": "Radial extension by a cutoff plus five reserved-patch bumps, and the affine block moment solve",
"section": "5",
"pages": "45-62",
"refs": [
"p50 (Lemma 5.2 statement, Step 1, X- < Xkeep < Xcut < a^2 < inf Ipos, κ, bumps)",
"p51 ((5.14), (5.15), Step 2, E0 on Ipos, the mn,5 rewrite, ∂RΠn, B_U, B_E)",
"p52 (d_{U,n}, d_{E,n}, Lemma A.1, (5.16))."
],
"statement": "Lemma 5.2, Steps 1-2 (p. 50-52): fix X- < Xkeep < Xcut < a² < inf Ipos and an η-independent cutoff κ (1 on [0, Xkeep], 0 for X ≥ Xcut). Set Un = κUn^in + Σ_{j≤2}αn,j(η)b^U_j(R), En = κEn^in + Σ_{j≤3}βn,j(η)b^E_j(R) (5.14), with fixed unit-mass bumps in Jpos, and rebuild Fn, Vn, Πn by (5.15). On Ipos (U0 = 0, E0 = e∗fR^{-1-2λ}) the moments are affine in (αn, βn): mn = 0 iff B_Uαn = -d_{U,n}, B_Eβn = -d_{E,n}, with B_U, B_E moment matrices of distinct powers, invertible by Lemma A.1; so (5.16) αn = -B_U^{-1}d_{U,n}, βn = -B_E^{-1}d_{E,n}.",
"description": "Lemma 5.2, Steps 1-2 (p. 50-52): fix X- < Xkeep < Xcut < a² < inf Ipos and an η-independent cutoff κ (1 on [0, Xkeep], 0 for X ≥ Xcut). Set Un = κUn^in + Σ_{j≤2}αn,j(η)b^U_j(R), En = κEn^in + Σ_{j≤3}βn,j(η)b^E_j(R) (5.14), with fixed unit-mass bumps in Jpos, and rebuild Fn, Vn, Πn by (5.15). On Ipos (U0 = 0, E0 = e∗fR^{-1-2λ}) the moments are affine in (αn, βn): mn = 0 iff B_Uαn = -d_{U,n}, B_Eβn = -d_{E,n}, with B_U, B_E moment matrices of distinct powers, invertible by Lemma A.1; so (5.16) αn = -B_U^{-1}d_{U,n}, βn = -B_E^{-1}d_{E,n}. OBLIGATION: The inner solution lives only on [0, a^2]. The order-n profiles must: - be defined for all X ≥ 0, with (5.2) and (5.5) holding globally. This means exact incompressibility and exact radial balance, since the waves supply only the rθ and rz stresses and. REFS: p50 (Lemma 5.2 statement, Step 1, X- < Xkeep < Xcut < a^2 < inf Ipos, κ, bumps); p51 ((5.14), (5.15), Step 2, E0 on Ipos, the mn,5 rewrite, ∂RΠn, B_U, B_E); p52 (d_{U,n}, d_{E,n}, Lemma A.1, (5.16)).",
"obligation": "The inner solution lives only on [0, a^2]. The order-n profiles must: - be defined for all X ≥ 0, with (5.2) and (5.5) holding globally. This means exact incompressibility and exact radial balance, since the waves supply only the rθ and rz stresses and nothing in the radial equation; - equal the inner solution on [0, X-]; - keep the η-analyticity on [0, a^2] that the next order needs; - zero the five moments.",
"backward_question": "Where can I add finitely many adjustable profiles so that the five moment conditions become a linear system invertible uniformly in η? It must not disturb the inner solution, its analytic region, the exterior heat flow, or the patch reserved for mean corrections.",
"mechanism": "κ is η-independent and the bumps vanish on [0, a^2], so the reconstructed profiles there are the analytic inner ones. On [0, X-], forward integration from zero axis data reproduces the inner solution exactly. The bumps sit on the reserved patch, where the leading profile has no axial velocity and a pure-power swirl. This decouples the moments: - U-bumps enter only mn,1 (weight R) and mn,4 (through R^2E0Un, weight R^{1-2λ}); - E-bumps enter only mn,2 (weight R^2), mn,3 (through ∂RΠn = 2E0En/R + ..., weight R^{-2-2λ}), and mn,5. - For mn,5, the pressure equation rewrites the moment as ∫(ΣUiUj - (1/2)ΣEiEj + (1/2)Ω_{n-1}) dX, so the E-bumps enter with weight R^{-2λ}. After dividing by e∗f(η), the matrices are η-independent moment matrices of distinct powers against ordered disjoint bumps. They are invertible by Lemma A.1: a nonzero combination of m distinct powers has at most m - 1 positive zeros, so the determinant integrand has one sign. Since i + j = n never pairs two order-n factors, the system is affine. It is solved for discrepancies of any size, with no smallness needed. This differs from the quadratic moment systems of Section 4, which needed Lemma A.2.",
"antecedent": "No external citation. Internal: - Lemma A.1 (restated as Lemma 4.7), which the manuscript proves by Rolle's theorem and multilinearity of the determinant; - the reserved patch of Theorem 4.6(vi) and (4.30).",
"cost": "- It uses the reserved interval Ipos at every order. - The coefficients αn, βn are not small and grow with n. - The bumps and the cutoff transition add order-n stress inside the annulus. - Distinct exponents require λ > 0. The inverse bound noted after Lemma A.1 degrades like O(λ^{-1}) as exponents merge, which is harmless for fixed λ.",
"checkable": "1. Choose λ, say 0.02; the paper fixes λ but does not give its value. 2. Place five standard mollifier bumps on disjoint ordered subintervals of an R-interval. 3. Compute B_U (2 by 2) and B_E (3 by 3) by quadrature and confirm the determinants are nonzero. 4. Track condition numbers as λ decreases toward 0; expect B_U to grow like λ^{-1}. 5. With test lower-order profiles, compute the five moments by quadrature for random (α, β). 6. Confirm the map is affine with Jacobian rows (B_U)_{1·}, e∗f (B_U)_{2·}, (B_E)_{1·}, 2e∗f (B_E)_{2·}, -e∗f (B_E)_{3·}, and that solving (5.16) zeros all five moments.",
"depends_on": [
"M5.6",
"MA.1",
"M5.3",
"M4.8"
],
"constrains": [],
"reasons": {
"M5.6": "the five bump coefficients are fixed by zeroing the total moments m_n of (5.10), (5.11).",
"MA.1": "B_U and B_E are distinct-power moment matrices against ordered disjoint bumps, invertible by Lemma A.1, giving (5.16).",
"M5.3": "it cuts off the inner solution of Lemma 5.1, kept exactly on [0, X_keep] with its analytic region [0, a²] untouched.",
"M4.8": "the bumps sit on the reserved patch I_pos of Theorem 4.6(vi), where U0 = 0 and E0 is a pure power, which decouples the moments."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62",
"analogous_to": [],
"relations": {
"M5.6": "prerequisite",
"MA.1": "prerequisite",
"M5.3": "prerequisite",
"M4.8": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M5.8",
"kind": "move",
"name": "ns-m5-8-support-closure-past-x-and-exact-vanishing-on-the-mean",
"title": "Support closure past X+ and exact vanishing on the mean patch",
"section": "5",
"pages": "45-62",
"refs": [
"p52 (Step 3, (5.17), (5.18), the remark on Ω0)."
],
"statement": "Lemma 5.2, Step 3 (p. 52): with X+ beyond the leading axial-velocity perturbation (hence beyond Xv), beyond every positive-order patch and before the terminal collar, the zero moments give Fn = Vn = 0 and Πn = 0 for X ≥ X+, since every Ωk term has a V factor and each ϕiϕj (i + j = n ≥ 1) a positive-order factor. Hence (5.12) supp_X Pn ⊂ [0, X+] with mn = 0; Fn/X and Vn/X are smooth at the axis; (5.17) max_{k+ℓ≤m} sup |∂X^k∂η^ℓPn| ≤ C_{n,m}; and (5.18) En = Un = Fn = Vn = 0 on the mean patch Imean for every n ≥ 1.",
"description": "Lemma 5.2, Step 3 (p. 52): with X+ beyond the leading axial-velocity perturbation (hence beyond Xv), beyond every positive-order patch and before the terminal collar, the zero moments give Fn = Vn = 0 and Πn = 0 for X ≥ X+, since every Ωk term has a V factor and each ϕiϕj (i + j = n ≥ 1) a positive-order factor. Hence (5.12) supp_X Pn ⊂ [0, X+] with mn = 0; Fn/X and Vn/X are smooth at the axis; (5.17) max_{k+ℓ≤m} sup |∂X^k∂η^ℓPn| ≤ C_{n,m}; and (5.18) En = Un = Fn = Vn = 0 on the mean patch Imean for every n ≥ 1. OBLIGATION: Positive orders must not touch the exterior heat flow (4.29), whose residual is identically zero; Theorem 3.1(iii) and the localization need this. They must also leave the mean patch Imean exactly at the leading power law, with zero axial velocity, for the corrections of Section 8. MECHANISM: A radially integrated field vanishes past a support radius exactly when its total integral vanishes. The streamfunction vanishes by mn,1. The radial velocity then vanishes by (5.2). REFS: p52 (Step 3, (5.17), (5.18), the remark on Ω0).",
"obligation": "Positive orders must not touch the exterior heat flow (4.29), whose residual is identically zero; Theorem 3.1(iii) and the localization need this. They must also leave the mean patch Imean exactly at the leading power law, with zero axial velocity, for the corrections of Section 8.",
"backward_question": "Once the moments are zeroed, do all radially integrated fields vanish beyond a single n-independent radius, and what constrains where that radius may sit?",
"mechanism": "A radially integrated field vanishes past a support radius exactly when its total integral vanishes. The streamfunction vanishes by mn,1. The radial velocity then vanishes by (5.2). The pressure vanishes by mn,3, once its radial derivative vanishes. That radial derivative contains Ω_{n-1}, which involves the leading radial velocity V0, nonzero until Xv. The manuscript: \"placing X+ beyond the leading axial-velocity perturbation is essential for the pressure support: Ω0 can remain nonzero beyond the positive-order patches.\" Imean lies to the right of both the inner cutoff and Ipos (sup Ipos < inf Imean). There, En = Un = 0 by construction. Fn = 0 because the axial flux has already been zeroed once Ipos is passed, and then Vn = 0 by (5.2).",
"antecedent": "None cited. Internal: Theorem 4.6(v) (U = V0 = 0 on [Xv, ∞)) and Theorem 4.6(vi) (Ipos and Imean lie in (Xa, Xv), with sup Ipos < inf Imean).",
"cost": "- Positive-order corrections occupy [X-, X+], a subinterval of the wave annulus. - The pressure corrections Πn need not vanish on Imean; only the velocity components are claimed to. - The constants C_{n,m} are uncontrolled in n.",
"checkable": "A toy order-one computation. 1. Prescribe smooth test lower-order data with U0 = V0 = 0 beyond a radius Xv. 2. Build (5.14) with coefficients from (5.16) and reconstruct (5.15) by cumulative quadrature. 3. Confirm that Fn, Vn, Πn vanish on [X+, 2X+] to quadrature tolerance. 4. With α = β = 0 instead, confirm they tend to nonzero constants: m^0_{n,1} for Fn and m^0_{n,3} for Πn.",
"depends_on": [
"M5.7",
"M4.8",
"M5.2"
],
"constrains": [],
"reasons": {
"M5.7": "the zeroed moments m_n,1 and m_n,3 from the bump solve make the streamfunction and pressure vanish past the patches.",
"M4.8": "X+ lies beyond X_v, where Theorem 4.6(v) gives U = V0 = 0, and I_mean lies right of I_pos by Theorem 4.6(vi).",
"M5.2": "V_n follows from A_X(U_n) by (5.2), and Π_n' from (5.5), whose Ω_{n-1} terms all carry a V factor."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62",
"analogous_to": [],
"relations": {
"M5.7": "prerequisite",
"M4.8": "prerequisite",
"M5.2": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M5.9",
"kind": "move",
"name": "ns-m5-9-conservative-forms-make-the-total-tangential-residual",
"title": "Conservative forms make the total tangential residual integrals vanish",
"section": "5",
"pages": "45-62",
"refs": [
"p53 (conservative forms, moment scalings, (5.19), (5.20), (5.21))",
"p54 (removal of powers, backward representation)."
],
"statement": "Lemma 5.2, Step 4 (p. 53-54): for smooth axisymmetric divergence-free fields, r²Rθ and rRz are conservative (sums of ∂t, ∂r, ∂z, ∂zz of fluxes). Integrating in r, with the moment scalings (5.20) (e.g. ∫r uz,n dr = q^{1-A+λn}∫RUn dR), ∫RΠn dR = -(1/2)∫R²∂RΠn dR, and at n = 1 the identity (5.19) ∫_0^∞ r²(uθ,0 - P)dr = 0, the five vanishing moments give (5.21): ∫r²Rθ,n dr = ∫rRz,n dr = 0. Hence ∫R²rθ,n dR = ∫Rrz,n dR = 0, and (5.9) equals the backward form Tn,θ = R^{-2}∫_R^∞ ϱ²rθ,n dϱ, Tn,z = R^{-1}∫_R^∞ ϱrz,n dϱ.",
"description": "Lemma 5.2, Step 4 (p. 53-54): for smooth axisymmetric divergence-free fields, r²Rθ and rRz are conservative (sums of ∂t, ∂r, ∂z, ∂zz of fluxes). Integrating in r, with the moment scalings (5.20) (e.g. ∫r uz,n dr = q^{1-A+λn}∫RUn dR), ∫RΠn dR = -(1/2)∫R²∂RΠn dR, and at n = 1 the identity (5.19) ∫_0^∞ r²(uθ,0 - P)dr = 0, the five vanishing moments give (5.21): ∫r²Rθ,n dr = ∫rRz,n dr = 0. Hence ∫R²rθ,n dR = ∫Rrz,n dR = 0, and (5.9) equals the backward form Tn,θ = R^{-2}∫_R^∞ ϱ²rθ,n dϱ, Tn,z = R^{-1}∫_R^∞ ϱrz,n dϱ. OBLIGATION: Proves that zeroing the five moments makes the order-n stress vanish past the correction support, so the forward and backward primitives coincide. MECHANISM: Integrating the conservative forms in r removes all radial flux terms: axis parity handles r = 0, and compact positive-order support handles infinity. What remains is ∂t and ∂z of radial integrals: - angular momentum (mn,2); - axial transport of angular momentum (mn,4); - axial flux (mn,1); ANTECEDENT: None cited. Internal: (4.28), (A.45), and Lemma A.8 (the same argument at order zero). REFS: p53 (conservative forms, moment scalings, (5.19), (5.20), (5.21)); p54 (removal of powers, backward representation).",
"obligation": "Proves that zeroing the five moments makes the order-n stress vanish past the correction support, so the forward and backward primitives coincide.",
"backward_question": "Which terms of the tangential residual survive integration against r^2 dr and r dr? Are five moments exactly enough to kill them all, including the pressure contribution and the axial viscosity inherited from the previous order?",
"mechanism": "Integrating the conservative forms in r removes all radial flux terms: axis parity handles r = 0, and compact positive-order support handles infinity. What remains is ∂t and ∂z of radial integrals: - angular momentum (mn,2); - axial transport of angular momentum (mn,4); - axial flux (mn,1); - axial momentum flux including pressure (mn,5, after integrating the pressure by parts); - the order n-1 integrals hit by axial viscosity, which vanish by the previous order's moments, or at order zero by (4.28). The product power q^{...+λn} does not depend on the split i + j = n. So each integral vanishes identically in (z, t) before the physical derivatives are taken. At n = 1 the leading angular momentum integral diverges, since uθ,0 decays like r^{-1-2h}. The z-independent pure power P, which ∂zz does not see, is therefore subtracted. Differentiation under the integral is justified because beyond the terminal collar uθ,0 = K(r, t) is z-independent.",
"antecedent": "None cited. Internal: (4.28), (A.45), and Lemma A.8 (the same argument at order zero).",
"cost": "Order one depends on the renormalized angular moment identity of the leading construction. The resulting representation is for a signed stress; there is no positivity.",
"checkable": "1. Symbolic (sympy): take ur = -∂zS/r and uz = ∂rS/r for a generic S(r, z, t), with generic uθ and p. Expand r^2 times the azimuthal residual and r times the axial residual, and confirm they equal the displayed conservative forms. 2. Quadrature: for compactly supported test En(R) and Πn(R), confirm ∫r^2uθ,n dr / (q^{3/2-A+λn}∫R^2En dR) = 1 with r = √q R. 3. Confirm ∫RΠn dR = -(1/2)∫R^2∂RΠn dR.",
"depends_on": [
"M5.8",
"M5.6",
"MA.12",
"M4.8"
],
"constrains": [],
"reasons": {
"M5.8": "uses m_n = 0 and the compact support of positive orders in [0, X+] to drop the flux terms at infinity.",
"M5.6": "the conservative forms reduce the weighted residual integrals to derivatives of the moments (5.10), (5.11), giving the backward form of (5.9).",
"MA.12": "repeats Lemma A.8's order-zero argument; at n = 1 it subtracts the pure-power exterior P of (A.45) so the angular moment converges.",
"M4.8": "the n = 1 axial-viscosity term needs the order-zero identities (4.28) and the z-independent heat exterior (4.29)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62",
"analogous_to": [],
"relations": {
"M5.8": "prerequisite",
"M5.6": "prerequisite",
"MA.12": "prerequisite",
"M4.8": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: TRUNCATED; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M5.10",
"kind": "move",
"name": "ns-m5-10-order-one-stress-at-the-outer-edge-is-flat-at-the-rate-of",
"title": "Order-one stress at the outer edge is flat at the rate of ζ",
"section": "5",
"pages": "45-62",
"refs": [
"p54 (Step 5, az, bz, bounds on fo, Lemma A.9, (5.22))",
"p50 ((5.13))",
"p44 (definition of ζ in the proof of Theorem 4.6)."
],
"statement": "Lemma 5.2, Step 5, and (5.13) (p. 50, 54): for n ≥ 2, supp Tn ⊂ [X-, X+] and every derivative of Tn/ζ is bounded. For n = 1 the only exterior source is -∂zz uθ,0 on the terminal collar, where uθ,0 = K fo with 1 - fo = e^{-4/δb²} times a smooth factor, δb = log(Xb/X); so supp T1 ⊂ [X-, Xb], and Lemma A.9 gives (5.22): |T1| ≤ Ce^{-4/δb²}δb^{-3}, |∂^IT1| ≤ C_Ie^{-4/δb²}δb^{-N_I}. With ζ = exp(-ca/ya² - 4/yb²) this yields (5.13): |∂^ITn| ≤ C_{n,I}ζδ^{-N_{n,I}} on Xa < X < Xb for every n ≥ 1.",
"description": "Lemma 5.2, Step 5, and (5.13) (p. 50, 54): for n ≥ 2, supp Tn ⊂ [X-, X+] and every derivative of Tn/ζ is bounded. For n = 1 the only exterior source is -∂zz uθ,0 on the terminal collar, where uθ,0 = K fo with 1 - fo = e^{-4/δb²} times a smooth factor, δb = log(Xb/X); so supp T1 ⊂ [X-, Xb], and Lemma A.9 gives (5.22): |T1| ≤ Ce^{-4/δb²}δb^{-3}, |∂^IT1| ≤ C_Ie^{-4/δb²}δb^{-N_I}. With ζ = exp(-ca/ya² - 4/yb²) this yields (5.13): |∂^ITn| ≤ C_{n,I}ζδ^{-N_{n,I}} on Xa < X < Xb for every n ≥ 1. OBLIGATION: Later sections build wave amplitudes on the weight ζ; amplitudes carry √ζ in the class W_α. They must also absorb the higher-order stress by signed corrections. So that stress must vanish at the annulus edges as fast as ζ, up to finite inverse powers of δ. Without Step 5, T1 could reach the outer edge Xb at a rate not dominated by ζ. MECHANISM: At order one, inside the terminal collar, the leading swirl is the heat field times a terminal multiplier fo(log X). Since X = s/q depends on z, axial viscosity produces a source built from ∂y fo. REFS: p54 (Step 5, az, bz, bounds on fo, Lemma A.9, (5.22)); p50 ((5.13)); p44 (definition of ζ in the proof of Theorem 4.6).",
"obligation": "Later sections build wave amplitudes on the weight ζ; amplitudes carry √ζ in the class W_α. They must also absorb the higher-order stress by signed corrections. So that stress must vanish at the annulus edges as fast as ζ, up to finite inverse powers of δ. Without Step 5, T1 could reach the outer edge Xb at a rate not dominated by ζ.",
"backward_question": "At order one the leading exterior is not compactly supported and depends on z inside the terminal collar. Does axial viscosity acting on it leave stress at the outer edge, and does that stress vanish as fast as the weight ζ that controls the wave amplitudes?",
"mechanism": "At order one, inside the terminal collar, the leading swirl is the heat field times a terminal multiplier fo(log X). Since X = s/q depends on z, axial viscosity produces a source built from ∂y fo and ∂yy fo. These are flat at Xb at the rate e^{-4/δb^2}, the same exponent as the outer factor of ζ and as the outer rate (4.32) of T0. The backward representation of M5.9 integrates this source inward from the edge. Lemma A.9 (substitution u = δ/(1 + δ^2v)^{1/2}) gives ∫_0^δ e^{-c/u^2} u^{-j} b(u, η) du = (1/2) e^{-c/δ^2} δ^{3-j} B(δ, η), with B smooth and B(0, η) = b(0, η)/c. In words: integrating a flat factor from the edge gains δ^3. Derivatives cost only finite inverse powers of δb. Near the inner edge, T1 vanishes identically on [0, X-].",
"antecedent": "None cited. Internal: Lemma A.9, the terminal multiplier (A.12), the heat profile (4.29), and the edge factorization (4.32).",
"cost": "Unlike Tn for n ≥ 2, T1 reaches the outer edge Xb, with a finite inverse-power loss δ^{-N}. Later stages must accept stress weighted by ζ δ^{-N}.",
"checkable": "1. mpmath at 40 digits: for c = 4, j ∈ {3, 6} and b ≡ 1, compute I(δ) = ∫_0^δ e^{-4/u^2} u^{-j} du after the substitution w = u^{-2}, which removes the endpoint peak. Use δ = 0.3, 0.1, 0.05, 0.02. 2. Compare I(δ)/((1/2) e^{-4/δ^2} δ^{3-j}) with b(0)/c = 0.25; for j = 3 the ratio is exactly 1/c. I ran this while digesting: j = 3 gives 0.25, and j = 6 gives 0.2585, 0.2509, 0.2502, 0.25004. 3. Symbolically, verify the ∂zz(K fo) formula from the chain rule of Lemma 4.1 (X_z = -2ηX/(q^D L), Z_b of (4.2)), with K independent of z.",
"depends_on": [
"MA.13",
"M5.9",
"M4.15",
"MA.14"
],
"constrains": [],
"reasons": {
"MA.13": "Lemma A.9 with c = 4, j = 3, 6 factors e^{-4/δ_b²} out of the backward integral of the order-one source, gaining δ_b³ in (5.22).",
"M5.9": "integrates the order-one residual inward from the edge with the backward stress form that the zeroed moments make valid.",
"M4.15": "the target weight ζ = exp(-c_a/y_a² - 4/y_b²) is defined in Step 4 of the proof of Theorem 4.6.",
"MA.14": "on the terminal collar u_θ,0 = K f_o with f_o' flat at the rate e^{-4/δ²}δ^{-3}, the same exponent as the outer factor of ζ."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62",
"analogous_to": [],
"relations": {
"MA.13": "prerequisite",
"M5.9": "prerequisite",
"M4.15": "prerequisite",
"MA.14": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M5.11",
"kind": "move",
"name": "ns-m5-11-finite-truncations-the-residual-gain-grows-with-n-the",
"title": "Finite truncations: the residual gain grows with N, the derivative loss does not",
"section": "5",
"pages": "45-62",
"refs": [
"p54 (plan of subsection 5.3)",
"p55 ((5.23), (5.24), Proposition 5.3, (5.25), proof Step 1, (5.26))",
"p56 (chain rule, r^{-1} factor)."
],
"statement": "Proposition 5.3. Define: - U^[N] = Σ_{n=0}^N (un, pn, q^{-A-1/2+λn} Tn), where the profiles include their cutoffs and moment corrections; - (5.24): Fslow(u, p, T) = R(u, p) + (∂r + 2/r)Tθ eθ + (∂r + 1/r)Tz ez; - (5.23): |V|_m = max_{|α|+b≤m} |∂x^α ∂t^b V|. Then each u^[N]_slow is divergence-free, and (5.25) holds: |Fslow(U^[N])|_m ≤ C_{N,m} q^{2h(N+1)-Km} on 0 ≤ X ≤ Xmax, -1 ≤ η ≤ 1, 0 < q ≤ 1, with Km independent of N.",
"description": "Proposition 5.3. Define: - U^[N] = Σ_{n=0}^N (un, pn, q^{-A-1/2+λn} Tn), where the profiles include their cutoffs and moment corrections; - (5.24): Fslow(u, p, T) = R(u, p) + (∂r + 2/r)Tθ eθ + (∂r + 1/r)Tz ez; - (5.23): |V|_m = max_{|α|+b≤m} |∂x^α ∂t^b V|. Then each u^[N]_slow is divergence-free, and (5.25) holds: |Fslow(U^[N])|_m ≤ C_{N,m} q^{2h(N+1)-Km} on 0 ≤ X ≤ Xmax, -1 ≤ η ≤ 1, 0 < q ≤ 1, with Km independent of N. OBLIGATION: Supplies the finite-residual hypothesis (5.33) of Lemma 5.4, with ρN = 2h(N+1) and no flat remainder. The gain must grow with N while the loss from physical differentiation stays fixed. MECHANISM: At every retained order: - (5.2) gives exact incompressibility; - (5.5) holds globally, so the radial residual is canceled; - differentiating the primitives gives (∂R + 2/R)Tn,θ = -rθ,n and (∂R + 1/R)Tn,z = -rz,n, so the tangential residual is exactly minus the stress divergence; - order zero holds by Proposition 4.2. ANTECEDENT: None cited. Internal: Lemma 4.1 and Proposition 4.2. REFS: p54 (plan of subsection 5.3); p55 ((5.23), (5.24), Proposition 5.3, (5.25), proof Step 1, (5.26)); p56 (chain rule, r^{-1} factor).",
"obligation": "Supplies the finite-residual hypothesis (5.33) of Lemma 5.4, with ρN = 2h(N+1) and no flat remainder. The gain must grow with N while the loss from physical differentiation stays fixed.",
"backward_question": "If I stop at order N, does the residual gain grow with N while each physical derivative costs a power of q that does not depend on N?",
"mechanism": "At every retained order: - (5.2) gives exact incompressibility; - (5.5) holds globally, so the radial residual is canceled; - differentiating the primitives gives (∂R + 2/R)Tn,θ = -rθ,n and (∂R + 1/R)Tn,z = -rz,n, so the tangential residual is exactly minus the stress divergence; - order zero holds by Proposition 4.2. After truncation, every uncancelled product or shifted viscous term carries relative power at least q^{2h(N+1)}. For N = 1, for example, products of two order-one coefficients and axial viscosity on order one first enter at order two. In the similarity chart, each transverse derivative costs q^{-1/2}, each axial derivative q^{-D}, and each time derivative q^{-1}, whatever the base power b. The powers of n produced by differentiating q^{λn} enter only the constants, through (1 + |b|)^m. On the stress support X ≥ Xa > 0, r^{-1} = q^{-1/2}(2X)^{-1/2}; near the axis the smooth Cartesian representatives are used.",
"antecedent": "None cited. Internal: Lemma 4.1 and Proposition 4.2.",
"cost": "Bounds hold only on fixed compact profile ranges and for q ≤ 1. C_{N,m} depends on N and on Xmax. The losses Km must be carried into the summation.",
"checkable": "A slope test of (5.26). 1. Take g(x⊥, η) = e^{-|x⊥|^2}(1 + η^2)^{-1}, b = -A + 2nh for several n, and h = 0.005. 2. Compute mixed derivatives of q^b g in Cartesian (x1, x2, z, t) by high-order finite differences in mpmath. Obtain q(z, t) by root finding on q - z^2q^{2h} = 1 - t. 3. Work at points of fixed (X, η) = (1, 0.3), for q from 1e-2 to 1e-8. 4. Fit the log-log slope and compare with b - a/2 - Dk - l. The full (5.25) needs the actual profiles. Appendices A to C construct them analytically, not in closed form.",
"depends_on": [
"M5.7",
"M5.6",
"M4.1",
"M4.4"
],
"constrains": [],
"reasons": {
"M5.7": "the extended profiles satisfy (5.2) and (5.5) globally, so each truncation is divergence-free and cancels the radial residual.",
"M5.6": "differentiating the primitives (5.9) makes each order's tangential residual exactly minus the stress divergence.",
"M4.1": "the loss K_m comes from (5.26): each physical derivative costs a fixed power of q via Lemma 4.1's chain rule, at every order.",
"M4.4": "order zero enters through Proposition 4.2, whose tangential residual is exactly minus the divergence of the leading stress."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62",
"analogous_to": [],
"relations": {
"M5.7": "prerequisite",
"M5.6": "prerequisite",
"M4.1": "prerequisite",
"M4.4": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "digest-only",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M5.12",
"kind": "move",
"name": "ns-m5-12-stokes-streamfunction-potentials-so-that-cutoffs-in-q",
"title": "Stokes streamfunction potentials, so that cutoffs in q keep div u = 0",
"section": "5",
"pages": "45-62",
"refs": [
"p56 (plan of subsection 5.4, potential formulas, (5.27), Cartesian form, summation tuple)."
],
"statement": "(5.27): - Fn = X AX(Un), Sn = q^{1-A+λn} Fn, and An = (Sn/r) eθ; - uz,n = ∂s Sn and r ur,n = -∂z Sn (s = r^2/2), so curl An = ur,n er + uz,n ez. In Cartesian form, An = (Sn/r^2)(-x2, x1, 0) = (1/2) q^{-A+λn} (Fn/X)(-x2, x1, 0). This is smooth across the axis for q > 0, because Fn/X is smooth at X = 0. The summation tuple is An = An, Bn = uθ,n eθ, pn = q^{-2A+λn} Πn, Tn = q^{-A-1/2+λn} Tn, with decay orders gn = 2nh and differential polynomial Fslow.",
"description": "(5.27): - Fn = X AX(Un), Sn = q^{1-A+λn} Fn, and An = (Sn/r) eθ; - uz,n = ∂s Sn and r ur,n = -∂z Sn (s = r^2/2), so curl An = ur,n er + uz,n ez. In Cartesian form, An = (Sn/r^2)(-x2, x1, 0) = (1/2) q^{-A+λn} (Fn/X)(-x2, x1, 0). This is smooth across the axis for q > 0, because Fn/X is smooth at X = 0. The summation tuple is An = An, Bn = uθ,n eθ, pn = q^{-2A+λn} Πn, Tn = q^{-A-1/2+λn} Tn, with decay orders gn = 2nh and differential polynomial Fslow. OBLIGATION: The summation cutoffs χ(cn q) depend on (z, t) through q. Multiplying the velocity coefficients by them would break div u = 0. Cutting the potential before taking the curl keeps exact incompressibility. The swirl Bn stays divergence-free under multiplication by any function of (z, t), because it is independent of θ. MECHANISM: Axisymmetric divergence-free (ur, uz) fields are curls of azimuthal potentials (S/r)eθ, with S the Stokes streamfunction. Given uz,n = ∂s Sn, the relation -∂zSn = q^{λn}Vn is exactly (5.2), using A + D = 1 and the operator Z of. ANTECEDENT: None cited; the Stokes streamfunction is named without citation. REFS: p56 (plan of subsection 5.4, potential formulas, (5.27), Cartesian form, summation tuple).",
"obligation": "The summation cutoffs χ(cn q) depend on (z, t) through q. Multiplying the velocity coefficients by them would break div u = 0. Cutting the potential before taking the curl keeps exact incompressibility. The swirl Bn stays divergence-free under multiplication by any function of (z, t), because it is independent of θ.",
"backward_question": "How can each order be multiplied by a cutoff depending on q = q(z, t) without destroying exact incompressibility or smoothness at the axis?",
"mechanism": "Axisymmetric divergence-free (ur, uz) fields are curls of azimuthal potentials (S/r)eθ, with S the Stokes streamfunction. Given uz,n = ∂s Sn, the relation -∂zSn = q^{λn}Vn is exactly (5.2), using A + D = 1 and the operator Z of (4.2). Smoothness at the axis follows because S/r^2 is a smooth function of (r^2, z, t). The first moment mn,1 = 0 makes Fn, and hence Sn, compactly supported in X. The curl of a cut potential includes the term from differentiating the cutoff, so the result stays divergence-free.",
"antecedent": "None cited; the Stokes streamfunction is named without citation.",
"cost": "It needs Fn/X smooth at the axis and Fn compactly supported, both from Lemma 5.2. Cutting the potential produces an extra radial velocity term, displayed as (5.45).",
"checkable": "1. Take Un = (1 - X) e^{-X} g(η). Then ∫_0^∞ Un dX = 0 and Fn = X e^{-X} g(η). 2. Obtain q(z, t) by root finding. 3. By finite differences in z at fixed (r, t), check that -∂zSn = q^{λn}Vn with Vn from (5.2), and that ∂sSn = q^{-A+λn}Un. 4. Check that the Cartesian divergence of curl(χ(cq)An) vanishes to finite-difference accuracy.",
"depends_on": [
"M5.2",
"M5.8",
"M5.11"
],
"constrains": [],
"reasons": {
"M5.2": "u_z,n = ∂_s S_n and r u_r,n = -∂_z S_n reproduce the order-n incompressibility relation (5.2), using A + D = 1.",
"M5.8": "F_n/X is smooth at the axis and F_n vanishes past X+ because m_n,1 = 0, so each potential is smooth and compactly supported.",
"M5.11": "the summation tuple carries the differential polynomial F_slow of (5.24) and the stresses of the truncations."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62",
"analogous_to": [],
"relations": {
"M5.2": "prerequisite",
"M5.8": "prerequisite",
"M5.11": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "digest-only",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M5.13",
"kind": "move",
"name": "ns-m5-13-lemma-5-4-an-abstract-borel-type-summation-with-shrinking",
"title": "Lemma 5.4, an abstract Borel-type summation with shrinking cutoffs",
"section": "5",
"pages": "57-59",
"refs": [
"p56 (summation plan, Λlog)",
"p57 ((5.28) to (5.33), Lemma 5.4 statement, (5.34))",
"p58 ((5.35), (5.36), Steps 1 and 2, (5.37))",
"p59 (Step 3, (5.38), (5.39), choice of J, initial block, residual comparison formula, (5.40), recovery of the expansion)."
],
"statement": "Lemma 5.4 (Borel-type summation, pp. 57-59): let 0 < q < q0 ≤ 1, |∂z^a∂t^b q| ≤ Cq^{1-aD-b}, 0 < D < 1 (5.28); a base U0, div u0 = 0, |U0|_m ≤ C_m q^{-Km}Λlog^{Pm}, Λlog = 1 + |log q|; increments Zj = (Aj, Bj eθ, pj, Tj) with smooth zero extensions, |Zj|_m ≤ C_{j,m}q^{gj-ℓm}Λlog^{P_{j,m}}, gj ↑ ∞ (5.29)-(5.30); and a differential polynomial F (5.31)-(5.32) whose partial-sum residuals are O(q^{ρJ-K^F_m}) plus flat, ρJ → ∞ (5.33). Then there are scales aj with U = U0 + Σ_j χ(ajq)Zj (curl after cutoff) smooth, divergence-free, close to U[J] (5.35), and F(U) = O(q^N) for all N (5.36).",
"description": "Lemma 5.4 (Borel-type summation, pp. 57-59): let 0 < q < q0 ≤ 1, |∂z^a∂t^b q| ≤ Cq^{1-aD-b}, 0 < D < 1 (5.28); a base U0, div u0 = 0, |U0|_m ≤ C_m q^{-Km}Λlog^{Pm}, Λlog = 1 + |log q|; increments Zj = (Aj, Bj eθ, pj, Tj) with smooth zero extensions, |Zj|_m ≤ C_{j,m}q^{gj-ℓm}Λlog^{P_{j,m}}, gj ↑ ∞ (5.29)-(5.30); and a differential polynomial F (5.31)-(5.32) whose partial-sum residuals are O(q^{ρJ-K^F_m}) plus flat, ρJ → ∞ (5.33). Then there are scales aj with U = U0 + Σ_j χ(ajq)Zj (curl after cutoff) smooth, divergence-free, close to U[J] (5.35), and F(U) = O(q^N) for all N (5.36). OBLIGATION: The constants of (5.17) may grow too fast for (5.1) to converge. The lemma produces genuine smooth, exactly divergence-free fields with the same asymptotics and a flat residual, in a form that the wave and mean correction sequence can reuse (Proposition 9.9). MECHANISM: Three steps. 1. Scale invariance. On the support of χ^{(k)}(aq), 1/2 ≤ aq ≤ 1. So each factor a from the chain rule pairs with a factor q from (5.28), giving |∂z^{a'}∂t^{b'}χ(aq)| ≤ C q^{-a'D-b'} uniformly in a.",
"obligation": "The constants of (5.17) may grow too fast for (5.1) to converge. The lemma produces genuine smooth, exactly divergence-free fields with the same asymptotics and a flat residual, in a form that the wave and mean correction sequence can reuse (Proposition 9.9).",
"backward_question": "Given a formal expansion whose coefficient bounds may grow arbitrarily fast with the order, how do I build an actual smooth, exactly divergence-free field with the same asymptotics and a residual flat at the singular point? And how do I state it abstractly enough to reuse for the later correction cycle?",
"mechanism": "Three steps. 1. Scale invariance. On the support of χ^{(k)}(aq), 1/2 ≤ aq ≤ 1. So each factor a from the chain rule pairs with a factor q from (5.28), giving |∂z^{a'}∂t^{b'}χ(aq)| ≤ C q^{-a'D-b'} uniformly in a. Since q depends only on (z, t), curl(χ(aq)Aj) = χ(aq) curl Aj + aχ'(aq)∇q × Aj is controlled by the potential bounds, with a loss ℓ'm depending only on m and ℓ_{m+1}. 2. Diagonal choice (5.37). At step j, pick aj so large that Ĉ_{j,m} Λlog^{P̂_{j,m}} q^{gj/2} ≤ 2^{-j} on q ≤ aj^{-1}, for all m ≤ j. Half of the decay exponent pays for arbitrarily large constants. The tail beyond J is then at most 2^{-J} q^{g_{J+1}/2 - ℓ'm}. On {q ≥ δ}, only terms with aj ≤ δ^{-1} survive, which gives local finiteness. 3. Flatness. Fix (m, N), then a large J, and compare F(U) with F(U[J]) on q < 1/(2aJ), where the first J cutoffs equal one. - (5.38) bounds U[J] by q^{-Km}, with Km independent of J. - (5.39) bounds the difference by C_m q^{-Hm} |e|_{m+s}(1 + |U[J]|_{m+s} + |e|_{m+s})^{d-1}, with e = U - U[J] and Hm independent of J. - Choose J with g_{J+1}/2 - ℓ'_{m+s} ≥ N + Hm + (d - 1)(K_{m+s} + 1) and ρJ - K^F_m ≥ N + 1. Both pieces are then O(q^N).",
"antecedent": "None cited. The diagonal cutoff construction is the one in the classical proof of Borel's lemma (a smooth function with a prescribed Taylor series); that attribution is mine.",
"cost": "- The scales aj are not explicit; they are chosen after all constants. - The summed field equals the partial sums only on the shrinking neighborhoods q < 1/(2aJ). - The tail estimates use only half the decay exponent. - Every summand needs common supports, smooth Cartesian representatives, and smooth zero extensions, plus a common domain for all partial sums (later supplied by Lemma 9.7).",
"checkable": "Mostly a pure estimate. Two ingredients are computable: - (a) For a standard smooth step χ built from e^{-1/x}, confirm numerically that sup_{q>0} |(q∂q)^j χ(aq)| is the same for a = 1, 10, 1e4. It equals sup_σ |(σ∂σ)^j χ(σ)|. - (b) A toy summation: take gj = 2jh with h = 0.005 and constants Ĉ_{j,m} = ((j + m)!)^2. Choose aj from (5.37) by root finding, then verify the tail bound (5.35) on a grid in q.",
"depends_on": [
"M5.12",
"M4.1"
],
"constrains": [],
"reasons": {
"M5.12": "its increments are potentials A_j cut before the curl plus θ-independent swirl B_j e_θ, the device of (5.27) that keeps div u = 0.",
"M4.1": "the cutoffs χ(a_j q) use the concentration scale q of (4.1), whose derivative bounds (5.28) make them scale invariant."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62",
"analogous_to": [],
"relations": {
"M5.12": "prerequisite",
"M4.1": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "astra-spot-check-2026-10-01",
"computation_checked": false,
"astra_spot_check": "statement-rewritten"
}
},
{
"id": "M5.14",
"kind": "move",
"name": "ns-m5-14-proposition-5-5-the-realized-base-field-and-what-it",
"title": "Proposition 5.5, the realized base field and what it guarantees",
"section": "5",
"pages": "45-62",
"refs": [
"p60 (subsection 5.5, Proposition 5.5, (5.41) to (5.44), Step 1, ℓm = 2A + m, cutoff scale invariance)",
"p61 (ρN, Step 2, (5.45), Step 3, (5.46), O(q^{3h}), the Step 4 split)",
"p62 (tail bound, endpoint extension)."
],
"statement": "Proposition 5.5 (p. 60-62): there are smooth axisymmetric (uB, pB) for q > 0 and stresses Tphys supported in Xa ≤ X ≤ Xb with: div uB = 0; R(uB, pB) = -(∂r + 2/r)Tphys,θeθ - (∂r + 1/r)Tphys,zez + EB, EB = O(q^M) for all M (5.41); on [Xlo, Xhi], q^Auθ,B - E0, q^Auz,B - U0 = O(q^{2h}) and q^Aur,B = O(q^h) (5.42); |D^I(q^{A+1/2}Tphys - T0)| ≤ C_Iq^{2h}ζδ^{-N_I} on Xa < X < Xb (5.43); continuous extension to η = ±1; uB - u(0), pB - p(0) vanish for X ≥ X+, preserving (4.29); on Imean, uz,B = 0, q^Auθ,B = E0 (5.44).",
"description": "Proposition 5.5 (p. 60-62): there are smooth axisymmetric (uB, pB) for q > 0 and stresses Tphys supported in Xa ≤ X ≤ Xb with: div uB = 0; R(uB, pB) = -(∂r + 2/r)Tphys,θeθ - (∂r + 1/r)Tphys,zez + EB, EB = O(q^M) for all M (5.41); on [Xlo, Xhi], q^Auθ,B - E0, q^Auz,B - U0 = O(q^{2h}) and q^Aur,B = O(q^h) (5.42); |D^I(q^{A+1/2}Tphys - T0)| ≤ C_Iq^{2h}ζδ^{-N_I} on Xa < X < Xb (5.43); continuous extension to η = ±1; uB - u(0), pB - p(0) vanish for X ≥ X+, preserving (4.29); on Imean, uz,B = 0, q^Auθ,B = E0 (5.44). OBLIGATION: Delivers the background every later section uses: - exact incompressibility; - residual equal to an annular stress divergence plus a flat error; - the untouched heat exterior; - the untouched mean patch; - normalized closeness to the leading field, used for the chart base velocity in Section 7 and for the growth asymptotic (3.6) at a fixed Xin ∈ (0, Xa); ANTECEDENT: None cited. Internal: Lemma 5.4, Proposition 5.3, Lemma 5.2, Theorem 4.6. REFS: p60 (subsection 5.5, Proposition 5.5, (5.41) to (5.44), Step 1, ℓm = 2A + m, cutoff scale invariance); p61 (ρN, Step 2, (5.45), Step 3, (5.46), O(q^{3h}), the Step 4 split); p62 (tail bound, endpoint extension).",
"obligation": "Delivers the background every later section uses: - exact incompressibility; - residual equal to an annular stress divergence plus a flat error; - the untouched heat exterior; - the untouched mean patch; - normalized closeness to the leading field, used for the chart base velocity in Section 7 and for the growth asymptotic (3.6) at a fixed Xin ∈ (0, Xa); - weighted closeness of the stress to T0, used to choose wave amplitudes (Propositions 7.5 and 7.6); - smooth limits at t = 1 away from the origin.",
"backward_question": "Does summation with shrinking cutoffs preserve exactly what later sections need, without changing any asymptotic coefficient? That means the heat exterior, the untouched mean patch, closeness to the leading field and to the stress with the ζ weight, and smooth limits at t = 1 away from the origin.",
"mechanism": "Apply Lemma 5.4 to the tuples of M5.12 on each compact profile range, keeping order zero uncut. By (5.26) and D < 1/2, the loss is ℓm = 2A + m, and (5.25) is (5.33) with ρN = 2h(N+1) and no remainder. Cutoffs are scale invariant in the normalized variables: (q∂q)^j χ(cn q) = (σ∂σ)^j χ(σ) at σ = cn q, bounded uniformly in n. Cutting the potential gives (5.45): r u^cut_{r,n} = q^{2nh}[χ(cn q)Vn - (2η/L)(cn q)χ'(cn q)Fn] and u^cut_{z,n} = q^{-A+2nh}χ(cn q)Un. This field is divergence-free identically, and (5.18) kills both bracket terms on Imean, which proves (5.44). Extra diagonal requirements of type (5.40) give (5.46): |D^I[χ(cn q) q^{2nh} an]| ≤ 2^{-n} q^{nh} for n ≥ max{2, |I|}. Here an is one of En, Un, Πn, Vn/√(2X), Fn/√(2X) on the enlarged rectangle, or a component of Tn/ζ for n ≥ 2. Summing gives (5.42); in the normalization q^A, the positive-order radial correction is even O(q^{3h}). Together with (5.22) for n = 1, summing also gives (5.43). The asymptotic coefficients are unchanged. Split at J = max{2N + 2, m + 1}. Keep the finitely many terms N < n < J with their original powers, which are at least q^{2h(N+1)}. Bound the tail by Σ_{n≥J} 2^{-n}q^{nh} ≤ 2^{1-J}q^{Jh} ≤ 2^{1-J}q^{2h(N+1)}. On compact sets with q bounded below, only finitely many terms survive, so their analytic η-neighborhoods intersect. Since L > 0, the one-sided extensions at η = ±1 transfer to physical variables; η = ±1 is the time t = 1 away from the origin (Section 3.1).",
"antecedent": "None cited. Internal: Lemma 5.4, Proposition 5.3, Lemma 5.2, Theorem 4.6.",
"cost": "- The higher-order stress T̂ - T0 is signed and bounded only by q^{2h}ζδ^{-N}. The δ^{-N} loss near the annulus edges rules out a uniform relative bound against |T0| ≥ cζ. So Section 7 keeps the fixed positive representation of T0 and treats the rest by signed corrections. - The diagonal bound gives q^{nh} rather than q^{2nh}; splitting at 2N + 2 compensates. - All estimates are uniform only on compact profile rectangles and for q > 0.",
"checkable": "- (a) Symbolic: derive (5.45) as -∂z[χ(cn q)Sn], using ∂zq = 2ηq^{1-D}/L (Lemma 4.1), Sn = q^{1-A+2nh}Fn and A + D = 1. Confirm the divergence of the cut field vanishes. - (b) Numeric: for h = 0.005, N ≤ 5, m ≤ 5 and a grid of q in (0, 1], confirm Σ_{n≥J} 2^{-n}q^{nh} ≤ 2^{1-J}q^{2h(N+1)} with J = max{2N + 2, m + 1}. - (c) The quantitative bounds (5.42) and (5.43) require the constructed profiles.",
"depends_on": [
"M5.13",
"M5.11",
"M5.10",
"M5.8"
],
"constrains": [],
"reasons": {
"M5.13": "Lemma 5.4 applied to the order-n tuples gives smooth, exactly divergence-free fields with a flat residual E_B and unchanged asymptotics.",
"M5.11": "Proposition 5.3's truncation bound (5.25) supplies the hypothesis (5.33) with ρ_N = 2h(N + 1) and an N-independent loss.",
"M5.10": "the ζδ^{-N} bounds (5.13), (5.22) on T_n give the weighted closeness (5.43) of the summed stress to T0.",
"M5.8": "positive orders vanish past X+ and, by (5.18), on I_mean, so the heat exterior and the mean patch (5.44) are untouched."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62",
"analogous_to": [],
"relations": {
"M5.13": "prerequisite",
"M5.11": "prerequisite",
"M5.10": "prerequisite",
"M5.8": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: TRUNCATED; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M6.1",
"kind": "move",
"name": "ns-m6-1-dyadic-charts-and-normalized-units",
"title": "Dyadic charts and normalized units",
"section": "6",
"pages": "62",
"refs": [
"p. 62, (6.1)",
"p. 63 (the normalizations, and the time and viscous factors after (6.6))",
"p. 17 (normalized operators)."
],
"statement": "Section 6, dyadic charts (p. 62): on a dyadic band where q ≍ Q set Q = 2^(−ℓ), ε = Q^h, S* = ℓ^2, R = r/√Q, Z = z/Q^D, T = τ/Q, τ = 1 − t (6.1), with A = 1/2 + h and D = 1/2 − h. Velocity, pressure, and residual get chart representatives by the factors Q^A, Q^(2A), Q^(2A+1/2), so the normalized time derivative carries Q^(1+h) and the viscous term ε (p. 63); R_chart = √(q/Q) R_profile. All geometric choices are made on one domain 0 < q < qbig; qbig may shrink while base and pulse coefficients are fixed, not after the correction iteration begins (p. 62).",
"description": "Section 6, dyadic charts (p. 62): on a dyadic band where q ≍ Q set Q = 2^(−ℓ), ε = Q^h, S* = ℓ^2, R = r/√Q, Z = z/Q^D, T = τ/Q, τ = 1 − t (6.1), with A = 1/2 + h and D = 1/2 − h. Velocity, pressure, and residual get chart representatives by the factors Q^A, Q^(2A), Q^(2A+1/2), so the normalized time derivative carries Q^(1+h) and the viscous term ε (p. 63); R_chart = √(q/Q) R_profile. All geometric choices are made on one domain 0 < q < qbig; qbig may shrink while base and pulse coefficients are fixed, not after the correction iteration begins (p. 62). OBLIGATION: It makes the active annulus Xa < X < Xb a bounded set in every band, so estimates can be uniform over infinitely many scales. It identifies ε as the parameter in which all later residual orders are measured (the classes of M6.11 and the stage exponents σj of Section 9). And it separates harmless losses (powers of S* ≍ log^2(1/q)) from the gains that matter (powers of ε). MECHANISM: In the annulus r ≍ √q, z ≍ q^D, and τ ≍ q. Rescaling by the frozen band scale Q, not by the variable q, gives chart variables of order one, while Q, ε, and S* stay constant inside a. ANTECEDENT: None cited.",
"obligation": "It makes the active annulus Xa < X < Xb a bounded set in every band, so estimates can be uniform over infinitely many scales. It identifies ε as the parameter in which all later residual orders are measured (the classes of M6.11 and the stage exponents σj of Section 9). And it separates harmless losses (powers of S* ≍ log^2(1/q)) from the gains that matter (powers of ε).",
"backward_question": "In what frozen units does the collapsing annulus look the same at every scale, and which single parameter measures how far each term sits below the leading balance?",
"mechanism": "In the annulus r ≍ √q, z ≍ q^D, and τ ≍ q. Rescaling by the frozen band scale Q, not by the variable q, gives chart variables of order one, while Q, ε, and S* stay constant inside a chart (\"held fixed in derivatives\"). The residual normalization Q^(2A+1/2) is the one that makes the transport term (u·∇)u of normalized size one. The slow time derivative then becomes −ε∂T and viscosity becomes ε times the normalized Laplacian, so both sit one power of ε below transport. The logarithmic parameter S* = ℓ^2 has two properties. Any fixed power of S* is beaten by any positive power of ε as ℓ → ∞, so polynomial losses in S* can always be absorbed. And exp(−c S*) = exp(−c ℓ^2) is smaller than every power of Q, which is what later makes pulse tails flat.",
"antecedent": "None cited.",
"cost": "Every later estimate must be uniform over bands ℓ ≥ ℓ0, labels, and rectangle copies, with constants that depend only on fixed data, the derivative order, and the stage. Neighboring bands overlap (q/Q ∈ [1/2, 2]), which creates the multi-band bookkeeping of M6.8. And qbig must be small.",
"checkable": "Exact arithmetic on the exponents with A = 1/2 + h and D = 1/2 − h. Check that (2A + 1/2) − A = 1 + h; that (2A + 1/2) − A − 1 = h; that √Q ∂z = Q^(1/2−D) ∂Z = ε∂Z; and that the leading stress-divergence scale q^(−3/2−h) (Section 3.3), multiplied by Q^(2A+1/2), is of order ε. All four were verified here for h = 1/200 and h = 1/101. Numerically, also confirm that ℓ^(2b) 2^(−ηhℓ) → 0 and exp(−cℓ^2) 2^(Nℓ) → 0 for sample b, η, c, N > 0.",
"depends_on": [
"M4.1",
"M4.2",
"M4.8",
"M5.14"
],
"constrains": [],
"reasons": {
"M4.1": "The chart variables R = r/√Q, Z = z/Q^D, T = τ/Q rescale by the concentration scale q and its anisotropic lengths q^{1/2}, q^D from the similarity coordinates.",
"M4.2": "The factors Q^A for velocity and Q^{2A} for pressure match the leading field's growth u ~ q^{-A}E and p ~ q^{-2A}Π.",
"M4.8": "Takes the fixed exponent h, so ε = Q^h, and the fixed annulus Xa < X < Xb of Theorem 4.6, which the charts turn into a bounded set in every band.",
"M5.14": "The charted fields are those of the realized background, whose stress-divergence scale q^{-3/2-h} becomes order ε after the Q^{2A+1/2} normalization."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 62",
"analogous_to": [],
"relations": {
"M4.1": "prerequisite",
"M4.2": "prerequisite",
"M4.8": "prerequisite",
"M5.14": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": true,
"astra_spot_check": null
}
},
{
"id": "M6.2",
"kind": "move",
"name": "ns-m6-2-integer-covering-matrix-and-the-physical-phase-map",
"title": "Integer covering matrix and the physical phase map",
"section": "6",
"pages": "62",
"refs": [
"p. 62 (motivation)",
"p. 63, (6.2), (6.3), (6.4)",
"p. 64 (commutation, support away from the axis, no spatial periodicity)."
],
"statement": "Section 6 (p. 63): fix Jg = [[3, 1], [1, 5]], Λg = 4 − √2, Tg = 4 + √2, bg = √2 − 1, vr = (1, −bg), vt = (bg, 1), ρg = log Λg/log Tg, κs = 10^(−5), dr = 2((1 + h)ρg − hκs) > 0 (6.2); Jg vr = Λg vr, Jg vt = Tg vt, 1 < Λg < Tg. Physical fields are evaluations of extended fields F(r, θ, z, t, Y), Y ∈ T^2, on Y = vr r^(dr) + vt t (mod Z^2) (6.3). Physical ∂t and ∂r then act as 𝔱 = ∂t + Nabs and 𝔯 = ∂r + dr r^(dr−1) Labs, Nabs = vt·∂Y, Labs = vr·∂Y (6.4), and 𝔯, ∂z, ∂θ, 𝔱 commute (p. 64).",
"description": "Section 6 (p. 63): fix Jg = [[3, 1], [1, 5]], Λg = 4 − √2, Tg = 4 + √2, bg = √2 − 1, vr = (1, −bg), vt = (bg, 1), ρg = log Λg/log Tg, κs = 10^(−5), dr = 2((1 + h)ρg − hκs) > 0 (6.2); Jg vr = Λg vr, Jg vt = Tg vt, 1 < Λg < Tg. Physical fields are evaluations of extended fields F(r, θ, z, t, Y), Y ∈ T^2, on Y = vr r^(dr) + vt t (mod Z^2) (6.3). Physical ∂t and ∂r then act as 𝔱 = ∂t + Nabs and 𝔯 = ∂r + dr r^(dr−1) Labs, Nabs = vt·∂Y, Labs = vr·∂Y (6.4), and 𝔯, ∂z, ∂θ, 𝔱 commute (p. 64). OBLIGATION: It meets the section's stated requirement (p. 62): localize the waves, separate their supports, and \"permit rapid temporal variation without introducing radial derivatives large enough to spoil the residual estimates.\" Localizing waves in time becomes localizing them in an independent periodic variable. MECHANISM: Because Y is an independent variable, the construction is a two-scale ansatz made exact. Identities for extended fields are written with 𝔯 and 𝔱 in place of ∂r and ∂t, and restricting to Y(r, t) turns them into physical identities with no remainder; covariances and averages are taken on the extended domain before evaluation. ANTECEDENT: None cited.",
"obligation": "It meets the section's stated requirement (p. 62): localize the waves, separate their supports, and \"permit rapid temporal variation without introducing radial derivatives large enough to spoil the residual estimates.\" Localizing waves in time becomes localizing them in an independent periodic variable.",
"backward_question": "Can I attach to space-time a periodic fast variable that runs quickly in time, runs only barely faster than the slow scale in radius, is one fixed map for every scale, and turns the product of two fields with disjoint fast supports into an exact zero?",
"mechanism": "Because Y is an independent variable, the construction is a two-scale ansatz made exact. Identities for extended fields are written with 𝔯 and 𝔱 in place of ∂r and ∂t, and restricting to Y(r, t) turns them into physical identities with no remainder; covariances and averages are taken on the extended domain before evaluation. The map moves along vt in time and along vr in radius, and these are the two eigen-directions of Jg. So the integer coverings Y ↦ Jg^i Y, which preserve periodicity, multiply the time rate by Tg^i and the radial rate by Λg^i = (Tg^i)^(ρg), a strictly smaller power (ρg ≈ 0.5625). A circle carries only one direction; two eigen-directions of one integer matrix let the band coverings scale time and radius at different, prescribed rates. The only variable coefficient, dr r^(dr−1), depends on r alone and multiplies a constant torus direction, so all the evaluated derivatives commute, and identities such as the exact divergence-freeness of curls survive on the extended domain. The power r^(dr) is what lets one band-independent map serve every band: in the annulus r^2 ≍ q ≍ Q, so r^(dr) contributes a factor Q^(dr/2), which cancels the band dependence of Λg^(i(ℓ)) (M6.3). Periodicity in Y imposes no spatial periodicity after restriction.",
"antecedent": "None cited.",
"cost": "r^(dr) is not smooth at r = 0, so every correction that depends on Y must be supported away from the axis, in the active shell (p. 64). Each fast radial derivative costs up to a factor ε^(−κs) (times powers of S*), so κs appears in essentially every later exponent (for example 1/2 − κs and 1 − 3κs in Sections 7 to 9). It adds the fixed constants Jg, κs, and dr, and fields now live on an extended domain.",
"checkable": "Linear algebra: Jg vr = Λg vr, Jg vt = Tg vt, vr·vt = 0, det Jg = 14. Numerically Λg = 2.5857864, Tg = 5.4142136, and ρg = 0.5624714, and dr ranges over (1.12494, 1.13618) for 0 < h < 1/100 (all computed here). Symbolically, for a trigonometric polynomial F(r, t, Y), check that d/dr[F(r, t, Y(r, t))] = (𝔯F)(r, t, Y(r, t)), that d/dt[F(r, t, Y(r, t))] = (𝔱F)(r, t, Y(r, t)), and that the commutator of 𝔯 and 𝔱 vanishes.",
"depends_on": [
"M6.1"
],
"constrains": [],
"reasons": {
"M6.1": "The radial phase exponent d_r = 2((1+h)ρ_g − hκ_s) is built from the chart time exponent 1+h and ε = Q^h, so band coverings produce prescribed chart rates."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 62",
"analogous_to": [],
"relations": {
"M6.1": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": true,
"astra_spot_check": null
}
},
{
"id": "M6.3",
"kind": "move",
"name": "ns-m6-3-band-covering-index-and-the-two-derivative-scales",
"title": "Band covering index and the two derivative scales",
"section": "6",
"pages": "63",
"refs": [
"p. 63, (6.5), (6.6)",
"p. 64 (the comparison inequalities)",
"used at p. 91 to 92 (Lemma 8.2, M^(−1) ≤ C ε^(κs) S*^(ρg)) and p. 96 ((8.20))."
],
"statement": "Section 6 (p. 63): band ℓ uses Yi = Jg^i Y (mod Z^2), i = i(ℓ) = ⌊log_Tg(Q^(−1−h)/S*)⌋ (6.5), only where i(ℓ) ≥ 0; a function descends to the band torus if invariant under Y ↦ Y + a with Jg^i a ∈ Z^2. With Ni = vt·∂Yi, Li = vr·∂Yi: Nabs = Tg^i Ni, Labs = Λg^i Li. Chart operators (6.6): t* = Q^(1+h)𝔱 = −ε∂T + ci Ni, ci = Tg^i Q^(1+h) ≍ S*^(−1); Dr = √Q 𝔯 = ∂R + Mi dr R^(dr−1) Li, Mi = Λg^i Q^(dr/2) ≍ ε^(−κs) S*^(−ρg); Dz = ε∂Z; Dθ = R^(−1)∂θ. The comparisons follow from (1/Tg)Q^(−1−h)/S* < Tg^i ≤ Q^(−1−h)/S* and Λg^i = (Tg^i)^(ρg) (p. 64).",
"description": "Section 6 (p. 63): band ℓ uses Yi = Jg^i Y (mod Z^2), i = i(ℓ) = ⌊log_Tg(Q^(−1−h)/S*)⌋ (6.5), only where i(ℓ) ≥ 0; a function descends to the band torus if invariant under Y ↦ Y + a with Jg^i a ∈ Z^2. With Ni = vt·∂Yi, Li = vr·∂Yi: Nabs = Tg^i Ni, Labs = Λg^i Li. Chart operators (6.6): t* = Q^(1+h)𝔱 = −ε∂T + ci Ni, ci = Tg^i Q^(1+h) ≍ S*^(−1); Dr = √Q 𝔯 = ∂R + Mi dr R^(dr−1) Li, Mi = Λg^i Q^(dr/2) ≍ ε^(−κs) S*^(−ρg); Dz = ε∂Z; Dθ = R^(−1)∂θ. The comparisons follow from (1/Tg)Q^(−1−h)/S* < Tg^i ≤ Q^(−1−h)/S* and Λg^i = (Tg^i)^(ρg) (p. 64). OBLIGATION: It makes the fast clock run at the right speed in every band. The rectangles have a fixed torus size r0, so a pulse lasts Ls = 2r0/ci ≍ S* normalized time units, which is long enough for the Gaussian envelope of Section 7 ((7.16)) to be exp(−cS*)-small at both ends. It keeps the fast radial derivative at the size ε^(−κs) S*^(−ρg). And it supplies the radial winding that Lemma 8.2 uses: there M^(−1) ≤ C ε^(κs) S*^(ρg) (p. 92). MECHANISM: In time, t* on the band torus has a slow part −ε∂T (one power of ε) and a fast part ci Ni with ci ≍ 1/S*; ANTECEDENT: None cited.",
"obligation": "It makes the fast clock run at the right speed in every band. The rectangles have a fixed torus size r0, so a pulse lasts Ls = 2r0/ci ≍ S* normalized time units, which is long enough for the Gaussian envelope of Section 7 ((7.16)) to be exp(−cS*)-small at both ends. It keeps the fast radial derivative at the size ε^(−κs) S*^(−ρg). And it supplies the radial winding that Lemma 8.2 uses: there M^(−1) ≤ C ε^(κs) S*^(ρg) (p. 92).",
"backward_question": "Given one fixed phase map, how do I make its time winding match a pulse lifetime of about S* shear times in every band, and how small can I keep the radial winding while still getting unlimited averaging out of it?",
"mechanism": "In time, t* on the band torus has a slow part −ε∂T (one power of ε) and a fast part ci Ni with ci ≍ 1/S*; the floor in (6.5) pins Tg^i within a factor Tg of Q^(−1−h)/S*. In radius, Λg^i = (Tg^i)^(ρg) ≍ (Q^(−1−h)/S*)^(ρg). Multiplying by Q^(dr/2) = Q^((1+h)ρg − hκs) leaves exactly ε^(−κs) S*^(−ρg), up to a factor between Tg^(−ρg) and 1. The −hκs inside dr is deliberate. It costs a factor ε^(κs) per radial derivative, and it gains ε^(κs) per integration by parts along vr, which can be repeated. So Lemma 8.2 can make the zero-Haar-mean part of a full radial integral O(ε^(pκs)) for any p, that is, flat. Without that term, Mi ≍ S*^(−ρg) → 0 and integrating by parts along vr would lose instead of gain.",
"antecedent": "None cited.",
"cost": "It adds the covering index i(ℓ) and the deck-translation descent conditions. Different bands live on different tori, which M6.8 resolves. It introduces polynomial factors S*^(±1) and S*^(−ρg); the fast-time inverse costs ci^(−1) ≤ C S* ((8.20), p. 96); and a radial derivative loses ε^(κs) ((6.32)). A computation done here, not stated in the paper: Mi ≤ ε^(−κs) S*^(−ρg) can exceed 1 only when ε^(−κs) > S*^(ρg), which for h near 1/100 happens only beyond ℓ ≈ 3.2 × 10^8 (ℓ ≈ 6.6 × 10^8 at h = 0.005). The gains from radial winding are therefore purely asymptotic in q.",
"checkable": "For h ∈ {0.001, 0.005, 0.0099} and ℓ from 20 to 10^6, compute i(ℓ) in log arithmetic and check that i ≥ 0, ci·S* ∈ (1/Tg, 1], and Mi·ε^(κs)·S*^(ρg) ∈ (Tg^(−ρg), 1]. This was run here for ℓ in [20, 3000) and for ℓ = 10^4, 10^5, 10^6 with no violations. The same run gives the thresholds for Mi > 1 quoted above.",
"depends_on": [
"M6.2",
"M6.1"
],
"constrains": [],
"reasons": {
"M6.2": "Uses the integer matrix J_g, its eigen-directions v_r, v_t with rates T_g > Λ_g, the phase map, and its chain-rule operators to define band coverings.",
"M6.1": "Chooses i(ℓ) from the chart factor Q^{1+h} and S* so that c_i ≍ S*^{-1} and M_i ≍ ε^{-κ_s}S*^{-ρ_g} in normalized units."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 63",
"analogous_to": [],
"relations": {
"M6.2": "prerequisite",
"M6.1": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: TRUNCATED; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M6.4",
"kind": "move",
"name": "ns-m6-4-diophantine-bound-for-the-two-torus-directions",
"title": "Diophantine bound for the two torus directions",
"section": "6",
"pages": "64",
"refs": [
"p. 64, (6.7)",
"used at p. 91 ((8.10)) and p. 95 to 96 ((8.19), Lemma 8.6)."
],
"statement": "For n ∈ Z^2 \\ {0}, |vr·n| ≥ c/(1 + |n|) and |vt·n| ≥ c/(1 + |n|) (6.7). Proof: vr·n = (n1 + n2) − √2 n2, and multiplying it by its algebraic conjugate gives the nonzero integer (n1 + n2)^2 − 2 n2^2, while the conjugate has absolute value at most C|n|. The same argument works for vt·n = (n2 − n1) + √2 n1.",
"description": "For n ∈ Z^2 \\ {0}, |vr·n| ≥ c/(1 + |n|) and |vt·n| ≥ c/(1 + |n|) (6.7). Proof: vr·n = (n1 + n2) − √2 n2, and multiplying it by its algebraic conjugate gives the nonzero integer (n1 + n2)^2 − 2 n2^2, while the conjugate has absolute value at most C|n|. The same argument works for vt·n = (n2 − n1) + √2 n1. OBLIGATION: The inverse directional operators on zero-mean torus functions lose only a finite number of torus derivatives (p. 64). Later sections need this for the fast-time inverse (8.19) in Lemma 8.6, which loses four derivatives and removes the zero-auxiliary-mean part of the angular-mean residual, and for the cutoff-remainder estimate (8.10) in Lemma 8.2, which loses p + 3 derivatives. MECHANISM: Jg is an integer matrix with irrational eigenvalues, so the slopes of its eigenvectors are quadratic irrationals built from √2. For a quadratic irrational, a small linear form times its Galois conjugate is a nonzero integer, so the linear form is at least one over the. ANTECEDENT: None cited in the section. The inline argument is the classical Liouville-type bound for the quadratic irrational √2. REFS: p. 64, (6.7); used at p. 91 ((8.10)) and p. 95 to 96 ((8.19), Lemma 8.6).",
"obligation": "The inverse directional operators on zero-mean torus functions lose only a finite number of torus derivatives (p. 64). Later sections need this for the fast-time inverse (8.19) in Lemma 8.6, which loses four derivatives and removes the zero-auxiliary-mean part of the angular-mean residual, and for the cutoff-remainder estimate (8.10) in Lemma 8.2, which loses p + 3 derivatives.",
"backward_question": "If I must divide by v·k at every nonzero torus frequency, can I choose the directions so that small divisors cost only a fixed number of derivatives?",
"mechanism": "Jg is an integer matrix with irrational eigenvalues, so the slopes of its eigenvectors are quadratic irrationals built from √2. For a quadratic irrational, a small linear form times its Galois conjugate is a nonzero integer, so the linear form is at least one over the conjugate's size. The Fourier multipliers (2πi v·k)^(−p) are then bounded by C(1 + |k|)^p, and a few extra derivatives make the Fourier series converge absolutely in two dimensions.",
"antecedent": "None cited in the section. The inline argument is the classical Liouville-type bound for the quadratic irrational √2.",
"cost": "Each inversion loses a finite number of torus derivatives, so estimates must hold at every derivative order in the torus variables. The paper notes (p. 92) that a fixed finite regularity would yield only a finite flatness order, because frequencies comparable to M can be nearly resonant with vr.",
"checkable": "Compute the infimum of (1 + |n|)|vr·n| and of (1 + |n|)|vt·n| over 0 < |n|∞ ≤ N. For N = 400 both are about 0.3848, attained near Pell-type vectors such as (−70, −169) and (−169, 70) (run here), and the value is stable as N grows. Also check in exact integer arithmetic that (n1 + n2)^2 − 2 n2^2 ≠ 0 for n ≠ 0.",
"depends_on": [
"M6.2"
],
"constrains": [],
"reasons": {
"M6.2": "The bound concerns the fixed directions v_r = (1, −b_g) and v_t = (b_g, 1) with b_g = √2 − 1, whose quadratic-irrational slopes allow the conjugate argument."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 64",
"analogous_to": [],
"relations": {
"M6.2": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "astra-spot-check-2026-10-01",
"hypotheses_checked": "astra-spot-check-2026-10-01",
"computation_checked": false,
"astra_spot_check": "correct"
}
},
{
"id": "M6.5",
"kind": "move",
"name": "ns-m6-5-squared-partitions-of-unity-slow-boxes-and-labels",
"title": "Squared partitions of unity, slow boxes, and labels",
"section": "6",
"pages": "64",
"refs": [
"p. 64 (the partitions, Cℓ, Aℓ, (6.8))",
"p. 65 ((6.9), the partition identity, the compactness of supports)",
"used at p. 74 and p. 84 ((7.30))."
],
"statement": "Section 6 (pp. 64-65): Σℓ χℓ(q)^2 = 1 with supp χℓ in q/Q ∈ [1/2, 2]; in each band a product squared partition Σa χℓ,a(R, Z, T)^2 = 1 of mesh S*^(−3), supports within one mesh length of grid points. Active part Aℓ: 0 < q < qbig, 1/2 ≤ q/Q ≤ 2, τ ≥ 0, Xa ≤ r^2/(2q) ≤ Xb, qbig ≤ 2^(−ℓ0). Labels (6.8): Iℓ = boxes meeting Aℓ, each with a representative x0ℓ,a ∈ Bℓ,a ∩ Aℓ; Γ = {(ℓ, a, σ) : ℓ ≥ ℓ0, a ∈ Iℓ, σ = ±}. Slow cutoff ηγ = χℓ(q)χℓ,a(R, Z, T) with support Kγ (6.9), shared by both signs; Σℓ Σa (η(ℓ,a,+) ∘ Cℓ)^2 = 1 on the active shell.",
"description": "Section 6 (pp. 64-65): Σℓ χℓ(q)^2 = 1 with supp χℓ in q/Q ∈ [1/2, 2]; in each band a product squared partition Σa χℓ,a(R, Z, T)^2 = 1 of mesh S*^(−3), supports within one mesh length of grid points. Active part Aℓ: 0 < q < qbig, 1/2 ≤ q/Q ≤ 2, τ ≥ 0, Xa ≤ r^2/(2q) ≤ Xb, qbig ≤ 2^(−ℓ0). Labels (6.8): Iℓ = boxes meeting Aℓ, each with a representative x0ℓ,a ∈ Bℓ,a ∩ Aℓ; Γ = {(ℓ, a, σ) : ℓ ≥ ℓ0, a ∈ Iℓ, σ = ±}. Slow cutoff ηγ = χℓ(q)χℓ,a(R, Z, T) with support Kγ (6.9), shared by both signs; Σℓ Σa (η(ℓ,a,+) ∘ Cℓ)^2 = 1 on the active shell. OBLIGATION: It localizes each wave to a region where the background shear varies little: Section 7 freezes the frame and growth parameters at x0ℓ,a, and every point of a box is within C S*^(−3) of its representative (p. 74). The squared partition lets quadratic covariances of locally built waves sum exactly to the target stress: (7.30) uses Σβ ηβ^2 = 1. The two signs give each box two wave families, which a two-component stress needs (T = c1 v1 + c2 v2). ANTECEDENT: None cited. REFS: p. 64 (the partitions, Cℓ, Aℓ, (6.8)); p. 65 ((6.9), the partition identity, the compactness of supports); used at p. 74 and p. 84 ((7.30)).",
"obligation": "It localizes each wave to a region where the background shear varies little: Section 7 freezes the frame and growth parameters at x0ℓ,a, and every point of a box is within C S*^(−3) of its representative (p. 74). The squared partition lets quadratic covariances of locally built waves sum exactly to the target stress: (7.30) uses Σβ ηβ^2 = 1. The two signs give each box two wave families, which a two-component stress needs (T = c1 v1 + c2 v2).",
"backward_question": "How do I cut the annulus into pieces small enough that the shear is effectively constant on each, yet recover the prescribed stress exactly when the quadratic fluxes of the pieces are added?",
"mechanism": "If the waves ηβ Wβ of different boxes never multiply each other (M6.7), their quadratic fluxes add as Σβ ηβ^2 C(Wβ). If each box's waves have covariance equal to the target, a squared partition returns the target exactly. The mesh S*^(−3) is small enough to make frozen-coefficient errors small in inverse powers of S*, and differentiating the cutoffs costs only powers of S*, which are harmless logarithmic losses. On the supports, R lies in a fixed compact subinterval of (0, ∞) and Z, T lie in bounded intervals.",
"antecedent": "None cited.",
"cost": "The number of boxes grows polynomially in S* (Lemma 6.3), and cutoff derivatives grow like powers of S*. Representatives, labels, and all other discrete choices are fixed before any differentiation. It needs a large lower band index ℓ0 and qbig ≤ 2^(−ℓ0), and supports are taken in the coordinate domain including its smooth extension near τ = 0.",
"checkable": "Build the one-dimensional squared partition χa = φa / √(Σb φb^2) from translates φa of a bump on a grid with mesh S^(−3). Check that Σ χa^2 = 1 to machine precision, that supports stay within one mesh length of their grid points, and that sup|∂^k χa| scales like S^(3k). Tensorize to (R, Z, T) and repeat, and do the same construction in log2 q for the dyadic partition.",
"depends_on": [
"M6.1",
"M4.8"
],
"constrains": [],
"reasons": {
"M6.1": "The dyadic partition runs over bands q ≍ Q = 2^{-ℓ}, and the box partition has mesh S*^{-3} in the chart coordinates (R, Z, T).",
"M4.8": "The active part A_ℓ is cut out by the fixed annulus Xa ≤ r²/(2q) ≤ Xb of Theorem 4.6, where the stress lives."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 64",
"analogous_to": [],
"relations": {
"M6.1": "prerequisite",
"M4.8": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M6.6",
"kind": "move",
"name": "ns-m6-6-auxiliary-rectangles-the-pulse-clock-and-the-rectangle",
"title": "Auxiliary rectangles, the pulse clock, and the rectangle cutoffs",
"section": "6",
"pages": "65",
"refs": [
"p. 65, (6.10), (6.11), (6.12)",
"p. 66, (6.16)",
"used at p. 78 (Proposition 7.2) and p. 82 to 83 ((7.27))."
],
"statement": "Section 6 (pp. 65-66): each label gets a band-torus rectangle Rγ = {cγ + ξvr + ηvt : |ξ|, |η| < r0} (mod Z^2), an enlargement R+γ (2r0), and preimages Rabs_γ, Rabs,+_γ under π_(i(ℓ)) (6.10). On a lift Yi − cγ − kcopy = ξg vr + ηg vt, v = (ηg + r0)/ci, Ls = 2r0/ci ≍ S* (6.11); Li ηg = Ni ξg = 0, Ni ηg = Li ξg = 1, so Dr v = Dz v = 0, t* v = 1 (6.12). Cutoffs: χg ∈ C∞c((−r0, r0)), 0 ≤ χg ≤ 1; ψ = 1 on |v − Ls/2| ≤ Ls/5, supp ψ ⊂ {|v − Ls/2| < Ls/3} (6.16); both lie strictly inside the enlarged rectangle.",
"description": "Section 6 (pp. 65-66): each label gets a band-torus rectangle Rγ = {cγ + ξvr + ηvt : |ξ|, |η| < r0} (mod Z^2), an enlargement R+γ (2r0), and preimages Rabs_γ, Rabs,+_γ under π_(i(ℓ)) (6.10). On a lift Yi − cγ − kcopy = ξg vr + ηg vt, v = (ηg + r0)/ci, Ls = 2r0/ci ≍ S* (6.11); Li ηg = Ni ξg = 0, Ni ηg = Li ξg = 1, so Dr v = Dz v = 0, t* v = 1 (6.12). Cutoffs: χg ∈ C∞c((−r0, r0)), 0 ≤ χg ≤ 1; ψ = 1 on |v − Ls/2| ≤ Ls/5, supp ψ ⊂ {|v − Ls/2| < Ls/3} (6.16); both lie strictly inside the enlarged rectangle. OBLIGATION: It supplies a clock along which the linear pulse equation (7.5) becomes an ordinary differential equation in v (Proposition 7.2, Lemma 7.4), and the clock never enters a spatial derivative. It gives each label its own auxiliary territory for Lemma 6.1. ANTECEDENT: None cited for the clock or the rectangles. The introduction credits the evolution of wavevectors and polarizations along a background flow, which the clock hosts, to Lifschitz and Hameiri and to Friedlander and Vishik [17, 14]. REFS: p. 65, (6.10), (6.11), (6.12); p. 66, (6.16); used at p. 78 (Proposition 7.2) and p. 82 to 83 ((7.27)).",
"obligation": "It supplies a clock along which the linear pulse equation (7.5) becomes an ordinary differential equation in v (Proposition 7.2, Lemma 7.4), and the clock never enters a spatial derivative. It gives each label its own auxiliary territory for Lemma 6.1. And its area element |det(vr, vt)| dξg dηg, with dηg = ci dv, is what turns the Haar average of a pulse into a time integral in Proposition 7.5 ((7.27)).",
"backward_question": "Which torus coordinate can serve as \"time since the pulse began\", advancing at exactly unit rate under the normalized time derivative while staying invisible to radial and axial derivatives?",
"mechanism": "Because the rectangle's sides are aligned with the eigen-directions, time and radius decouple after evaluation: ηg depends on t alone (the vr component carries no ηg, since λt(vr) = 0) and ξg on r alone. So v is rescaled physical time during one pass through the rectangle, advancing at unit speed under t*, and ξg is a radial variable localized by χg. The torus is periodic, so as t increases the band coordinate re-enters the rectangles again and again; each pass is one pulse lasting Ls ≍ S* in v, during which the slow chart time moves by only ε Ls ≍ ε S*. The construction does not rely on this recurrence being equidistributed: it works with exact Haar averages and exactly inverts the fast derivative (Lemma 8.6). The cutoff ψ is applied only after the pulse equation is solved, and it equals 1 on the middle two-fifths of the interval. With the Gaussian envelope (7.16), the cutoff therefore acts only where the pulse is exp(−cS*)-small.",
"antecedent": "None cited for the clock or the rectangles. The introduction credits the evolution of wavevectors and polarizations along a background flow, which the clock hosts, to Lifschitz and Hameiri and to Friedlander and Vishik [17, 14].",
"cost": "It fixes a radius r0, which must be small for Lemma 6.1, and ties the pulse duration to ci and hence to the covering index. The envelope, and with it the flatness of the cutoff errors, is deferred to Section 7. The transverse cutoff χg(ξg) produces fast radial derivatives of size Mi, which is the source of the κs loss. Converting v derivatives into torus derivatives costs a power of S* ((6.22)).",
"checkable": "For sample (h, ℓ, r0, cγ), compute on a lift Yi(r, t) = Λg^i r^(dr) vr + Tg^i t vt, ηg = λt(Yi − cγ − kcopy) with λt(w) = vt·w/(1 + bg^2), and v = (ηg + r0)/ci. Verify by finite differences that Q^(1+h) ∂t v = 1 and ∂r v = 0 to rounding error, and that ξg does not depend on t. Given (7.16), also evaluate exp(−c (Ls/5)^2 / Ls) with Ls ≍ ℓ^2 against 2^(−Nℓ) to confirm that the region where ψ < 1 carries only flat pulse mass.",
"depends_on": [
"M6.3",
"M6.5",
"M6.2"
],
"constrains": [],
"reasons": {
"M6.3": "Rectangles live on the band torus of Y_i, and the clock v = (η_g + r_0)/c_i uses c_i, N_i, L_i so that t*v = 1 and D_r v = D_z v = 0.",
"M6.5": "Each label γ = (ℓ, a, σ) of the slow partition receives its own rectangle R_γ and its enlargement.",
"M6.2": "Rectangle sides are aligned with the eigen-directions v_r, v_t, which decouples radius and time after evaluation on the phase map."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 65",
"analogous_to": [],
"relations": {
"M6.3": "prerequisite",
"M6.5": "prerequisite",
"M6.2": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M6.7",
"kind": "move",
"name": "ns-m6-7-lemma-6-1-disjoint-auxiliary-supports-for-interacting",
"title": "Lemma 6.1, disjoint auxiliary supports for interacting labels",
"section": "6",
"pages": "65",
"refs": [
"p. 65 (statement, (6.13))",
"p. 66 ((6.14), (6.15), Steps 1 to 3, the product consequence)",
"used at p. 12, p. 82 (Proposition 7.5), and p. 84 ((7.30))."
],
"statement": "There are centers cγ and one radius r0 > 0, common to all labels and independent of the band, such that the enlarged rectangles are injectively parametrized and γ ≠ γ′ with Kγ ∩ Kγ′ ≠ ∅ implies Rabs,+_γ ∩ Rabs,+_γ′ = ∅ (6.13). Consequently, if supp Fγ ⊂ Kγ × Rabs,+_γ for every γ, then Fγ Fγ′ = 0 for γ ≠ γ′. This also holds for derivatives of smoothly extended fields and after evaluation on (6.3) (p. 66).",
"description": "There are centers cγ and one radius r0 > 0, common to all labels and independent of the band, such that the enlarged rectangles are injectively parametrized and γ ≠ γ′ with Kγ ∩ Kγ′ ≠ ∅ implies Rabs,+_γ ∩ Rabs,+_γ′ = ∅ (6.13). Consequently, if supp Fγ ⊂ Kγ × Rabs,+_γ for every γ, then Fγ Fγ′ = 0 for γ ≠ γ′. This also holds for derivatives of smoothly extended fields and after evaluation on (6.3) (p. 66). OBLIGATION: It removes every quadratic cross-interaction between distinct localized waves: the two families (signs) in one box, neighboring boxes, and overlapping neighboring bands. Without it, products of distinct overlapping waves would enter ∇·(w ⊗ w) at the same order as the target covariance. ANTECEDENT: None cited in Section 6. The introduction attributes realizing a prescribed stress with oscillations to the Euler constructions of Daneri and Székelyhidi [10]. The coloring step is a standard greedy coloring and is not cited. REFS: p. 65 (statement, (6.13)); p. 66 ((6.14), (6.15), Steps 1 to 3, the product consequence); used at p. 12, p. 82 (Proposition 7.5), and p. 84 ((7.30)).",
"obligation": "It removes every quadratic cross-interaction between distinct localized waves: the two families (signs) in one box, neighboring boxes, and overlapping neighboring bands. Without it, products of distinct overlapping waves would enter ∇·(w ⊗ w) at the same order as the target covariance. The lemma is what gives C(a+ b+ + a− b−) = H (a+^2, a−^2)^T in Proposition 7.5 and the cross-term-free sum (7.30). Throughout the correction cycle, harmonics and corrections with the same label still interact, but distinct labels never do.",
"backward_question": "Infinitely many localized waves at infinitely many scales overlap in space-time. Is there one finite choice of auxiliary positions that makes every pair with overlapping slow supports disjoint on the torus, even though each scale sees the torus through a different covering?",
"mechanism": "Three steps. (1) Build an interaction graph. Join two labels if their enlarged slow boxes meet and their band indices differ by at most four, and also join the two signs of one box. Meeting dyadic supports force |ℓ − ℓ′| ≤ 2, and bands within four of each other have comparable chart scales and comparable ratios ℓ^2/ℓ′^2, so the degree is bounded independently of the band. Their covering indices differ by at most ∆max, by (6.14). (2) Greedily color the countable bounded-degree graph with finitely many colors. Give each color a rational center that avoids the finitely many relations cµ ≡ Jg^∆ cν (mod Z^2) for 0 ≤ ∆ ≤ ∆max, except the trivial case (∆, ν, µ) = (0, ν, ν) (6.15). Each forbidden relation is a proper closed condition; for a color paired with itself and ∆ > 0 this uses the invertibility of Jg^∆ − I. So a rational tuple avoiding all of them exists, and the forbidden differences keep a positive distance from the lattice. (3) If a point lay in the lifted rectangles of adjacent labels at levels i and i + ∆, then cµ − Jg^∆ cν ≡ Jg^∆ eν − eµ with |eν| + |eµ| ≤ C r0. Since ∆ is bounded, this is impossible for one small fixed r0. Only finitely many colors and values of ∆ occur, so a single r0 works for all bands.",
"antecedent": "None cited in Section 6. The introduction attributes realizing a prescribed stress with oscillations to the Euler constructions of Daneri and Székelyhidi [10]. The coloring step is a standard greedy coloring and is not cited.",
"cost": "It fixes a finite palette of colors, the centers, r0, and ∆max. Every wave coefficient and correction must stay supported in Kγ × Rabs,+_γ (precisely, in Ωγ or Ωcut_γ of (6.28)) through the whole correction cycle, which Proposition 9.6 must preserve. Separating the supports of derivatives requires smooth zero extension, so cross-label products are formed only after the time cutoff; before the cutoff the algebra is used on one labeled rectangle only.",
"checkable": "Take K colors, with K equal to the graph degree plus one, and random rational centers. Compute d_min, the minimum over ordered (ν, µ, ∆) ≠ (ν, ν, 0) with 0 ≤ ∆ ≤ ∆max of dist(cµ − Jg^∆ cν, Z^2), and confirm d_min > 0. Choose r0 with (1 + ‖Jg‖^(∆max)) · 2√2 · |vr| · r0 < d_min, then sample Y ∈ T^2 by Monte Carlo and confirm that no sample lies in both Jg^(−i)(R+ν) and Jg^(−(i+∆))(R+µ). Also check det(Jg^∆ − I) ≠ 0: it equals 7, 161, and 2569 for ∆ = 1, 2, 3 (computed here). And check the observed maximum of |i(ℓ) − i(ℓ′)| over |ℓ − ℓ′| ≤ 4: it is 2 for ℓ in [20, 5000) (computed here), below the bound in (6.14).",
"depends_on": [
"M6.6",
"M6.5",
"M6.3",
"M6.2"
],
"constrains": [],
"reasons": {
"M6.6": "Separates the enlarged rectangles R^+_γ, with centers c_γ and one radius r_0, attached to the labels.",
"M6.5": "The labels, their slow supports K_γ, and the bounded-degree interaction graph (both signs, neighboring boxes and bands) come from the slow partition.",
"M6.3": "Bands whose supports meet have covering indices i(ℓ) differing by at most Δmax by (6.14), so one finite choice of centers serves all bands.",
"M6.2": "The forbidden center relations are avoided using the invertibility of J_g^Δ − I for the fixed integer matrix J_g."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 65",
"analogous_to": [],
"relations": {
"M6.6": "prerequisite",
"M6.5": "prerequisite",
"M6.3": "prerequisite",
"M6.2": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "digest-only",
"hypotheses_checked": "not-checked",
"computation_checked": true,
"astra_spot_check": null
}
},
{
"id": "M6.8",
"kind": "move",
"name": "ns-m6-8-lemma-6-2-a-common-torus-for-overlapping-bands",
"title": "Lemma 6.2, a common torus for overlapping bands",
"section": "6",
"pages": "66-67",
"refs": [
"p. 66 to 67 ((6.17), (6.18), Lemma 6.2, (6.19), (6.20))",
"p. 68 (c_(i0), M_(i0))",
"p. 17 (convention (3.8) citing (6.19))."
],
"statement": "Section 6 (pp. 66-68): fix (z, t) and a small U with band indices within four; i0 = min i(ℓ) over bands meeting U, H = π_(i0)(Y) (6.17); ∆ℓ = i(ℓ) − i0 ∈ {0, ..., ∆max}, Yi = Jg^(∆ℓ)H, RH_γ = π_(∆ℓ)^(−1)(Rγ) (6.18). Lemma 6.2: H ↦ Yi has uniformly bounded derivative factors; RH_γ is 14^(∆ℓ) ≤ 14^(∆max) disjoint lifts of Rγ; ∫f(Jg^∆H)dH = ∫f(Yi)dYi (6.19); radial integration at fixed (z, t), torus translation, averaging, and directional Fourier inversion on zero-mean functions keep common-torus descent and add no band. Overlaps obey (6.20); c_(i0) = Tg^(−∆)ci, M_(i0) = Λg^(−∆)Mi (p. 68).",
"description": "Section 6 (pp. 66-68): fix (z, t) and a small U with band indices within four; i0 = min i(ℓ) over bands meeting U, H = π_(i0)(Y) (6.17); ∆ℓ = i(ℓ) − i0 ∈ {0, ..., ∆max}, Yi = Jg^(∆ℓ)H, RH_γ = π_(∆ℓ)^(−1)(Rγ) (6.18). Lemma 6.2: H ↦ Yi has uniformly bounded derivative factors; RH_γ is 14^(∆ℓ) ≤ 14^(∆max) disjoint lifts of Rγ; ∫f(Jg^∆H)dH = ∫f(Yi)dYi (6.19); radial integration at fixed (z, t), torus translation, averaging, and directional Fourier inversion on zero-mean functions keep common-torus descent and add no band. Overlaps obey (6.20); c_(i0) = Tg^(−∆)ci, M_(i0) = Λg^(−∆)Mi (p. 68). OBLIGATION: Fields from bands with different coverings can be added, multiplied, averaged, and inverted in one coordinate system without changing their physical values. Haar averages, and with them covariances and the \"mean\" parts of Sections 7 and 8, do not depend on the representation, as the averaging convention (3.8) requires. The separation (6.13) carries over to the common torus because π_(i0) is surjective. MECHANISM: All band tori are quotients of the absolute torus through powers of one matrix, and the bands meeting a small neighborhood have covering indices within ∆max of each.",
"obligation": "Fields from bands with different coverings can be added, multiplied, averaged, and inverted in one coordinate system without changing their physical values. Haar averages, and with them covariances and the \"mean\" parts of Sections 7 and 8, do not depend on the representation, as the averaging convention (3.8) requires. The separation (6.13) carries over to the common torus because π_(i0) is surjective.",
"backward_question": "Waves from neighboring scales overlap but live on differently covered tori. Is there one torus on which all of them are genuine functions, with the same averages and comparable derivatives?",
"mechanism": "All band tori are quotients of the absolute torus through powers of one matrix, and the bands meeting a small neighborhood have covering indices within ∆max of each other. Each band torus near the point is the image of H under Jg^(∆ℓ), so band fields pull back to the common cover H, and the bounded powers Jg^(∆ℓ) change derivatives only by bounded matrices. Haar compatibility is checked on characters: a character of frequency n pulls back to frequency (Jg^∆)^T n, which is zero exactly when n = 0. The number of lifts is |det Jg|^∆ = 14^∆. Radial integration holds (z, t) fixed, hence q and every band cutoff, so no new band enters even though the integral crosses many radial boxes. Translations commute with deck translations, and averaging and directional multipliers preserve the lattice of pullback frequencies.",
"antecedent": "None cited.",
"cost": "The common torus is only a local representation that depends on U, and every coefficient must satisfy (6.20) on overlaps. A sum of band fields descends to H but in general not to any single band torus, since it can take different values at distinct preimages; this forces the per-lift path of M6.10. Lift counts pick up a fixed factor 14^(∆max).",
"checkable": "Verify #(Z^2 / Jg^∆ Z^2) = |det Jg^∆| = 14^∆ from Smith normal forms: diag(1, 14) for Jg, diag(2, 98) for Jg^2 = [[10, 8], [8, 26]], and diag(2, 1372) for Jg^3 (computed here). Verify (6.19) by quadrature of f(Jg^∆ H) over T^2 for random trigonometric polynomials f; the result should equal the zero Fourier coefficient. Check c_(i0) = Tg^(−∆) ci and M_(i0) = Λg^(−∆) Mi from the definitions.",
"depends_on": [
"M6.3",
"M6.7",
"M6.5",
"M6.6"
],
"constrains": [],
"reasons": {
"M6.3": "Unifies the band tori Y_i = J_g^i Y of overlapping bands on the coarsest covering H = π_{i0}(Y), with deck translations and rescaled c_i, M_i.",
"M6.7": "The bound Δ_ℓ ≤ Δmax on covering-index differences comes from (6.14), and the separation (6.13) carries over to the common torus.",
"M6.5": "The band set L(U) is read off the supports of the dyadic cutoffs χ_ℓ(q), which overlap only for neighboring bands.",
"M6.6": "Lifts each label rectangle R_γ to the common torus as 14^{Δ_ℓ} disjoint copies R^H_γ."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 66-67",
"analogous_to": [],
"relations": {
"M6.3": "prerequisite",
"M6.7": "prerequisite",
"M6.5": "prerequisite",
"M6.6": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: TRUNCATED; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": true,
"astra_spot_check": null
}
},
{
"id": "M6.9",
"kind": "move",
"name": "ns-m6-9-lemma-6-3-counting-relevant-labels",
"title": "Lemma 6.3, counting relevant labels",
"section": "6",
"pages": "68",
"refs": [
"p. 68 (Lemma 6.3 and the paragraph after it)."
],
"statement": "At any point, #{γ ∈ Γ : (r, z, t) ∈ Kγ} ≤ C. For a fixed band ℓ, a compact chart set B, and a bounded normalized radial interval IR: #{(ℓ, a, σ) : Bℓ,a ∩ B ≠ ∅} ≤ C_B Sℓ^9, and the supremum over (Z, T) of #{(ℓ, a, σ) : Bℓ,a ∩ (IR × {Z} × {T}) ≠ ∅} is at most C_IR Sℓ^3. The same bounds hold for fixed-factor enlargements of the boxes. During radial integration the band set L(z, t) is fixed, so one integral meets O(S_ref^3) labels, and the common-torus lifts add at most the factor 14^(∆max).",
"description": "At any point, #{γ ∈ Γ : (r, z, t) ∈ Kγ} ≤ C. For a fixed band ℓ, a compact chart set B, and a bounded normalized radial interval IR: #{(ℓ, a, σ) : Bℓ,a ∩ B ≠ ∅} ≤ C_B Sℓ^9, and the supremum over (Z, T) of #{(ℓ, a, σ) : Bℓ,a ∩ (IR × {Z} × {T}) ≠ ∅} is at most C_IR Sℓ^3. The same bounds hold for fixed-factor enlargements of the boxes. During radial integration the band set L(z, t) is fixed, so one integral meets O(S_ref^3) labels, and the common-torus lifts add at most the factor 14^(∆max). OBLIGATION: Pointwise sums over labels have bounded overlap and cost only a constant. Radial integrals (pressure reconstruction, stress primitives, radial moments), which collect many boxes, cost only polynomial factors in S*, and the classes absorb those. MECHANISM: Pure counting. At a point, the dyadic partition and each one-dimensional grid partition overlap boundedly, and the two signs add a factor of two. A mesh of size S^(−3) has O(S^3) positions on a bounded interval, so a compact three-dimensional chart set meets O(S^9) boxes and a radial line meets O(S^3). ANTECEDENT: None cited. REFS: p. 68 (Lemma 6.3 and the paragraph after it).",
"obligation": "Pointwise sums over labels have bounded overlap and cost only a constant. Radial integrals (pressure reconstruction, stress primitives, radial moments), which collect many boxes, cost only polynomial factors in S*, and the classes absorb those.",
"backward_question": "When an operation such as radial integration sums contributions from many slow boxes, how many can there be, and is the count only logarithmic in 1/q?",
"mechanism": "Pure counting. At a point, the dyadic partition and each one-dimensional grid partition overlap boundedly, and the two signs add a factor of two. A mesh of size S^(−3) has O(S^3) positions on a bounded interval, so a compact three-dimensional chart set meets O(S^9) boxes and a radial line meets O(S^3). Enlarging the boxes by a fixed factor changes only the constants.",
"antecedent": "None cited.",
"cost": "Polynomial growth S^3 along radial lines and S^9 on compact chart sets, absorbed into the S*^b factors of the classes. It requires the values Sℓ for ℓ ∈ L(U) to be comparable, which holds because those bands differ by at most four.",
"checkable": "An elementary count, essentially a pure estimate. Count grid boxes of side S^(−3), enlarged by a fixed factor, that meet a unit cube and a unit radial segment for S = ℓ^2 with ℓ from 10 to 100, and fit the growth exponents 9 and 3.",
"depends_on": [
"M6.5",
"M6.8"
],
"constrains": [],
"reasons": {
"M6.5": "Counts boxes of mesh S*^{-3} and the two signs of the slow partition, using bounded overlap of the dyadic and grid cutoffs.",
"M6.8": "The factor 14^{Δmax} from common-torus lifts and the fixed band set during radial integration come from Lemma 6.2."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 68",
"analogous_to": [],
"relations": {
"M6.5": "prerequisite",
"M6.8": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "digest-only",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M6.10",
"kind": "move",
"name": "ns-m6-10-the-pulse-path-on-the-common-torus",
"title": "The pulse path on the common torus",
"section": "6",
"pages": "68",
"refs": [
"p. 68 ((6.21), (6.22))",
"p. 69 (the Y form, deck translations, descent)",
"used at p. 78 to 80 (Proposition 7.2, Step 3)."
],
"statement": "Section 6 (pp. 68-69): with λt(w) = vt·w/(1 + bg^2) and ηg(H) = λt(Jg^∆H − cγ − kcopy) on a lifted band rectangle, the path Hw = H + Tg^(−∆)ci(w − v(H))vt = H0 + Tg^(−∆)ci w vt, H0 = H − Tg^(−∆)(ηg(H) + r0)vt, w ∈ [0, Ls] (6.21), keeps the slow coordinates and ξg of H and has pulse coordinate w; DH Hw = I − vtλt, DH v = (Tg^∆/ci)λt = O(S*), higher derivatives vanish (6.22). In Y the path is Y′ = Y + Tg^(−i)(η′g − ηg)vt; deck translations preserving H translate it, so a unique zero-data solution descends to the common torus (p. 69).",
"description": "Section 6 (pp. 68-69): with λt(w) = vt·w/(1 + bg^2) and ηg(H) = λt(Jg^∆H − cγ − kcopy) on a lifted band rectangle, the path Hw = H + Tg^(−∆)ci(w − v(H))vt = H0 + Tg^(−∆)ci w vt, H0 = H − Tg^(−∆)(ηg(H) + r0)vt, w ∈ [0, Ls] (6.21), keeps the slow coordinates and ξg of H and has pulse coordinate w; DH Hw = I − vtλt, DH v = (Tg^∆/ci)λt = O(S*), higher derivatives vanish (6.22). In Y the path is Y′ = Y + Tg^(−i)(η′g − ηg)vt; deck translations preserving H translate it, so a unique zero-data solution descends to the common torus (p. 69). OBLIGATION: Proposition 7.2 must integrate the amplitude equation from the start of a pulse to the current v, evaluating a source f(R, Z, T, Hw) along the path \"without averaging over the other preimages\", because a source built from several bands descends to H but not to Yi. (6.22) supplies this change of coordinates \"without a new power of ε.\" MECHANISM: vt is an eigenvector of Jg, so moving H by s vt moves Yi = Jg^∆ H by Tg^∆ s vt. That raises ηg by Tg^∆ s and v by Tg^∆ s / ci, and choosing s = Tg^(−∆) ci (w − v(H)) lands at pulse coordinate w. ANTECEDENT: None cited.",
"obligation": "Proposition 7.2 must integrate the amplitude equation from the start of a pulse to the current v, evaluating a source f(R, Z, T, Hw) along the path \"without averaging over the other preimages\", because a source built from several bands descends to H but not to Yi. (6.22) supplies this change of coordinates \"without a new power of ε.\"",
"backward_question": "If a source lives on the finer common torus but not on the band torus, along which curve do I integrate the pulse equation so that the solution is a well-defined function on the common torus?",
"mechanism": "vt is an eigenvector of Jg, so moving H by s vt moves Yi = Jg^∆ H by Tg^∆ s vt. That raises ηg by Tg^∆ s and v by Tg^∆ s / ci, and choosing s = Tg^(−∆) ci (w − v(H)) lands at pulse coordinate w. Nothing else changes: the vr component (ξg) is untouched, and the slow variables are parameters. The map is affine in H, its Jacobian is the bounded projection I − vt λt, and the gradient of the v coordinate is O(S*). Uniqueness for the zero-data initial value problem, combined with deck equivariance of the path, gives descent.",
"antecedent": "None cited.",
"cost": "Converting pulse-coordinate derivatives into H derivatives costs powers of S* (DH v = O(S*)). The solution is defined lift by lift, so the copy index kcopy matters. Support containment holds when the source vanishes along the whole rectangle.",
"checkable": "For random H on a lift, ∆ ∈ {0, 1, 2, 3}, and sample ci, r0, cγ, compute Hw from (6.21). Verify v(Hw) = w and ξg(Hw) = ξg(H) (using the dual functional for vr), and compare finite-difference Jacobians with I − vt λt and (Tg^∆ / ci) λt. This is an exact linear-algebra check.",
"depends_on": [
"M6.8",
"M6.6",
"M6.2"
],
"constrains": [],
"reasons": {
"M6.8": "The path lives on the common torus H with Y_i = J_g^Δ H, since a source built from several bands descends to H but not to a band torus.",
"M6.6": "Moves only the pulse coordinate v = (η_g + r_0)/c_i of a lifted rectangle, keeping the transverse coordinate ξ_g and the slow variables fixed.",
"M6.2": "Uses that v_t is an eigenvector of J_g, so a shift along v_t on H moves Y_i along v_t by the factor T_g^Δ."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 68",
"analogous_to": [],
"relations": {
"M6.8": "prerequisite",
"M6.6": "prerequisite",
"M6.2": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},