Other material · A dividing-plane barrier in the OpenAI forced Navier-Stokes blow-up construction
The ledger as data, version 1.0, September 30, 2026
The first version of the ledger (see ledger.md) in machine-readable form, generated on September 30, 2026, and kept frozen as exactly what the three small open models of Hypnos, the research harness this site describes (Gemma 4 31B, Gemma 4 26B and Qwen3 32B), were shown in a one-time test on the manuscript's moves with the reasons withheld: in 16,018 lines of their output, graded blind by Claude Opus 5.5 sessions, they never recovered the reason for a move. It is shown here in pages of whole records.
- Written by
- Claude Opus sessions and Claude Fable 5.1 (Anthropic)
- Size
- 897,753 bytes
- SHA-256
f2f7a98d815175f32ec70f1d694bf138920b250608d0376a13191fe89b8120a2
The note's pageEvery file published with itThis file on GitHub
{
"id": "M5.8",
"kind": "move",
"name": "ns-m5-8-support-closure-past-x-and-exact-vanishing-on-the-mean",
"title": "Support closure past X+ and exact vanishing on the mean patch",
"section": "5",
"pages": "45-62",
"refs": [
"p52 (Step 3, (5.17), (5.18), the remark on Ω0)."
],
"statement": "Lemma 5.2, Step 3. Choose X+ beyond the leading axial-velocity perturbation U0 (hence beyond Xv), beyond every positive-order patch, and before the terminal outer collar. Then: - Fn = mn,1 = 0, hence AX(Un) = Vn = 0, for X ≥ X+. - Every term of every Ωk contains a V factor or a V derivative, and each ϕiϕj (i + j = n ≥ 1) has a positive-order factor. So ∂XΠn = 0 beyond X+, and Πn = mn,3 = 0 there. Consequences: - (5.12): supp_X Pn ⊂ [0, X+], with mn(η) = 0.",
"description": "Lemma 5.2, Step 3. Choose X+ beyond the leading axial-velocity perturbation U0 (hence beyond Xv), beyond every positive-order patch, and before the terminal outer collar. Then: - Fn = mn,1 = 0, hence AX(Un) = Vn = 0, for X ≥ X+. - Every term of every Ωk contains a V factor or a V derivative, and each ϕiϕj (i + j = n ≥ 1) has a positive-order factor. So ∂XΠn = 0 beyond X+, and Πn = mn,3 = 0 there. Consequences: - (5.12): supp_X Pn ⊂ [0, X+], with mn(η) = 0. OBLIGATION: Positive orders must not touch the exterior heat flow (4.29), whose residual is identically zero; Theorem 3.1(iii) and the localization need this. They must also leave the mean patch Imean exactly at the leading power law, with zero axial velocity, for the corrections of Section 8. MECHANISM: A radially integrated field vanishes past a support radius exactly when its total integral vanishes. The streamfunction vanishes by mn,1. The radial velocity then vanishes by (5.2). ANTECEDENT: None cited. Internal: Theorem 4.6(v) (U = V0 = 0 on [Xv, ∞)) and Theorem 4.6(vi) (Ipos and Imean lie in (Xa, Xv), with sup Ipos < inf Imean). REFS: p52 (Step 3, (5.17), (5.18), the remark on Ω0).",
"obligation": "Positive orders must not touch the exterior heat flow (4.29), whose residual is identically zero; Theorem 3.1(iii) and the localization need this. They must also leave the mean patch Imean exactly at the leading power law, with zero axial velocity, for the corrections of Section 8.",
"backward_question": "Once the moments are zeroed, do all radially integrated fields vanish beyond a single n-independent radius, and what constrains where that radius may sit?",
"mechanism": "A radially integrated field vanishes past a support radius exactly when its total integral vanishes. The streamfunction vanishes by mn,1. The radial velocity then vanishes by (5.2). The pressure vanishes by mn,3, once its radial derivative vanishes. That radial derivative contains Ω_{n-1}, which involves the leading radial velocity V0, nonzero until Xv. The manuscript: \"placing X+ beyond the leading axial-velocity perturbation is essential for the pressure support: Ω0 can remain nonzero beyond the positive-order patches.\" Imean lies to the right of both the inner cutoff and Ipos (sup Ipos < inf Imean). There, En = Un = 0 by construction. Fn = 0 because the axial flux has already been zeroed once Ipos is passed, and then Vn = 0 by (5.2).",
"antecedent": "None cited. Internal: Theorem 4.6(v) (U = V0 = 0 on [Xv, ∞)) and Theorem 4.6(vi) (Ipos and Imean lie in (Xa, Xv), with sup Ipos < inf Imean).",
"cost": "- Positive-order corrections occupy [X-, X+], a subinterval of the wave annulus. - The pressure corrections Πn need not vanish on Imean; only the velocity components are claimed to. - The constants C_{n,m} are uncontrolled in n.",
"checkable": "A toy order-one computation. 1. Prescribe smooth test lower-order data with U0 = V0 = 0 beyond a radius Xv. 2. Build (5.14) with coefficients from (5.16) and reconstruct (5.15) by cumulative quadrature. 3. Confirm that Fn, Vn, Πn vanish on [X+, 2X+] to quadrature tolerance. 4. With α = β = 0 instead, confirm they tend to nonzero constants: m^0_{n,1} for Fn and m^0_{n,3} for Πn.",
"depends_on": [
"M5.7",
"M4.8",
"M5.2"
],
"constrains": [],
"reasons": {
"M5.7": "the zeroed moments m_n,1 and m_n,3 from the bump solve make the streamfunction and pressure vanish past the patches.",
"M4.8": "X+ lies beyond X_v, where Theorem 4.6(v) gives U = V0 = 0, and I_mean lies right of I_pos by Theorem 4.6(vi).",
"M5.2": "V_n follows from A_X(U_n) by (5.2), and Π_n' from (5.5), whose Ω_{n-1} terms all carry a V factor."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62"
},
{
"id": "M5.9",
"kind": "move",
"name": "ns-m5-9-conservative-forms-make-the-total-tangential-residual",
"title": "Conservative forms make the total tangential residual integrals vanish",
"section": "5",
"pages": "45-62",
"refs": [
"p53 (conservative forms, moment scalings, (5.19), (5.20), (5.21))",
"p54 (removal of powers, backward representation)."
],
"statement": "Lemma 5.2, Step 4. For smooth axisymmetric divergence-free fields: - r^2Rθ = ∂t(r^2uθ) + ∂r(r^2uruθ) + ∂z(r^2uzuθ) - ∂r(r^2∂ruθ - ruθ) - ∂zz(r^2uθ); - rRz = ∂t(ruz) + ∂r(ruruz) + ∂z(r(uz^2 + p)) - ∂r(r∂ruz) - ∂zz(ruz). The order-n moments scale as: - ∫r^2uθ,n dr = q^{3/2-A+λn} ∫R^2En dR; - ∫r^2 Σ uz,i uθ,j dr = q^{3/2-2A+λn} ∫R^2 Σ Ui Ej dR; - (5.20): ∫ruz,n dr = q^{1-A+λn} ∫RUn dR and ∫r(Σuz,iuz,j + pn) dr = q^{1-2A+λn} ∫R(ΣUiUj + Πn) dR;",
"description": "Lemma 5.2, Step 4. For smooth axisymmetric divergence-free fields: - r^2Rθ = ∂t(r^2uθ) + ∂r(r^2uruθ) + ∂z(r^2uzuθ) - ∂r(r^2∂ruθ - ruθ) - ∂zz(r^2uθ); - rRz = ∂t(ruz) + ∂r(ruruz) + ∂z(r(uz^2 + p)) - ∂r(r∂ruz) - ∂zz(ruz). The order-n moments scale as: - ∫r^2uθ,n dr = q^{3/2-A+λn} ∫R^2En dR; - ∫r^2 Σ uz,i uθ,j dr = q^{3/2-2A+λn} ∫R^2 Σ Ui Ej dR; - (5.20): ∫ruz,n dr = q^{1-A+λn} ∫RUn dR and ∫r(Σuz,iuz,j + pn) dr = q^{1-2A+λn} ∫R(ΣUiUj + Πn) dR; OBLIGATION: Proves that zeroing the five moments makes the order-n stress vanish past the correction support, so the forward and backward primitives coincide. MECHANISM: Integrating the conservative forms in r removes all radial flux terms: axis parity handles r = 0, and compact positive-order support handles infinity. What remains is ∂t and ∂z of radial integrals: - angular momentum (mn,2); - axial transport of angular momentum (mn,4); - axial flux (mn,1); ANTECEDENT: None cited. Internal: (4.28), (A.45), and Lemma A.8 (the same argument at order zero). REFS: p53 (conservative forms, moment scalings, (5.19), (5.20), (5.21)); p54 (removal of powers, backward representation).",
"obligation": "Proves that zeroing the five moments makes the order-n stress vanish past the correction support, so the forward and backward primitives coincide.",
"backward_question": "Which terms of the tangential residual survive integration against r^2 dr and r dr? Are five moments exactly enough to kill them all, including the pressure contribution and the axial viscosity inherited from the previous order?",
"mechanism": "Integrating the conservative forms in r removes all radial flux terms: axis parity handles r = 0, and compact positive-order support handles infinity. What remains is ∂t and ∂z of radial integrals: - angular momentum (mn,2); - axial transport of angular momentum (mn,4); - axial flux (mn,1); - axial momentum flux including pressure (mn,5, after integrating the pressure by parts); - the order n-1 integrals hit by axial viscosity, which vanish by the previous order's moments, or at order zero by (4.28). The product power q^{...+λn} does not depend on the split i + j = n. So each integral vanishes identically in (z, t) before the physical derivatives are taken. At n = 1 the leading angular momentum integral diverges, since uθ,0 decays like r^{-1-2h}. The z-independent pure power P, which ∂zz does not see, is therefore subtracted. Differentiation under the integral is justified because beyond the terminal collar uθ,0 = K(r, t) is z-independent.",
"antecedent": "None cited. Internal: (4.28), (A.45), and Lemma A.8 (the same argument at order zero).",
"cost": "Order one depends on the renormalized angular moment identity of the leading construction. The resulting representation is for a signed stress; there is no positivity.",
"checkable": "1. Symbolic (sympy): take ur = -∂zS/r and uz = ∂rS/r for a generic S(r, z, t), with generic uθ and p. Expand r^2 times the azimuthal residual and r times the axial residual, and confirm they equal the displayed conservative forms. 2. Quadrature: for compactly supported test En(R) and Πn(R), confirm ∫r^2uθ,n dr / (q^{3/2-A+λn}∫R^2En dR) = 1 with r = √q R. 3. Confirm ∫RΠn dR = -(1/2)∫R^2∂RΠn dR.",
"depends_on": [
"M5.8",
"M5.6",
"MA.12",
"M4.8"
],
"constrains": [],
"reasons": {
"M5.8": "uses m_n = 0 and the compact support of positive orders in [0, X+] to drop the flux terms at infinity.",
"M5.6": "the conservative forms reduce the weighted residual integrals to derivatives of the moments (5.10), (5.11), giving the backward form of (5.9).",
"MA.12": "repeats Lemma A.8's order-zero argument; at n = 1 it subtracts the pure-power exterior P of (A.45) so the angular moment converges.",
"M4.8": "the n = 1 axial-viscosity term needs the order-zero identities (4.28) and the z-independent heat exterior (4.29)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62"
},
{
"id": "M5.10",
"kind": "move",
"name": "ns-m5-10-order-one-stress-at-the-outer-edge-is-flat-at-the-rate-of",
"title": "Order-one stress at the outer edge is flat at the rate of ζ",
"section": "5",
"pages": "45-62",
"refs": [
"p54 (Step 5, az, bz, bounds on fo, Lemma A.9, (5.22))",
"p50 ((5.13))",
"p44 (definition of ζ in the proof of Theorem 4.6)."
],
"statement": "Lemma 5.2, Step 5, and (5.13). - For n ≥ 2 the residual vanishes beyond X+: same-order terms have a positive-order factor, and axial viscosity acts on order n - 1 > 0. So supp Tn ⊂ [X-, X+], and every derivative of Tn/ζ is bounded (N_{n,I} = 0). - For n = 1 the only exterior source is -∂zz uθ,0. Beyond Xb the leading swirl is the z-independent heat field, so supp T1 ⊂ [X-, Xb].",
"description": "Lemma 5.2, Step 5, and (5.13). - For n ≥ 2 the residual vanishes beyond X+: same-order terms have a positive-order factor, and axial viscosity acts on order n - 1 > 0. So supp Tn ⊂ [X-, X+], and every derivative of Tn/ζ is bounded (N_{n,I} = 0). - For n = 1 the only exterior source is -∂zz uθ,0. Beyond Xb the leading swirl is the z-independent heat field, so supp T1 ⊂ [X-, Xb]. OBLIGATION: Later sections build wave amplitudes on the weight ζ; amplitudes carry √ζ in the class W_α. They must also absorb the higher-order stress by signed corrections. So that stress must vanish at the annulus edges as fast as ζ, up to finite inverse powers of δ. Without Step 5, T1 could reach the outer edge Xb at a rate not dominated by ζ. MECHANISM: At order one, inside the terminal collar, the leading swirl is the heat field times a terminal multiplier fo(log X). Since X = s/q depends on z, axial viscosity produces a source built from ∂y fo. ANTECEDENT: None cited. Internal: Lemma A.9, the terminal multiplier (A.12), the heat profile (4.29), and the edge factorization (4.32). REFS: p54 (Step 5, az, bz, bounds on fo, Lemma A.9, (5.22)); p50 ((5.13)); p44 (definition of ζ in the proof of Theorem 4.6).",
"obligation": "Later sections build wave amplitudes on the weight ζ; amplitudes carry √ζ in the class W_α. They must also absorb the higher-order stress by signed corrections. So that stress must vanish at the annulus edges as fast as ζ, up to finite inverse powers of δ. Without Step 5, T1 could reach the outer edge Xb at a rate not dominated by ζ.",
"backward_question": "At order one the leading exterior is not compactly supported and depends on z inside the terminal collar. Does axial viscosity acting on it leave stress at the outer edge, and does that stress vanish as fast as the weight ζ that controls the wave amplitudes?",
"mechanism": "At order one, inside the terminal collar, the leading swirl is the heat field times a terminal multiplier fo(log X). Since X = s/q depends on z, axial viscosity produces a source built from ∂y fo and ∂yy fo. These are flat at Xb at the rate e^{-4/δb^2}, the same exponent as the outer factor of ζ and as the outer rate (4.32) of T0. The backward representation of M5.9 integrates this source inward from the edge. Lemma A.9 (substitution u = δ/(1 + δ^2v)^{1/2}) gives ∫_0^δ e^{-c/u^2} u^{-j} b(u, η) du = (1/2) e^{-c/δ^2} δ^{3-j} B(δ, η), with B smooth and B(0, η) = b(0, η)/c. In words: integrating a flat factor from the edge gains δ^3. Derivatives cost only finite inverse powers of δb. Near the inner edge, T1 vanishes identically on [0, X-].",
"antecedent": "None cited. Internal: Lemma A.9, the terminal multiplier (A.12), the heat profile (4.29), and the edge factorization (4.32).",
"cost": "Unlike Tn for n ≥ 2, T1 reaches the outer edge Xb, with a finite inverse-power loss δ^{-N}. Later stages must accept stress weighted by ζ δ^{-N}.",
"checkable": "1. mpmath at 40 digits: for c = 4, j ∈ {3, 6} and b ≡ 1, compute I(δ) = ∫_0^δ e^{-4/u^2} u^{-j} du after the substitution w = u^{-2}, which removes the endpoint peak. Use δ = 0.3, 0.1, 0.05, 0.02. 2. Compare I(δ)/((1/2) e^{-4/δ^2} δ^{3-j}) with b(0)/c = 0.25; for j = 3 the ratio is exactly 1/c. I ran this while digesting: j = 3 gives 0.25, and j = 6 gives 0.2585, 0.2509, 0.2502, 0.25004. 3. Symbolically, verify the ∂zz(K fo) formula from the chain rule of Lemma 4.1 (X_z = -2ηX/(q^D L), Z_b of (4.2)), with K independent of z.",
"depends_on": [
"MA.13",
"M5.9",
"M4.15",
"MA.14"
],
"constrains": [],
"reasons": {
"MA.13": "Lemma A.9 with c = 4, j = 3, 6 factors e^{-4/δ_b²} out of the backward integral of the order-one source, gaining δ_b³ in (5.22).",
"M5.9": "integrates the order-one residual inward from the edge with the backward stress form that the zeroed moments make valid.",
"M4.15": "the target weight ζ = exp(-c_a/y_a² - 4/y_b²) is defined in Step 4 of the proof of Theorem 4.6.",
"MA.14": "on the terminal collar u_θ,0 = K f_o with f_o' flat at the rate e^{-4/δ²}δ^{-3}, the same exponent as the outer factor of ζ."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62"
},
{
"id": "M5.11",
"kind": "move",
"name": "ns-m5-11-finite-truncations-the-residual-gain-grows-with-n-the",
"title": "Finite truncations: the residual gain grows with N, the derivative loss does not",
"section": "5",
"pages": "45-62",
"refs": [
"p54 (plan of subsection 5.3)",
"p55 ((5.23), (5.24), Proposition 5.3, (5.25), proof Step 1, (5.26))",
"p56 (chain rule, r^{-1} factor)."
],
"statement": "Proposition 5.3. Define: - U^[N] = Σ_{n=0}^N (un, pn, q^{-A-1/2+λn} Tn), where the profiles include their cutoffs and moment corrections; - (5.24): Fslow(u, p, T) = R(u, p) + (∂r + 2/r)Tθ eθ + (∂r + 1/r)Tz ez; - (5.23): |V|_m = max_{|α|+b≤m} |∂x^α ∂t^b V|. Then each u^[N]_slow is divergence-free, and (5.25) holds: |Fslow(U^[N])|_m ≤ C_{N,m} q^{2h(N+1)-Km} on 0 ≤ X ≤ Xmax, -1 ≤ η ≤ 1, 0 < q ≤ 1, with Km independent of N.",
"description": "Proposition 5.3. Define: - U^[N] = Σ_{n=0}^N (un, pn, q^{-A-1/2+λn} Tn), where the profiles include their cutoffs and moment corrections; - (5.24): Fslow(u, p, T) = R(u, p) + (∂r + 2/r)Tθ eθ + (∂r + 1/r)Tz ez; - (5.23): |V|_m = max_{|α|+b≤m} |∂x^α ∂t^b V|. Then each u^[N]_slow is divergence-free, and (5.25) holds: |Fslow(U^[N])|_m ≤ C_{N,m} q^{2h(N+1)-Km} on 0 ≤ X ≤ Xmax, -1 ≤ η ≤ 1, 0 < q ≤ 1, with Km independent of N. OBLIGATION: Supplies the finite-residual hypothesis (5.33) of Lemma 5.4, with ρN = 2h(N+1) and no flat remainder. The gain must grow with N while the loss from physical differentiation stays fixed. MECHANISM: At every retained order: - (5.2) gives exact incompressibility; - (5.5) holds globally, so the radial residual is canceled; - differentiating the primitives gives (∂R + 2/R)Tn,θ = -rθ,n and (∂R + 1/R)Tn,z = -rz,n, so the tangential residual is exactly minus the stress divergence; - order zero holds by Proposition 4.2. ANTECEDENT: None cited. Internal: Lemma 4.1 and Proposition 4.2. REFS: p54 (plan of subsection 5.3); p55 ((5.23), (5.24), Proposition 5.3, (5.25), proof Step 1, (5.26)); p56 (chain rule, r^{-1} factor).",
"obligation": "Supplies the finite-residual hypothesis (5.33) of Lemma 5.4, with ρN = 2h(N+1) and no flat remainder. The gain must grow with N while the loss from physical differentiation stays fixed.",
"backward_question": "If I stop at order N, does the residual gain grow with N while each physical derivative costs a power of q that does not depend on N?",
"mechanism": "At every retained order: - (5.2) gives exact incompressibility; - (5.5) holds globally, so the radial residual is canceled; - differentiating the primitives gives (∂R + 2/R)Tn,θ = -rθ,n and (∂R + 1/R)Tn,z = -rz,n, so the tangential residual is exactly minus the stress divergence; - order zero holds by Proposition 4.2. After truncation, every uncancelled product or shifted viscous term carries relative power at least q^{2h(N+1)}. For N = 1, for example, products of two order-one coefficients and axial viscosity on order one first enter at order two. In the similarity chart, each transverse derivative costs q^{-1/2}, each axial derivative q^{-D}, and each time derivative q^{-1}, whatever the base power b. The powers of n produced by differentiating q^{λn} enter only the constants, through (1 + |b|)^m. On the stress support X ≥ Xa > 0, r^{-1} = q^{-1/2}(2X)^{-1/2}; near the axis the smooth Cartesian representatives are used.",
"antecedent": "None cited. Internal: Lemma 4.1 and Proposition 4.2.",
"cost": "Bounds hold only on fixed compact profile ranges and for q ≤ 1. C_{N,m} depends on N and on Xmax. The losses Km must be carried into the summation.",
"checkable": "A slope test of (5.26). 1. Take g(x⊥, η) = e^{-|x⊥|^2}(1 + η^2)^{-1}, b = -A + 2nh for several n, and h = 0.005. 2. Compute mixed derivatives of q^b g in Cartesian (x1, x2, z, t) by high-order finite differences in mpmath. Obtain q(z, t) by root finding on q - z^2q^{2h} = 1 - t. 3. Work at points of fixed (X, η) = (1, 0.3), for q from 1e-2 to 1e-8. 4. Fit the log-log slope and compare with b - a/2 - Dk - l. The full (5.25) needs the actual profiles. Appendices A to C construct them analytically, not in closed form.",
"depends_on": [
"M5.7",
"M5.6",
"M4.1",
"M4.4"
],
"constrains": [],
"reasons": {
"M5.7": "the extended profiles satisfy (5.2) and (5.5) globally, so each truncation is divergence-free and cancels the radial residual.",
"M5.6": "differentiating the primitives (5.9) makes each order's tangential residual exactly minus the stress divergence.",
"M4.1": "the loss K_m comes from (5.26): each physical derivative costs a fixed power of q via Lemma 4.1's chain rule, at every order.",
"M4.4": "order zero enters through Proposition 4.2, whose tangential residual is exactly minus the divergence of the leading stress."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62"
},
{
"id": "M5.12",
"kind": "move",
"name": "ns-m5-12-stokes-streamfunction-potentials-so-that-cutoffs-in-q",
"title": "Stokes streamfunction potentials, so that cutoffs in q keep div u = 0",
"section": "5",
"pages": "45-62",
"refs": [
"p56 (plan of subsection 5.4, potential formulas, (5.27), Cartesian form, summation tuple)."
],
"statement": "(5.27): - Fn = X AX(Un), Sn = q^{1-A+λn} Fn, and An = (Sn/r) eθ; - uz,n = ∂s Sn and r ur,n = -∂z Sn (s = r^2/2), so curl An = ur,n er + uz,n ez. In Cartesian form, An = (Sn/r^2)(-x2, x1, 0) = (1/2) q^{-A+λn} (Fn/X)(-x2, x1, 0). This is smooth across the axis for q > 0, because Fn/X is smooth at X = 0. The summation tuple is An = An, Bn = uθ,n eθ, pn = q^{-2A+λn} Πn, Tn = q^{-A-1/2+λn} Tn, with decay orders gn = 2nh and differential polynomial Fslow.",
"description": "(5.27): - Fn = X AX(Un), Sn = q^{1-A+λn} Fn, and An = (Sn/r) eθ; - uz,n = ∂s Sn and r ur,n = -∂z Sn (s = r^2/2), so curl An = ur,n er + uz,n ez. In Cartesian form, An = (Sn/r^2)(-x2, x1, 0) = (1/2) q^{-A+λn} (Fn/X)(-x2, x1, 0). This is smooth across the axis for q > 0, because Fn/X is smooth at X = 0. The summation tuple is An = An, Bn = uθ,n eθ, pn = q^{-2A+λn} Πn, Tn = q^{-A-1/2+λn} Tn, with decay orders gn = 2nh and differential polynomial Fslow. OBLIGATION: The summation cutoffs χ(cn q) depend on (z, t) through q. Multiplying the velocity coefficients by them would break div u = 0. Cutting the potential before taking the curl keeps exact incompressibility. The swirl Bn stays divergence-free under multiplication by any function of (z, t), because it is independent of θ. MECHANISM: Axisymmetric divergence-free (ur, uz) fields are curls of azimuthal potentials (S/r)eθ, with S the Stokes streamfunction. Given uz,n = ∂s Sn, the relation -∂zSn = q^{λn}Vn is exactly (5.2), using A + D = 1 and the operator Z of. ANTECEDENT: None cited; the Stokes streamfunction is named without citation. REFS: p56 (plan of subsection 5.4, potential formulas, (5.27), Cartesian form, summation tuple).",
"obligation": "The summation cutoffs χ(cn q) depend on (z, t) through q. Multiplying the velocity coefficients by them would break div u = 0. Cutting the potential before taking the curl keeps exact incompressibility. The swirl Bn stays divergence-free under multiplication by any function of (z, t), because it is independent of θ.",
"backward_question": "How can each order be multiplied by a cutoff depending on q = q(z, t) without destroying exact incompressibility or smoothness at the axis?",
"mechanism": "Axisymmetric divergence-free (ur, uz) fields are curls of azimuthal potentials (S/r)eθ, with S the Stokes streamfunction. Given uz,n = ∂s Sn, the relation -∂zSn = q^{λn}Vn is exactly (5.2), using A + D = 1 and the operator Z of (4.2). Smoothness at the axis follows because S/r^2 is a smooth function of (r^2, z, t). The first moment mn,1 = 0 makes Fn, and hence Sn, compactly supported in X. The curl of a cut potential includes the term from differentiating the cutoff, so the result stays divergence-free.",
"antecedent": "None cited; the Stokes streamfunction is named without citation.",
"cost": "It needs Fn/X smooth at the axis and Fn compactly supported, both from Lemma 5.2. Cutting the potential produces an extra radial velocity term, displayed as (5.45).",
"checkable": "1. Take Un = (1 - X) e^{-X} g(η). Then ∫_0^∞ Un dX = 0 and Fn = X e^{-X} g(η). 2. Obtain q(z, t) by root finding. 3. By finite differences in z at fixed (r, t), check that -∂zSn = q^{λn}Vn with Vn from (5.2), and that ∂sSn = q^{-A+λn}Un. 4. Check that the Cartesian divergence of curl(χ(cq)An) vanishes to finite-difference accuracy.",
"depends_on": [
"M5.2",
"M5.8",
"M5.11"
],
"constrains": [],
"reasons": {
"M5.2": "u_z,n = ∂_s S_n and r u_r,n = -∂_z S_n reproduce the order-n incompressibility relation (5.2), using A + D = 1.",
"M5.8": "F_n/X is smooth at the axis and F_n vanishes past X+ because m_n,1 = 0, so each potential is smooth and compactly supported.",
"M5.11": "the summation tuple carries the differential polynomial F_slow of (5.24) and the stresses of the truncations."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62"
},
{
"id": "M5.13",
"kind": "move",
"name": "ns-m5-13-lemma-5-4-an-abstract-borel-type-summation-with-shrinking",
"title": "Lemma 5.4, an abstract Borel-type summation with shrinking cutoffs",
"section": "5",
"pages": "45-62",
"refs": [
"p56 (summation plan, Λlog)",
"p57 ((5.28) to (5.33), Lemma 5.4 statement, (5.34))",
"p58 ((5.35), (5.36), Steps 1 and 2, (5.37))",
"p59 (Step 3, (5.38), (5.39), choice of J, initial block, residual comparison formula, (5.40), recovery of the expansion)."
],
"statement": "Hypotheses: - a domain with 0 < q < q0 ≤ 1 and (5.28): |∂z^a ∂t^b q| ≤ C_{a,b} q^{1-aD-b}, with 0 < D < 1; - a base U0 = (u0, p0, T0) with div u0 = 0 and |U0|_m ≤ C_m q^{-Km} Λlog(q)^{Pm}, where Λlog = 1 + |log q|; - increments (5.29): Zj = (Aj, Bj, pj, Tj) with Bj = bj(r, z, t)eθ and Uj = (curl Aj + Bj, pj, Tj), having smooth Cartesian representatives and smooth zero extensions; - (5.30): |Zj|_m ≤ C_{j,m} q^{gj - ℓm} Λlog^{P_{j,m}}, with 0 < g1 ≤ g2 ≤ ... → ∞ and ℓm independent of j;",
"description": "Hypotheses: - a domain with 0 < q < q0 ≤ 1 and (5.28): |∂z^a ∂t^b q| ≤ C_{a,b} q^{1-aD-b}, with 0 < D < 1; - a base U0 = (u0, p0, T0) with div u0 = 0 and |U0|_m ≤ C_m q^{-Km} Λlog(q)^{Pm}, where Λlog = 1 + |log q|; - increments (5.29): Zj = (Aj, Bj, pj, Tj) with Bj = bj(r, z, t)eθ and Uj = (curl Aj + Bj, pj, Tj), having smooth Cartesian representatives and smooth zero extensions; - (5.30): |Zj|_m ≤ C_{j,m} q^{gj - ℓm} Λlog^{P_{j,m}}, with 0 < g1 ≤ g2 ≤ ... → ∞ and ℓm independent of j; OBLIGATION: The constants of (5.17) may grow too fast for (5.1) to converge. The lemma produces genuine smooth, exactly divergence-free fields with the same asymptotics and a flat residual, in a form that the wave and mean correction. ANTECEDENT: None cited. The diagonal cutoff construction is the one in the classical proof of Borel's lemma (a smooth function with a prescribed Taylor series); that attribution is mine. REFS: p56 (summation plan, Λlog); p57 ((5.28) to (5.33), Lemma 5.4 statement, (5.34)); p58 ((5.35), (5.36), Steps 1 and 2, (5.37)); p59 (Step 3, (5.38), (5.39), choice of J, initial block, residual comparison formula, (5.40), recovery of the expansion).",
"obligation": "The constants of (5.17) may grow too fast for (5.1) to converge. The lemma produces genuine smooth, exactly divergence-free fields with the same asymptotics and a flat residual, in a form that the wave and mean correction sequence can reuse (Proposition 9.9).",
"backward_question": "Given a formal expansion whose coefficient bounds may grow arbitrarily fast with the order, how do I build an actual smooth, exactly divergence-free field with the same asymptotics and a residual flat at the singular point? And how do I state it abstractly enough to reuse for the later correction cycle?",
"mechanism": "Three steps. 1. Scale invariance. On the support of χ^{(k)}(aq), 1/2 ≤ aq ≤ 1. So each factor a from the chain rule pairs with a factor q from (5.28), giving |∂z^{a'}∂t^{b'}χ(aq)| ≤ C q^{-a'D-b'} uniformly in a. Since q depends only on (z, t), curl(χ(aq)Aj) = χ(aq) curl Aj + aχ'(aq)∇q × Aj is controlled by the potential bounds, with a loss ℓ'm depending only on m and ℓ_{m+1}. 2. Diagonal choice (5.37). At step j, pick aj so large that Ĉ_{j,m} Λlog^{P̂_{j,m}} q^{gj/2} ≤ 2^{-j} on q ≤ aj^{-1}, for all m ≤ j. Half of the decay exponent pays for arbitrarily large constants. The tail beyond J is then at most 2^{-J} q^{g_{J+1}/2 - ℓ'm}. On {q ≥ δ}, only terms with aj ≤ δ^{-1} survive, which gives local finiteness. 3. Flatness. Fix (m, N), then a large J, and compare F(U) with F(U[J]) on q < 1/(2aJ), where the first J cutoffs equal one. - (5.38) bounds U[J] by q^{-Km}, with Km independent of J. - (5.39) bounds the difference by C_m q^{-Hm} |e|_{m+s}(1 + |U[J]|_{m+s} + |e|_{m+s})^{d-1}, with e = U - U[J] and Hm independent of J. - Choose J with g_{J+1}/2 - ℓ'_{m+s} ≥ N + Hm + (d - 1)(K_{m+s} + 1) and ρJ - K^F_m ≥ N + 1. Both pieces are then O(q^N).",
"antecedent": "None cited. The diagonal cutoff construction is the one in the classical proof of Borel's lemma (a smooth function with a prescribed Taylor series); that attribution is mine.",
"cost": "- The scales aj are not explicit; they are chosen after all constants. - The summed field equals the partial sums only on the shrinking neighborhoods q < 1/(2aJ). - The tail estimates use only half the decay exponent. - Every summand needs common supports, smooth Cartesian representatives, and smooth zero extensions, plus a common domain for all partial sums (later supplied by Lemma 9.7).",
"checkable": "Mostly a pure estimate. Two ingredients are computable: - (a) For a standard smooth step χ built from e^{-1/x}, confirm numerically that sup_{q>0} |(q∂q)^j χ(aq)| is the same for a = 1, 10, 1e4. It equals sup_σ |(σ∂σ)^j χ(σ)|. - (b) A toy summation: take gj = 2jh with h = 0.005 and constants Ĉ_{j,m} = ((j + m)!)^2. Choose aj from (5.37) by root finding, then verify the tail bound (5.35) on a grid in q.",
"depends_on": [
"M5.12",
"M4.1"
],
"constrains": [],
"reasons": {
"M5.12": "its increments are potentials A_j cut before the curl plus θ-independent swirl B_j e_θ, the device of (5.27) that keeps div u = 0.",
"M4.1": "the cutoffs χ(a_j q) use the concentration scale q of (4.1), whose derivative bounds (5.28) make them scale invariant."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62"
},
{
"id": "M5.14",
"kind": "move",
"name": "ns-m5-14-proposition-5-5-the-realized-base-field-and-what-it",
"title": "Proposition 5.5, the realized base field and what it guarantees",
"section": "5",
"pages": "45-62",
"refs": [
"p60 (subsection 5.5, Proposition 5.5, (5.41) to (5.44), Step 1, ℓm = 2A + m, cutoff scale invariance)",
"p61 (ρN, Step 2, (5.45), Step 3, (5.46), O(q^{3h}), the Step 4 split)",
"p62 (tail bound, endpoint extension)."
],
"statement": "There are smooth axisymmetric fields (uB, pB) for q > 0, and tangential stresses Tphys supported where Xa ≤ X ≤ Xb, such that: - div uB = 0; - (5.41): R(uB, pB) = -(∂r + 2/r)Tphys,θ eθ - (∂r + 1/r)Tphys,z ez + EB, with |∂^α EB| ≤ C_{α,M} q^M on each [0, Xmax] × [-1, 1]; - (5.42), on [Xlo, Xhi] × [-1, 1] (0 < Xlo < Xa < Xb < Xhi) and for compositions D^I of q∂q, ∂X, ∂η: q^A uθ,B - E0, q^A uz,B - U0 and q^{1/2} ur,B - V0/√(2X) are O_I(q^{2h}), and q^A ur,B = O_I(q^h);",
"description": "There are smooth axisymmetric fields (uB, pB) for q > 0, and tangential stresses Tphys supported where Xa ≤ X ≤ Xb, such that: - div uB = 0; - (5.41): R(uB, pB) = -(∂r + 2/r)Tphys,θ eθ - (∂r + 1/r)Tphys,z ez + EB, with |∂^α EB| ≤ C_{α,M} q^M on each [0, Xmax] × [-1, 1]; - (5.42), on [Xlo, Xhi] × [-1, 1] (0 < Xlo < Xa < Xb < Xhi) and for compositions D^I of q∂q, ∂X, ∂η: q^A uθ,B - E0, q^A uz,B - U0 and q^{1/2} ur,B - V0/√(2X) are O_I(q^{2h}), and q^A ur,B = O_I(q^h); OBLIGATION: Delivers the background every later section uses: - exact incompressibility; - residual equal to an annular stress divergence plus a flat error; - the untouched heat exterior; - the untouched mean patch; - normalized closeness to the leading field, used for the chart base velocity in Section 7 and for the growth asymptotic (3.6) at a fixed Xin ∈ (0, Xa); ANTECEDENT: None cited. Internal: Lemma 5.4, Proposition 5.3, Lemma 5.2, Theorem 4.6. REFS: p60 (subsection 5.5, Proposition 5.5, (5.41) to (5.44), Step 1, ℓm = 2A + m, cutoff scale invariance); p61 (ρN, Step 2, (5.45), Step 3, (5.46), O(q^{3h}), the Step 4 split); p62 (tail bound, endpoint extension).",
"obligation": "Delivers the background every later section uses: - exact incompressibility; - residual equal to an annular stress divergence plus a flat error; - the untouched heat exterior; - the untouched mean patch; - normalized closeness to the leading field, used for the chart base velocity in Section 7 and for the growth asymptotic (3.6) at a fixed Xin ∈ (0, Xa); - weighted closeness of the stress to T0, used to choose wave amplitudes (Propositions 7.5 and 7.6); - smooth limits at t = 1 away from the origin.",
"backward_question": "Does summation with shrinking cutoffs preserve exactly what later sections need, without changing any asymptotic coefficient? That means the heat exterior, the untouched mean patch, closeness to the leading field and to the stress with the ζ weight, and smooth limits at t = 1 away from the origin.",
"mechanism": "Apply Lemma 5.4 to the tuples of M5.12 on each compact profile range, keeping order zero uncut. By (5.26) and D < 1/2, the loss is ℓm = 2A + m, and (5.25) is (5.33) with ρN = 2h(N+1) and no remainder. Cutoffs are scale invariant in the normalized variables: (q∂q)^j χ(cn q) = (σ∂σ)^j χ(σ) at σ = cn q, bounded uniformly in n. Cutting the potential gives (5.45): r u^cut_{r,n} = q^{2nh}[χ(cn q)Vn - (2η/L)(cn q)χ'(cn q)Fn] and u^cut_{z,n} = q^{-A+2nh}χ(cn q)Un. This field is divergence-free identically, and (5.18) kills both bracket terms on Imean, which proves (5.44). Extra diagonal requirements of type (5.40) give (5.46): |D^I[χ(cn q) q^{2nh} an]| ≤ 2^{-n} q^{nh} for n ≥ max{2, |I|}. Here an is one of En, Un, Πn, Vn/√(2X), Fn/√(2X) on the enlarged rectangle, or a component of Tn/ζ for n ≥ 2. Summing gives (5.42); in the normalization q^A, the positive-order radial correction is even O(q^{3h}). Together with (5.22) for n = 1, summing also gives (5.43). The asymptotic coefficients are unchanged. Split at J = max{2N + 2, m + 1}. Keep the finitely many terms N < n < J with their original powers, which are at least q^{2h(N+1)}. Bound the tail by Σ_{n≥J} 2^{-n}q^{nh} ≤ 2^{1-J}q^{Jh} ≤ 2^{1-J}q^{2h(N+1)}. On compact sets with q bounded below, only finitely many terms survive, so their analytic η-neighborhoods intersect. Since L > 0, the one-sided extensions at η = ±1 transfer to physical variables; η = ±1 is the time t = 1 away from the origin (Section 3.1).",
"antecedent": "None cited. Internal: Lemma 5.4, Proposition 5.3, Lemma 5.2, Theorem 4.6.",
"cost": "- The higher-order stress T̂ - T0 is signed and bounded only by q^{2h}ζδ^{-N}. The δ^{-N} loss near the annulus edges rules out a uniform relative bound against |T0| ≥ cζ. So Section 7 keeps the fixed positive representation of T0 and treats the rest by signed corrections. - The diagonal bound gives q^{nh} rather than q^{2nh}; splitting at 2N + 2 compensates. - All estimates are uniform only on compact profile rectangles and for q > 0.",
"checkable": "- (a) Symbolic: derive (5.45) as -∂z[χ(cn q)Sn], using ∂zq = 2ηq^{1-D}/L (Lemma 4.1), Sn = q^{1-A+2nh}Fn and A + D = 1. Confirm the divergence of the cut field vanishes. - (b) Numeric: for h = 0.005, N ≤ 5, m ≤ 5 and a grid of q in (0, 1], confirm Σ_{n≥J} 2^{-n}q^{nh} ≤ 2^{1-J}q^{2h(N+1)} with J = max{2N + 2, m + 1}. - (c) The quantitative bounds (5.42) and (5.43) require the constructed profiles.",
"depends_on": [
"M5.13",
"M5.11",
"M5.10",
"M5.8"
],
"constrains": [],
"reasons": {
"M5.13": "Lemma 5.4 applied to the order-n tuples gives smooth, exactly divergence-free fields with a flat residual E_B and unchanged asymptotics.",
"M5.11": "Proposition 5.3's truncation bound (5.25) supplies the hypothesis (5.33) with ρ_N = 2h(N + 1) and an N-independent loss.",
"M5.10": "the ζδ^{-N} bounds (5.13), (5.22) on T_n give the weighted closeness (5.43) of the summed stress to T0.",
"M5.8": "positive orders vanish past X+ and, by (5.18), on I_mean, so the heat exterior and the mean patch (5.44) are untouched."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 45-62"
},
{
"id": "M6.1",
"kind": "move",
"name": "ns-m6-1-dyadic-charts-and-normalized-units",
"title": "Dyadic charts and normalized units",
"section": "6",
"pages": "62",
"refs": [
"p. 62, (6.1)",
"p. 63 (the normalizations, and the time and viscous factors after (6.6))",
"p. 17 (normalized operators)."
],
"statement": "On a dyadic band where q ≍ Q, set Q = 2^(−ℓ), ε = Q^h, S* = ℓ^2, R = r/√Q, Z = z/Q^D, T = τ/Q, τ = 1 − t (6.1). A physical velocity, pressure, and residual get chart representatives by multiplying by Q^A, Q^(2A), and Q^(2A+1/2). The normalized time derivative therefore carries the factor Q^(2A+1/2) Q^(−A) = Q^(1+h), and the viscous term carries Q^(2A+1/2) Q^(−A) Q^(−1) = ε (p. 63). The chart radius and the profile radius are related by R_chart = √(q/Q) R_profile.",
"description": "On a dyadic band where q ≍ Q, set Q = 2^(−ℓ), ε = Q^h, S* = ℓ^2, R = r/√Q, Z = z/Q^D, T = τ/Q, τ = 1 − t (6.1). A physical velocity, pressure, and residual get chart representatives by multiplying by Q^A, Q^(2A), and Q^(2A+1/2). The normalized time derivative therefore carries the factor Q^(2A+1/2) Q^(−A) = Q^(1+h), and the viscous term carries Q^(2A+1/2) Q^(−A) Q^(−1) = ε (p. 63). The chart radius and the profile radius are related by R_chart = √(q/Q) R_profile. OBLIGATION: It makes the active annulus Xa < X < Xb a bounded set in every band, so estimates can be uniform over infinitely many scales. It identifies ε as the parameter in which all later residual orders are measured (the classes of M6.11 and the stage exponents σj of Section 9). And it separates harmless losses (powers of S* ≍ log^2(1/q)) from the gains that matter (powers of ε). MECHANISM: In the annulus r ≍ √q, z ≍ q^D, and τ ≍ q. Rescaling by the frozen band scale Q, not by the variable q, gives chart variables of order one, while Q, ε, and S* stay constant inside a. ANTECEDENT: None cited. REFS: p. 62, (6.1); p. 63 (the normalizations, and the time and viscous factors after (6.6)); p. 17 (normalized operators).",
"obligation": "It makes the active annulus Xa < X < Xb a bounded set in every band, so estimates can be uniform over infinitely many scales. It identifies ε as the parameter in which all later residual orders are measured (the classes of M6.11 and the stage exponents σj of Section 9). And it separates harmless losses (powers of S* ≍ log^2(1/q)) from the gains that matter (powers of ε).",
"backward_question": "In what frozen units does the collapsing annulus look the same at every scale, and which single parameter measures how far each term sits below the leading balance?",
"mechanism": "In the annulus r ≍ √q, z ≍ q^D, and τ ≍ q. Rescaling by the frozen band scale Q, not by the variable q, gives chart variables of order one, while Q, ε, and S* stay constant inside a chart (\"held fixed in derivatives\"). The residual normalization Q^(2A+1/2) is the one that makes the transport term (u·∇)u of normalized size one. The slow time derivative then becomes −ε∂T and viscosity becomes ε times the normalized Laplacian, so both sit one power of ε below transport. The logarithmic parameter S* = ℓ^2 has two properties. Any fixed power of S* is beaten by any positive power of ε as ℓ → ∞, so polynomial losses in S* can always be absorbed. And exp(−c S*) = exp(−c ℓ^2) is smaller than every power of Q, which is what later makes pulse tails flat.",
"antecedent": "None cited.",
"cost": "Every later estimate must be uniform over bands ℓ ≥ ℓ0, labels, and rectangle copies, with constants that depend only on fixed data, the derivative order, and the stage. Neighboring bands overlap (q/Q ∈ [1/2, 2]), which creates the multi-band bookkeeping of M6.8. And qbig must be small.",
"checkable": "Exact arithmetic on the exponents with A = 1/2 + h and D = 1/2 − h. Check that (2A + 1/2) − A = 1 + h; that (2A + 1/2) − A − 1 = h; that √Q ∂z = Q^(1/2−D) ∂Z = ε∂Z; and that the leading stress-divergence scale q^(−3/2−h) (Section 3.3), multiplied by Q^(2A+1/2), is of order ε. All four were verified here for h = 1/200 and h = 1/101. Numerically, also confirm that ℓ^(2b) 2^(−ηhℓ) → 0 and exp(−cℓ^2) 2^(Nℓ) → 0 for sample b, η, c, N > 0.",
"depends_on": [
"M4.1",
"M4.2",
"M4.8",
"M5.14"
],
"constrains": [],
"reasons": {
"M4.1": "The chart variables R = r/√Q, Z = z/Q^D, T = τ/Q rescale by the concentration scale q and its anisotropic lengths q^{1/2}, q^D from the similarity coordinates.",
"M4.2": "The factors Q^A for velocity and Q^{2A} for pressure match the leading field's growth u ~ q^{-A}E and p ~ q^{-2A}Π.",
"M4.8": "Takes the fixed exponent h, so ε = Q^h, and the fixed annulus Xa < X < Xb of Theorem 4.6, which the charts turn into a bounded set in every band.",
"M5.14": "The charted fields are those of the realized background, whose stress-divergence scale q^{-3/2-h} becomes order ε after the Q^{2A+1/2} normalization."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 62"
},
{
"id": "M6.2",
"kind": "move",
"name": "ns-m6-2-integer-covering-matrix-and-the-physical-phase-map",
"title": "Integer covering matrix and the physical phase map",
"section": "6",
"pages": "62",
"refs": [
"p. 62 (motivation)",
"p. 63, (6.2), (6.3), (6.4)",
"p. 64 (commutation, support away from the axis, no spatial periodicity)."
],
"statement": "Fix Jg = [[3, 1], [1, 5]], Λg = 4 − √2, Tg = 4 + √2, bg = √2 − 1, vr = (1, −bg), vt = (bg, 1), ρg = log Λg / log Tg, κs = 10^(−5), and dr = 2((1 + h)ρg − hκs) > 0 (6.2). These satisfy Jg vr = Λg vr, Jg vt = Tg vt, and 1 < Λg < Tg. Physical fields are evaluations of extended fields F(r, θ, z, t, Y), with Y ∈ T^2, on the map Y = vr r^(dr) + vt t (mod Z^2) (6.3).",
"description": "Fix Jg = [[3, 1], [1, 5]], Λg = 4 − √2, Tg = 4 + √2, bg = √2 − 1, vr = (1, −bg), vt = (bg, 1), ρg = log Λg / log Tg, κs = 10^(−5), and dr = 2((1 + h)ρg − hκs) > 0 (6.2). These satisfy Jg vr = Λg vr, Jg vt = Tg vt, and 1 < Λg < Tg. Physical fields are evaluations of extended fields F(r, θ, z, t, Y), with Y ∈ T^2, on the map Y = vr r^(dr) + vt t (mod Z^2) (6.3). OBLIGATION: It meets the section's stated requirement (p. 62): localize the waves, separate their supports, and \"permit rapid temporal variation without introducing radial derivatives large enough to spoil the residual estimates.\" Localizing waves in time becomes localizing them in an independent periodic variable. MECHANISM: Because Y is an independent variable, the construction is a two-scale ansatz made exact. Identities for extended fields are written with 𝔯 and 𝔱 in place of ∂r and ∂t, and restricting to Y(r, t) turns them into physical identities with no remainder; covariances and averages are taken on the extended domain before evaluation. ANTECEDENT: None cited. REFS: p. 62 (motivation); p. 63, (6.2), (6.3), (6.4); p. 64 (commutation, support away from the axis, no spatial periodicity).",
"obligation": "It meets the section's stated requirement (p. 62): localize the waves, separate their supports, and \"permit rapid temporal variation without introducing radial derivatives large enough to spoil the residual estimates.\" Localizing waves in time becomes localizing them in an independent periodic variable.",
"backward_question": "Can I attach to space-time a periodic fast variable that runs quickly in time, runs only barely faster than the slow scale in radius, is one fixed map for every scale, and turns the product of two fields with disjoint fast supports into an exact zero?",
"mechanism": "Because Y is an independent variable, the construction is a two-scale ansatz made exact. Identities for extended fields are written with 𝔯 and 𝔱 in place of ∂r and ∂t, and restricting to Y(r, t) turns them into physical identities with no remainder; covariances and averages are taken on the extended domain before evaluation. The map moves along vt in time and along vr in radius, and these are the two eigen-directions of Jg. So the integer coverings Y ↦ Jg^i Y, which preserve periodicity, multiply the time rate by Tg^i and the radial rate by Λg^i = (Tg^i)^(ρg), a strictly smaller power (ρg ≈ 0.5625). A circle carries only one direction; two eigen-directions of one integer matrix let the band coverings scale time and radius at different, prescribed rates. The only variable coefficient, dr r^(dr−1), depends on r alone and multiplies a constant torus direction, so all the evaluated derivatives commute, and identities such as the exact divergence-freeness of curls survive on the extended domain. The power r^(dr) is what lets one band-independent map serve every band: in the annulus r^2 ≍ q ≍ Q, so r^(dr) contributes a factor Q^(dr/2), which cancels the band dependence of Λg^(i(ℓ)) (M6.3). Periodicity in Y imposes no spatial periodicity after restriction.",
"antecedent": "None cited.",
"cost": "r^(dr) is not smooth at r = 0, so every correction that depends on Y must be supported away from the axis, in the active shell (p. 64). Each fast radial derivative costs up to a factor ε^(−κs) (times powers of S*), so κs appears in essentially every later exponent (for example 1/2 − κs and 1 − 3κs in Sections 7 to 9). It adds the fixed constants Jg, κs, and dr, and fields now live on an extended domain.",
"checkable": "Linear algebra: Jg vr = Λg vr, Jg vt = Tg vt, vr·vt = 0, det Jg = 14. Numerically Λg = 2.5857864, Tg = 5.4142136, and ρg = 0.5624714, and dr ranges over (1.12494, 1.13618) for 0 < h < 1/100 (all computed here). Symbolically, for a trigonometric polynomial F(r, t, Y), check that d/dr[F(r, t, Y(r, t))] = (𝔯F)(r, t, Y(r, t)), that d/dt[F(r, t, Y(r, t))] = (𝔱F)(r, t, Y(r, t)), and that the commutator of 𝔯 and 𝔱 vanishes.",
"depends_on": [
"M6.1"
],
"constrains": [],
"reasons": {
"M6.1": "The radial phase exponent d_r = 2((1+h)ρ_g − hκ_s) is built from the chart time exponent 1+h and ε = Q^h, so band coverings produce prescribed chart rates."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 62"
},
{
"id": "M6.3",
"kind": "move",
"name": "ns-m6-3-band-covering-index-and-the-two-derivative-scales",
"title": "Band covering index and the two derivative scales",
"section": "6",
"pages": "63",
"refs": [
"p. 63, (6.5), (6.6)",
"p. 64 (the comparison inequalities)",
"used at p. 91 to 92 (Lemma 8.2, M^(−1) ≤ C ε^(κs) S*^(ρg)) and p. 96 ((8.20))."
],
"statement": "Band ℓ uses the representative Yi = Jg^i Y (mod Z^2), with i = i(ℓ) = ⌊log_Tg(Q^(−1−h)/S*)⌋ (6.5). Only large ℓ, with i(ℓ) ≥ 0, are used. A function descends to the band torus if it is invariant under every deck translation Y ↦ Y + a with Jg^i a ∈ Z^2. With Ni = vt·∂Yi and Li = vr·∂Yi, one has Nabs = Tg^i Ni and Labs = Λg^i Li. The chart operators are (6.6): t* = Q^(1+h) 𝔱 = −ε∂T + ci Ni, with ci = Tg^i Q^(1+h) ≍ S*^(−1);",
"description": "Band ℓ uses the representative Yi = Jg^i Y (mod Z^2), with i = i(ℓ) = ⌊log_Tg(Q^(−1−h)/S*)⌋ (6.5). Only large ℓ, with i(ℓ) ≥ 0, are used. A function descends to the band torus if it is invariant under every deck translation Y ↦ Y + a with Jg^i a ∈ Z^2. With Ni = vt·∂Yi and Li = vr·∂Yi, one has Nabs = Tg^i Ni and Labs = Λg^i Li. The chart operators are (6.6): t* = Q^(1+h) 𝔱 = −ε∂T + ci Ni, with ci = Tg^i Q^(1+h) ≍ S*^(−1); OBLIGATION: It makes the fast clock run at the right speed in every band. The rectangles have a fixed torus size r0, so a pulse lasts Ls = 2r0/ci ≍ S* normalized time units, which is long enough for the Gaussian envelope of Section 7 ((7.16)) to be exp(−cS*)-small at both ends. It keeps the fast radial derivative at the size ε^(−κs) S*^(−ρg). And it supplies the radial winding that Lemma 8.2 uses: there M^(−1) ≤ C ε^(κs) S*^(ρg) (p. 92). MECHANISM: In time, t* on the band torus has a slow part −ε∂T (one power of ε) and a fast part ci Ni with ci ≍ 1/S*; ANTECEDENT: None cited. REFS: p. 63, (6.5), (6.6); p. 64 (the comparison inequalities); used at p. 91 to 92 (Lemma 8.2, M^(−1) ≤ C ε^(κs) S*^(ρg)) and p. 96 ((8.20)).",
"obligation": "It makes the fast clock run at the right speed in every band. The rectangles have a fixed torus size r0, so a pulse lasts Ls = 2r0/ci ≍ S* normalized time units, which is long enough for the Gaussian envelope of Section 7 ((7.16)) to be exp(−cS*)-small at both ends. It keeps the fast radial derivative at the size ε^(−κs) S*^(−ρg). And it supplies the radial winding that Lemma 8.2 uses: there M^(−1) ≤ C ε^(κs) S*^(ρg) (p. 92).",
"backward_question": "Given one fixed phase map, how do I make its time winding match a pulse lifetime of about S* shear times in every band, and how small can I keep the radial winding while still getting unlimited averaging out of it?",
"mechanism": "In time, t* on the band torus has a slow part −ε∂T (one power of ε) and a fast part ci Ni with ci ≍ 1/S*; the floor in (6.5) pins Tg^i within a factor Tg of Q^(−1−h)/S*. In radius, Λg^i = (Tg^i)^(ρg) ≍ (Q^(−1−h)/S*)^(ρg). Multiplying by Q^(dr/2) = Q^((1+h)ρg − hκs) leaves exactly ε^(−κs) S*^(−ρg), up to a factor between Tg^(−ρg) and 1. The −hκs inside dr is deliberate. It costs a factor ε^(κs) per radial derivative, and it gains ε^(κs) per integration by parts along vr, which can be repeated. So Lemma 8.2 can make the zero-Haar-mean part of a full radial integral O(ε^(pκs)) for any p, that is, flat. Without that term, Mi ≍ S*^(−ρg) → 0 and integrating by parts along vr would lose instead of gain.",
"antecedent": "None cited.",
"cost": "It adds the covering index i(ℓ) and the deck-translation descent conditions. Different bands live on different tori, which M6.8 resolves. It introduces polynomial factors S*^(±1) and S*^(−ρg); the fast-time inverse costs ci^(−1) ≤ C S* ((8.20), p. 96); and a radial derivative loses ε^(κs) ((6.32)). A computation done here, not stated in the paper: Mi ≤ ε^(−κs) S*^(−ρg) can exceed 1 only when ε^(−κs) > S*^(ρg), which for h near 1/100 happens only beyond ℓ ≈ 3.2 × 10^8 (ℓ ≈ 6.6 × 10^8 at h = 0.005). The gains from radial winding are therefore purely asymptotic in q.",
"checkable": "For h ∈ {0.001, 0.005, 0.0099} and ℓ from 20 to 10^6, compute i(ℓ) in log arithmetic and check that i ≥ 0, ci·S* ∈ (1/Tg, 1], and Mi·ε^(κs)·S*^(ρg) ∈ (Tg^(−ρg), 1]. This was run here for ℓ in [20, 3000) and for ℓ = 10^4, 10^5, 10^6 with no violations. The same run gives the thresholds for Mi > 1 quoted above.",
"depends_on": [
"M6.2",
"M6.1"
],
"constrains": [],
"reasons": {
"M6.2": "Uses the integer matrix J_g, its eigen-directions v_r, v_t with rates T_g > Λ_g, the phase map, and its chain-rule operators to define band coverings.",
"M6.1": "Chooses i(ℓ) from the chart factor Q^{1+h} and S* so that c_i ≍ S*^{-1} and M_i ≍ ε^{-κ_s}S*^{-ρ_g} in normalized units."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 63"
},
{
"id": "M6.4",
"kind": "move",
"name": "ns-m6-4-diophantine-bound-for-the-two-torus-directions",
"title": "Diophantine bound for the two torus directions",
"section": "6",
"pages": "64",
"refs": [
"p. 64, (6.7)",
"used at p. 91 ((8.10)) and p. 95 to 96 ((8.19), Lemma 8.6)."
],
"statement": "For n ∈ Z^2 \\ {0}, |vr·n| ≥ c/(1 + |n|) and |vt·n| ≥ c/(1 + |n|) (6.7). Proof: vr·n = (n1 + n2) − √2 n2, and multiplying it by its algebraic conjugate gives the nonzero integer (n1 + n2)^2 − 2 n2^2, while the conjugate has absolute value at most C|n|. The same argument works for vt·n = (n2 − n1) + √2 n1.",
"description": "For n ∈ Z^2 \\ {0}, |vr·n| ≥ c/(1 + |n|) and |vt·n| ≥ c/(1 + |n|) (6.7). Proof: vr·n = (n1 + n2) − √2 n2, and multiplying it by its algebraic conjugate gives the nonzero integer (n1 + n2)^2 − 2 n2^2, while the conjugate has absolute value at most C|n|. The same argument works for vt·n = (n2 − n1) + √2 n1. OBLIGATION: The inverse directional operators on zero-mean torus functions lose only a finite number of torus derivatives (p. 64). Later sections need this for the fast-time inverse (8.19) in Lemma 8.6, which loses four derivatives and removes the zero-auxiliary-mean part of the angular-mean residual, and for the cutoff-remainder estimate (8.10) in Lemma 8.2, which loses p + 3 derivatives. MECHANISM: Jg is an integer matrix with irrational eigenvalues, so the slopes of its eigenvectors are quadratic irrationals built from √2. For a quadratic irrational, a small linear form times its Galois conjugate is a nonzero integer, so the linear form is at least one over the. ANTECEDENT: None cited in the section. The inline argument is the classical Liouville-type bound for the quadratic irrational √2. REFS: p. 64, (6.7); used at p. 91 ((8.10)) and p. 95 to 96 ((8.19), Lemma 8.6).",
"obligation": "The inverse directional operators on zero-mean torus functions lose only a finite number of torus derivatives (p. 64). Later sections need this for the fast-time inverse (8.19) in Lemma 8.6, which loses four derivatives and removes the zero-auxiliary-mean part of the angular-mean residual, and for the cutoff-remainder estimate (8.10) in Lemma 8.2, which loses p + 3 derivatives.",
"backward_question": "If I must divide by v·k at every nonzero torus frequency, can I choose the directions so that small divisors cost only a fixed number of derivatives?",
"mechanism": "Jg is an integer matrix with irrational eigenvalues, so the slopes of its eigenvectors are quadratic irrationals built from √2. For a quadratic irrational, a small linear form times its Galois conjugate is a nonzero integer, so the linear form is at least one over the conjugate's size. The Fourier multipliers (2πi v·k)^(−p) are then bounded by C(1 + |k|)^p, and a few extra derivatives make the Fourier series converge absolutely in two dimensions.",
"antecedent": "None cited in the section. The inline argument is the classical Liouville-type bound for the quadratic irrational √2.",
"cost": "Each inversion loses a finite number of torus derivatives, so estimates must hold at every derivative order in the torus variables. The paper notes (p. 92) that a fixed finite regularity would yield only a finite flatness order, because frequencies comparable to M can be nearly resonant with vr.",
"checkable": "Compute the infimum of (1 + |n|)|vr·n| and of (1 + |n|)|vt·n| over 0 < |n|∞ ≤ N. For N = 400 both are about 0.3848, attained near Pell-type vectors such as (−70, −169) and (−169, 70) (run here), and the value is stable as N grows. Also check in exact integer arithmetic that (n1 + n2)^2 − 2 n2^2 ≠ 0 for n ≠ 0.",
"depends_on": [
"M6.2"
],
"constrains": [],
"reasons": {
"M6.2": "The bound concerns the fixed directions v_r = (1, −b_g) and v_t = (b_g, 1) with b_g = √2 − 1, whose quadratic-irrational slopes allow the conjugate argument."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 64"
},
{
"id": "M6.5",
"kind": "move",
"name": "ns-m6-5-squared-partitions-of-unity-slow-boxes-and-labels",
"title": "Squared partitions of unity, slow boxes, and labels",
"section": "6",
"pages": "64",
"refs": [
"p. 64 (the partitions, Cℓ, Aℓ, (6.8))",
"p. 65 ((6.9), the partition identity, the compactness of supports)",
"used at p. 74 and p. 84 ((7.30))."
],
"statement": "The dyadic squared partition is Σℓ χℓ(q)^2 = 1, with χℓ supported where q/Q ∈ [1/2, 2]. Inside each band there is a product squared partition Σa χℓ,a(R, Z, T)^2 = 1 with mesh S*^(−3) in each coordinate and supports extending at most one mesh length on either side of a grid point, built by normalizing translates of a smooth bump by the square root of their squared sum. The active part Aℓ is defined by 0 < q < qbig, 1/2 ≤ q/Q ≤ 2, τ ≥ 0, and Xa ≤ r^2/(2q) ≤ Xb, with qbig ≤ 2^(−ℓ0).",
"description": "The dyadic squared partition is Σℓ χℓ(q)^2 = 1, with χℓ supported where q/Q ∈ [1/2, 2]. Inside each band there is a product squared partition Σa χℓ,a(R, Z, T)^2 = 1 with mesh S*^(−3) in each coordinate and supports extending at most one mesh length on either side of a grid point, built by normalizing translates of a smooth bump by the square root of their squared sum. The active part Aℓ is defined by 0 < q < qbig, 1/2 ≤ q/Q ≤ 2, τ ≥ 0, and Xa ≤ r^2/(2q) ≤ Xb, with qbig ≤ 2^(−ℓ0). OBLIGATION: It localizes each wave to a region where the background shear varies little: Section 7 freezes the frame and growth parameters at x0ℓ,a, and every point of a box is within C S*^(−3) of its representative (p. 74). The squared partition lets quadratic covariances of locally built waves sum exactly to the target stress: (7.30) uses Σβ ηβ^2 = 1. The two signs give each box two wave families, which a two-component stress needs (T = c1 v1 + c2 v2). ANTECEDENT: None cited. REFS: p. 64 (the partitions, Cℓ, Aℓ, (6.8)); p. 65 ((6.9), the partition identity, the compactness of supports); used at p. 74 and p. 84 ((7.30)).",
"obligation": "It localizes each wave to a region where the background shear varies little: Section 7 freezes the frame and growth parameters at x0ℓ,a, and every point of a box is within C S*^(−3) of its representative (p. 74). The squared partition lets quadratic covariances of locally built waves sum exactly to the target stress: (7.30) uses Σβ ηβ^2 = 1. The two signs give each box two wave families, which a two-component stress needs (T = c1 v1 + c2 v2).",
"backward_question": "How do I cut the annulus into pieces small enough that the shear is effectively constant on each, yet recover the prescribed stress exactly when the quadratic fluxes of the pieces are added?",
"mechanism": "If the waves ηβ Wβ of different boxes never multiply each other (M6.7), their quadratic fluxes add as Σβ ηβ^2 C(Wβ). If each box's waves have covariance equal to the target, a squared partition returns the target exactly. The mesh S*^(−3) is small enough to make frozen-coefficient errors small in inverse powers of S*, and differentiating the cutoffs costs only powers of S*, which are harmless logarithmic losses. On the supports, R lies in a fixed compact subinterval of (0, ∞) and Z, T lie in bounded intervals.",
"antecedent": "None cited.",
"cost": "The number of boxes grows polynomially in S* (Lemma 6.3), and cutoff derivatives grow like powers of S*. Representatives, labels, and all other discrete choices are fixed before any differentiation. It needs a large lower band index ℓ0 and qbig ≤ 2^(−ℓ0), and supports are taken in the coordinate domain including its smooth extension near τ = 0.",
"checkable": "Build the one-dimensional squared partition χa = φa / √(Σb φb^2) from translates φa of a bump on a grid with mesh S^(−3). Check that Σ χa^2 = 1 to machine precision, that supports stay within one mesh length of their grid points, and that sup|∂^k χa| scales like S^(3k). Tensorize to (R, Z, T) and repeat, and do the same construction in log2 q for the dyadic partition.",
"depends_on": [
"M6.1",
"M4.8"
],
"constrains": [],
"reasons": {
"M6.1": "The dyadic partition runs over bands q ≍ Q = 2^{-ℓ}, and the box partition has mesh S*^{-3} in the chart coordinates (R, Z, T).",
"M4.8": "The active part A_ℓ is cut out by the fixed annulus Xa ≤ r²/(2q) ≤ Xb of Theorem 4.6, where the stress lives."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 64"
},
{
"id": "M6.6",
"kind": "move",
"name": "ns-m6-6-auxiliary-rectangles-the-pulse-clock-and-the-rectangle",
"title": "Auxiliary rectangles, the pulse clock, and the rectangle cutoffs",
"section": "6",
"pages": "65",
"refs": [
"p. 65, (6.10), (6.11), (6.12)",
"p. 66, (6.16)",
"used at p. 78 (Proposition 7.2) and p. 82 to 83 ((7.27))."
],
"statement": "Each label gets a band-torus rectangle Rγ = {cγ + ξ vr + η vt : |ξ|, |η| < r0} (mod Z^2), an enlargement R+γ with 2r0 in place of r0, and their preimages on the absolute torus, Rabs_γ = π_(i(ℓ))^(−1)(Rγ) and Rabs,+_γ = π_(i(ℓ))^(−1)(R+γ) (6.10). On a local lift, Yi − cγ − kcopy = ξg vr + ηg vt, v = (ηg + r0)/ci, and Ls = 2r0/ci ≍ S* (6.11). The dual coordinates satisfy Li ηg = Ni ξg = 0 and Ni ηg = Li ξg = 1, so Dr v = Dz v = 0, t* v = 1, and Ni ξg = 0 (6.12).",
"description": "Each label gets a band-torus rectangle Rγ = {cγ + ξ vr + η vt : |ξ|, |η| < r0} (mod Z^2), an enlargement R+γ with 2r0 in place of r0, and their preimages on the absolute torus, Rabs_γ = π_(i(ℓ))^(−1)(Rγ) and Rabs,+_γ = π_(i(ℓ))^(−1)(R+γ) (6.10). On a local lift, Yi − cγ − kcopy = ξg vr + ηg vt, v = (ηg + r0)/ci, and Ls = 2r0/ci ≍ S* (6.11). The dual coordinates satisfy Li ηg = Ni ξg = 0 and Ni ηg = Li ξg = 1, so Dr v = Dz v = 0, t* v = 1, and Ni ξg = 0 (6.12). OBLIGATION: It supplies a clock along which the linear pulse equation (7.5) becomes an ordinary differential equation in v (Proposition 7.2, Lemma 7.4), and the clock never enters a spatial derivative. It gives each label its own auxiliary territory for Lemma 6.1. ANTECEDENT: None cited for the clock or the rectangles. The introduction credits the evolution of wavevectors and polarizations along a background flow, which the clock hosts, to Lifschitz and Hameiri and to Friedlander and Vishik [17, 14]. REFS: p. 65, (6.10), (6.11), (6.12); p. 66, (6.16); used at p. 78 (Proposition 7.2) and p. 82 to 83 ((7.27)).",
"obligation": "It supplies a clock along which the linear pulse equation (7.5) becomes an ordinary differential equation in v (Proposition 7.2, Lemma 7.4), and the clock never enters a spatial derivative. It gives each label its own auxiliary territory for Lemma 6.1. And its area element |det(vr, vt)| dξg dηg, with dηg = ci dv, is what turns the Haar average of a pulse into a time integral in Proposition 7.5 ((7.27)).",
"backward_question": "Which torus coordinate can serve as \"time since the pulse began\", advancing at exactly unit rate under the normalized time derivative while staying invisible to radial and axial derivatives?",
"mechanism": "Because the rectangle's sides are aligned with the eigen-directions, time and radius decouple after evaluation: ηg depends on t alone (the vr component carries no ηg, since λt(vr) = 0) and ξg on r alone. So v is rescaled physical time during one pass through the rectangle, advancing at unit speed under t*, and ξg is a radial variable localized by χg. The torus is periodic, so as t increases the band coordinate re-enters the rectangles again and again; each pass is one pulse lasting Ls ≍ S* in v, during which the slow chart time moves by only ε Ls ≍ ε S*. The construction does not rely on this recurrence being equidistributed: it works with exact Haar averages and exactly inverts the fast derivative (Lemma 8.6). The cutoff ψ is applied only after the pulse equation is solved, and it equals 1 on the middle two-fifths of the interval. With the Gaussian envelope (7.16), the cutoff therefore acts only where the pulse is exp(−cS*)-small.",
"antecedent": "None cited for the clock or the rectangles. The introduction credits the evolution of wavevectors and polarizations along a background flow, which the clock hosts, to Lifschitz and Hameiri and to Friedlander and Vishik [17, 14].",
"cost": "It fixes a radius r0, which must be small for Lemma 6.1, and ties the pulse duration to ci and hence to the covering index. The envelope, and with it the flatness of the cutoff errors, is deferred to Section 7. The transverse cutoff χg(ξg) produces fast radial derivatives of size Mi, which is the source of the κs loss. Converting v derivatives into torus derivatives costs a power of S* ((6.22)).",
"checkable": "For sample (h, ℓ, r0, cγ), compute on a lift Yi(r, t) = Λg^i r^(dr) vr + Tg^i t vt, ηg = λt(Yi − cγ − kcopy) with λt(w) = vt·w/(1 + bg^2), and v = (ηg + r0)/ci. Verify by finite differences that Q^(1+h) ∂t v = 1 and ∂r v = 0 to rounding error, and that ξg does not depend on t. Given (7.16), also evaluate exp(−c (Ls/5)^2 / Ls) with Ls ≍ ℓ^2 against 2^(−Nℓ) to confirm that the region where ψ < 1 carries only flat pulse mass.",
"depends_on": [
"M6.3",
"M6.5",
"M6.2"
],
"constrains": [],
"reasons": {
"M6.3": "Rectangles live on the band torus of Y_i, and the clock v = (η_g + r_0)/c_i uses c_i, N_i, L_i so that t*v = 1 and D_r v = D_z v = 0.",
"M6.5": "Each label γ = (ℓ, a, σ) of the slow partition receives its own rectangle R_γ and its enlargement.",
"M6.2": "Rectangle sides are aligned with the eigen-directions v_r, v_t, which decouples radius and time after evaluation on the phase map."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 65"
},
{
"id": "M6.7",
"kind": "move",
"name": "ns-m6-7-lemma-6-1-disjoint-auxiliary-supports-for-interacting",
"title": "Lemma 6.1, disjoint auxiliary supports for interacting labels",
"section": "6",
"pages": "65",
"refs": [
"p. 65 (statement, (6.13))",
"p. 66 ((6.14), (6.15), Steps 1 to 3, the product consequence)",
"used at p. 12, p. 82 (Proposition 7.5), and p. 84 ((7.30))."
],
"statement": "There are centers cγ and one radius r0 > 0, common to all labels and independent of the band, such that the enlarged rectangles are injectively parametrized and γ ≠ γ′ with Kγ ∩ Kγ′ ≠ ∅ implies Rabs,+_γ ∩ Rabs,+_γ′ = ∅ (6.13). Consequently, if supp Fγ ⊂ Kγ × Rabs,+_γ for every γ, then Fγ Fγ′ = 0 for γ ≠ γ′. This also holds for derivatives of smoothly extended fields and after evaluation on (6.3) (p. 66).",
"description": "There are centers cγ and one radius r0 > 0, common to all labels and independent of the band, such that the enlarged rectangles are injectively parametrized and γ ≠ γ′ with Kγ ∩ Kγ′ ≠ ∅ implies Rabs,+_γ ∩ Rabs,+_γ′ = ∅ (6.13). Consequently, if supp Fγ ⊂ Kγ × Rabs,+_γ for every γ, then Fγ Fγ′ = 0 for γ ≠ γ′. This also holds for derivatives of smoothly extended fields and after evaluation on (6.3) (p. 66). OBLIGATION: It removes every quadratic cross-interaction between distinct localized waves: the two families (signs) in one box, neighboring boxes, and overlapping neighboring bands. Without it, products of distinct overlapping waves would enter ∇·(w ⊗ w) at the same order as the target covariance. ANTECEDENT: None cited in Section 6. The introduction attributes realizing a prescribed stress with oscillations to the Euler constructions of Daneri and Székelyhidi [10]. The coloring step is a standard greedy coloring and is not cited. REFS: p. 65 (statement, (6.13)); p. 66 ((6.14), (6.15), Steps 1 to 3, the product consequence); used at p. 12, p. 82 (Proposition 7.5), and p. 84 ((7.30)).",
"obligation": "It removes every quadratic cross-interaction between distinct localized waves: the two families (signs) in one box, neighboring boxes, and overlapping neighboring bands. Without it, products of distinct overlapping waves would enter ∇·(w ⊗ w) at the same order as the target covariance. The lemma is what gives C(a+ b+ + a− b−) = H (a+^2, a−^2)^T in Proposition 7.5 and the cross-term-free sum (7.30). Throughout the correction cycle, harmonics and corrections with the same label still interact, but distinct labels never do.",
"backward_question": "Infinitely many localized waves at infinitely many scales overlap in space-time. Is there one finite choice of auxiliary positions that makes every pair with overlapping slow supports disjoint on the torus, even though each scale sees the torus through a different covering?",
"mechanism": "Three steps. (1) Build an interaction graph. Join two labels if their enlarged slow boxes meet and their band indices differ by at most four, and also join the two signs of one box. Meeting dyadic supports force |ℓ − ℓ′| ≤ 2, and bands within four of each other have comparable chart scales and comparable ratios ℓ^2/ℓ′^2, so the degree is bounded independently of the band. Their covering indices differ by at most ∆max, by (6.14). (2) Greedily color the countable bounded-degree graph with finitely many colors. Give each color a rational center that avoids the finitely many relations cµ ≡ Jg^∆ cν (mod Z^2) for 0 ≤ ∆ ≤ ∆max, except the trivial case (∆, ν, µ) = (0, ν, ν) (6.15). Each forbidden relation is a proper closed condition; for a color paired with itself and ∆ > 0 this uses the invertibility of Jg^∆ − I. So a rational tuple avoiding all of them exists, and the forbidden differences keep a positive distance from the lattice. (3) If a point lay in the lifted rectangles of adjacent labels at levels i and i + ∆, then cµ − Jg^∆ cν ≡ Jg^∆ eν − eµ with |eν| + |eµ| ≤ C r0. Since ∆ is bounded, this is impossible for one small fixed r0. Only finitely many colors and values of ∆ occur, so a single r0 works for all bands.",
"antecedent": "None cited in Section 6. The introduction attributes realizing a prescribed stress with oscillations to the Euler constructions of Daneri and Székelyhidi [10]. The coloring step is a standard greedy coloring and is not cited.",
"cost": "It fixes a finite palette of colors, the centers, r0, and ∆max. Every wave coefficient and correction must stay supported in Kγ × Rabs,+_γ (precisely, in Ωγ or Ωcut_γ of (6.28)) through the whole correction cycle, which Proposition 9.6 must preserve. Separating the supports of derivatives requires smooth zero extension, so cross-label products are formed only after the time cutoff; before the cutoff the algebra is used on one labeled rectangle only.",
"checkable": "Take K colors, with K equal to the graph degree plus one, and random rational centers. Compute d_min, the minimum over ordered (ν, µ, ∆) ≠ (ν, ν, 0) with 0 ≤ ∆ ≤ ∆max of dist(cµ − Jg^∆ cν, Z^2), and confirm d_min > 0. Choose r0 with (1 + ‖Jg‖^(∆max)) · 2√2 · |vr| · r0 < d_min, then sample Y ∈ T^2 by Monte Carlo and confirm that no sample lies in both Jg^(−i)(R+ν) and Jg^(−(i+∆))(R+µ). Also check det(Jg^∆ − I) ≠ 0: it equals 7, 161, and 2569 for ∆ = 1, 2, 3 (computed here). And check the observed maximum of |i(ℓ) − i(ℓ′)| over |ℓ − ℓ′| ≤ 4: it is 2 for ℓ in [20, 5000) (computed here), below the bound in (6.14).",
"depends_on": [
"M6.6",
"M6.5",
"M6.3",
"M6.2"
],
"constrains": [],
"reasons": {
"M6.6": "Separates the enlarged rectangles R^+_γ, with centers c_γ and one radius r_0, attached to the labels.",
"M6.5": "The labels, their slow supports K_γ, and the bounded-degree interaction graph (both signs, neighboring boxes and bands) come from the slow partition.",
"M6.3": "Bands whose supports meet have covering indices i(ℓ) differing by at most Δmax by (6.14), so one finite choice of centers serves all bands.",
"M6.2": "The forbidden center relations are avoided using the invertibility of J_g^Δ − I for the fixed integer matrix J_g."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 65"
},
{
"id": "M6.8",
"kind": "move",
"name": "ns-m6-8-lemma-6-2-a-common-torus-for-overlapping-bands",
"title": "Lemma 6.2, a common torus for overlapping bands",
"section": "6",
"pages": "66-67",
"refs": [
"p. 66 to 67 ((6.17), (6.18), Lemma 6.2, (6.19), (6.20))",
"p. 68 (c_(i0), M_(i0))",
"p. 17 (convention (3.8) citing (6.19))."
],
"statement": "Fix (z, t) and a small neighborhood U whose band indices differ by at most four. Let Dℓ = supp_(z,t) χℓ(q(z, t)) and L(U) = {ℓ : Dℓ ∩ U ≠ ∅}, and set i0 = min over L(U) of i(ℓ) and H = π_(i0)(Y) (6.17). Then ∆ℓ = i(ℓ) − i0 ∈ {0, ..., ∆max}, π_(i(ℓ)) = π_(∆ℓ) ∘ π_(i0), Yi = Jg^(∆ℓ) H, and RH_γ = π_(∆ℓ)^(−1)(Rγ) (6.18), so Σℓ fℓ(Yi(ℓ)) = Σℓ fℓ(Jg^(∆ℓ) H). Lemma 6.2 states: each change of coordinates H ↦ Yi has uniformly bounded derivative factors;",
"description": "Fix (z, t) and a small neighborhood U whose band indices differ by at most four. Let Dℓ = supp_(z,t) χℓ(q(z, t)) and L(U) = {ℓ : Dℓ ∩ U ≠ ∅}, and set i0 = min over L(U) of i(ℓ) and H = π_(i0)(Y) (6.17). Then ∆ℓ = i(ℓ) − i0 ∈ {0, ..., ∆max}, π_(i(ℓ)) = π_(∆ℓ) ∘ π_(i0), Yi = Jg^(∆ℓ) H, and RH_γ = π_(∆ℓ)^(−1)(Rγ) (6.18), so Σℓ fℓ(Yi(ℓ)) = Σℓ fℓ(Jg^(∆ℓ) H). Lemma 6.2 states: each change of coordinates H ↦ Yi has uniformly bounded derivative factors; OBLIGATION: Fields from bands with different coverings can be added, multiplied, averaged, and inverted in one coordinate system without changing their physical values. Haar averages, and with them covariances and the \"mean\" parts of Sections 7 and 8, do not depend on the representation, as the averaging convention (3.8) requires. The separation (6.13) carries over to the common torus because π_(i0) is surjective. MECHANISM: All band tori are quotients of the absolute torus through powers of one matrix, and the bands meeting a small neighborhood have covering indices within ∆max of each. ANTECEDENT: None cited. REFS: p. 66 to 67 ((6.17), (6.18), Lemma 6.2, (6.19), (6.20)); p. 68 (c_(i0), M_(i0)); p. 17 (convention (3.8) citing (6.19)).",
"obligation": "Fields from bands with different coverings can be added, multiplied, averaged, and inverted in one coordinate system without changing their physical values. Haar averages, and with them covariances and the \"mean\" parts of Sections 7 and 8, do not depend on the representation, as the averaging convention (3.8) requires. The separation (6.13) carries over to the common torus because π_(i0) is surjective.",
"backward_question": "Waves from neighboring scales overlap but live on differently covered tori. Is there one torus on which all of them are genuine functions, with the same averages and comparable derivatives?",
"mechanism": "All band tori are quotients of the absolute torus through powers of one matrix, and the bands meeting a small neighborhood have covering indices within ∆max of each other. Each band torus near the point is the image of H under Jg^(∆ℓ), so band fields pull back to the common cover H, and the bounded powers Jg^(∆ℓ) change derivatives only by bounded matrices. Haar compatibility is checked on characters: a character of frequency n pulls back to frequency (Jg^∆)^T n, which is zero exactly when n = 0. The number of lifts is |det Jg|^∆ = 14^∆. Radial integration holds (z, t) fixed, hence q and every band cutoff, so no new band enters even though the integral crosses many radial boxes. Translations commute with deck translations, and averaging and directional multipliers preserve the lattice of pullback frequencies.",
"antecedent": "None cited.",
"cost": "The common torus is only a local representation that depends on U, and every coefficient must satisfy (6.20) on overlaps. A sum of band fields descends to H but in general not to any single band torus, since it can take different values at distinct preimages; this forces the per-lift path of M6.10. Lift counts pick up a fixed factor 14^(∆max).",
"checkable": "Verify #(Z^2 / Jg^∆ Z^2) = |det Jg^∆| = 14^∆ from Smith normal forms: diag(1, 14) for Jg, diag(2, 98) for Jg^2 = [[10, 8], [8, 26]], and diag(2, 1372) for Jg^3 (computed here). Verify (6.19) by quadrature of f(Jg^∆ H) over T^2 for random trigonometric polynomials f; the result should equal the zero Fourier coefficient. Check c_(i0) = Tg^(−∆) ci and M_(i0) = Λg^(−∆) Mi from the definitions.",
"depends_on": [
"M6.3",
"M6.7",
"M6.5",
"M6.6"
],
"constrains": [],
"reasons": {
"M6.3": "Unifies the band tori Y_i = J_g^i Y of overlapping bands on the coarsest covering H = π_{i0}(Y), with deck translations and rescaled c_i, M_i.",
"M6.7": "The bound Δ_ℓ ≤ Δmax on covering-index differences comes from (6.14), and the separation (6.13) carries over to the common torus.",
"M6.5": "The band set L(U) is read off the supports of the dyadic cutoffs χ_ℓ(q), which overlap only for neighboring bands.",
"M6.6": "Lifts each label rectangle R_γ to the common torus as 14^{Δ_ℓ} disjoint copies R^H_γ."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 66-67"
},
{
"id": "M6.9",
"kind": "move",
"name": "ns-m6-9-lemma-6-3-counting-relevant-labels",
"title": "Lemma 6.3, counting relevant labels",
"section": "6",
"pages": "68",
"refs": [
"p. 68 (Lemma 6.3 and the paragraph after it)."
],
"statement": "At any point, #{γ ∈ Γ : (r, z, t) ∈ Kγ} ≤ C. For a fixed band ℓ, a compact chart set B, and a bounded normalized radial interval IR: #{(ℓ, a, σ) : Bℓ,a ∩ B ≠ ∅} ≤ C_B Sℓ^9, and the supremum over (Z, T) of #{(ℓ, a, σ) : Bℓ,a ∩ (IR × {Z} × {T}) ≠ ∅} is at most C_IR Sℓ^3. The same bounds hold for fixed-factor enlargements of the boxes. During radial integration the band set L(z, t) is fixed, so one integral meets O(S_ref^3) labels, and the common-torus lifts add at most the factor 14^(∆max).",
"description": "At any point, #{γ ∈ Γ : (r, z, t) ∈ Kγ} ≤ C. For a fixed band ℓ, a compact chart set B, and a bounded normalized radial interval IR: #{(ℓ, a, σ) : Bℓ,a ∩ B ≠ ∅} ≤ C_B Sℓ^9, and the supremum over (Z, T) of #{(ℓ, a, σ) : Bℓ,a ∩ (IR × {Z} × {T}) ≠ ∅} is at most C_IR Sℓ^3. The same bounds hold for fixed-factor enlargements of the boxes. During radial integration the band set L(z, t) is fixed, so one integral meets O(S_ref^3) labels, and the common-torus lifts add at most the factor 14^(∆max). OBLIGATION: Pointwise sums over labels have bounded overlap and cost only a constant. Radial integrals (pressure reconstruction, stress primitives, radial moments), which collect many boxes, cost only polynomial factors in S*, and the classes absorb those. MECHANISM: Pure counting. At a point, the dyadic partition and each one-dimensional grid partition overlap boundedly, and the two signs add a factor of two. A mesh of size S^(−3) has O(S^3) positions on a bounded interval, so a compact three-dimensional chart set meets O(S^9) boxes and a radial line meets O(S^3). ANTECEDENT: None cited. REFS: p. 68 (Lemma 6.3 and the paragraph after it).",
"obligation": "Pointwise sums over labels have bounded overlap and cost only a constant. Radial integrals (pressure reconstruction, stress primitives, radial moments), which collect many boxes, cost only polynomial factors in S*, and the classes absorb those.",
"backward_question": "When an operation such as radial integration sums contributions from many slow boxes, how many can there be, and is the count only logarithmic in 1/q?",
"mechanism": "Pure counting. At a point, the dyadic partition and each one-dimensional grid partition overlap boundedly, and the two signs add a factor of two. A mesh of size S^(−3) has O(S^3) positions on a bounded interval, so a compact three-dimensional chart set meets O(S^9) boxes and a radial line meets O(S^3). Enlarging the boxes by a fixed factor changes only the constants.",
"antecedent": "None cited.",
"cost": "Polynomial growth S^3 along radial lines and S^9 on compact chart sets, absorbed into the S*^b factors of the classes. It requires the values Sℓ for ℓ ∈ L(U) to be comparable, which holds because those bands differ by at most four.",
"checkable": "An elementary count, essentially a pure estimate. Count grid boxes of side S^(−3), enlarged by a fixed factor, that meet a unit cube and a unit radial segment for S = ℓ^2 with ℓ from 10 to 100, and fit the growth exponents 9 and 3.",
"depends_on": [
"M6.5",
"M6.8"
],
"constrains": [],
"reasons": {
"M6.5": "Counts boxes of mesh S*^{-3} and the two signs of the slow partition, using bounded overlap of the dyadic and grid cutoffs.",
"M6.8": "The factor 14^{Δmax} from common-torus lifts and the fixed band set during radial integration come from Lemma 6.2."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 68"
},
{
"id": "M6.10",
"kind": "move",
"name": "ns-m6-10-the-pulse-path-on-the-common-torus",
"title": "The pulse path on the common torus",
"section": "6",
"pages": "68",
"refs": [
"p. 68 ((6.21), (6.22))",
"p. 69 (the Y form, deck translations, descent)",
"used at p. 78 to 80 (Proposition 7.2, Step 3)."
],
"statement": "Let λt(w) = vt·w / (1 + bg^2), so λt(vr) = 0 and λt(vt) = 1, and on one lifted band rectangle let ηg(H) = λt(Jg^∆ H − cγ − kcopy). For w ∈ [0, Ls], define Hw = H + Tg^(−∆) ci (w − v(H)) vt = H0 + Tg^(−∆) ci w vt, with H0 = H − Tg^(−∆) (ηg(H) + r0) vt (6.21). The point Hw has the same slow coordinates and the same transverse coordinate ξg as H, and pulse coordinate w. Moreover DH Hw = I − vt λt and DH v = (Tg^∆ / ci) λt = O(S*) (6.22), and all higher derivatives vanish.",
"description": "Let λt(w) = vt·w / (1 + bg^2), so λt(vr) = 0 and λt(vt) = 1, and on one lifted band rectangle let ηg(H) = λt(Jg^∆ H − cγ − kcopy). For w ∈ [0, Ls], define Hw = H + Tg^(−∆) ci (w − v(H)) vt = H0 + Tg^(−∆) ci w vt, with H0 = H − Tg^(−∆) (ηg(H) + r0) vt (6.21). The point Hw has the same slow coordinates and the same transverse coordinate ξg as H, and pulse coordinate w. Moreover DH Hw = I − vt λt and DH v = (Tg^∆ / ci) λt = O(S*) (6.22), and all higher derivatives vanish. OBLIGATION: Proposition 7.2 must integrate the amplitude equation from the start of a pulse to the current v, evaluating a source f(R, Z, T, Hw) along the path \"without averaging over the other preimages\", because a source built from several bands descends to H but not to Yi. (6.22) supplies this change of coordinates \"without a new power of ε.\" MECHANISM: vt is an eigenvector of Jg, so moving H by s vt moves Yi = Jg^∆ H by Tg^∆ s vt. That raises ηg by Tg^∆ s and v by Tg^∆ s / ci, and choosing s = Tg^(−∆) ci (w − v(H)) lands at pulse coordinate w. ANTECEDENT: None cited. REFS: p. 68 ((6.21), (6.22)); p. 69 (the Y form, deck translations, descent); used at p. 78 to 80 (Proposition 7.2, Step 3).",
"obligation": "Proposition 7.2 must integrate the amplitude equation from the start of a pulse to the current v, evaluating a source f(R, Z, T, Hw) along the path \"without averaging over the other preimages\", because a source built from several bands descends to H but not to Yi. (6.22) supplies this change of coordinates \"without a new power of ε.\"",
"backward_question": "If a source lives on the finer common torus but not on the band torus, along which curve do I integrate the pulse equation so that the solution is a well-defined function on the common torus?",
"mechanism": "vt is an eigenvector of Jg, so moving H by s vt moves Yi = Jg^∆ H by Tg^∆ s vt. That raises ηg by Tg^∆ s and v by Tg^∆ s / ci, and choosing s = Tg^(−∆) ci (w − v(H)) lands at pulse coordinate w. Nothing else changes: the vr component (ξg) is untouched, and the slow variables are parameters. The map is affine in H, its Jacobian is the bounded projection I − vt λt, and the gradient of the v coordinate is O(S*). Uniqueness for the zero-data initial value problem, combined with deck equivariance of the path, gives descent.",
"antecedent": "None cited.",
"cost": "Converting pulse-coordinate derivatives into H derivatives costs powers of S* (DH v = O(S*)). The solution is defined lift by lift, so the copy index kcopy matters. Support containment holds when the source vanishes along the whole rectangle.",
"checkable": "For random H on a lift, ∆ ∈ {0, 1, 2, 3}, and sample ci, r0, cγ, compute Hw from (6.21). Verify v(Hw) = w and ξg(Hw) = ξg(H) (using the dual functional for vr), and compare finite-difference Jacobians with I − vt λt and (Tg^∆ / ci) λt. This is an exact linear-algebra check.",
"depends_on": [
"M6.8",
"M6.6",
"M6.2"
],
"constrains": [],
"reasons": {
"M6.8": "The path lives on the common torus H with Y_i = J_g^Δ H, since a source built from several bands descends to H but not to a band torus.",
"M6.6": "Moves only the pulse coordinate v = (η_g + r_0)/c_i of a lifted rectangle, keeping the transverse coordinate ξ_g and the slow variables fixed.",
"M6.2": "Uses that v_t is an eigenvector of J_g, so a shift along v_t on H moves Y_i along v_t by the factor T_g^Δ."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 68"
},
{
"id": "M6.11",
"kind": "move",
"name": "ns-m6-11-edge-weights-and-the-coefficient-classes-m-w-s",
"title": "Edge weights and the coefficient classes Mα, Wα, Sα",
"section": "6",
"pages": "69",
"refs": [
"p. 69 ((6.23), (6.24), Definition 6.4)",
"p. 70 ((6.25) to (6.29), Definition 6.5)",
"p. 71 (collected sums, smooth extension)",
"p. 18 (overview)."
],
"statement": "The flat edge weight on Xa < X < Xb is ζ(X) = exp(−aa / log^2(X/Xa) − ab / log^2(Xb/X)), extended by zero outside, and δ(X) = min{1, log(X/Xa), log(Xb/X)}, with aa, ab > 0 fixed (6.23). For every b > 0 and finite N, ζ^b δ^(−N) vanishes faster than any power at both edges, and both weights depend only on X, so they are constant along (6.21). Coefficient derivatives are ∂I, with I ∈ N0^5 counting derivatives in R, Z, T, H1, H2, taken with the oscillatory exponential factored out.",
"description": "The flat edge weight on Xa < X < Xb is ζ(X) = exp(−aa / log^2(X/Xa) − ab / log^2(Xb/X)), extended by zero outside, and δ(X) = min{1, log(X/Xa), log(Xb/X)}, with aa, ab > 0 fixed (6.23). For every b > 0 and finite N, ζ^b δ^(−N) vanishes faster than any power at both edges, and both weights depend only on X, so they are constant along (6.21). Coefficient derivatives are ∂I, with I ∈ N0^5 counting derivatives in R, Z, T, H1, H2, taken with the oscillatory exponential factored out. OBLIGATION: The residual estimates must record both the size of a correction (a power of ε) and how it vanishes at the edge of its support. Bounds at every derivative order make the shell extensions smooth and survive products and derivatives. This is the language in which Section 9 runs its induction (the orders σj, Bj, C*j). Smooth zero extension comes for free, because ζ and √ζ absorb every inverse power of δ that differentiation introduces. ANTECEDENT: None cited. The weight ζ is \"the flat edge weight of Theorem 4.6.\" REFS: p. 69 ((6.23), (6.24), Definition 6.4); p. 70 ((6.25) to (6.29), Definition 6.5); p. 71 (collected sums, smooth extension); p. 18 (overview).",
"obligation": "The residual estimates must record both the size of a correction (a power of ε) and how it vanishes at the edge of its support. Bounds at every derivative order make the shell extensions smooth and survive products and derivatives. This is the language in which Section 9 runs its induction (the orders σj, Bj, C*j). Smooth zero extension comes for free, because ζ and √ζ absorb every inverse power of δ that differentiation introduces.",
"backward_question": "What minimal set of quantitative properties of a coefficient (order, logarithmic loss, vanishing at the edges, temporal envelope, support, descent) is stable under everything the correction cycle does to it?",
"mechanism": "Each factor records one thing. ε^α records the order. S*^b records logarithmic losses, which are harmless. δ^(−d) records the losses from differentiating near the shell edges, since derivatives of the flat weight produce inverse powers of the log distance. ζ for means, and √ζ for waves (whose squares are means), record flat vanishing at the edges, inherited from the flat stress weight of Theorem 4.6. Pv records the temporal envelope of a pulse. Amplitudes are differentiated with e^(ikmΦ) factored out, so derivatives of the phase, which carry an explicit factor km, are tracked separately. Moments depend only on (Z, T) and include the radial measure in their normalization, so radial integration fits the scaling.",
"antecedent": "None cited. The weight ζ is \"the flat edge weight of Theorem 4.6.\"",
"cost": "Each coefficient carries infinitely many conditions, one for each derivative order. The compatibility, support, and smooth-extension conditions must survive every later operation. The wave envelope bound holds only on 0 ≤ v ≤ Ls, with no temporal zero extension until ψ is applied. The harmonic set must stay finite and band-independent at every stage.",
"checkable": "Evaluate ζ^b δ^(−N) at X = Xa e^s as s → 0+ for sample values (for example aa = 1, b = 1/2, N = 20) and confirm it drops below s^M for every M tested. Verify the scaling identity (6.26) by quadrature for a test profile, substituting r = √Q R. The rest is definitions.",
"depends_on": [
"M4.8",
"M6.1",
"M6.8",
"M6.6"
],
"constrains": [],
"reasons": {
"M4.8": "ζ is the flat edge weight of Theorem 4.6, and the classes carry its weighted stress bounds (4.27) with the weights ζ and δ.",
"M6.1": "Orders are powers of ε = Q^h and harmless logarithmic losses are powers of S* = ℓ² in chart units.",
"M6.8": "Coefficients must descend to each common torus with compatible representatives (6.20), and derivatives count the common coordinates H1, H2.",
"M6.6": "The wave class W_α is supported in the label rectangles and bounded along the pulse coordinate 0 ≤ v ≤ L_s."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 69"
},
{
"id": "M6.12",
"kind": "move",
"name": "ns-m6-12-proposition-6-6-the-class-algebra-and-the-derivative-cost",
"title": "Proposition 6.6, the class algebra and the derivative cost table",
"section": "6",
"pages": "71",
"refs": [
"p. 71 (Proposition 6.6, (6.30), (6.31), (6.32))",
"p. 72 (proof Steps 1 to 3)",
"p. 72 to 73 (support convention for the initial value problems",
"Proposition 9.6 preserves containment)."
],
"statement": "Each class is closed under finite sums at a fixed exponent. Products satisfy Mα Mβ ⊂ Mα+β and Mα Wβ ⊂ Wα+β (6.30). For the same label, aγ,m bγ,m′ belongs to Wα+β with harmonic m + m′ when m + m′ ≠ 0, and to Mα+β when m + m′ = 0, after the temporal cutoff (6.31); before the cutoff, a zero harmonic satisfies the mean bounds on its labeled rectangle. Distinct labels satisfy (∂I wγ)(∂J wγ′) = 0. Coefficient derivatives preserve ε exponents.",
"description": "Each class is closed under finite sums at a fixed exponent. Products satisfy Mα Mβ ⊂ Mα+β and Mα Wβ ⊂ Wα+β (6.30). For the same label, aγ,m bγ,m′ belongs to Wα+β with harmonic m + m′ when m + m′ ≠ 0, and to Mα+β when m + m′ = 0, after the temporal cutoff (6.31); before the cutoff, a zero harmonic satisfies the mean bounds on its labeled rectangle. Distinct labels satisfy (∂I wγ)(∂J wγ′) = 0. Coefficient derivatives preserve ε exponents. OBLIGATION: It lets Sections 7 to 9 read off the order of every term in the residual (transport products, curl remainders, viscosity, slow and fast time derivatives) from a table. The angular-average rule separates the zero harmonic of wave products, which feeds the mean corrections of Section 8, from the oscillating harmonics, which feed the wave inverse of Proposition 7.2. MECHANISM: Leibniz's rule plus weight inequalities: ζ^2 ≤ ζ; ζ^(3/2) Pv ≤ √ζ Pv; ζ Pv^2 ≤ ζ when m + m′ = 0; and ζ Pv^2 ≤ √ζ Pv when m + m′ ≠ 0. ANTECEDENT: None cited. REFS: p. 71 (Proposition 6.6, (6.30), (6.31), (6.32)); p. 72 (proof Steps 1 to 3); p. 72 to 73 (support convention for the initial value problems; Proposition 9.6 preserves containment).",
"obligation": "It lets Sections 7 to 9 read off the order of every term in the residual (transport products, curl remainders, viscosity, slow and fast time derivatives) from a table. The angular-average rule separates the zero harmonic of wave products, which feeds the mean corrections of Section 8, from the oscillating harmonics, which feed the wave inverse of Proposition 7.2.",
"backward_question": "Once every coefficient carries an order in ε, what does each operation in the Navier-Stokes residual (products, the three normalized spatial derivatives, the slow and fast time derivatives, angular averaging) do to that order?",
"mechanism": "Leibniz's rule plus weight inequalities: ζ^2 ≤ ζ; ζ^(3/2) Pv ≤ √ζ Pv; ζ Pv^2 ≤ ζ when m + m′ = 0; and ζ Pv^2 ≤ √ζ Pv when m + m′ ≠ 0. Powers of S* and of δ^(−1) simply add. Because k pγ is a nonzero integer, ⟨aγ,m aγ,m′ e^(ik(m+m′)Φγ)⟩θ equals aγ,m aγ,m′ if m + m′ = 0 and 0 otherwise, so a single nonzero harmonic has zero angular mean. The cost table follows from (6.6). The coordinate coefficients of Dr, including the fast term Mi dr R^(dr−1) Li, are bounded by C ε^(−κs) S*^C. Dz and −ε∂T carry an explicit ε. The fast time derivative has coefficient c_(i0) ≍ S*^(−1). Switching between band and common tori adds only bounded matrices (Lemma 6.2). Cross-label products vanish by Lemma 6.1 once the time cutoff has given smooth extension.",
"antecedent": "None cited.",
"cost": "Every explicit radial derivative costs κs, so later gains must exceed accumulated multiples of κs = 10^(−5) (exponents such as α + 1/2 − κs and 1 − 3κs appear later). The zero harmonic of a wave product counts as a mean coefficient only after the temporal cutoff. Differentiating e^(ikmΦ) produces an explicit factor km, with k ≍ ε^(−1/2), which is tracked outside the table.",
"checkable": "Mostly a pure estimate (Leibniz bookkeeping). Concrete pieces: verify the four weight inequalities on a grid of (ζ, P) ∈ [0, 1] × (0, 1]; verify that (1/2π) ∫ e^(inθ) dθ = 0 for integers n = k(m + m′)pγ ≠ 0; and apply Dr = ∂R + Mi dr R^(dr−1) Li to test products f(R) g(Yi) to confirm that the size ratio is bounded by C(1 + Mi) ≤ C ε^(−κs) S*^C.",
"depends_on": [
"M6.11",
"M6.3",
"M6.7",
"M6.8"
],
"constrains": [],
"reasons": {
"M6.11": "States the sum, product, and derivative rules for the classes M_α, W_α, S_α with their weights ζ, √ζ, δ and P_v.",
"M6.3": "The cost table is read off the chart operators: D_r carries M_i ≍ ε^{-κ_s}, D_z = ε∂_Z, and t* = −ε∂_T + c_iN_i with c_i ≍ S*^{-1}.",
"M6.7": "Distinct labels have vanishing products (∂^I w_γ)(∂^J w_γ′) = 0 by the disjoint auxiliary supports.",
"M6.8": "Switching between band and common tori changes derivatives only by bounded matrices, so exponents are unchanged."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 71"
},
{
"id": "M7.1",
"kind": "move",
"name": "ns-m7-1-tangential-shear-frame-growth-rate-and-the-cone-restated",
"title": "Tangential shear frame, growth rate, and the cone restated in the wave frame",
"section": "7",
"pages": "73-74",
"refs": [
"pp. 73 to 74",
"(7.1)",
"uses (4.11), (4.20), (4.22), (4.26), (5.42)."
],
"statement": "At each slow-box representative define N = g0/|g0|, K = N⊥ = (-Nz, Nθ), λ0^2 = -2F0Nθ(2F0Nθ + |g0|) > 0, c0 = λ0/(2F0Nθ) < 0 (p. 74). Since g0 = F0(-a, bs) by (4.11) and (4.20), λ0^2 = 2aF0^2(1 - 2/vs) and c0^2 = (vs - 2)/2, so both signs follow from the lower bounds of Theorem 4.6(iii); they are consequences of the profile, not new choices. The admissible stress cone of Lemma 4.5 is equivalent to (7.1): T0,∗·N < 0 and |c0 (T0,∗·K)/(T0,∗·N)| < 1, with T0,∗ = (Q/q)^{A+1/2}T0.",
"description": "At each slow-box representative define N = g0/|g0|, K = N⊥ = (-Nz, Nθ), λ0^2 = -2F0Nθ(2F0Nθ + |g0|) > 0, c0 = λ0/(2F0Nθ) < 0 (p. 74). Since g0 = F0(-a, bs) by (4.11) and (4.20), λ0^2 = 2aF0^2(1 - 2/vs) and c0^2 = (vs - 2)/2, so both signs follow from the lower bounds of Theorem 4.6(iii); they are consequences of the profile, not new choices. The admissible stress cone of Lemma 4.5 is equivalent to (7.1): T0,∗·N < 0 and |c0 (T0,∗·K)/(T0,∗·N)| < 1, with T0,∗ = (Q/q)^{A+1/2}T0. OBLIGATION: Converts the profile-level cone condition ((4.21), (4.22), (4.26)) into the exact form the. ANTECEDENT: Internal: Lemma 4.5, Theorem 4.6(iii), (4.26). Section 7 cites nothing. The introduction (p. 2) lists the centrifugal-instability criteria of Leibovich-Stewartson [15] and Billant-Gallaire [2, 3] among precedents for the wave dynamics. (Digest's rewriting, not stated in the manuscript: with Nθ = R∂RF/|g0|, Ω = F, V = RF, Γ = R^2F, one gets λ0^2 = -2V∂RΩ(∂RΩ ∂RΓ + (∂RG)^2)/((R∂RΩ)^2 + (∂RG)^2), positive exactly when V∂RΩ(∂RΩ ∂RΓ + (∂RG)^2) < 0, which is the Leibovich-Stewartson sufficient condition, and Rayleigh's criterion when ∂RG = 0.) REFS: pp. 73 to 74; (7.1);",
"obligation": "Converts the profile-level cone condition ((4.21), (4.22), (4.26)) into the exact form the two-pulse covariance construction of Proposition 7.5 needs, with a strict margin that survives freezing the frame on slow boxes (every point within C S∗^{-3} of its representative) and the O(S∗^{-1/2}) column errors of (7.28). The positivity λ0^2 > 0, equivalent to vs > 2 (the extra inequality that Section 4, p. 31, adds to the relaxed cone for the sake of the viscous waves), is what makes pulses grow at all. Without a strict margin no finite u∗ exists; without λ0^2 > 0 there is no amplification.",
"backward_question": "Which momentum fluxes can a growing viscous wave on a swirling, axially sheared column carry, and can the required leading stress be placed strictly inside that set with a margin that survives freezing the frame at one point per slow box?",
"mechanism": "In the tangential (θ, z) plane, N points along the base shear and K across it. Energy exchange between a wave and the base is -g0·T = -|g0|TN (M7.8), so a wave that grows by drawing energy from the shear can only carry stresses with TN < 0; the energy-neutral component TK must be steered by tilting the wavevector. With T0 = F(ps - s) and s = (a, -bs) one has N = -s/|s|, T0·N = -Fa(Pc - vs)/|s| and (T0·K)/(T0·N) = Jc/(Pc - vs), so (7.1) is literally (4.22) once c0^2 = (vs - 2)/2 is inserted. The two pulses of M7.9 produce covariance directions -AcN ∓ u∗K with Ac = |c0|√(1 + u∗^2); their positive cone has half-opening ratio u∗/Ac, which increases to 1/|c0| as u∗ grows, so the strict inequality |c0 TK/TN| < 1 is exactly what lets some finite u∗ capture the stress. Theorem 4.6(iii) extends the unit stress direction smoothly to the closed annulus, so uniform continuity keeps the margin when N, K, c0 are frozen per box.",
"antecedent": "Internal: Lemma 4.5, Theorem 4.6(iii), (4.26). Section 7 cites nothing. The introduction (p. 2) lists the centrifugal-instability criteria of Leibovich-Stewartson [15] and Billant-Gallaire [2, 3] among precedents for the wave dynamics. (Digest's rewriting, not stated in the manuscript: with Nθ = R∂RF/|g0|, Ω = F, V = RF, Γ = R^2F, one gets λ0^2 = -2V∂RΩ(∂RΩ ∂RΓ + (∂RG)^2)/((R∂RΩ)^2 + (∂RG)^2), positive exactly when V∂RΩ(∂RΩ ∂RΓ + (∂RG)^2) < 0, which is the Leibovich-Stewartson sufficient condition, and Rayleigh's criterion when ∂RG = 0.)",
"cost": "One fixed tilt parameter u∗ > 0, uniform over bands and labels, set by the margin κ of (4.26); slow boxes of mesh S∗^{-3} small enough that the frozen frame keeps a uniform margin; dependence on positive lower bounds for F, a, vs - 2 on the closed annulus.",
"checkable": "Sample (a, bs, ps,1, ps,2, F0) with a > 0, F0 > 0, vs = a + bs^2/a > 2. Form g0 = F0(-a, bs), N, K, λ0^2, c0, and T0 = F0(ps - s). Compare λ0^2 with 2aF0^2(1 - 2/vs); c0^2 with (vs - 2)/2; |T0·K|/|T0·N| with |Jc|/(Pc - vs) computed from (4.20); and the truth value of (7.1) with that of (4.22), over many random samples. Separately verify the Leibovich-Stewartson rewriting of λ0^2 given under Antecedent as a symbolic identity.",
"depends_on": [
"M4.7",
"M4.8",
"M4.4",
"M5.14",
"ME.14",
"L.11"
],
"constrains": [],
"reasons": {
"M4.7": "Restates the admissible stress cone (4.21), (4.22) of Lemma 4.5 as (7.1) through T0·N = −Fa(Pc − vs)/|s| and (T0·K)/(T0·N) = Jc/(Pc − vs).",
"M4.8": "The signs λ0² > 0, c0 < 0 and a finite tilt u* follow from Theorem 4.6(iii): F, a > 0, vs > 2 and the margin (4.26) on the closed annulus.",
"M4.4": "Uses the shear s = (a, −bs) and stress T0 = F(ps − s) of (4.11), so g0 = F0(−a, bs) and λ0² = 2aF0²(1 − 2/vs).",
"M5.14": "The frame is built from the realized background's swirl and axial shear, which (5.42) puts within O(ε²) of the leading profile values.",
"ME.14": "Sets a frame by the shear direction N = g0/|g0| and gets growth lambda_0^2 > 0 from rotation plus shear, as ME.14's frame makes strain plus shear a hyperbolic loop.",
"L.11": "Pulses grow only if λ0^2 = 2aF0^2(1 - 2/v_s) > 0, a centrifugal criterion with axial shear of the kind in [15, 2, 3], which are listed as precedents for the wave dynamics."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 73-74"
},
{
"id": "M7.2",
"kind": "move",
"name": "ns-m7-2-transported-phase-with-carrier-k-1-2-and-a-shear-driven",
"title": "Transported phase with carrier k = ⌈ε^{-1/2}⌉ and a shear-driven tilt schedule",
"section": "7",
"pages": "74-77",
"refs": [
"pp. 74 to 77",
"(7.2), (7.3), (7.4), (7.9)",
"scale check p. 81."
],
"statement": "For a label γ = (ℓ, a, σ), (7.2): k = ⌈ε^{-1/2}⌉, Bs^2 = λ0/(εk^2(1 + u∗^2)^{3/2}), s(v) = σ(u∗/2 + u∗v/Ls). Tangential wave numbers (p̃/R0, pz) = Bs(K - σu∗g0/(Ls|g0|^2)), then kp is rounded to a nearest nonzero integer; x0 = σBsu∗/2. Phase (7.3): Φ = pθ + pzZ/ε + x0R - v(pF + pzG); phase normal (7.4): nΦ = ∇∗Φ = (x0 - v(p∂RF + pz∂RG), p/R, pz - εv(p∂ZF + pz∂ZG)). Lemma 7.1, first part (7.9): each e^{ikmΦ}, m ≠ 0, is single-valued in θ with nonzero angular frequency;",
"description": "For a label γ = (ℓ, a, σ), (7.2): k = ⌈ε^{-1/2}⌉, Bs^2 = λ0/(εk^2(1 + u∗^2)^{3/2}), s(v) = σ(u∗/2 + u∗v/Ls). Tangential wave numbers (p̃/R0, pz) = Bs(K - σu∗g0/(Ls|g0|^2)), then kp is rounded to a nearest nonzero integer; x0 = σBsu∗/2. Phase (7.3): Φ = pθ + pzZ/ε + x0R - v(pF + pzG); phase normal (7.4): nΦ = ∇∗Φ = (x0 - v(p∂RF + pz∂RG), p/R, pz - εv(p∂ZF + pz∂ZG)). Lemma 7.1, first part (7.9): each e^{ikmΦ}, m ≠ 0, is single-valued in θ with nonzero angular frequency; OBLIGATION: Supplies the fast phase for all waves of a label. It must (i) have nonzero integer angular frequency, so every wave has zero angular mean and cos^2 averages to exactly 1/2 (used in (7.27) and in every mean computation); ANTECEDENT: Section 7 cites nothing. The introduction (p. 2) names Lifschitz-Hameiri and Friedlander-Vishik [17, 14] (evolution of wavevectors and polarizations along a background flow) and the exact shearing waves of Craik-Criminale [9] and Singh-Sridhar [19] as precedents for the wave dynamics; the linear-in-v growth of the radial wavenumber is the shearing-wave kinematics of those works. REFS: pp. 74 to 77; (7.2), (7.3), (7.4), (7.9); scale check p. 81.",
"obligation": "Supplies the fast phase for all waves of a label. It must (i) have nonzero integer angular frequency, so every wave has zero angular mean and cos^2 averages to exactly 1/2 (used in (7.27) and in every mean computation); (ii) be carried by the base swirl and axial flow, so the leading transport terms of the linearized operator cancel up to Eik; (iii) keep viscosity in the leading balance (1 ≤ εk^2 ≤ 4) so damping can end each pulse; (iv) tilt the wavevector through a fixed range over each pulse, which produces growth followed by decay.",
"backward_question": "How should the phase be chosen so that differential rotation and axial shear tilt the wavevector slowly through a prescribed range, making amplification win early and viscous damping win late, while the angular wavenumber stays an integer and viscosity stays at leading order?",
"mechanism": "The pulse coordinate v is normalized time: it advances at unit speed under t∗ and is constant under Dr, Dz (6.12). Its coefficient -(pF + pzG) in Φ cancels F∂θΦ + GDzΦ, so the phase is carried by the local rotation and axial flow; what survives in Eik is εv(∂T HΦ - G∂Z HΦ) + b nΦ,r with HΦ = pF + pzG, each term carrying ε or b = O(ε). Because F and G vary in R, the radial component of nΦ changes linearly in v at rate -(p/R, pz)·g: wave crests are sheared by differential rotation and axial shear. The tangential wavevector is taken almost along K (perpendicular to the shear, so tilting is slow) plus a small part -σu∗g0/(Ls|g0|^2) along g0; before rounding (p/R0, pz)·g0 = -σBsu∗/Ls, so nΦ,r = Bs s(v) runs from σBsu∗/2 to 3σBsu∗/2 over a pulse. The magnitude Bs is tuned so growth and damping balance at the midpoint (M7.5). The choice k = ⌈ε^{-1/2}⌉ makes the viscous coefficient εk^2|nΦ|^2 of order one; physically the carrier wavelength √Q/k ≍ Q^{1/2+h/2} times the wave amplitude Q^{-1/2-h/2} is of order one, a wave Reynolds number of order one (p. 81). Rounding kp costs O(k^{-1}) ≤ ε^{1/2}, which multiplied by v = O(S∗) stays below C/S∗ once S∗^2(ε + ε^2 + k^{-1}) ≤ 1.",
"antecedent": "Section 7 cites nothing. The introduction (p. 2) names Lifschitz-Hameiri and Friedlander-Vishik [17, 14] (evolution of wavevectors and polarizations along a background flow) and the exact shearing waves of Craik-Criminale [9] and Singh-Sridhar [19] as precedents for the wave dynamics; the linear-in-v growth of the radial wavenumber is the shearing-wave kinematics of those works.",
"cost": "Label constants k, Bs, p, pz, x0 and the tilt s(v); the phase normal matches Bs(s(v), K) only to C/S∗; the defect Eik = O(εS∗^C) is not removed here and is estimated in Proposition 9.1 (gain 1/2 in the table after (9.2)); two phases per slow box on disjoint auxiliary rectangles.",
"checkable": "Symbolic: treat Φ of (7.3) as a function of (R, θ, Z, T, v) with t∗ = -ε∂T + ∂v, Dr = ∂R, Dz = ε∂Z, and confirm (t∗ + bDr + F∂θ + GDz)Φ = εv(∂T HΦ - G∂Z HΦ) + b nΦ,r (the identity in Step 1, p. 76). Numeric: for smooth sample F(R, Z, T), G(R, Z, T), take ε = 2^{-hℓ}, k = ⌈ε^{-1/2}⌉, Ls proportional to ℓ^2, and compute max over v in [0, Ls] of |nΦ(v) - Bs(s(v), K)| for ℓ = 10, 20, 40; confirm decay like ℓ^{-2}. Confirm kmp is a nonzero integer and 1 ≤ εk^2 ≤ 4.",
"depends_on": [
"M7.1",
"M6.6",
"M5.14",
"M6.5",
"ME.3",
"L.10"
],
"constrains": [],
"reasons": {
"M7.1": "The wave numbers use the frame N, K, the shear g0, the rate λ0 inside Bs, and the tilt parameter u* fixed with the cone margin.",
"M6.6": "The pulse coordinate v, with t*v = 1, D_r v = D_z v = 0 and length L_s, carries the tilt schedule s(v) and the transport term of Φ.",
"M5.14": "The phase is carried by the background swirl F and axial flow G, so base transport cancels up to E_ik, small because b = O(ε).",
"M6.5": "Each label γ = (ℓ, a, σ) gets one phase frozen at its slow-box representative, the sign σ choosing the tilt direction.",
"ME.3": "Its phase (7.3) is advected by the background, so the normal n_Phi of (7.4) is sheared as m = F^{-T} m0 is under m_t = -M^T m in (2.4).",
"L.10": "The shear-driven tilt of each pulse's wavevector is the wavevector evolution along a background flow described in [17, 14]: shear increases the radial component."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 74-77"
},