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": "M8.4",
"kind": "move",
"name": "ns-m8-4-flatness-of-the-cutoff-remainder-under-the-weighted-mean",
"title": "Flatness of the cutoff remainder under the weighted mean condition",
"section": "8",
"pages": "90-92",
"refs": [
"pages 90 to 92",
"(8.8), (8.10)",
"Lemma 8.2, Step 3",
"(6.7) on page 64."
],
"statement": "Lemma 8.2, remainder clause: if ∫R^e ⟨f⟩_Y dR = 0 at every (Z, T), then ⟨A_e f⟩_Y = 0 and, for every fixed I and integer p ≥ 1, |∂^I A_e f| ≤ C_{j,I,p} ε^{α + pκ_s} S_*^{B_{j,I,p}} ζ δ^{−B_{j,I,p}} (8.8). If f is Y-independent with ∫R^e f dR = 0, then A_e f ≡ 0. The torus inverse obeys ‖L^{−p}H‖_{C^m_y} ≤ C_{m,p}‖H‖_{C^{m+p+3}_y} for zero-mean H, L = v_r·∂_y (8.10).",
"description": "Lemma 8.2, remainder clause: if ∫R^e ⟨f⟩_Y dR = 0 at every (Z, T), then ⟨A_e f⟩_Y = 0 and, for every fixed I and integer p ≥ 1, |∂^I A_e f| ≤ C_{j,I,p} ε^{α + pκ_s} S_*^{B_{j,I,p}} ζ δ^{−B_{j,I,p}} (8.8). If f is Y-independent with ∫R^e f dR = 0, then A_e f ≡ 0. The torus inverse obeys ‖L^{−p}H‖_{C^m_y} ≤ C_{m,p}‖H‖_{C^{m+p+3}_y} for zero-mean H, L = v_r·∂_y (8.10). OBLIGATION: Makes the inverse exact up to a flat error even when the source depends on the torus, which is precisely the case of the axial increments produced by the temporal inverse (8.20). Without it, the torus-oscillating part of J g would leave a non-flat error where χ_m varies. MECHANISM: Haar invariance gives ⟨J g⟩_Y = ∫⟨g⟩_Y dR, which vanishes by hypothesis for g = R^e f. ANTECEDENT: None cited. Internal: the Diophantine inequality (6.7), proved in Section 6 by multiplying v_r·n = (n_1 + n_2) − √2 n_2 by its algebraic conjugate, which gives a nonzero integer. Recognizable classical ingredients (not cited): small divisors for a linear flow on T^2 with a badly approximable slope, and repeated integration by parts. REFS: pages 90 to 92; (8.8), (8.10); Lemma 8.2, Step 3; (6.7) on page 64.",
"obligation": "Makes the inverse exact up to a flat error even when the source depends on the torus, which is precisely the case of the axial increments produced by the temporal inverse (8.20). Without it, the torus-oscillating part of J g would leave a non-flat error where χ_m varies.",
"backward_question": "When a torus-dependent source has zero weighted torus-mean integral but a nonzero full radial integral at each torus point, is the oscillating part of that integral small, and how small?",
"mechanism": "Haar invariance gives ⟨J g⟩_Y = ∫⟨g⟩_Y dR, which vanishes by hypothesis for g = R^e f. The zero-mean part is a nonstationary-phase integral: along u ↦ (U + u, y + Mu v_r) a torus mode k oscillates at frequency 2πM(v_r·k). Since d/du of L^{-1}F° along the path equals ∂_U L^{-1}F° + M F°, integrating p times gives the exact identity J g = (−M^{−1})^p ∫_R ∂_U^p L^{−p} F°(U + u, y + Mu v_r) du, with no endpoint terms by compact support. L^{−1} exists on zero-mean functions with finite derivative loss because of the Diophantine bound |v_r·k| ≥ c/(1 + |k|) of (6.7). Because M^{−1} ≤ C ε^{κ_s} S_*^{ρ_g}, each integration gains ε^{κ_s}; for a target flatness order N and a physical derivative order with q-loss L, choose p with h(α + pκ_s) > N + L, and the strict excess absorbs the fixed powers of S_* = ℓ^2 (only logarithmic in 1/Q). Near-resonant frequencies (v_r·k small, |k| comparable to M) are paid for by the extra torus derivatives in (8.10); with only finite regularity one would get only finite flatness.",
"antecedent": "None cited. Internal: the Diophantine inequality (6.7), proved in Section 6 by multiplying v_r·n = (n_1 + n_2) − √2 n_2 by its algebraic conjugate, which gives a nonzero integer. Recognizable classical ingredients (not cited): small divisors for a linear flow on T^2 with a badly approximable slope, and repeated integration by parts.",
"cost": "Flatness holds only at each fixed derivative order. The number of torus derivatives needed grows like m + p + 3, constants depend on p, and no estimate uniform in p is asserted. Since κ_s = 10^{−5}, p must be of order (N + L)/(hκ_s), so every torus-dependent source must be controlled at every derivative order.",
"checkable": "Take F(U, y) = exp(−U^2)cos(2πk·y) with k ≠ 0; compute ∫F(U + u, y + Mu v_r) du by quadrature for increasing M and compare with the closed form, whose amplitude is √π exp(−π^2 M^2 (v_r·k)^2), faster than any power of M. Separately check that |v·n|(1 + |n|) stays bounded below for v = v_r, v_t. Run while digesting: the minimum over 0 < max(|n_1|, |n_2|) ≤ 300 is about 0.385 for both.",
"depends_on": [
"M8.3",
"M6.4",
"M6.3",
"M6.8"
],
"constrains": [],
"reasons": {
"M8.3": "Estimates the cutoff remainder A_e f = R^{-e}(∂_Rχ_m)J(R^e f) of the primitive T_e.",
"M6.4": "The torus inverse L^{-p} on zero-mean functions loses only p + 3 derivatives by the Diophantine bound (6.7) for v_r.",
"M6.3": "Each integration by parts along the path gains M^{-1} ≤ Cε^{κ_s}S*^{ρ_g}, the radial winding of the covering.",
"M6.8": "Haar invariance on the common torus gives ⟨Jg⟩_Y = ∫⟨g⟩_Y dR, which vanishes under the weighted mean condition."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 90-92",
"analogous_to": [],
"relations": {
"M8.3": "prerequisite",
"M6.4": "prerequisite",
"M6.3": "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": "M8.5",
"kind": "move",
"name": "ns-m8-5-compactly-supported-pressure-with-the-defect-p-isolated",
"title": "Compactly supported pressure with the defect P isolated on a bump",
"section": "8",
"pages": "92-93",
"refs": [
"pages 92 to 93",
"(8.11), (8.12), (8.13)",
"Proposition 8.3(i)."
],
"statement": "Proposition 8.3(i): with a fixed bump ρ_phys = q^{−1/2} ρ̂(r/√q) in the mean patch, ∫ρ̂ = 1, ρ = Q^{1/2} ρ_phys, define P = ∫⟨g_r⟩_Y dR and p_m = T_0(g_r − ρP) (8.12). Then D_r p_m − g_r = −ρP − A_0(g_r − ρP) and ∂_R⟨p_m⟩_Y = ⟨g_r⟩_Y − ρP (8.13). If g_r ∈ M^α then P ∈ S^α and p_m ∈ M^α, changes of g_r in M^α give pressure changes in M^α, and the remainder has zero auxiliary mean and is flat.",
"description": "Proposition 8.3(i): with a fixed bump ρ_phys = q^{−1/2} ρ̂(r/√q) in the mean patch, ∫ρ̂ = 1, ρ = Q^{1/2} ρ_phys, define P = ∫⟨g_r⟩_Y dR and p_m = T_0(g_r − ρP) (8.12). Then D_r p_m − g_r = −ρP − A_0(g_r − ρP) and ∂_R⟨p_m⟩_Y = ⟨g_r⟩_Y − ρP (8.13). If g_r ∈ M^α then P ∈ S^α and p_m ∈ M^α, changes of g_r in M^α give pressure changes in M^α, and the remainder has zero auxiliary mean and is flat. OBLIGATION: Solves the radial mean balance by pressure alone while keeping p_m compactly supported in the shell. A direct radial integral of g_r would leave the constant P beyond the shell and alter the exterior pressure normalization of (3.5). The obstruction is compressed into one scalar P(Z, T) times a fixed interior bump, to be cancelled later by the third row of (8.25). MECHANISM: The shifted source g_r − ρP has zero weighted auxiliary-mean integral, P − P∫ρ dR = 0, so Lemma 8.2 with e = 0 applies and its. ANTECEDENT: None cited. Internal parallel: the pressure increment C_p among the five cumulative profile integrals (4.15), whose preservation keeps the exterior pressure unchanged across profile joins (Lemma 4.4). REFS: pages 92 to 93; (8.11), (8.12), (8.13); Proposition 8.3(i).",
"obligation": "Solves the radial mean balance by pressure alone while keeping p_m compactly supported in the shell. A direct radial integral of g_r would leave the constant P beyond the shell and alter the exterior pressure normalization of (3.5). The obstruction is compressed into one scalar P(Z, T) times a fixed interior bump, to be cancelled later by the third row of (8.25).",
"backward_question": "The pressure obtained by integrating the centrifugal balance outward is a nonzero constant beyond the shell; how can the pressure stay compactly supported, and where should the obstruction go?",
"mechanism": "The shifted source g_r − ρP has zero weighted auxiliary-mean integral, P − P∫ρ dR = 0, so Lemma 8.2 with e = 0 applies and its remainder is flat with zero auxiliary mean; after auxiliary averaging, ∂_R⟨p_m⟩_Y = ⟨g_r⟩_Y − ρP holds exactly. P ∈ S^α follows by integrating derivatives over the bounded shell; ρP ∈ M^α because ρ is an interior bump. Since ρ is fixed independently of the velocity, the same argument bounds pressure differences by source differences.",
"antecedent": "None cited. Internal parallel: the pressure increment C_p among the five cumulative profile integrals (4.15), whose preservation keeps the exterior pressure unchanged across profile joins (Lemma 4.4).",
"cost": "The defect P ∈ S^α and a standing term −ρP in the radial equation until it is corrected. The pressure must be reconstructed after every velocity change; the radial residual of every correction state is −ρP plus a flat remainder (Definition 9.4).",
"checkable": "For Y-independent compactly supported g_r(R) and a unit-mass bump ρ, compute P = ∫g_r dR and p_m(R) = ∫_0^R (g_r − ρP) dR′, and check p_m = 0 beyond the shell and ∂_R p_m − g_r = −ρP. Run while digesting inside the (8.16) test of M8.7: p_m vanishes exactly at the outer edge.",
"depends_on": [
"M8.3",
"M8.4",
"M8.2"
],
"constrains": [],
"reasons": {
"M8.3": "Defines p_m = T_0(g_r − ρP) with the e = 0 primitive, compactly supported in the shell, with D_r T_0 f = f − A_0 f.",
"M8.4": "The shifted source has zero weighted auxiliary-mean integral, so the remainder A_0(g_r − ρP) has zero mean and is flat.",
"M8.2": "Solves the radial row D_r p_m = g_r of the angular-mean balance, with g_r from (8.3)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 92-93",
"analogous_to": [],
"relations": {
"M8.3": "prerequisite",
"M8.4": "prerequisite",
"M8.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": "M8.6",
"kind": "move",
"name": "ns-m8-6-axial-increments-realized-by-a-compactly-supported",
"title": "Axial increments realized by a compactly supported azimuthal potential",
"section": "8",
"pages": "93",
"refs": [
"page 93",
"(8.14)",
"Proposition 8.3(ii)."
],
"statement": "Proposition 8.3(ii): for a shell-supported desired axial increment γ_d with ∫R⟨γ_d⟩_Y dR = 0 at every (Z, T), set Ψ = r^{−1} I_c(r γ_{d,phys}) using (8.4), and Ψ_* = T_1 γ_d, ∆β = −ε∂_Z Ψ_*, ∆γ = (D_r + 1/R)Ψ_* = γ_d − A_1 γ_d (8.14). The increment (∆β, 0, ∆γ) is exactly divergence-free and ⟨∆γ⟩_Y = ⟨γ_d⟩_Y. If γ_d ∈ M^α then Ψ_*, ∆γ ∈ M^α and ∆β ∈ M^{α+1}; if γ_d is Y-independent, ∆γ = γ_d pointwise. Pressure and potential stay in the shell and in the (Z, T)-projection of the source.",
"description": "Proposition 8.3(ii): for a shell-supported desired axial increment γ_d with ∫R⟨γ_d⟩_Y dR = 0 at every (Z, T), set Ψ = r^{−1} I_c(r γ_{d,phys}) using (8.4), and Ψ_* = T_1 γ_d, ∆β = −ε∂_Z Ψ_*, ∆γ = (D_r + 1/R)Ψ_* = γ_d − A_1 γ_d (8.14). The increment (∆β, 0, ∆γ) is exactly divergence-free and ⟨∆γ⟩_Y = ⟨γ_d⟩_Y. If γ_d ∈ M^α then Ψ_*, ∆γ ∈ M^α and ∆β ∈ M^{α+1}; if γ_d is Y-independent, ∆γ = γ_d pointwise. Pressure and potential stay in the shell and in the (Z, T)-projection of the source. OBLIGATION: Lets later steps prescribe the axial mean velocity (from the temporal inverse and from the five-equation map) while preserving exact incompressibility, required by Theorem 3.1(i), and compact support, and supplies the induced radial velocity without solving an elliptic problem. MECHANISM: The potential Ψe_θ generates the meridional velocity (−∂_z Ψ, 0, (r + 1/r)Ψ); ANTECEDENT: None cited. Recognizable classical ingredient (not cited): the Stokes streamfunction (azimuthal vector potential) of an axisymmetric meridional flow. Internal: the same device builds the background, A_n = (S_n/r)e_θ in (5.27). REFS: page 93; (8.14); Proposition 8.3(ii).",
"obligation": "Lets later steps prescribe the axial mean velocity (from the temporal inverse and from the five-equation map) while preserving exact incompressibility, required by Theorem 3.1(i), and compact support, and supplies the induced radial velocity without solving an elliptic problem.",
"backward_question": "How can one prescribe the axial mean velocity inside a thin shell and keep the field exactly divergence-free and compactly supported, and what does the anisotropic geometry say about the size of the radial velocity this forces?",
"mechanism": "The potential Ψe_θ generates the meridional velocity (−∂_z Ψ, 0, (r + 1/r)Ψ); because r and ∂_z commute after phase evaluation, (r + r^{−1})(−∂_z Ψ) + ∂_z((r + r^{−1})Ψ) = 0 identically. The weighted primitive identity (8.7) with e = 1 gives ∆γ = γ_d − A_1 γ_d, and the zero axial-flux integral makes the remainder mean-zero and flat and makes Ψ vanish beyond the shell. The radial component gains ε = Q^{1/2 − D} = Q^h because axial lengths Q^D exceed radial lengths Q^{1/2}: in the slender geometry, induced radial flows are one order smaller.",
"antecedent": "None cited. Recognizable classical ingredient (not cited): the Stokes streamfunction (azimuthal vector potential) of an axisymmetric meridional flow. Internal: the same device builds the background, A_n = (S_n/r)e_θ in (5.27).",
"cost": "Every desired axial increment must have zero axial flux. The realized ∆γ differs from γ_d by the flat remainder A_1 γ_d, which must be carried, since its products can acquire nonzero auxiliary means (M8.13).",
"checkable": "For γ_d(R) with ∫Rγ_d dR = 0, compute Ψ_* = R^{−1}∫_0^R R′γ_d dR′; verify (∂_R + 1/R)Ψ_* = γ_d, Ψ_* = 0 beyond the support, and symbolically (∂_R + 1/R)(−ε∂_Z Ψ_*) + ε∂_Z((∂_R + 1/R)Ψ_*) = 0.",
"depends_on": [
"M8.3",
"M8.4",
"M8.1",
"M6.12"
],
"constrains": [],
"reasons": {
"M8.3": "Ψ* = T_1γ_d uses the e = 1 primitive, so (D_r + 1/R)Ψ* = γ_d − A_1γ_d and Ψ vanishes beyond the shell.",
"M8.4": "Under zero axial flux the remainder A_1γ_d has zero auxiliary mean and is flat, and it vanishes when γ_d is Y-independent.",
"M8.1": "The increment has the mean-correction form (β, 0, γ), and its zero-flux hypothesis is the moment M_z of (8.2).",
"M6.12": "∆β = −ε∂_ZΨ* is one order smaller because D_z = ε∂_Z raises the class exponent by one."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 93",
"analogous_to": [],
"relations": {
"M8.3": "prerequisite",
"M8.4": "prerequisite",
"M8.1": "prerequisite",
"M6.12": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "digest-only",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M8.7",
"kind": "move",
"name": "ns-m8-7-the-three-compatibility-defects-and-the-integrated",
"title": "The three compatibility defects and the integrated identities",
"section": "8",
"pages": "93-94",
"refs": [
"pages 93 to 94",
"(8.15), (8.16), (8.17)",
"Proposition 8.4",
"consumer (9.12) on page 108."
],
"statement": "Define J_θ = ∫R^2⟨Gv + Vγ + γv + W_zθ⟩_Y dR, J_z = ∫R⟨2Gγ + γ^2 + W_zz⟩_Y dR − (1/2)∫R^2⟨g_r⟩_Y dR, and c_ρ = (1/2)∫R^2 ρ dR (8.15). Proposition 8.4: if (8.2) holds at every (Z, T) and p_m is reconstructed by (8.12), then ∫R^2⟨E_θ⟩_Y dR = ε∂_Z J_θ and ∫R⟨E_z⟩_Y dR = ε∂_Z(J_z + c_ρ P) (8.16). Physical and normalized moments are related by (8.17).",
"description": "Define J_θ = ∫R^2⟨Gv + Vγ + γv + W_zθ⟩_Y dR, J_z = ∫R⟨2Gγ + γ^2 + W_zz⟩_Y dR − (1/2)∫R^2⟨g_r⟩_Y dR, and c_ρ = (1/2)∫R^2 ρ dR (8.15). Proposition 8.4: if (8.2) holds at every (Z, T) and p_m is reconstructed by (8.12), then ∫R^2⟨E_θ⟩_Y dR = ε∂_Z J_θ and ∫R⟨E_z⟩_Y dR = ε∂_Z(J_z + c_ρ P) (8.16). Physical and normalized moments are related by (8.17). OBLIGATION: Characterizes exactly when the auxiliary-averaged tangential residuals can be written as radial divergences of compactly supported stresses (their R^2- and R-weighted integrals must vanish), reducing an infinite-dimensional obstruction to three scalar functions P, J_θ, J_z of (Z, T). It also shows the weighted moments carry an explicit factor ε∂_Z, a free gain of one order that Section 9 uses as (9.12). MECHANISM: The weights are exactly those that turn the cylindrical divergences into exact derivatives: R^2(∂_R + 2/R)F = ∂_R(R^2 F) and R(∂_R + 1/R)F = ∂_R(RF). ANTECEDENT: None cited. Internal: the zero-moment conditions with the same weights for the leading stress in Section 3.2 and Lemma A.8. REFS: pages 93 to 94; (8.15), (8.16), (8.17); Proposition 8.4; consumer (9.12) on page 108.",
"obligation": "Characterizes exactly when the auxiliary-averaged tangential residuals can be written as radial divergences of compactly supported stresses (their R^2- and R-weighted integrals must vanish), reducing an infinite-dimensional obstruction to three scalar functions P, J_θ, J_z of (Z, T). It also shows the weighted moments carry an explicit factor ε∂_Z, a free gain of one order that Section 9 uses as (9.12).",
"backward_question": "After every radial divergence integrates to zero by compact support, which scalar obstructions survive in the weighted integrals of the mean equations, and do they carry any extra small factor?",
"mechanism": "The weights are exactly those that turn the cylindrical divergences into exact derivatives: R^2(∂_R + 2/R)F = ∂_R(R^2 F) and R(∂_R + 1/R)F = ∂_R(RF). Hence every radial flux, including W and the base stress Σ, integrates to zero by compact support. Radial viscosity integrates to zero by two integrations by parts: for θ the coefficient is (2 − 1 − 1) = 0, for z it is −∫γ_R + ∫γ_R = 0. Auxiliary averaging turns t_* into −ε∂_T and D_r into ∂_R, so the time and axial-viscosity terms are ∂_T and ∂_Z^2 of the constrained moments (8.2), hence zero. Only the axial fluxes D_z(...) = ε∂_Z(...) survive. The pressure moment follows from the compactly supported reconstruction by one more integration by parts, ∫R⟨p_m⟩_Y dR = −(1/2)∫R^2 ∂_R⟨p_m⟩_Y dR = −(1/2)∫R^2⟨g_r⟩_Y dR + c_ρ P, which is why J_z contains the g_r moment. Because ρ is scaled by the moving q, c_ρ depends on (Z, T), so the whole product c_ρ P stays inside ∂_Z.",
"antecedent": "None cited. Internal: the zero-moment conditions with the same weights for the leading stress in Section 3.2 and Lemma A.8.",
"cost": "Three scalar defects that must be corrected at every cycle (M8.11). The (Z, T)-dependent c_ρ couples the P and J_z corrections.",
"checkable": "Symbolic check with Y-independent fields, run while digesting with exact residual 0 for both identities: on R ∈ [1, 2] with φ = (R − 1)^4(2 − R)^4, take the meridional correction from Ψ = φA(Z, T), v = φ(R − c)B(Z, T) with c chosen so ∫R^2 v dR = 0, an arbitrary polynomial base (b, V, G), compactly supported W and Σ, and a unit-mass ρ whose second moment depends on Z; compute g_r, P, p_m, E_θ, E_z, J_θ, J_z, c_ρ from (8.3), (8.12), (8.15), and compare both sides of (8.16).",
"depends_on": [
"M8.2",
"M8.1",
"M8.5",
"M6.3"
],
"constrains": [],
"reasons": {
"M8.2": "Integrates the conservative rows E_θ, E_z of (8.3), whose radial fluxes are cylindrical divergences that vanish under the R² and R weights.",
"M8.1": "The moments M_θ = M_z = 0 of (8.2) remove the time-derivative and axial-viscosity terms from the weighted integrals.",
"M8.5": "The pressure moment comes from the reconstruction (8.12), which puts −½∫R²⟨g_r⟩_Y and c_ρP into J_z.",
"M6.3": "Auxiliary averaging turns t* = −ε∂_T + c_{i0}N_{i0} into −ε∂_T and D_r into ∂_R, since torus derivatives average to zero."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 93-94",
"analogous_to": [],
"relations": {
"M8.2": "prerequisite",
"M8.1": "prerequisite",
"M8.5": "prerequisite",
"M6.3": "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": "M8.8",
"kind": "move",
"name": "ns-m8-8-auxiliary-independent-covariance-targets-for-the-averaged",
"title": "Auxiliary-independent covariance targets for the averaged tangential residual",
"section": "8",
"pages": "94-95",
"refs": [
"pages 94 to 95",
"(8.18)",
"Corollary 8.5",
"Proposition 7.6 and (7.31) on page 84",
"Proposition 9.6, Step 2 on pages 108 to 109."
],
"statement": "Corollary 8.5 (8.18): with interior bumps σ_{θ,phys} = q^{−3/2}σ̂_θ(r/√q), σ_{z,phys} = q^{−1}σ̂_z(r/√q), ∫ξ^2σ̂_θ = ∫ξσ̂_z = 1, and chart forms σ_θ = Q^{3/2}σ_{θ,phys}, σ_z = Qσ_{z,phys} (so ∫R^2σ_θ dR = ∫Rσ_z dR = 1), the targets H_θ = −T_2(⟨E_θ⟩_Y − σ_θε∂_Z J_θ) and H_z = −T_1(⟨E_z⟩_Y − σ_zε∂_Z(J_z + c_ρP)) are Y-independent, supported in the active shell, do not enlarge Z-support, and satisfy (D_r + 2/R)H_θ = −⟨E_θ⟩_Y + σ_θε∂_Z J_θ and (D_r + 1/R)H_z = −⟨E_z⟩_Y + σ_zε∂_Z(J_z + c_ρP).",
"description": "Corollary 8.5 (8.18): with interior bumps σ_{θ,phys} = q^{−3/2}σ̂_θ(r/√q), σ_{z,phys} = q^{−1}σ̂_z(r/√q), ∫ξ^2σ̂_θ = ∫ξσ̂_z = 1, and chart forms σ_θ = Q^{3/2}σ_{θ,phys}, σ_z = Qσ_{z,phys} (so ∫R^2σ_θ dR = ∫Rσ_z dR = 1), the targets H_θ = −T_2(⟨E_θ⟩_Y − σ_θε∂_Z J_θ) and H_z = −T_1(⟨E_z⟩_Y − σ_zε∂_Z(J_z + c_ρP)) are Y-independent, supported in the active shell, do not enlarge Z-support, and satisfy (D_r + 2/R)H_θ = −⟨E_θ⟩_Y + σ_θε∂_Z J_θ and (D_r + 1/R)H_z = −⟨E_z⟩_Y + σ_zε∂_Z(J_z + c_ρP). OBLIGATION: Converts the auxiliary-averaged tangential residual into a compactly supported stress target that waves can supply. Since W_rθ, W_rz enter E_θ, E_z through +(D_r + 2/R) and +(D_r + 1/R), a covariance increment equal to (H_θ, H_z) cancels ⟨E_θ⟩_Y, ⟨E_z⟩_Y except for bump terms carrying ε∂_Z J_θ and ε∂_Z(J_z + c_ρ P). Auxiliary independence is exactly the hypothesis of the signed amplitude map of Proposition 7.6. REFS: pages 94 to 95; (8.18); Corollary 8.5; Proposition 7.6 and (7.31) on page 84; Proposition 9.6, Step 2 on pages 108 to 109.",
"obligation": "Converts the auxiliary-averaged tangential residual into a compactly supported stress target that waves can supply. Since W_rθ, W_rz enter E_θ, E_z through +(D_r + 2/R) and +(D_r + 1/R), a covariance increment equal to (H_θ, H_z) cancels ⟨E_θ⟩_Y, ⟨E_z⟩_Y except for bump terms carrying ε∂_Z J_θ and ε∂_Z(J_z + c_ρ P). Auxiliary independence is exactly the hypothesis of the signed amplitude map of Proposition 7.6.",
"backward_question": "What compactly supported, torus-independent stress pair, added as wave covariance, would cancel the averaged tangential residual, and what minimal remainder must be conceded to make it compactly supported?",
"mechanism": "Subtracting the bump times the weighted moment makes each source Y-independent with zero weighted integral (by (8.16) and the unit moments), so by the last clause of Lemma 8.2 the cutoff remainder vanishes identically and T_2, T_1 invert exactly. The primitives act at fixed (Z, T), so axial support is preserved. The bumps are defined physically, so they agree on chart overlaps. The factors ε∂_Z are retained in the bump terms so the three defects can later be corrected at fixed (Z, T) without losing them.",
"antecedent": "None cited in Section 8. Internal: the stress formulas of Section 3.2 and Proposition 4.2, here with a cutoff and a moment subtraction. The introduction credits Daneri and Székelyhidi [10] with the general use of oscillations to realize a prescribed stress.",
"cost": "Leaves σ_θ ε∂_Z J_θ and σ_z ε∂_Z(J_z + c_ρ P) in the residual, small only once the defects are improved. H_θ, H_z are targets only; realizing them is Section 9's job (Proposition 9.6, Step 2 redoes this construction in physical variables with bumps b_e and moments M_e).",
"checkable": "For Y-independent E_θ(R) with M = ∫R^2 E_θ dR, compute H_θ = −R^{−2}∫_0^R R′^2(E_θ − σ_θ M) dR′ and check that it vanishes beyond the shell and that (∂_R + 2/R)H_θ = −E_θ + σ_θ M; same for z with weight R and T_1.",
"depends_on": [
"M8.7",
"M8.3",
"M8.4",
"M8.2"
],
"constrains": [],
"reasons": {
"M8.7": "By (8.16) the weighted moments of ⟨E_θ⟩_Y, ⟨E_z⟩_Y equal ε∂_Z J_θ and ε∂_Z(J_z + c_ρP), which the unit-moment bumps subtract.",
"M8.3": "H_θ and H_z are built with the compactly supported primitives T_2 and T_1, which act at fixed (Z, T).",
"M8.4": "The sources are Y-independent with zero weighted integral, so the cutoff remainders vanish identically and T_2, T_1 invert exactly.",
"M8.2": "The covariances W_rθ, W_rz enter E_θ, E_z through (D_r + 2/R) and (D_r + 1/R), so covariance targets can cancel them."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 94-95",
"analogous_to": [],
"relations": {
"M8.7": "prerequisite",
"M8.3": "prerequisite",
"M8.4": "prerequisite",
"M8.2": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: FRAGMENT; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M8.9",
"kind": "move",
"name": "ns-m8-9-temporal-corrector-inverting-the-fast-auxiliary-time",
"title": "Temporal corrector: inverting the fast auxiliary-time derivative",
"section": "8",
"pages": "95-96",
"refs": [
"pages 95 to 96",
"Lemma 8.6, (8.19) to (8.23)",
"(6.2), (6.6) on page 63, (6.7) on page 64."
],
"statement": "Lemma 8.6 (8.19)-(8.23): on T^2, N = v_t·∂_y has on zero-mean F the unique smooth zero-mean inverse N^{−1}F = Σ_{k≠0}F̂(k)e^{2πik·y}/(2πi v_t·k), ‖N^{−1}F‖_{C^m_y} ≤ C_m‖F‖_{C^{m+4}_y} (8.19). For the zero-auxiliary-mean residuals E°_θ, E°_z set ∆v = −c_{i0}^{−1}N_{i0}^{−1}E°_θ, γ_d = −c_{i0}^{−1}N_{i0}^{−1}E°_z, c_{i0}^{−1} ≤ CS_* (8.20). Then (∆β, ∆v, ∆γ) = (−ε∂_Z T_1γ_d, ∆v, γ_d − A_1γ_d) ∈ M^{α+1} × M^α × M^α (8.21) is divergence-free, preserves (8.2), and gives c_{i0}N_{i0}∆v = −E°_θ, c_{i0}N_{i0}∆γ = −E°_z + c_{i0}N_{i0}a, a = −A_1γ_d flat (8.22); chart-consistent by (8.23).",
"description": "Lemma 8.6 (8.19)-(8.23): on T^2, N = v_t·∂_y has on zero-mean F the unique smooth zero-mean inverse N^{−1}F = Σ_{k≠0}F̂(k)e^{2πik·y}/(2πi v_t·k), ‖N^{−1}F‖_{C^m_y} ≤ C_m‖F‖_{C^{m+4}_y} (8.19). For the zero-auxiliary-mean residuals E°_θ, E°_z set ∆v = −c_{i0}^{−1}N_{i0}^{−1}E°_θ, γ_d = −c_{i0}^{−1}N_{i0}^{−1}E°_z, c_{i0}^{−1} ≤ CS_* (8.20). Then (∆β, ∆v, ∆γ) = (−ε∂_Z T_1γ_d, ∆v, γ_d − A_1γ_d) ∈ M^{α+1} × M^α × M^α (8.21) is divergence-free, preserves (8.2), and gives c_{i0}N_{i0}∆v = −E°_θ, c_{i0}N_{i0}∆γ = −E°_z + c_{i0}N_{i0}a, a = −A_1γ_d flat (8.22); chart-consistent by (8.23). OBLIGATION: Cancels the zero-auxiliary-mean part E°_θ, E°_z of the tangential mean residual, which cannot be handled by a stress target (Proposition 7.6 requires Y-independent stresses). What remains is the slow time derivative −ε∂_T of the increment (one extra ε) plus transport and viscous changes. MECHANISM: In chart variables t_* = −ε∂_T + c_{i0}N_{i0} with c_{i0} ≍ S_*^{−1}: the fast term is order one, the slow term costs ε. REFS: pages 95 to 96; Lemma 8.6, (8.19) to (8.23); (6.2), (6.6) on page 63, (6.7) on page 64.",
"obligation": "Cancels the zero-auxiliary-mean part E°_θ, E°_z of the tangential mean residual, which cannot be handled by a stress target (Proposition 7.6 requires Y-independent stresses). What remains is the slow time derivative −ε∂_T of the increment (one extra ε) plus transport and viscous changes.",
"backward_question": "Can a mean residual that oscillates on the auxiliary torus with zero average be absorbed by a mean velocity whose fast time derivative equals it, and what do the small divisors of the irrational time direction cost?",
"mechanism": "In chart variables t_* = −ε∂_T + c_{i0}N_{i0} with c_{i0} ≍ S_*^{−1}: the fast term is order one, the slow term costs ε. An increment whose fast time derivative equals −E° cancels E° exactly, and its slow derivative is smaller by ε. N^{−1} is a Fourier multiplier on nonzero frequencies, bounded because |v_t·k|^{−1} ≤ C(1 + |k|) by (6.7); four torus derivatives are lost (one for the divisor, three for summability of (1 + |k|)^{−3} in two dimensions). Both increments have zero auxiliary mean at every point, so they preserve (8.2) and satisfy the flux hypothesis of Proposition 8.3(ii). N commutes with I, J, and I_c (the shifts are torus translations and χ_m is torus independent), so the axial realization error c_{i0}N_{i0}a is flat by (8.8). The velocity factor Q^{A − (2A + 1/2)} T_g^{−i0} = Q^{−1−h} T_g^{−i0} = c_{i0}^{−1}, and (8.23), which follows from J_g v_t = T_g v_t, makes the physical definition agree on chart overlaps.",
"antecedent": "None cited. Internal: (6.7), the covering (6.5), the operators (6.6), Lemma 6.2. Recognizable classical ingredient (not cited): the cohomological equation for a linear flow on T^2 with Diophantine frequency, used here as a temporal corrector.",
"cost": "Loss of four torus derivatives and a factor c_{i0}^{−1} ≤ CS_* (polynomial in S_* = ℓ^2). The inverse need not preserve auxiliary-torus support, so mean fields may occupy the whole torus. The slow term −ε∂_T of the increments and the flat remainder F_ax = c_{i0}N_{i0}(∆γ − γ_d) are carried into the next residual.",
"checkable": "FFT on a 2D torus grid: for random smooth zero-mean F, apply the multiplier 1/(2πi v_t·k), verify N(N^{−1}F) = F and the C^m versus C^{m+4} bound across resolutions. Verify J_g v_t = T_g v_t and J_g v_r = Λ_g v_r for J_g = [[3, 1], [1, 5]], T_g = 4 + √2, Λ_g = 4 − √2, v_t = (√2 − 1, 1), v_r = (1, 1 − √2). Run while digesting: both hold to machine precision and det J_g = 14.",
"depends_on": [
"M6.4",
"M6.3",
"M8.2",
"M8.6"
],
"constrains": [],
"reasons": {
"M6.4": "The multiplier 1/(2πi v_t·k) is bounded by C(1 + |k|) by the Diophantine bound (6.7), which costs four torus derivatives.",
"M6.3": "In t* = −ε∂_T + c_{i0}N_{i0}, c_{i0}^{-1} ≤ CS* makes the fast derivative order one, and N_abs = T_g^i N_i gives chart consistency.",
"M8.2": "The inverted quantities are the zero-auxiliary-mean parts E°_θ, E°_z of the tangential mean residuals of (8.3).",
"M8.6": "The axial increment γ_d is realized by the potential of (8.14), with a flat remainder since γ_d has zero auxiliary mean."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 95-96",
"analogous_to": [],
"relations": {
"M6.4": "prerequisite",
"M6.3": "prerequisite",
"M8.2": "prerequisite",
"M8.6": "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": "M8.10",
"kind": "move",
"name": "ns-m8-10-the-reserved-mean-patch-power-law-swirl-no-axial-base-flow",
"title": "The reserved mean patch: power-law swirl, no axial base flow",
"section": "8",
"pages": "96-97",
"refs": [
"pages 96 to 97",
"(8.24)",
"Theorem 4.6(vi) on page 33 and (4.30) on page 34",
"(5.18) on page 52",
"(5.44) on page 60."
],
"statement": "On x = r/√q ∈ I_m, the image of I_mean (Theorem 4.6(vi)) under X ↦ √(2X), the q-normalized summed base is G_q = 0, V_q = a(η) x^{−1−2λ}, |a(η)| ≥ a_0 > 0, a(η) = 2^{1/2+λ} c_patch (1 + η^2)^{−1}, with the fixed λ > 0 (8.24). The exact summed-base statement is (5.44); higher-order coefficients vanish there by (5.18).",
"description": "On x = r/√q ∈ I_m, the image of I_mean (Theorem 4.6(vi)) under X ↦ √(2X), the q-normalized summed base is G_q = 0, V_q = a(η) x^{−1−2λ}, |a(η)| ≥ a_0 > 0, a(η) = 2^{1/2+λ} c_patch (1 + η^2)^{−1}, with the fixed λ > 0 (8.24). The exact summed-base statement is (5.44); higher-order coefficients vanish there by (5.18). OBLIGATION: Supplies an explicit, torus-independent base on which the five-equation map (M8.11) is exactly block diagonal and explicitly invertible, with the same inverse at every correction stage. MECHANISM: Theorem 4.6(vi) reserves I_mean ⊂ (X_a, X_v), where U = 0 and E = c_patch(1 + η^2)^{−1} X^{−1/2−λ} (4.30). Section 5 keeps every positive-order background coefficient zero there (5.18), so u_B = u^{(0)} on the patch (5.44). Cutoffs in q applied to azimuthal potentials create no axial component there, because q does not depend on r. Substituting X = x^2/2 gives (8.24). ANTECEDENT: None cited. Internal: Theorem 4.6(vi) and (4.30), (5.18), (5.44). The same reserved-patch device is used on I_pos in Lemma 5.2 and in Appendix A. REFS: pages 96 to 97; (8.24); Theorem 4.6(vi) on page 33 and (4.30) on page 34; (5.18) on page 52; (5.44) on page 60.",
"obligation": "Supplies an explicit, torus-independent base on which the five-equation map (M8.11) is exactly block diagonal and explicitly invertible, with the same inverse at every correction stage.",
"backward_question": "On what region is the base simple enough that three defects and two constraints can be corrected by an explicit finite-dimensional linear map, and why must the swirl there differ from a free vortex?",
"mechanism": "Theorem 4.6(vi) reserves I_mean ⊂ (X_a, X_v), where U = 0 and E = c_patch(1 + η^2)^{−1} X^{−1/2−λ} (4.30). Section 5 keeps every positive-order background coefficient zero there (5.18), so u_B = u^{(0)} on the patch (5.44). Cutoffs in q applied to azimuthal potentials create no axial component there, because q does not depend on r. Substituting X = x^2/2 gives (8.24). G = 0 removes the G∆v and 2RGγ_d couplings from (8.25). λ > 0 makes the base angular momentum RV ∝ x^{−2λ} vary with radius; for a free vortex (λ = 0) the J_θ row ∫R^2 Vγ_d dR would be a multiple of the axial-flux row ∫Rγ_d dR, so a zero-flux axial increment could not move J_θ.",
"antecedent": "None cited. Internal: Theorem 4.6(vi) and (4.30), (5.18), (5.44). The same reserved-patch device is used on I_pos in Lemma 5.2 and in Appendix A.",
"cost": "A structural condition that Sections 4 and 5 must preserve (an exact power law with zero axial velocity on I_mean, for every η ∈ [−1, 1]). Constants in the mean correction depend on λ and deteriorate as λ ↓ 0.",
"checkable": "Substitute X = x^2/2 into E_0 = c_patch(1 + η^2)^{−1} X^{−1/2−λ} and confirm V_q = 2^{1/2+λ} c_patch(1 + η^2)^{−1} x^{−1−2λ}. Check that at λ = 0 the vector of moments (∫R γ_d, ∫R^2 V γ_d) is rank one over all γ_d supported in the patch.",
"depends_on": [
"M4.8",
"M5.14",
"M5.8"
],
"constrains": [],
"reasons": {
"M4.8": "Theorem 4.6(vi) reserves I_mean with U = 0 and E = c_patch(1 + η²)^{-1}X^{-1/2−λ} (4.30), which becomes (8.24) under X = x²/2.",
"M5.14": "The summed background equals the leading field on the patch, the exact statement (5.44).",
"M5.8": "Every positive-order background coefficient vanishes on the mean patch by (5.18)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 96-97",
"analogous_to": [],
"relations": {
"M4.8": "prerequisite",
"M5.14": "prerequisite",
"M5.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": "M8.11",
"kind": "move",
"name": "ns-m8-11-five-equation-moment-correction-block-vandermonde",
"title": "Five-equation moment correction (block Vandermonde)",
"section": "8",
"pages": "97-98",
"refs": [
"pages 97 to 98",
"Lemma 8.7, (8.25), matrices A_θ and A_z on page 98",
"(8.17) on page 94."
],
"statement": "Lemma 8.7 (8.25): with three azimuthal bumps η_0, η_1, η_2 and two axial bumps η_0, η_1 in I_m, geometric copies η_j(x) = a_j^{−1}η_0(x/a_j), a_j = e^{jd}, on disjoint subintervals (not the similarity variable η), any targets (P, J_θ, J_z) at each (Z, T) admit a unique linear combination (∆v, γ_d) with ∫R^2∆v dR = 0, ∫Rγ_d dR = 0, ∫(2V/R)∆v dR = −P, ∫R^2(G∆v + Vγ_d) dR = −J_θ, ∫(2RGγ_d − RV∆v) dR = −J_z. Targets in S^α give Y-independent increments in M^α, linear in the targets; (8.14) gives ∆γ = γ_d and ∆β ∈ M^{α+1}; (8.2) is preserved exactly.",
"description": "Lemma 8.7 (8.25): with three azimuthal bumps η_0, η_1, η_2 and two axial bumps η_0, η_1 in I_m, geometric copies η_j(x) = a_j^{−1}η_0(x/a_j), a_j = e^{jd}, on disjoint subintervals (not the similarity variable η), any targets (P, J_θ, J_z) at each (Z, T) admit a unique linear combination (∆v, γ_d) with ∫R^2∆v dR = 0, ∫Rγ_d dR = 0, ∫(2V/R)∆v dR = −P, ∫R^2(G∆v + Vγ_d) dR = −J_θ, ∫(2RGγ_d − RV∆v) dR = −J_z. Targets in S^α give Y-independent increments in M^α, linear in the targets; (8.14) gives ∆γ = γ_d and ∆β ∈ M^{α+1}; (8.2) is preserved exactly. OBLIGATION: Cancels the linear parts of the three defects P, J_θ, J_z of (8.12) and (8.15), which obstruct the compactly supported pressure (the −ρP in (8.13)) and the compactly supported stresses (the bump. REFS: pages 97 to 98; Lemma 8.7, (8.25), matrices A_θ and A_z on page 98; (8.17) on page 94.",
"obligation": "Cancels the linear parts of the three defects P, J_θ, J_z of (8.12) and (8.15), which obstruct the compactly supported pressure (the −ρP in (8.13)) and the compactly supported stresses (the bump terms in (8.18)), while preserving the two moments (9.10).",
"backward_question": "With three scalar defects to cancel and two moments to hold fixed, how many free coefficients are needed, which linear functionals of the base do they probe, and when is the resulting 5x5 system nonsingular?",
"mechanism": "Each row is linear in the increments. A swirl increment ∆v enters P through the centrifugal force 2V∆v/R and enters J_z through the pressure moment, −(1/2)∫R^2(2V/R)∆v = −∫RV∆v; an axial increment enters J_θ through axial transport of base angular momentum, ∫R^2 Vγ_d. With G = 0 the system splits into an angular block (unknowns u_j; rows: angular-momentum constraint, P, J_z; powers x^2, x^{−2−2λ}, x^{−2λ}) and an axial block (unknowns s_j; rows: flux constraint, J_θ; powers x^1, x^{1−2λ}). Power moments of geometric copies factor as ∫x^p η_j dx = μ_p e^{jdp} with μ_p = ∫x^p η_0 dx > 0, so after dividing rows by μ_p and the constants 2a, −a, a, each block is an ordinary Vandermonde matrix in the nodes e^{dp}, nonsingular because the powers are distinct for λ > 0. The resulting map is fixed once, independent of the target values; the Y-independent γ_d with zero flux has identically zero cutoff remainder, and its potential and radial velocity stay inside the patch, including between the bump supports.",
"antecedent": "None cited in the proof. Internal parallel: Lemma 4.7 and Lemma A.1 (distinct power weights against ordered disjoint bumps give an invertible moment matrix, proved there by a Rolle-type count of zeros), used for the five-moment corrections on I_pos (Lemma 5.2) and in Appendix A. The five equations (8.25) are not the five cumulative profile integrals (M, I, J, S, C_p) of (4.15), though the design is the same.",
"cost": "Inverse bounds depend on λ, d, and the bump, and degenerate as λ ↓ 0. Only the axial block degenerates: its nodes e^d and e^{d(1−2λ)} coalesce (the free-vortex degeneracy of M8.10), while the angular nodes e^{2d}, e^{−2d(1+λ)}, e^{−2dλ} stay distinct at λ = 0. Requires the patch structure of M8.10 at every stage.",
"checkable": "The natural candidate. Choose λ > 0, a, d, and a bump η_0; build A_θ and A_z as printed on page 98; solve for arbitrary targets; assemble ∆v and γ_d; verify all five integrals of (8.25) by quadrature with G = 0, V = a x^{−1−2λ}; track condition numbers as λ ↓ 0. Run while digesting (λ = 0.2, a = 1.3, d = 0.15, bump of half-width 0.05 at x_0 = 1, targets P = 0.7, J_θ = −0.4, J_z = 0.25): all five rows hold to about 1e−15; cond(A_z) ≈ 69, 278, 1.39e3, 1.39e4 at λ = 0.2, 0.05, 0.01, 0.001 (growth like 1/λ), while cond(A_θ) stays between about 100 and 118.",
"depends_on": [
"M8.10",
"M8.7",
"M8.5",
"M8.1"
],
"constrains": [],
"reasons": {
"M8.10": "On the patch G = 0 and V = a x^{-1−2λ} with λ > 0, so the five weighted integrals split into two Vandermonde blocks with distinct powers.",
"M8.7": "The targets J_θ, J_z are the flux defects of (8.15), and the last rows are their linearizations in the increments.",
"M8.5": "The target P is the radial source integral of (8.12), reached through the centrifugal term ∫(2V/R)∆v.",
"M8.1": "The first two rows keep the moments M_θ = M_z = 0 of (8.2)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 97-98",
"analogous_to": [],
"relations": {
"M8.10": "prerequisite",
"M8.7": "prerequisite",
"M8.5": "prerequisite",
"M8.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": "correct"
}
},
{
"id": "M8.12",
"kind": "move",
"name": "ns-m8-12-exact-nonlinear-defect-update-and-its-gain",
"title": "Exact nonlinear defect update and its gain",
"section": "8",
"pages": "98-99",
"refs": [
"pages 98 to 99",
"Lemma 8.8, (8.26), (8.27), class table on page 99",
"consumer Proposition 9.6, Step 4 on page 111."
],
"statement": "Lemma 8.8 (8.26), (8.27): with base and w fixed, apply Lemma 8.7 to the current defects and realize γ_d by (8.14). The new defects are P_new = ∫⟨R_g⟩_Y dR, (J_θ)_new = ∫R^2⟨γ∆v + v∆γ + ∆γ∆v⟩_Y dR, (J_z)_new = ∫R⟨2γ∆γ + (∆γ)^2⟩_Y dR − (1/2)∫R^2⟨R_g⟩_Y dR, with R_g = g_{r,new} − g_r − (2V/R)∆v given exactly by (8.26). If on the potential's support derivatives of b are O(εS_*^{B_I}) and of V, G are O(S_*^{B_I}), v, γ ∈ M^{0.9}, β ∈ M^{1.9}, and targets lie in S^α, α ≥ 0.9, then R_g ∈ M^{α+0.9−2κ_s} and the new defects lie in S^{α+0.9−2κ_s}.",
"description": "Lemma 8.8 (8.26), (8.27): with base and w fixed, apply Lemma 8.7 to the current defects and realize γ_d by (8.14). The new defects are P_new = ∫⟨R_g⟩_Y dR, (J_θ)_new = ∫R^2⟨γ∆v + v∆γ + ∆γ∆v⟩_Y dR, (J_z)_new = ∫R⟨2γ∆γ + (∆γ)^2⟩_Y dR − (1/2)∫R^2⟨R_g⟩_Y dR, with R_g = g_{r,new} − g_r − (2V/R)∆v given exactly by (8.26). If on the potential's support derivatives of b are O(εS_*^{B_I}) and of V, G are O(S_*^{B_I}), v, γ ∈ M^{0.9}, β ∈ M^{1.9}, and targets lie in S^α, α ≥ 0.9, then R_g ∈ M^{α+0.9−2κ_s} and the new defects lie in S^{α+0.9−2κ_s}. OBLIGATION: Proves the five-equation correction improves the defects by a fixed power ε^{0.9−2κ_s}, which is Step 4 of Proposition 9.6 (defects in S^{H+0.9−2κ_s}), closing the defect part of the cycle. MECHANISM: Since W and the base are fixed, subtracting the two versions of the g_r row of (8.3) and expanding each quadratic product gives (8.26). The third row of (8.25) cancels the old P against ∫(2V/R)∆v; the fourth and fifth rows cancel the old J_θ, J_z against the terms linear in the base, ∫R^2(G∆v + V∆γ) and ∫(2RG∆γ − RV∆v), the latter's second part coming from −(1/2)∫R^2(2V/R)∆v. ANTECEDENT: None cited.",
"obligation": "Proves the five-equation correction improves the defects by a fixed power ε^{0.9−2κ_s}, which is Step 4 of Proposition 9.6 (defects in S^{H+0.9−2κ_s}), closing the defect part of the cycle.",
"backward_question": "Once a fixed linear map cancels the linear parts of the defects, what exactly is left, and is it smaller by a fixed power of ε so that repeating the cycle raises the exponent?",
"mechanism": "Since W and the base are fixed, subtracting the two versions of the g_r row of (8.3) and expanding each quadratic product gives (8.26). The third row of (8.25) cancels the old P against ∫(2V/R)∆v; the fourth and fifth rows cancel the old J_θ, J_z against the terms linear in the base, ∫R^2(G∆v + V∆γ) and ∫(2RG∆γ − RV∆v), the latter's second part coming from −(1/2)∫R^2(2V/R)∆v. What remains is quadratic in small quantities or carries an extra ε: the slow time derivative of ∆β (t_*∆β = −ε∂_T ∆β since ∆β is Y-independent), radial fluxes with b = O(ε) or with radial means, axial fluxes (D_z = ε∂_Z), viscosity on ∆β, and products of ∆v, ∆γ with the current means v, γ. Class table (page 99): −t_*∆β in M^{α+2}; (D_r + 1/R)(2b∆β) in M^{α+2−κ_s}; D_z(b∆γ + G∆β) in M^{α+2}; 2v∆v/R in M^{α+0.9}; (∆v)^2/R in M^{2α}; ε(∆_0 − R^{−2})∆β in M^{α+2−2κ_s}; remaining transport in M^{α+2−κ_s}. With α ≥ 0.9 every entry is at least α + 0.9 − 2κ_s.",
"antecedent": "None cited.",
"cost": "The gain depends on the cumulative bounds v, γ ∈ M^{0.9}, β ∈ M^{1.9}, which Section 9 must maintain as (9.9), on b = O(ε) near the patch, and on α ≥ 0.9. The limiting term is 2v∆v/R, the interaction of the new swirl increment with the accumulated swirl correction.",
"checkable": "Symbolic check, run while digesting with exact residual 0: for arbitrary compactly supported increments with ∆β = −ε∂_Z Ψ, ∆γ = (∂_R + 1/R)Ψ, verify that g_{r,new} − g_r − (2V/R)∆v equals (8.26), and that P_new = P + ∫(2V/R)∆v + ∫R_g, (J_θ)_new = J_θ + ∫R^2(G∆v + V∆γ) + ∫R^2(γ∆v + v∆γ + ∆γ∆v), and (J_z)_new = J_z + ∫(2RG∆γ − RV∆v) + ∫R(2γ∆γ + (∆γ)^2) − (1/2)∫R^2 R_g; substituting rows three to five of (8.25) gives (8.27). A scaling check: set v, γ ∝ ε^{0.9}, β ∝ ε^{1.9}, targets ∝ ε^α, and fit the log-log slope of the new defects in ε (expect at least α + 0.9).",
"depends_on": [
"M8.11",
"M8.6",
"M8.2",
"M8.7"
],
"constrains": [],
"reasons": {
"M8.11": "Applies the five-equation map of Lemma 8.7, whose last three rows cancel the parts of the defect changes that are linear in the base.",
"M8.6": "γ_d is realized by (8.14), giving the induced radial velocity ∆β = −ε∂_ZΨ* that enters R_g.",
"M8.2": "R_g is the exact difference of the g_r row of (8.3) before and after the update.",
"M8.7": "The new defects are recomputed from the definitions (8.15) of J_θ, J_z and the pressure integral P."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 98-99",
"analogous_to": [],
"relations": {
"M8.11": "prerequisite",
"M8.6": "prerequisite",
"M8.2": "prerequisite",
"M8.7": "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": "M8.13",
"kind": "move",
"name": "ns-m8-13-recomputation-order-and-chart-compatibility",
"title": "Recomputation order and chart compatibility",
"section": "8",
"pages": "99-100",
"refs": [
"pages 99 to 100",
"Section 8.7."
],
"statement": "Section 8.7: for fixed base coefficients and stress, an actual tuple (β, v, γ, w) determines in order: (1) W_ab = ⟨w_a w_b⟩_θ from the full wave velocities, and g_r from the third row of (8.3); (2) P = ∫⟨g_r⟩_Y dR and p_m = T_0(g_r − ρP); (3) E_θ, E_z from the first two rows of (8.3) with this pressure; (4) J_θ, J_z from (8.15). After either mean update the tuple is (β + ∆β, v + ∆v, γ + ∆γ, w), with ∆γ the actual increment of (8.14), cutoff remainder included; the temporal update uses the current E°_θ, E°_z in (8.20), the moment update the current (P, J_θ, J_z) in (8.25).",
"description": "Section 8.7: for fixed base coefficients and stress, an actual tuple (β, v, γ, w) determines in order: (1) W_ab = ⟨w_a w_b⟩_θ from the full wave velocities, and g_r from the third row of (8.3); (2) P = ∫⟨g_r⟩_Y dR and p_m = T_0(g_r − ρP); (3) E_θ, E_z from the first two rows of (8.3) with this pressure; (4) J_θ, J_z from (8.15). After either mean update the tuple is (β + ∆β, v + ∆v, γ + ∆γ, w), with ∆γ the actual increment of (8.14), cutoff remainder included; the temporal update uses the current E°_θ, E°_z in (8.20), the moment update the current (P, J_θ, J_z) in (8.25). OBLIGATION: Guarantees that each correction acts on the residual of the actual current divergence-free field, so all newly created products enter the next step; that a zero-mean cutoff remainder which acquires a nonzero auxiliary mean after multiplication is retained in the pressure and compatibility integrals; and that the constructions are globally well defined (no new dyadic bands, chart independence, one-sided derivatives at η = ±1), as needed by Proposition 9.3 and Theorem 3.1(ii). REFS: pages 99 to 100; Section 8.7. ANTECEDENT: None cited. Internal: Lemma 6.2, (6.20), (8.4), (8.23).",
"obligation": "Guarantees that each correction acts on the residual of the actual current divergence-free field, so all newly created products enter the next step; that a zero-mean cutoff remainder which acquires a nonzero auxiliary mean after multiplication is retained in the pressure and compatibility integrals; and that the constructions are globally well defined (no new dyadic bands, chart independence, one-sided derivatives at η = ±1), as needed by Proposition 9.3 and Theorem 3.1(ii).",
"backward_question": "In what order must pressure, mean residuals, and defects be recomputed so that every correction sees the actual updated field, and are the resulting constructions independent of the chart in which they were built?",
"mechanism": "Radial integrals hold (z, t) fixed and q = q(z, t), so they introduce no new band, and one common covering index can be fixed on a neighborhood of all relevant support closures. The Fourier covariance (8.23) and bounded differences of the integer covering indices give agreement on overlaps; the radial formulas agree by their physical definition. On closed regions q ≥ c > 0, including η = ±1, only finitely many bands occur, so the fixed-shift integrals, the Fourier inverse, and the finite-dimensional correction preserve all one-sided source derivatives there.",
"antecedent": "None cited. Internal: Lemma 6.2, (6.20), (8.4), (8.23).",
"cost": "Every cutoff remainder must be kept and recomputed; one common torus index must be fixed per neighborhood; all estimates live on the single domain 0 < q < q_* fixed before the iteration.",
"checkable": "None: bookkeeping. (Its one computable ingredient, the intertwining (8.23), is covered under M8.9.)",
"depends_on": [
"M8.2",
"M8.5",
"M8.7",
"M6.8"
],
"constrains": [],
"reasons": {
"M8.2": "The order starts from W and g_r in the third row of (8.3) and ends with E_θ, E_z from its first two rows.",
"M8.5": "Step (2) reconstructs P and p_m = T_0(g_r − ρP) by (8.12) before E_z is formed.",
"M8.7": "Step (4) computes the defects J_θ, J_z from (8.15).",
"M6.8": "Chart independence uses the common torus and compatibility identity (6.20), and radial integrals at fixed (z, t) add no new band."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 99-100",
"analogous_to": [],
"relations": {
"M8.2": "prerequisite",
"M8.5": "prerequisite",
"M8.7": "prerequisite",
"M6.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": "M9.1",
"kind": "move",
"name": "ns-m9-1-principal-remainder-split-and-the-linear-residual-of-a",
"title": "Principal/remainder split and the linear residual of a curl-generated pulse",
"section": "9",
"pages": "101-102",
"refs": [
"pp. 101 to 102",
"(9.1), (9.2), Proposition 9.1",
"uses (7.5), (7.9), (7.38), (7.39), (7.40), Proposition 7.2, Lemma 7.7, (6.32)."
],
"statement": "Proposition 9.1: for a label, a harmonic m ≠ 0, and α ∈ R, let f_m ∈ W_α satisfy the support and smooth-extension hypotheses of Proposition 7.2, with f_m e^{ikmΦ} extending smoothly by zero outside the local rectangle including its pulse endpoints, and let L_m(t_m, π_m) = −f_m, where L_m(a, π) = Q^{1+h}N_abs a + Ka + εk^2m^2|n_Φ|^2a + ikm n_Φπ (9.1). After multiplying potential and pressure by the pulse cutoff ψ and taking the curl (7.38), the normalized linear residual plus f_m e^{ikmΦ} lies in W_{α+1/2−3κ_s} up to pulse-cutoff tails flat as q ↓ 0, and π_m ∈ W_{α+1/2}; likewise for f_m = 0.",
"description": "Proposition 9.1: for a label, a harmonic m ≠ 0, and α ∈ R, let f_m ∈ W_α satisfy the support and smooth-extension hypotheses of Proposition 7.2, with f_m e^{ikmΦ} extending smoothly by zero outside the local rectangle including its pulse endpoints, and let L_m(t_m, π_m) = −f_m, where L_m(a, π) = Q^{1+h}N_abs a + Ka + εk^2m^2|n_Φ|^2a + ikm n_Φπ (9.1). After multiplying potential and pressure by the pulse cutoff ψ and taking the curl (7.38), the normalized linear residual plus f_m e^{ikmΦ} lies in W_{α+1/2−3κ_s} up to pulse-cutoff tails flat as q ↓ 0, and π_m ∈ W_{α+1/2}; likewise for f_m = 0. OBLIGATION: The pulse inverse only solves the ODE (7.5) along the pulse. Without this proposition nothing controls the rest of the exact linearized operator (slow transport, phase-transport defect, base derivatives and cylindrical connections, pressure-amplitude gradient, viscous amplitude derivatives, the curl. REFS: pp. 101 to 102; (9.1), (9.2), Proposition 9.1; uses (7.5), (7.9), (7.38), (7.39), (7.40), Proposition 7.2, Lemma 7.7, (6.32).",
"obligation": "The pulse inverse only solves the ODE (7.5) along the pulse. Without this proposition nothing controls the rest of the exact linearized operator (slow transport, phase-transport defect, base derivatives and cylindrical connections, pressure-amplitude gradient, viscous amplitude derivatives, the curl remainder r_m, the temporal cutoff), so a correction could create an error as large as the source it removes.",
"backward_question": "Once my amplitude ODE cancels the principal part of the linearized operator on a harmonic, is every leftover term uniformly smaller by a fixed power of ε, including the curl remainder and the temporal-cutoff error?",
"mechanism": "Write the harmonic velocity as a e^{ikmΦ} with a = t_m + r_m, where Lemma 7.7 gives r_m ∈ W_{α+1/2-κ_s}. Expanding the linearized residual about the slow base (b, V, G), the terms in which the fast time derivative hits the amplitude, both viscous derivatives hit the exponential, the base shear and rotation act through the matrix K, or the pressure gradient hits the exponential make up exactly L_m, which (7.5) cancels. Everything else is (9.2), and each term carries an explicit gain from the class calculus (6.32): slow time -ε∂_T and D_z = ε∂_Z gain 1, D_r loses κ_s, (km)^{-1} = O(ε^{1/2}), b = O(ε), εk^2 = O(1), and the phase-transport defect E_ik = O(ε S_*^C) of (7.9) times km = O(ε^{-1/2}) gains 1/2. The gains table on p. 102 has minimum 1/2 - κ_s; the potential formula and chain-rule operators bring the common bound to α + 1/2 - 3κ_s, and the principal operator applied to r_m keeps r_m's exponent. Because ψ multiplies the potential and pressure before the curl, incompressibility stays exact. The leftover pieces (1 - ψ)f and ψ' t_m live where the Gaussian envelope P_v ≤ e^{-cS_*}; since S_* = ℓ^2 while Q = 2^{-ℓ}, the bound C Q^{-M} S_*^P e^{-cS_*} is O(q^N) for every N. These tails are retained additively and never fed to later forward solves.",
"antecedent": "None cited in Section 9. Internal: Proposition 7.2, Lemma 7.7, (7.40). The amplitude equation being completed is the transport of wavevector and polarization along a background flow, which the introduction (p. 2) attributes to Lifschitz and Hameiri [17] and Friedlander and Vishik [14].",
"cost": "An exponent loss of 3κ_s per application (gain 1/2 - 3κ_s rather than 1/2). Flat pulse-cutoff tails must be carried separately for the rest of the construction. Sources must extend smoothly by zero across the pulse endpoints.",
"checkable": "(a) Symbolic (sympy): in normalized cylindrical variables with D_r = ∂_R, D_z = ε∂_Z, and t_* = -ε∂_T + ∂_v on the amplitude, apply the linearized normalized Navier-Stokes operator about a general axisymmetric slow base (b, V, G)(R, Z, T) to (a(R, Z, T, v) e^{ikmΦ}, π e^{ikmΦ}) with Φ = pθ + φ(R, Z, T, v); verify that the result equals e^{ikmΦ}[L_m(a, π) + L^rem_m(a, π)] from (9.1) and (9.2) identically, with E_ik = (t_* + bD_r + (V/R)∂_θ + GD_z)Φ. (b) Numeric: evaluate exp(-cℓ^2 + (M + N)ℓ log 2 + 2C log ℓ) for ℓ up to 500 and several (c, M, N, C), and confirm it tends to 0 (flatness of the cutoff tails).",
"depends_on": [
"M7.6",
"M7.12",
"M7.13",
"M6.12"
],
"constrains": [],
"reasons": {
"M7.6": "The amplitude (t_m, π_m) solves the principal equation by Proposition 7.2, whose support and extension hypotheses the source must meet.",
"M7.12": "The velocity is the curl of the potential (7.38), with remainder r_m ∈ W_{α+1/2−κ_s} and the divergence identity (7.39).",
"M7.13": "Cutting potential and pressure by ψ leaves the flat tails of (7.40), which are retained additively.",
"M6.12": "Each non-principal term's gain is read from the cost table (6.32): −ε∂_T and D_z gain 1, D_r loses κ_s, and (km)^{-1} gains 1/2."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 101-102",
"analogous_to": [],
"relations": {
"M7.6": "prerequisite",
"M7.12": "prerequisite",
"M7.13": "prerequisite",
"M6.12": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: FRAGMENT; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M9.2",
"kind": "move",
"name": "ns-m9-2-interaction-estimates-and-the-transversality-cancellation",
"title": "Interaction estimates and the transversality cancellation",
"section": "9",
"pages": "102-103",
"refs": [
"pp. 102 to 103",
"Lemma 9.2",
"uses (7.37), (7.39), Lemma 6.1, (6.30), (6.31)."
],
"statement": "Lemma 9.2. If w ∈ W_α is a wave and v is a mean field with tangential components in M_µ and radial component in M_{µ+1}, the nonzero harmonics of (w·∇_*)v + (v·∇_*)w lie in W_{α+µ-1/2}. For two curl-generated waves w, w' with the same label and exponents α, α', the nonzero harmonics of (w·∇_*)w' + (w'·∇_*)w lie in W_{α+α'-κ_s} and the zero harmonic in M_{α+α'-κ_s}. Distinct labels have zero products on their closed supports.",
"description": "Lemma 9.2. If w ∈ W_α is a wave and v is a mean field with tangential components in M_µ and radial component in M_{µ+1}, the nonzero harmonics of (w·∇_*)v + (v·∇_*)w lie in W_{α+µ-1/2}. For two curl-generated waves w, w' with the same label and exponents α, α', the nonzero harmonics of (w·∇_*)w' + (w'·∇_*)w lie in W_{α+α'-κ_s} and the zero harmonic in M_{α+α'-κ_s}. Distinct labels have zero products on their closed supports. OBLIGATION: Every correction produces the quadratic term ∇·(δu ⊗ δu) and cross terms with all earlier fields; the cycle gains only if these are of higher order than the source they accompany. A naive count loses a factor k ≈ ε^{-1/2} in wave self-advection, which would erase the gain of the whole cycle. MECHANISM: Mean advection of a wave differentiates the phase and costs k = O(ε^{-1/2}); ANTECEDENT: None cited in Section 9. Internal: (7.39), Lemma 6.1, Proposition 6.6. The introduction (p. 2) cites Craik and Criminale [9] for exact waves on affine flows that exploit the cancellation of the wave's quadratic self-interaction, the same transversality mechanism. REFS: pp. 102 to 103; Lemma 9.2; uses (7.37), (7.39), Lemma 6.1, (6.30), (6.31).",
"obligation": "Every correction produces the quadratic term ∇·(δu ⊗ δu) and cross terms with all earlier fields; the cycle gains only if these are of higher order than the source they accompany. A naive count loses a factor k ≈ ε^{-1/2} in wave self-advection, which would erase the gain of the whole cycle.",
"backward_question": "Wave self-advection naively costs one power of k ≈ ε^{-1/2}; is there an exact identity, valid for the complete divergence-free amplitude, that removes this loss for every pair of harmonics of one label?",
"mechanism": "Mean advection of a wave differentiates the phase and costs k = O(ε^{-1/2}); that is the -1/2 in the mean-wave bound (radial transport of the amplitude is offset by the extra order of the radial mean, axial transport gains through D_z, and wave transport of a mean costs at most κ_s). For two harmonics of one label, the phase-derivative term in the transport of a' e^{ikm'Φ} by a e^{ikmΦ} is ikm'(a·n_Φ)a'. The exact divergence identity (7.39), ikm n_Φ·a_m = -((D_r + R^{-1})(a_m)_r + D_z(a_m)_z), puts a·n_Φ in W_{α+1/2-κ_s} for the complete curl-generated amplitude, so the factor k is removed up to κ_s. This is why the advecting factor must be the full divergence-free amplitude t_m + r_m and not the transverse part t_m alone. Products of weights obey P_v^2 ≤ P_v and ζ ≤ √ζ, so a nonzero output keeps the wave weight; Lemma 6.1 separates distinct labels by disjoint auxiliary supports; Leibniz' rule extends all bounds to every fixed amplitude derivative.",
"antecedent": "None cited in Section 9. Internal: (7.39), Lemma 6.1, Proposition 6.6. The introduction (p. 2) cites Craik and Criminale [9] for exact waves on affine flows that exploit the cancellation of the wave's quadratic self-interaction, the same transversality mechanism.",
"cost": "A κ_s loss per wave-wave product. The mean-wave product loses 1/2, so the cumulative mean correction must stay small: with µ = 0.9 from (9.9) the mean-wave error sits at B + 0.4. Curl remainders must be kept in every advecting factor.",
"checkable": "Symbolic: for a θ-independent potential coefficient C(R, Z) and phase Φ = pθ + φ(R, Z), form a e^{ikmΦ} = curl_*(C e^{ikmΦ}) with curl_* from (7.37); verify div_*(a e^{ikmΦ}) = 0 and hence (7.39); then expand (a e^{ikmΦ}·∇_*)(a' e^{ikm'Φ}) in cylindrical components and check that its only term proportional to k is ikm'(a·n_Φ)a' = -(m'/m)((D_r + R^{-1})a_r + D_z a_z)a', which contains no factor k.",
"depends_on": [
"M7.12",
"M6.12",
"M6.7",
"M7.2"
],
"constrains": [],
"reasons": {
"M7.12": "The divergence identity (7.39) puts a·n_Φ in W_{α+1/2−κ_s}, which removes the factor k from wave self-advection.",
"M6.12": "The product and zero-harmonic rules (6.30), (6.31) give the classes of the wave-mean and wave-wave products.",
"M6.7": "Products of waves with distinct labels vanish by the disjoint auxiliary supports.",
"M7.2": "Mean advection differentiates the phase and costs k = ⌈ε^{-1/2}⌉, the −1/2 in the wave-mean bound."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 102-103",
"analogous_to": [],
"relations": {
"M7.12": "prerequisite",
"M6.12": "prerequisite",
"M6.7": "prerequisite",
"M7.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": "M9.3",
"kind": "move",
"name": "ns-m9-3-residual-decomposition-with-a-quarantined-flat-part",
"title": "Residual decomposition with a quarantined flat part",
"section": "9",
"pages": "103-105",
"refs": [
"pp. 103 to 105",
"Proposition 9.3, (9.3), (9.4), (9.5), (9.6)",
"uses (6.23), (6.28), (7.25), (7.31), (7.33), Lemma 8.2, Proposition 8.1, (8.12)."
],
"statement": "Proposition 9.3: for a state from slow base and primary waves by finitely many pulse inverses, curls, signed amplitude maps for Y-independent stresses and Section 8 mean maps, pressure rebuilt by (8.12) per update, complete-field products: R(u^[j],p^[j])=G^[j]+F^[j] (9.3); (i) nonzero harmonics of G_*^[j] are locally finite sums over labels γ and finite band-independent H_j ⊂ Z∖{0} of f_{γ,m}e^{ik_γmΦ_γ} (9.4), supp(f|E_γ) ⊂ Ω_γ, f ∈ W_α smoothly zero-extended; ⟨G_*^[j]⟩_θ ∈ M_µ; (ii) |F^[j]|_m ≤ C_{j,m,N}q^N ∀N, uniform in bands, labels, points (9.5); (iii) exact mean equations (9.6) hold.",
"description": "Proposition 9.3: for a state from slow base and primary waves by finitely many pulse inverses, curls, signed amplitude maps for Y-independent stresses and Section 8 mean maps, pressure rebuilt by (8.12) per update, complete-field products: R(u^[j],p^[j])=G^[j]+F^[j] (9.3); (i) nonzero harmonics of G_*^[j] are locally finite sums over labels γ and finite band-independent H_j ⊂ Z∖{0} of f_{γ,m}e^{ik_γmΦ_γ} (9.4), supp(f|E_γ) ⊂ Ω_γ, f ∈ W_α smoothly zero-extended; ⟨G_*^[j]⟩_θ ∈ M_µ; (ii) |F^[j]|_m ≤ C_{j,m,N}q^N ∀N, uniform in bands, labels, points (9.5); (iii) exact mean equations (9.6) hold. OBLIGATION: The pulse inverse (Proposition 7.2) accepts only sources with prescribed slow, transverse, shell, and enlarged-rectangle supports and envelope bounds, and mean operations enlarge auxiliary support, so these hypotheses must be re-verified after every cycle. ANTECEDENT: None cited. Internal: Proposition 7.2, Proposition 7.6, (7.33), Lemma 8.2, Proposition 8.1, (8.12). REFS: pp. 103 to 105; Proposition 9.3, (9.3), (9.4), (9.5), (9.6); uses (6.23), (6.28), (7.25), (7.31), (7.33), Lemma 8.2, Proposition 8.1, (8.12).",
"obligation": "The pulse inverse (Proposition 7.2) accepts only sources with prescribed slow, transverse, shell, and enlarged-rectangle supports and envelope bounds, and mean operations enlarge auxiliary support, so these hypotheses must be re-verified after every cycle. The base error E_B, the pulse-cutoff tails, and the cutoff remainders of the compactly supported primitives do not satisfy those hypotheses but are already flat, so they must be kept out of the sources. Part (iii) guarantees that the Section 8 inverses act on the exact conservative mean balance of the full field.",
"backward_question": "Which parts of the residual must the next inverse see, and which are already flat, so that they can be set aside without ever having to satisfy that inverse's support hypotheses?",
"mechanism": "A nonzero harmonic can only come from a product containing a wave factor, and such a product inherits that wave's slow, transverse, and rectangle support and its envelope (P_v^2 ≤ P_v); mean operations never create nonzero harmonics; curls, pressure coefficients, and pulse propagation preserve the phase integer; a quadratic product at most doubles the harmonic range. The pulse inverse propagates along paths with fixed slow and transverse variables, so zero data on a whole path give a zero solution and support containment needs no divisibility by the original cutoffs. For the stress correction fed to Proposition 7.6, a supported interior profile with the same weighted radial moment is subtracted; the zero-moment remainder can be integrated forward from the left edge or backward from the right edge. Near an edge, where ζ ≈ e^{-a/s^2} with s the logarithmic distance, the weight survives integration through ∫_0^δ s^{-M} e^{-a/s^2} ds ≤ C_{M,a} δ^{3-M} e^{-a/δ^2} and |d^k/ds^k e^{-a/s^2}| ≤ C_{k,a} s^{-3k} e^{-a/s^2}. Division by the fixed amplitude a_σ, whose inverse has a ζ^{-1/2} bound, recovers (7.33) and the W_{α-1/2} estimate. The flat term F collects E_B, the Gaussian tails, and the cutoff remainders (Lemma 8.2 makes each O(q^N) at the cost of finitely many extra derivatives); summing polynomially many labels in S_* keeps these bounds; any flat term that a later mean inverse cancels is removed from F.",
"antecedent": "None cited. Internal: Proposition 7.2, Proposition 7.6, (7.33), Lemma 8.2, Proposition 8.1, (8.12).",
"cost": "The flat parts F^[j] are never summed over stages, so the final flatness has to come from comparison with one finite stage (M9.13). Constants and powers of S_* grow with j; H_j grows with j but stays finite at each stage; support containment must be re-checked after every step.",
"checkable": "Numeric check of the edge-weight integral: for a ∈ {0.5, 1, 2} and M ∈ {0, 2, 5, 10}, compute I(δ) = ∫_0^δ s^{-M} e^{-a/s^2} ds by quadrature or by the closed form (1/2) a^{(1-M)/2} Γ((M-1)/2, a/δ^2), and confirm that I(δ)/(δ^{3-M} e^{-a/δ^2}) stays bounded as δ ↓ 0 (it tends to 1/(2a)); also confirm that the supremum over 0 < s ≤ 1 of s^{3k} |∂_s^k e^{-a/s^2}| / e^{-a/s^2} is finite for k ≤ 6.",
"depends_on": [
"M7.6",
"M8.4",
"M7.11",
"M8.2"
],
"constrains": [],
"reasons": {
"M7.6": "The supported part must meet Proposition 7.2's support, extension and envelope hypotheses, which propagation along fixed paths preserves.",
"M8.4": "Cutoff remainders of the compactly supported primitives are flat by Lemma 8.2 and go into F^[j].",
"M7.11": "Stress corrections for the signed amplitude map keep the √ζ-weighted bound (7.33) after division by the fixed amplitudes.",
"M8.2": "Part (iii) is the exact conservative mean balance of Proposition 8.1 for the complete current tuple."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 103-105",
"analogous_to": [],
"relations": {
"M7.6": "prerequisite",
"M8.4": "prerequisite",
"M7.11": "prerequisite",
"M8.2": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: TRUNCATED; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M9.4",
"kind": "move",
"name": "ns-m9-4-the-finite-correction-state-and-the-j-schedule",
"title": "The finite correction state and the σ_j schedule",
"section": "9",
"pages": "106",
"refs": [
"p. 106",
"(9.7), Definition 9.4, (9.8), (9.9), (9.10)."
],
"statement": "Definition 9.4: a stage-j state is a real field (9.7) u_* = (b + β, V + v, G + γ) + w, p_* = p_{B,*} + p_m + p_w, ⟨w⟩_θ = ⟨p_w⟩_θ = 0, w a sum of curls of supported wave potentials with fixed label phases, (β, v, γ) an azimuthal-potential curl plus a direct azimuthal field, with: the structure of Proposition 9.3; (9.8) G^[j]_wave ∈ W_{B_j}, E_θ, E_z ∈ M_{C*_j}, (P, J_θ, J_z) ∈ S_{C*_j}, B_j = 1/2 + σ_j, C*_j = 1 + σ_j, σ_j = 1/5 + j/10; (9.9) w ∈ W_{1/2}, w − w_0^tan ∈ W_{0.68}, v, γ, p_m ∈ M_{0.9}, β ∈ M_{1.9}; (9.10) ∫R^2⟨v⟩_Y dR = ∫R⟨γ⟩_Y dR = 0; pressure reconstruction.",
"description": "Definition 9.4: a stage-j state is a real field (9.7) u_* = (b + β, V + v, G + γ) + w, p_* = p_{B,*} + p_m + p_w, ⟨w⟩_θ = ⟨p_w⟩_θ = 0, w a sum of curls of supported wave potentials with fixed label phases, (β, v, γ) an azimuthal-potential curl plus a direct azimuthal field, with: the structure of Proposition 9.3; (9.8) G^[j]_wave ∈ W_{B_j}, E_θ, E_z ∈ M_{C*_j}, (P, J_θ, J_z) ∈ S_{C*_j}, B_j = 1/2 + σ_j, C*_j = 1 + σ_j, σ_j = 1/5 + j/10; (9.9) w ∈ W_{1/2}, w − w_0^tan ∈ W_{0.68}, v, γ, p_m ∈ M_{0.9}, β ∈ M_{1.9}; (9.10) ∫R^2⟨v⟩_Y dR = ∫R⟨γ⟩_Y dR = 0; pressure reconstruction. OBLIGATION: It is the induction hypothesis: it must hold after initialization and be reproduced with a gain by one cycle. The cumulative bounds are needed because new increments interact with the total existing correction, not only with the last increment. The moment constraints are needed for the integrated identities (8.16), which make the tangential mean residual absorbable by compactly supported stresses. REFS: p. 106; (9.7), Definition 9.4, (9.8), (9.9), (9.10).",
"obligation": "It is the induction hypothesis: it must hold after initialization and be reproduced with a gain by one cycle. The cumulative bounds are needed because new increments interact with the total existing correction, not only with the last increment. The moment constraints are needed for the integrated identities (8.16), which make the tangential mean residual absorbable by compactly supported stresses.",
"backward_question": "What is the smallest list of residual orders and cumulative field sizes that holds after initialization and is reproduced, with a uniform gain, by one cycle of corrections?",
"mechanism": "Three residual components are tracked separately: nonzero harmonics at order B_j, tangential means at C*_j, and three scalar defects at C*_j. The offset of exactly 1/2 between wave and mean orders matches the proof of Proposition 9.6: a wave increment of order B changes the mean covariance, through its product with the order-1/2 primary wave, at order B + 1/2 = C*. The cumulative bounds pin the total correction: the wave stays at the primary size 1/2, its deviation from the primary transverse field w_0^tan has order at least 0.68, tangential means and the mean pressure have order at least 0.9, and the radial mean at least 1.9 (one better, because radial mean velocity is induced as -ε∂_Z of an azimuthal potential, (8.14)). Every residual and defect is recomputed from the updated complete field after each operation.",
"antecedent": "None cited. The introduction (p. 2) cites Córdoba and Martínez-Zoroa [7] for approximations of increasing order that keep every derivative of the source bounded, the nearest cited precedent for order-by-order residual improvement.",
"cost": "Every later increment must respect the thresholds 0.68, 0.9, and 1.9; the two moments must be preserved exactly at every step; pressure must be reconstructed after every update.",
"checkable": "None: this is the definition of the induction hypothesis; its arithmetic is checked in M9.5 and M9.10.",
"depends_on": [
"M9.3",
"M8.1",
"M8.5",
"M7.12"
],
"constrains": [],
"reasons": {
"M9.3": "A stage-j state has the residual structure of Proposition 9.3: supported harmonic sources plus a quarantined flat part.",
"M8.1": "The form (9.7) is the mean decomposition (8.1), and the exact moments (9.10) are the preserved functionals (8.2).",
"M8.5": "Pressure is reconstructed by (8.12), so the radial residual is −ρP plus a flat cutoff remainder.",
"M7.12": "w is a sum of curls of supported wave potentials with the fixed label phases, hence exactly divergence-free."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 106",
"analogous_to": [],
"relations": {
"M9.3": "prerequisite",
"M8.1": "prerequisite",
"M8.5": "prerequisite",
"M7.12": "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": "M9.5",
"kind": "move",
"name": "ns-m9-5-initialization-at-stage-0",
"title": "Initialization at stage 0",
"section": "9",
"pages": "106-107",
"refs": [
"pp. 106 to 107",
"Proposition 9.5, (9.11)",
"uses (7.24), (7.25), (7.26), (7.35), (8.12), (8.20), (8.25)."
],
"statement": "Proposition 9.5. Starting from the fixed base and the curls of the primary potentials, apply the temporal mean update (8.20) and then the five-equation correction (8.25), reconstructing pressure by (8.12) before and after each update. The result is a stage-0 state with B_0 = 0.7 and C*_0 = 1.2.",
"description": "Proposition 9.5. Starting from the fixed base and the curls of the primary potentials, apply the temporal mean update (8.20) and then the five-equation correction (8.25), reconstructing pressure by (8.12) before and after each update. The result is a stage-0 state with B_0 = 0.7 and C*_0 = 1.2. OBLIGATION: Seeds the induction. The raw primary field has linear residual of order 1 - 3κ_s, nonlinear wave residual 1 - κ_s, and mean balances and defects of order only 1 - κ_s, below the required C*_0 = 1.2. MECHANISM: The decisive fact is exact: the primary covariance of Proposition 7.5, assembled by (7.35), cancels the order-zero auxiliary radial-tangential stress Σ^(0) exactly, including the derivatives of the slow partition, because the squared partition functions sum to one. Written as (9.11), the auxiliary averages of E_θ and E_z are built from differences ⟨W_rθ⟩_Y - Σ^(0)_θ and ⟨W_rz⟩_Y - Σ^(0)_z that contain at least one curl remainder (order 1 - κ_s against the order-1/2 primary. ANTECEDENT: None cited. Internal: Proposition 7.5 and (7.26), (7.35), Lemma 8.6, Lemma 8.7. REFS: pp. 106 to 107; Proposition 9.5, (9.11); uses (7.24), (7.25), (7.26), (7.35), (8.12), (8.20), (8.25).",
"obligation": "Seeds the induction. The raw primary field has linear residual of order 1 - 3κ_s, nonlinear wave residual 1 - κ_s, and mean balances and defects of order only 1 - κ_s, below the required C*_0 = 1.2.",
"backward_question": "Does the leading covariance cancel the background stress exactly, partition derivatives included, so that after the primary pulses the auxiliary-averaged residual is controlled by curl-remainder cross terms rather than by the raw quadratic products?",
"mechanism": "The decisive fact is exact: the primary covariance of Proposition 7.5, assembled by (7.35), cancels the order-zero auxiliary radial-tangential stress Σ^(0) exactly, including the derivatives of the slow partition, because the squared partition functions sum to one. Written as (9.11), the auxiliary averages of E_θ and E_z are built from differences ⟨W_rθ⟩_Y - Σ^(0)_θ and ⟨W_rz⟩_Y - Σ^(0)_z that contain at least one curl remainder (order 1 - κ_s against the order-1/2 primary, hence M_{3/2-κ_s} before the divergence), plus axial fluxes, the axial pressure term, and higher-order stress at order at least 2 - κ_s; so ⟨E_θ⟩_Y, ⟨E_z⟩_Y ∈ M_{1.49} already. The torus-dependent part of the mean residual, of order H_0 = 1 - κ_s, is removed by the temporal inverse, whose leftovers have order at least H_0 + 1 - 2κ_s, with wave interactions at H_0. The five-equation map then cancels the linear parts of the defects, and every other term gains more than 0.8, so the defects end above 1.8 - κ_s. Hence waves ≥ 1 - 3κ_s ≥ 0.7, tangential means ≥ 1.49 ≥ 1.2, defects > 1.8 - κ_s ≥ 1.2. The primary curl correction 1 - κ_s > 0.68 and the mean increments H_0 > 0.9, H_0 + 1 > 1.9 give (9.9); the temporal increments have zero auxiliary mean, and the first two rows of (8.25) enforce (9.10).",
"antecedent": "None cited. Internal: Proposition 7.5 and (7.26), (7.35), Lemma 8.6, Lemma 8.7.",
"cost": "B_0 = 0.7 is set well below the available 1 - 3κ_s; this fixes the lower bound B ≥ 0.7 used in every later cycle and the thresholds of (9.9).",
"checkable": "(a) Exponent arithmetic with κ_s = 10^{-5}: 1 - 3κ_s ≥ 0.7; 3/2 - 2κ_s ≥ 1.49 ≥ 1.2; H_0 + 1 - 2κ_s ≥ 1.2; 1.8 - κ_s ≥ 1.2; 1 - κ_s > 0.68; H_0 > 0.9; H_0 + 1 > 1.9. (b) Quadrature check of the covariance identity behind (9.11): build two model real waves b_± = χ_g(ξ)ψ(v) t_± cos(kΦ_±) on disjoint rectangles of T^2, compute H = [C(b_+) | C(b_-)] by angular and Haar quadrature, set a = sqrt(H^{-1}T) componentwise for a target T inside the cone, and confirm C(√ε(a_+ b_+ + a_- b_-)) = εT to quadrature precision.",
"depends_on": [
"M7.10",
"M8.9",
"M8.11",
"M9.4"
],
"constrains": [],
"reasons": {
"M7.10": "The primary covariance, assembled over boxes and bands, cancels the order-zero stress exactly, slow-partition derivatives included.",
"M8.9": "The temporal mean update (8.20) removes the torus-dependent part of the mean residual, of order 1 − κ_s.",
"M8.11": "The five-equation correction (8.25) cancels the linear parts of the defects and enforces the moments (9.10).",
"M9.4": "The outcome must meet Definition 9.4 with B_0 = 0.7, C*_0 = 1.2 and the cumulative bounds (9.9)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 106-107",
"analogous_to": [],
"relations": {
"M7.10": "prerequisite",
"M8.9": "prerequisite",
"M8.11": "prerequisite",
"M9.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": "M9.6",
"kind": "move",
"name": "ns-m9-6-cycle-step-1-cancel-the-supported-harmonics",
"title": "Cycle step 1, cancel the supported harmonics",
"section": "9",
"pages": "108",
"refs": [
"p. 108",
"Proposition 9.6 Step 1, (9.12)",
"uses (7.13), Proposition 7.2, Proposition 9.1, Lemma 9.2, (8.15), (8.16)."
],
"statement": "Proposition 9.6, Step 1: for each grouped source f_m of (9.4), solve L_m(t_m, π_m) = −f_m by Proposition 7.2 with zero entrance data on the common torus and add ∆w_m = curl_*((i n_Φ × (ψt_m))/(km|n_Φ|^2)e^{ikmΦ}), ∆p_{w,m} = ψπ_m e^{ikmΦ}, summed over labels, harmonics, and conjugates. With B = 1/2 + σ_j, C* = 1 + σ_j, the increment is in W_B, its pressure in W_{B+1/2}; new harmonic errors have orders B + 1/2 − 3κ_s, B + 1/2 − κ_s, 2B − κ_s, B + 0.4; E_θ, E_z, ∆g_r, ∆p_m ∈ M_{C*−κ_s}, (P, J_θ, J_z) ∈ S_{C*−κ_s}, and ∫R^2⟨E_θ⟩_Y dR, ∫R⟨E_z⟩_Y dR ∈ S_{C*+1−κ_s} (9.12).",
"description": "Proposition 9.6, Step 1: for each grouped source f_m of (9.4), solve L_m(t_m, π_m) = −f_m by Proposition 7.2 with zero entrance data on the common torus and add ∆w_m = curl_*((i n_Φ × (ψt_m))/(km|n_Φ|^2)e^{ikmΦ}), ∆p_{w,m} = ψπ_m e^{ikmΦ}, summed over labels, harmonics, and conjugates. With B = 1/2 + σ_j, C* = 1 + σ_j, the increment is in W_B, its pressure in W_{B+1/2}; new harmonic errors have orders B + 1/2 − 3κ_s, B + 1/2 − κ_s, 2B − κ_s, B + 0.4; E_θ, E_z, ∆g_r, ∆p_m ∈ M_{C*−κ_s}, (P, J_θ, J_z) ∈ S_{C*−κ_s}, and ∫R^2⟨E_θ⟩_Y dR, ∫R⟨E_z⟩_Y dR ∈ S_{C*+1−κ_s} (9.12). OBLIGATION: Removes the entire nonzero-harmonic residual of order B, which no mean operation can reach, and produces the moment gain (9.12) that Step 2 needs. MECHANISM: The zero-data Duhamel inverse of Proposition 7.2 solves the principal ODE along each pulse; the cutoff and curl make the increment divergence-free; Proposition 9.1 bounds the linear error and Lemma 9.2 the interactions (old exact waves in W_{1/2}, mean correction in. REFS: p. 108; Proposition 9.6 Step 1, (9.12); uses (7.13), Proposition 7.2, Proposition 9.1, Lemma 9.2, (8.15), (8.16).",
"obligation": "Removes the entire nonzero-harmonic residual of order B, which no mean operation can reach, and produces the moment gain (9.12) that Step 2 needs.",
"backward_question": "After the harmonics are removed, how much does the angular mean degrade, and can the conservation constraints make the weighted radial moments of the mean residual better than the residual itself?",
"mechanism": "The zero-data Duhamel inverse of Proposition 7.2 solves the principal ODE along each pulse; the cutoff and curl make the increment divergence-free; Proposition 9.1 bounds the linear error and Lemma 9.2 the interactions (old exact waves in W_{1/2}, mean correction in M_{0.9}). The new waves change the angular mean only through covariance products with existing waves, at order B + 1/2 = C*, and a radial divergence costs κ_s. The moment gain uses conservation: with (9.10) preserved, the exact integrated identities (8.16), ∫R^2 ⟨E_θ⟩_Y dR = ε∂_Z J_θ and ∫R ⟨E_z⟩_Y dR = ε∂_Z(J_z + c_ρ P), express the weighted moments as axial derivatives carrying a factor ε, one full order better than the residual itself. The term c_ρ P inside ∂_Z accounts for the -ρP left in the radial equation by pressure reconstruction.",
"antecedent": "None cited. Internal: Proposition 7.2 (Duhamel formula along the pulse), Proposition 9.1, Lemma 9.2, Proposition 8.4 and (8.16).",
"cost": "The mean residual and defects degrade by κ_s (to C* - κ_s); new flat cutoff tails join F; the new products create auxiliary-dependent means that Steps 2 and 3 must remove.",
"checkable": "Numeric check of the identity (8.16) behind (9.12): on a grid in (R, Z, T), take smooth compactly supported, Y-independent mean fields with (β, γ) = (-ε∂_Z Ψ, (∂_R + R^{-1})Ψ) from a compactly supported Ψ (so ∫R γ dR = 0 automatically) and v with ∫R^2 v dR = 0 at every (Z, T); take a smooth symmetric covariance W, a base (b, V, G), and compactly supported base stresses Σ_θ, Σ_z; compute g_r, P, p_m = T_0(g_r - ρP), E_θ, E_z from (8.3) and (8.12) with t_* = -ε∂_T and D_r = ∂_R; compare ∫R^2 E_θ dR with ε∂_Z J_θ and ∫R E_z dR with ε∂_Z(J_z + c_ρ P) from (8.15). Agreement to discretization error is expected.",
"depends_on": [
"M7.6",
"M9.1",
"M9.2",
"M8.7"
],
"constrains": [],
"reasons": {
"M7.6": "Solves L_m(t_m, π_m) = −f_m for each supported source by Proposition 7.2 with zero data along the pulse path.",
"M9.1": "Proposition 9.1 bounds the new linear residual at B + 1/2 − 3κ_s.",
"M9.2": "Lemma 9.2 bounds the new interactions with old waves, with the mean correction (B + 0.4), and the self-interaction.",
"M8.7": "The integrated identities (8.16) turn the weighted moments into ε∂_Z of defects, giving the extra order of (9.12)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 108",
"analogous_to": [],
"relations": {
"M7.6": "prerequisite",
"M9.1": "prerequisite",
"M9.2": "prerequisite",
"M8.7": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: TRUNCATED; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M9.7",
"kind": "move",
"name": "ns-m9-7-cycle-step-2-signed-stress-correction-of-the-auxiliary",
"title": "Cycle step 2, signed stress correction of the auxiliary-averaged residual",
"section": "9",
"pages": "108-110",
"refs": [
"pp. 108 to 110",
"Proposition 9.6 Step 2, (9.13), (9.14)",
"uses (7.31), (7.34), (7.35), (7.36), (7.41), (7.42), (9.12)."
],
"statement": "Proposition 9.6, Step 2: with F_2 = Q^{−2A−1/2}⟨E_θ⟩_Y, F_1 = Q^{−2A−1/2}⟨E_z⟩_Y, profiles b_e = q^{−(e+1)/2}b̂_e(r/√q), ∫x^e b̂_e = 1, M_e = ∫r^eF_e dr, σ_e = −r^{−e}∫_0^r(r′)^e(F_e − b_eM_e)dr′ (e = 1, 2), σ_e is compactly supported, (∂_r + e/r)σ_e = −F_e + b_eM_e, and Σ = Q^{2A}(σ_2, σ_1) ∈ M_{C*−κ_s} is auxiliary-independent. The correction L^asΣ ∈ W_{B−κ_s} of (7.35) has B(w_0^tan, L^asΣ) = Σ (7.36); with the covariance change (9.13) and pressure reconstruction, (9.14): ⟨E_θ⟩_Y, ⟨E_z⟩_Y ∈ M_{C*+0.17}, E_θ, E_z ∈ M_H, (P, J_θ, J_z) ∈ S_H, H = C* − 2κ_s.",
"description": "Proposition 9.6, Step 2: with F_2 = Q^{−2A−1/2}⟨E_θ⟩_Y, F_1 = Q^{−2A−1/2}⟨E_z⟩_Y, profiles b_e = q^{−(e+1)/2}b̂_e(r/√q), ∫x^e b̂_e = 1, M_e = ∫r^eF_e dr, σ_e = −r^{−e}∫_0^r(r′)^e(F_e − b_eM_e)dr′ (e = 1, 2), σ_e is compactly supported, (∂_r + e/r)σ_e = −F_e + b_eM_e, and Σ = Q^{2A}(σ_2, σ_1) ∈ M_{C*−κ_s} is auxiliary-independent. The correction L^asΣ ∈ W_{B−κ_s} of (7.35) has B(w_0^tan, L^asΣ) = Σ (7.36); with the covariance change (9.13) and pressure reconstruction, (9.14): ⟨E_θ⟩_Y, ⟨E_z⟩_Y ∈ M_{C*+0.17}, E_θ, E_z ∈ M_H, (P, J_θ, J_z) ∈ S_H, H = C* − 2κ_s. OBLIGATION: The auxiliary-averaged tangential residual cannot be inverted by the fast-time derivative, which needs zero auxiliary mean, and would otherwise stay at order C*. It must be absorbed by changing the waves' radial fluxes of azimuthal and axial momentum through a compactly supported, chart-consistent stress. REFS: pp. 108 to 110; Proposition 9.6 Step 2, (9.13), (9.14); uses (7.31), (7.34), (7.35), (7.36), (7.41), (7.42), (9.12).",
"obligation": "The auxiliary-averaged tangential residual cannot be inverted by the fast-time derivative, which needs zero auxiliary mean, and would otherwise stay at order C*. It must be absorbed by changing the waves' radial fluxes of azimuthal and axial momentum through a compactly supported, chart-consistent stress.",
"backward_question": "The stress is realized as a positive combination of squared amplitudes; how can I make corrections of either sign without re-solving the positivity problem, and how can the correcting stress be compactly supported in the annulus?",
"mechanism": "Subtracting b_e M_e removes the weighted radial moment, so the primitive σ_e vanishes beyond the source support and no cutoff remainder appears; the subtracted bump term is harmless because M_e has order C* + 1 - κ_s by (9.12). The stress is realized by linearizing the covariance map at the fixed primary amplitudes: dΣ = H^{-1}(Σ/ε) and δa_σ = (dΣ)_σ/(2a_σ), so the symmetrized cross covariance with the primary wave is exactly Σ (L is a right inverse of DC(W_0), Proposition 7.6). Dividing by the fixed positive 2√y_σ allows increments of either sign, and no square root of the current covariance or of y + dΣ is ever taken. The exact expansion (9.13), ⟨∆W⟩_Y = B(w_0^tan, t_s) + B(w - w_0^tan, t_s) + B(w, r_s) + ⟨⟨s ⊗ s⟩_θ⟩_Y, isolates the term whose radial-tangential components equal Σ, whose divergence cancels F_e - b_e M_e, from three remainders: transverse correction times old-wave remainder (C* + 0.18 - κ_s, from w - w_0^tan ∈ W_{0.68}), signed curl remainder times old wave (C* + 1/2 - 2κ_s), and self-interaction (C* + σ_j - 2κ_s); the divergence costs one more κ_s. Since 0.18 - 2κ_s > 0.17 and σ_j - 3κ_s > 0.17, the auxiliary average improves by 0.17. The auxiliary-dependent part of the new products has order only H = C* - 2κ_s and is left for Step 3.",
"antecedent": "None cited in Section 9. Internal: Proposition 7.6, (7.35), (7.36), Corollary 7.8. The introduction (p. 2) credits Daneri and Székelyhidi [10] with the use of oscillations to realize a prescribed stress.",
"cost": "New wave errors of orders B + 1/2 - 4κ_s (linear), B + 0.4 - κ_s (mean interaction), B + 1/2 - 2κ_s (cross with old waves), 2B - 3κ_s (self-interaction); the full mean residual worsens to H = C* - 2κ_s; the averaged gain is capped at 0.17 by the 0.68 bound in (9.9); the primary amplitudes a_σ must stay fixed forever; the stress must be auxiliary-independent.",
"checkable": "(a) Numeric radial primitive: for a random smooth F supported in [r_1, r_2] and a bump b̂_e supported inside with ∫x^e b̂_e dx = 1, compute σ_e by cumulative quadrature and verify (∂_r + e/r)σ_e + F_e - b_e M_e = 0 on the grid and σ_e = 0 for r > r_2, for e = 1, 2. (b) Linear algebra: for a random invertible 2×2 H with y = H^{-1}T > 0, a = √y, and a random Σ, form δa = (H^{-1}Σ/ε)/(2a) componentwise; confirm εH(2a ⊙ δa) = Σ and εH((a + δa) ⊙ (a + δa)) - εH(a ⊙ a) - Σ = εH(δa ⊙ δa), the quadratic remainder kept in the residual.",
"depends_on": [
"M7.11",
"M7.14",
"M9.6",
"M9.4"
],
"constrains": [],
"reasons": {
"M7.11": "The stress Σ is realized by the signed amplitude map L^as, with B(w_0^tan, L^asΣ) = Σ by (7.36).",
"M7.14": "Corollary 7.8 gives the exact covariance change (9.13) and the orders of its three remainders.",
"M9.6": "By (9.12) the weighted moments M_e have order C* + 1 − κ_s, so the subtracted bump term b_eM_e is harmless.",
"M9.4": "The cumulative bound w − w_0^tan ∈ W_{0.68} of (9.9) sets the leading remainder order C* + 0.18 − κ_s."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 108-110",
"analogous_to": [],
"relations": {
"M7.11": "prerequisite",
"M7.14": "prerequisite",
"M9.6": "prerequisite",
"M9.4": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "completeness audit 2026-10-01: INCOMPLETE; statement replaced from the digest",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},
{
"id": "M9.8",
"kind": "move",
"name": "ns-m9-8-cycle-step-3-fast-time-inverse-on-the-auxiliary-dependent",
"title": "Cycle step 3, fast-time inverse on the auxiliary-dependent means",
"section": "9",
"pages": "110",
"refs": [
"p. 110",
"Proposition 9.6 Step 3",
"uses (8.3), (8.14), (8.20), (8.22), Lemma 8.6, (6.7)."
],
"statement": "Proposition 9.6, Step 3: for E°_a = E_a − ⟨E_a⟩_Y ∈ M_H (a = θ, z) set ∆v = −c_{i0}^{−1}N_{i0}^{−1}E°_θ, γ_d = −c_{i0}^{−1}N_{i0}^{−1}E°_z (N_{i0}^{−1} the zero-average inverse of Lemma 8.6), Ψ_* = T_1γ_d, ∆β = −ε∂_ZΨ_*, ∆γ = (D_r + R^{−1})Ψ_*. Then c_{i0}N_{i0}∆v = −E°_θ and c_{i0}N_{i0}∆γ = −E°_z + F_ax with F_ax flat; after pressure recomputation the residual changes minus F_ax lie in M_{H+1−2κ_s}, the wave change in W_H, E_θ, E_z ∈ M_{min(C*+0.17, H+1−2κ_s)}, and (P, J_θ, J_z) ∈ S_H.",
"description": "Proposition 9.6, Step 3: for E°_a = E_a − ⟨E_a⟩_Y ∈ M_H (a = θ, z) set ∆v = −c_{i0}^{−1}N_{i0}^{−1}E°_θ, γ_d = −c_{i0}^{−1}N_{i0}^{−1}E°_z (N_{i0}^{−1} the zero-average inverse of Lemma 8.6), Ψ_* = T_1γ_d, ∆β = −ε∂_ZΨ_*, ∆γ = (D_r + R^{−1})Ψ_*. Then c_{i0}N_{i0}∆v = −E°_θ and c_{i0}N_{i0}∆γ = −E°_z + F_ax with F_ax flat; after pressure recomputation the residual changes minus F_ax lie in M_{H+1−2κ_s}, the wave change in W_H, E_θ, E_z ∈ M_{min(C*+0.17, H+1−2κ_s)}, and (P, J_θ, J_z) ∈ S_H. OBLIGATION: Removes the auxiliary-dependent part of the mean residual, which Step 2 does not see and which a compactly supported radial primitive cannot absorb. MECHANISM: The normalized physical time derivative splits as t_* = -ε∂_T + c_{i0}N_{i0}, where N = v_t·∂_y differentiates along the irrational direction v_t = (√2 - 1, 1) of T^2. On zero-mean functions N is inverted by Fourier division, and the divisor bound |v_t·k| ≥ c/(1 + |k|) of (6.7) costs four torus derivatives and no power of ε (c_{i0}^{-1} ≤ C S_*). REFS: p. 110; Proposition 9.6 Step 3; uses (8.3), (8.14), (8.20), (8.22), Lemma 8.6, (6.7).",
"obligation": "Removes the auxiliary-dependent part of the mean residual, which Step 2 does not see and which a compactly supported radial primitive cannot absorb.",
"backward_question": "The auxiliary-dependent mean residual oscillates on the torus; since the physical time derivative contains a fast derivative along an irrational torus direction, can I invert that fast derivative instead of the slow evolution?",
"mechanism": "The normalized physical time derivative splits as t_* = -ε∂_T + c_{i0}N_{i0}, where N = v_t·∂_y differentiates along the irrational direction v_t = (√2 - 1, 1) of T^2. On zero-mean functions N is inverted by Fourier division, and the divisor bound |v_t·k| ≥ c/(1 + |k|) of (6.7) costs four torus derivatives and no power of ε (c_{i0}^{-1} ≤ C S_*). The azimuthal increment is added directly. The axial increment is realized through an azimuthal vector potential built with the compactly supported primitive of (8.14), so the increment is exactly divergence-free; because γ_d has zero auxiliary mean, the axial reconstruction error F_ax is flat (Lemma 8.2) and goes to F. What remains of the operator is slow: slow time (gain 1), radial fluxes containing b = O(ε) or a radial mean (gain 1 - κ_s), axial fluxes through D_z = ε∂_Z (gain 1), and viscosity with its factor ε and two D_r (gain 1 - 2κ_s). The pressure change 2V∆v/R has order H in ∆g_r but enters E_z only through D_z.",
"antecedent": "None cited in Section 9. Internal: Lemma 8.6, Proposition 8.3(ii), (6.7). (Not named by the manuscript: (6.7) is proved in Section 6 by the algebraic-conjugate argument for √2, a Liouville-type bound for a quadratic irrational.)",
"cost": "A polynomial loss c_{i0}^{-1} ≤ C S_*; four extra torus derivatives per application; a flat term F_ax added to F; the inverse preserves slow and radial supports but not auxiliary-torus support.",
"checkable": "FFT on T^2: take a smooth zero-mean trigonometric polynomial F(y), compute φ = N^{-1}F by dividing each Fourier coefficient by 2πi v_t·k with v_t = (√2 - 1, 1), and confirm v_t·∇φ = F to spectral precision; compute the minimum over 0 < |k|_∞ ≤ K of (1 + |k|)|v_t·k| for K up to 10^4 and confirm it stays bounded below (the constant in (6.7)).",
"depends_on": [
"M8.9",
"M8.6",
"M8.4",
"M9.7"
],
"constrains": [],
"reasons": {
"M8.9": "∆v and γ_d are the fast-time inverses (8.20) of Lemma 8.6 applied to the zero-auxiliary-mean parts E°_θ, E°_z.",
"M8.6": "The axial increment is realized through the azimuthal potential of (8.14), so it is exactly divergence-free.",
"M8.4": "Because γ_d has zero auxiliary mean, the axial reconstruction error F_ax is flat by Lemma 8.2.",
"M9.7": "Starts from the state after Step 2, where E_θ, E_z ∈ M_H and their auxiliary averages lie in M_{C*+0.17}."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 110",
"analogous_to": [],
"relations": {
"M8.9": "prerequisite",
"M8.6": "prerequisite",
"M8.4": "prerequisite",
"M9.7": "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": "M9.9",
"kind": "move",
"name": "ns-m9-9-cycle-step-4-five-equation-correction-of-the-defects",
"title": "Cycle step 4, five-equation correction of the defects",
"section": "9",
"pages": "111",
"refs": [
"p. 111",
"Proposition 9.6 Step 4",
"uses (8.24), (8.25), (8.26), (8.27), Lemma 8.7, Lemma 8.8."
],
"statement": "Proposition 9.6(iv). Apply the linear map (8.25) of Lemma 8.7 to the current defects (P, J_θ, J_z) at order H. The slow increments ∆v, γ_d ∈ M_H are supported on the fixed test-function profiles inside the reserved mean patch, the induced radial velocity is in M_{H+1}, the first two rows preserve (9.10), and the last three cancel the linear contributions to the changes of (P, J_θ, J_z). After pressure recomputation, (P, J_θ, J_z) ∈ S_{H+0.9-2κ_s} = S_{C*+0.9-4κ_s}.",
"description": "Proposition 9.6(iv). Apply the linear map (8.25) of Lemma 8.7 to the current defects (P, J_θ, J_z) at order H. The slow increments ∆v, γ_d ∈ M_H are supported on the fixed test-function profiles inside the reserved mean patch, the induced radial velocity is in M_{H+1}, the first two rows preserve (9.10), and the last three cancel the linear contributions to the changes of (P, J_θ, J_z). After pressure recomputation, (P, J_θ, J_z) ∈ S_{H+0.9-2κ_s} = S_{C*+0.9-4κ_s}. OBLIGATION: Pressure and stress corrections can be compactly supported in the annulus only if three scalar integrals vanish: the radial source integral P and the axial flux defects J_θ, J_z. Left alone, they would block the next pressure reconstruction and the next Step 2. The two exact moments (9.10) must also survive. MECHANISM: On the reserved mean patch the base is exactly G_q = 0, V_q = a(η)x^{-1-2λ} (8.24), so the five weighted integrals of three azimuthal bumps and two. ANTECEDENT: None cited in Section 9. Internal: Lemma 8.7 (invertibility via the ordinary Vandermonde determinant, named in Section 8) and Lemma 8.8. REFS: p. 111; Proposition 9.6 Step 4; uses (8.24), (8.25), (8.26), (8.27), Lemma 8.7, Lemma 8.8.",
"obligation": "Pressure and stress corrections can be compactly supported in the annulus only if three scalar integrals vanish: the radial source integral P and the axial flux defects J_θ, J_z. Left alone, they would block the next pressure reconstruction and the next Step 2. The two exact moments (9.10) must also survive.",
"backward_question": "Compact support of the pressure and stress corrections fails only through three scalar integrals at each (Z, T); which finite family of slow velocity bumps can zero them while keeping the two conserved moments at zero?",
"mechanism": "On the reserved mean patch the base is exactly G_q = 0, V_q = a(η)x^{-1-2λ} (8.24), so the five weighted integrals of three azimuthal bumps and two axial bumps reduce to power moments with distinct exponents: 2, -2-2λ, -2λ in the angular block and 1, 1-2λ in the axial block. With geometric copies η_j(x) = a_j^{-1}η_0(x/a_j), a_j = e^{jd}, the moment matrices are Vandermonde matrices in the numbers e^{dp}, hence invertible, and the map is fixed and linear. It cancels exactly the terms linear in the base. The exact recomputed defects (8.27) contain only products of tangential means (order at least H + 0.9, since the existing v, γ are in M_{0.9}) and moments of the slow radial remainder R_g of (8.26) (slow time of the induced radial velocity, radial fluxes with b or radial means, axial derivatives, radial viscosity), all of order at least H + 0.9 - 2κ_s by Lemma 8.8. Slow increments have no fast-time term to cancel, and their effect on the tangential residuals has order at least H + 1 - 2κ_s.",
"antecedent": "None cited in Section 9. Internal: Lemma 8.7 (invertibility via the ordinary Vandermonde determinant, named in Section 8) and Lemma 8.8.",
"cost": "Needs the reserved interval I_mean with the exact power law (8.24) and λ > 0; the inverse may deteriorate as λ ↓ 0 (no uniformity is required); the defect gain 0.9 - 4κ_s relies on the cumulative bound v, γ ∈ M_{0.9}.",
"checkable": "Numeric: choose λ = 0.1, a(η) = 1, d = 0.2, and a smooth normalized bump η_0; compute μ_p = ∫x^p η_0 dx, assemble A_θ (3×3) and A_z (2×2) as displayed on p. 98, and confirm nonzero determinants; for random targets (P, J_θ, J_z) solve for (u_0, u_1, u_2) and (s_0, s_1), form ∆v and γ_d, and verify the five equations (8.25) by quadrature. Then apply the increments to a model mean correction and covariance, recompute (P, J_θ, J_z) directly from (8.3), (8.12), (8.15), and confirm they equal the right sides of (8.27) with R_g from (8.26).",
"depends_on": [
"M8.11",
"M8.12",
"M9.4",
"M8.10"
],
"constrains": [],
"reasons": {
"M8.11": "Applies the five-equation map (8.25) of Lemma 8.7 to the current defects, preserving (9.10) with its first two rows.",
"M8.12": "Lemma 8.8 gives the exact recomputed defects (8.27) and their gain to order H + 0.9 − 2κ_s.",
"M9.4": "The gain uses the cumulative bounds v, γ ∈ M_{0.9} and β ∈ M_{1.9} of (9.9), and the moments (9.10) must survive.",
"M8.10": "The increments sit on fixed profiles in the reserved mean patch, where the base is the explicit power law (8.24)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 111",
"analogous_to": [],
"relations": {
"M8.11": "prerequisite",
"M8.12": "prerequisite",
"M9.4": "prerequisite",
"M8.10": "prerequisite"
},
"document": {
"id": "manuscript",
"sha256": "0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f"
},
"verification": {
"source_retrieved": true,
"statement_checked": "digest-only",
"hypotheses_checked": "not-checked",
"computation_checked": false,
"astra_spot_check": null
}
},