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": "MB.1",
"kind": "move",
"name": "ns-mb-1-symmetry-breaking-axis-velocity-and-the-two-region-split",
"title": "Symmetry-breaking axis velocity and the two-region split of the parameter interval",
"section": "B",
"pages": "144",
"refs": [
"p. 144, (B.1), (B.2)",
"Lemma A.5, (A.21) to (A.22), p. 133",
"Proposition 4.10 proof, p. 37",
"Section 2.1, pp. 3 to 5",
"p. 8."
],
"statement": "With Π0 from Lemma A.5 (real analytic near [−1, 1], even, Π0 ≤ −cP∗²f², ηΠ0η > 0 for η ≠ 0, f = (1 + η²)^{−1}) and h ≤ 10^{−2} already fixed, choose 0 < j0 ≤ .05 and set U∗ = 4η + j0, H∗ = Dη + dU∗, W∗ = 1 − dU∗η − 2DηU∗, Z∗ = −A(1 − 2ηU∗)U∗ − H∗U∗η − dΠ0η + 4AηΠ0 (B.1). Then H∗ has exactly one zero η0 ∈ (−1, 0) with |η0| ≍ j0; −W∗ = 3 − 8hη² + (1 − 2h)j0η > 2.8; and Z∗(η0) ≥ cj0P∗² > 0.",
"description": "With Π0 from Lemma A.5 (real analytic near [−1, 1], even, Π0 ≤ −cP∗²f², ηΠ0η > 0 for η ≠ 0, f = (1 + η²)^{−1}) and h ≤ 10^{−2} already fixed, choose 0 < j0 ≤ .05 and set U∗ = 4η + j0, H∗ = Dη + dU∗, W∗ = 1 − dU∗η − 2DηU∗, Z∗ = −A(1 − 2ηU∗)U∗ − H∗U∗η − dΠ0η + 4AηΠ0 (B.1). Then H∗ has exactly one zero η0 ∈ (−1, 0) with |η0| ≍ j0; −W∗ = 3 − 8hη² + (1 − 2h)j0η > 2.8; and Z∗(η0) ≥ cj0P∗² > 0. OBLIGATION: The inner-edge inequality (B.19), which is vs > 2 + cex at X0 = 4/Λ (the viscous part of the admissible stress cone at the edge where the stress is born parallel to the shear; Proposition 4.10(ii), Theorem 4.6(iii)), must hold for every η. H∗ is the axis value of the coefficient Hc of the η-derivative in the transport terms, so the rotational mechanism dies at its zero; Z∗ is the axis value of the axial source Sn (so ns ≈ Z∗/L), so the axial-shear mechanism dies at its zeros. ANTECEDENT: None cited. The physical motivation is Section 2.1 (pages 3 to 5). REFS: p. 144, (B.1), (B.2); Lemma A.5, (A.21) to (A.22), p. 133; Proposition 4.10 proof, p. 37; Section 2.1, pp. 3 to 5; p. 8.",
"obligation": "The inner-edge inequality (B.19), which is vs > 2 + cex at X0 = 4/Λ (the viscous part of the admissible stress cone at the edge where the stress is born parallel to the shear; Proposition 4.10(ii), Theorem 4.6(iii)), must hold for every η. H∗ is the axis value of the coefficient Hc of the η-derivative in the transport terms, so the rotational mechanism dies at its zero; Z∗ is the axis value of the axial source Sn (so ns ≈ Z∗/L), so the axial-shear mechanism dies at its zeros. With j0 = 0 both vanish at η = 0 (U∗(0) = 0, H∗(0) = 0, and Π0η(0) = 0 by evenness), leaving the midplane uncovered; this is the upward-biased, mildly asymmetric axial profile motivated physically in Section 2.1. The constant −W∗ > 2.8 also supplies the order-one part of the angular source in (B.17), and the nonzero axis datum U∗ gives the axial velocity lower bound ‖uz(0)‖ ≍ τ^{−1/2−h} on the core (page 8).",
"backward_question": "At which values of η does each available amplification mechanism (axial transport of angular momentum versus radial shear of axial velocity) degenerate, and can a single small symmetry-breaking parameter keep those degeneracy sets disjoint?",
"mechanism": "H∗/d = Dη/d + 4η + j0 increases strictly from −∞ to +∞ on (−1, 1) and equals j0 > 0 at η = 0, so its zero η0 is unique, negative, and about −j0/(D + 4). At η0 the H∗U∗η term of Z∗ drops out, 4Aη0Π0(η0) is positive (η0 < 0 and Π0 < 0) and at least cj0P∗², −dΠ0η(η0) ≥ 0 by the sign of ηΠ0η, and the remaining terms are O(j0), which the already large P∗ absorbs. So the zero set of Z∗ is separated from η0; δ∗ quantifies the separation, and σ∗ is then chosen so small that away from a neighborhood of η0 the regularized indicator χ of H∗ ≠ 0 exceeds .99. Every η then lies either in {χ > .99}, where the rotational branch of (B.19) will work, or in {|Z∗| > δ∗}, where the axial-shear branch will work. The formula for −W∗ is direct algebra from W∗ = 1 − 4d − 2Dη(4η + j0) with D = 1/2 − h.",
"antecedent": "None cited. The physical motivation is Section 2.1 (pages 3 to 5).",
"cost": "Parameters j0, δ∗, σ∗, the enlarged interval I and the complex domain Ω; the order j0 → δ∗, σ∗ → Λ in (B.40); dependence on the sign and size properties of the outer datum Π0 and on P∗ being already large. The offset also enters the final axial matching error (‖Gi − 4η‖ contains a Ckj0 term in the proof of Proposition 4.10), so j0 ≪ εm in the hierarchy of section 4.6.",
"checkable": "With the actual Π0 of (A.21) (or, as a smoke test, the reference inner contribution −(5/2)P∗²f², which has the same parity and sign properties), tabulate H∗, W∗, Z∗ on I for fixed h and several j0 ≤ .05; root-find η0 and compare with −j0/(D + 4); confirm min(−W∗) > 2.8 (digest check: at h = .01, j0 = .05 the minimum over [−1, 1] is 2.871 and η0 = −0.01114); confirm Z∗(η0) > 0; then compute the largest admissible δ∗ and the largest σ∗ giving χ > .99 on {|Z∗| ≤ δ∗}.",
"depends_on": [
"MA.8",
"M4.4"
],
"constrains": [],
"reasons": {
"MA.8": "the sign of Z*(η0) comes from Lemma A.5's datum: analytic, even, Π0 ≤ -(5/2)P*²f², and ηΠ0' > 0.",
"M4.4": "H*, W*, Z* are the axis values of the transport coefficient H_c, the factor W, and the axial source S_n of (4.8), (4.9)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 144"
},
{
"id": "MB.2",
"kind": "move",
"name": "ns-mb-2-steep-holomorphic-swirl-datum-on-the-axis",
"title": "Steep, holomorphic swirl datum on the axis",
"section": "B",
"pages": "144-145",
"refs": [
"pp. 144 to 145, (B.3)",
"p. 147, (B.16)",
"p. 37 (proof of Proposition 4.10)",
"(4.9), p. 26."
],
"statement": "For Λ ≥ 1 define ζ∗ = −LH∗/(H∗² + σ∗²), ξ0 = Λζ∗, ϕ∗ = exp(Λ ∫0^η ζ∗(w) dw) (B.3). The integral is well defined on Ω, ϕ∗ > 0 on the real interval, and ϕ(0, η) = ϕ∗. Consequently ∂η log ϕ∗ = ξ0 and −H∗ξ0 = ΛLχ exactly (the manuscript writes H∗ξ0/(ΛL) = −χ). The amplitude C is chosen after Λ.",
"description": "For Λ ≥ 1 define ζ∗ = −LH∗/(H∗² + σ∗²), ξ0 = Λζ∗, ϕ∗ = exp(Λ ∫0^η ζ∗(w) dw) (B.3). The integral is well defined on Ω, ϕ∗ > 0 on the real interval, and ϕ(0, η) = ϕ∗. Consequently ∂η log ϕ∗ = ξ0 and −H∗ξ0 = ΛLχ exactly (the manuscript writes H∗ξ0/(ΛL) = −χ). The amplitude C is chosen after Λ. OBLIGATION: Makes the angular source Sq = −Wl − h(1 − 2ηU) − Hc(log E)η of (4.9) large and positive where H∗ is not small. This gives p1 = a > 0 on the stress-free region, the bound (B.17), and the rotational branch of (B.19), while keeping ϕ > 0 and analytic in η, as Theorem 4.6(i) and Lemma 5.1 require. It is the axis value ϕ(0, η) specified in the proof of Proposition 4.10, and its Λ fixes the radial scale Y = ΛX and hence Xa = 4/Λ. MECHANISM: The term −Hc(log E)η in Sq is axial transport of angular momentum between η-layers. Prescribing (log ϕ)η ≈ −ΛL/H∗ would make it ≈ ΛL, a large positive source. The regularization H∗/(H∗² + σ∗²) in place of 1/H∗ keeps ϕ∗ holomorphic across the zero of H∗, at the price that the large source becomes ΛLχ and switches off near η0, which is. ANTECEDENT: None cited. REFS: pp. 144 to 145, (B.3); p. 147, (B.16); p. 37 (proof of Proposition 4.10); (4.9), p. 26.",
"obligation": "Makes the angular source Sq = −Wl − h(1 − 2ηU) − Hc(log E)η of (4.9) large and positive where H∗ is not small. This gives p1 = a > 0 on the stress-free region, the bound (B.17), and the rotational branch of (B.19), while keeping ϕ > 0 and analytic in η, as Theorem 4.6(i) and Lemma 5.1 require. It is the axis value ϕ(0, η) specified in the proof of Proposition 4.10, and its Λ fixes the radial scale Y = ΛX and hence Xa = 4/Λ.",
"backward_question": "Can the sign of the angular-momentum source be forced by prescribing the η-dependence of the swirl on the axis alone, and how can the natural prescription (log ϕ)η ∝ −1/H∗, singular where H∗ vanishes, be made holomorphic without losing positivity?",
"mechanism": "The term −Hc(log E)η in Sq is axial transport of angular momentum between η-layers. Prescribing (log ϕ)η ≈ −ΛL/H∗ would make it ≈ ΛL, a large positive source. The regularization H∗/(H∗² + σ∗²) in place of 1/H∗ keeps ϕ∗ holomorphic across the zero of H∗, at the price that the large source becomes ΛLχ and switches off near η0, which is exactly where the axial branch of MB.1 takes over. Physically, the swirl amplitude decreases in the direction of the axial characteristic speed H∗, so axial flow carries fluid from more rapidly rotating layers (Section 2.1). Because the leading source is proportional to Λ, balancing it against radial diffusion forces the radial scale X ~ 1/Λ, which is why the axis problem is posed in Y = ΛX.",
"antecedent": "None cited.",
"cost": "The large parameter Λ (Λ ≥ Λ0, chosen after σ∗). The manuscript notes that ϕ∗ can grow exponentially with Λ, which forces the amplitude condition C ≥ sup over Ω of |ϕ∗| in (B.16) and hence the Λ-dependent threshold C0(Λ). The stress-free region shrinks to X ≤ 4.1/Λ, X-derivative bounds carry factors Λ^{r−1}, and the O(Λ) slope of log ϕ∗ inflates ℓi = log(CE(Xi, ·)), which is why Tsh in (B.33) depends on Λ through Bk.",
"checkable": "Compute ζ∗ and ϕ∗ by quadrature on I for given j0, σ∗, Λ; verify the identity −H∗ξ0 = ΛLχ to rounding error; evaluate |ϕ∗| on a complex strip around I to size the threshold C0(Λ) ≥ sup|ϕ∗| and observe its growth in Λ.",
"depends_on": [
"MB.1",
"M4.4"
],
"constrains": [],
"reasons": {
"MB.1": "uses H* and the regularization σ* chosen there, so χ = H*²/(H*² + σ*²) > .99 where |Z*| ≤ δ*, on the complex domain Ω.",
"M4.4": "the datum targets the term -H_c(log E)_η of the angular source S_q in (4.9), making it ≈ ΛLχ on the axis."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 144-145"
},
{
"id": "MB.3",
"kind": "move",
"name": "ns-mb-3-weighted-analytic-coefficient-space-b-and-the-radial",
"title": "Weighted analytic coefficient space Bρ and the radial inverses (Lemma B.1)",
"section": "B",
"pages": "145-146",
"refs": [
"pp. 145 to 146, (B.4) to (B.10), Lemma B.1."
],
"statement": "In Y = ΛX, for F = Σα Fα(η)Y^α put aαβ = 20^{−α}ρ^{−β}β! C(α + β, β)/((α + 1)²(β + 1)²) and ‖F‖ρ = sup over α, β ≥ 0 and η ∈ I of |∂η^β Fα(η)|/aαβ (B.4); Bρ is complete. Lemma B.1: multiplication is bounded on Bρ; for ν = 1, 2, Jν (the solution G of YGYY + νGY = F that is regular at Y = 0 with G(0) = 0) acts by (JνF)α+1 = Fα/((α + 1)(α + ν)), (JνF)0 = 0 (B.5) and is bounded, as are radial averaging AX(F) = Y^{−1}IF, multiplication by Y, IF = ∫0^Y F dY', and ∂ηI;",
"description": "In Y = ΛX, for F = Σα Fα(η)Y^α put aαβ = 20^{−α}ρ^{−β}β! C(α + β, β)/((α + 1)²(β + 1)²) and ‖F‖ρ = sup over α, β ≥ 0 and η ∈ I of |∂η^β Fα(η)|/aαβ (B.4); Bρ is complete. Lemma B.1: multiplication is bounded on Bρ; for ν = 1, 2, Jν (the solution G of YGYY + νGY = F that is regular at Y = 0 with G(0) = 0) acts by (JνF)α+1 = Fα/((α + 1)(α + ν)), (JνF)0 = 0 (B.5) and is bounded, as are radial averaging AX(F) = Y^{−1}IF, multiplication by Y, IF = ∫0^Y F dY', and ∂ηI; OBLIGATION: The stress-free equations (4.13) have a regular singular point at X = 0 and contain first-order η-derivatives (Hc∂η in the transport, ∂ηAX(U) inside W, η-derivatives of the pressure). An iteration in functions of Y alone loses one η-derivative per step. ANTECEDENT: Named ingredients only: the Leibniz formula, an elementary convolution estimate (B.7), and completeness via uniform convergence of coefficients and derivatives. No classical theorem is cited. (Digest's identification, not the manuscript's: a majorant-series norm of Cauchy-Kovalevskaya type adapted to a regular singular, Fuchsian-type, radial operator.) REFS: pp. 145 to 146, (B.4) to (B.10), Lemma B.1.",
"obligation": "The stress-free equations (4.13) have a regular singular point at X = 0 and contain first-order η-derivatives (Hc∂η in the transport, ∂ηAX(U) inside W, η-derivatives of the pressure). An iteration in functions of Y alone loses one η-derivative per step. Without a space in which \"increasing the radial degree compensates for a parameter derivative\" (Section B.2, p. 145), the contraction for Proposition B.2 does not close, and neither analyticity in η nor regularity at the axis (a power series in X = r²/(2q)) would come out.",
"backward_question": "In which Banach space does inverting the regular singular radial operator gain exactly the one η-derivative that the transport terms cost, so that a fixed-point iteration closes without shrinking the domain?",
"mechanism": "The factor ρ^{−β}β! measures analyticity in η with radius about ρ, the factor 20^{−α} measures analyticity in Y with radius 20, and the binomial C(α + β, β) ties them: by (B.10), moving one unit from radial degree to η-derivative count costs (80/ρ)(i + 1), and the divisor i + 1 produced by one radial integration (or the divisor (α + 1)(α + ν) of Jν) pays for it. The quadratic denominators make Bρ a Banach algebra: in the Leibniz formula the derivative binomials cancel the factorials of the weights, (B.8) (a count of β-element subsets of a set split into two blocks) bounds the remaining binomial ratio by one, and (B.7), proved by splitting the sum at N/2, bounds the convolution of the (α + 1)^{−2} weights. In a mixed product (∂ηF)(DXG), the extra radial degree supplied by Jν is assigned to the factor carrying the η-derivative, while DX = Y∂Y multiplies a coefficient by its degree, which the (α + ν) divisor absorbs.",
"antecedent": "Named ingredients only: the Leibniz formula, an elementary convolution estimate (B.7), and completeness via uniform convergence of coefficients and derivatives. No classical theorem is cited. (Digest's identification, not the manuscript's: a majorant-series norm of Cauchy-Kovalevskaya type adapted to a regular singular, Fuchsian-type, radial operator.)",
"cost": "A fixed small η-radius ρ, later taken strictly below the distance from the working neighborhood to the boundary of Ω so that Cauchy's inequality absorbs the (β + 1)² factor; the fixed Y-radius 20, which must exceed 4.1; algebra constants Csq² and Cρ.",
"checkable": "Exact-arithmetic checks: (B.5) by substitution into YG'' + νG' = F; (B.8) by brute force over small indices; (B.9) and (B.10) as rational identities in the weights (digest check: both identities and bounds hold for all α, β < 40, and the supremum in (B.9) is 80, attained at α = β = 0); (B.7) numerically (digest check: the left side stays below 3.52 for N < 200, against the bound 8Σ i^{−2} = 4π²/3 ≈ 13.16).",
"depends_on": [
"M4.4",
"M4.3"
],
"constrains": [],
"reasons": {
"M4.4": "J_1, J_2 invert the radial viscous operators of the zero-stress equations (4.13), regular at Y = 0, for U and for ϕ.",
"M4.3": "it bounds the radial average A_X of (4.6), which enters (4.13) through V0 and W, together with ∂_η I."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 145-146"
},
{
"id": "MB.4",
"kind": "move",
"name": "ns-mb-4-explicit-leading-swirl-profile-f0-and-its-positivity",
"title": "Explicit leading swirl profile f0 and its positivity window",
"section": "B",
"pages": "146",
"refs": [
"p. 146, (B.11)",
"p. 148 (Φ0 = f0(Yχ))",
"pp. 149 to 150 (use at the endpoint)."
],
"statement": "f0(z) = Σα≥0 (−z/2)^α/(α!(α + 1)!). For 0 ≤ z ≤ 4.1 and t = z/2: f0(z) ≥ 1 − t/2 + t²/12 − t³/144 ≥ 305719/1152000 > .265 and f0(z) ≤ 1 (B.11); the cubic is decreasing on [0, 2.05]. It is the unperturbed angular profile: Φ0 = (1 + T)^{−1}1 = f0(Yχ), the solution regular at Y = 0 with value 1 of 2(YΦYY + 2ΦY) = −χΦ. The companion quantity f0 + zf0' enters (B.19) through the bound f0 + zf0' ≤ 1 − t + t²/4 − t³/36 + t⁴/576.",
"description": "f0(z) = Σα≥0 (−z/2)^α/(α!(α + 1)!). For 0 ≤ z ≤ 4.1 and t = z/2: f0(z) ≥ 1 − t/2 + t²/12 − t³/144 ≥ 305719/1152000 > .265 and f0(z) ≤ 1 (B.11); the cubic is decreasing on [0, 2.05]. It is the unperturbed angular profile: Φ0 = (1 + T)^{−1}1 = f0(Yχ), the solution regular at Y = 0 with value 1 of 2(YΦYY + 2ΦY) = −χΦ. The companion quantity f0 + zf0' enters (B.19) through the bound f0 + zf0' ≤ 1 − t + t²/4 − t³/36 + t⁴/576. OBLIGATION: Division by ϕ in the first equation of (B.15), and the use of log Φ in l and (log E)η, are legitimate only if Φ > 0 on the whole stress-free interval; (B.11) with (B.13) gives Φ ≥ c0 > 0 on 0 ≤ Y ≤ 4.1 for large Λ. f0 also fixes the rotational shear at the edge, a = −2YΦY/Φ ≈ −2zf0'(z)/f0(z) at Y = 4. MECHANISM: When the large source ΛLχ dominates, the angular equation in Y becomes a linear regular singular ODE whose coefficient χ(η) does not depend on Y; ANTECEDENT: None cited; alternating-series bounds are used directly. (Digest's identification, not the manuscript's: f0(z) = J1(2√t)/√t and f0 + zf0' = J0(2√t) with t = z/2, Bessel functions of the first kind.) REFS: p. 146, (B.11); p. 148 (Φ0 = f0(Yχ)); pp. 149 to 150 (use at the endpoint).",
"obligation": "Division by ϕ in the first equation of (B.15), and the use of log Φ in l and (log E)η, are legitimate only if Φ > 0 on the whole stress-free interval; (B.11) with (B.13) gives Φ ≥ c0 > 0 on 0 ≤ Y ≤ 4.1 for large Λ. f0 also fixes the rotational shear at the edge, a = −2YΦY/Φ ≈ −2zf0'(z)/f0(z) at Y = 4.",
"backward_question": "When axial transport of angular momentum dominates the source, what linear equation does the swirl obey near the axis, and on what radial interval is its explicit solution still positive while its logarithmic slope already exceeds the viscous threshold 2?",
"mechanism": "When the large source ΛLχ dominates, the angular equation in Y becomes a linear regular singular ODE whose coefficient χ(η) does not depend on Y; its regular solution is a power series with alternating coefficients of decreasing magnitude on the relevant range, so partial sums bound it from both sides. The cubic partial sum equals 305719/1152000 at t = 2.05, and since 0 ≤ χ ≤ 1 the argument z = Yχ stays in [0, 4.1]. The edge Y = 4 lies beyond the point where −2zf0'/f0 first reaches 2 (digest computation: z ≈ 2.8916, the first zero of f0 + zf0') and well before f0 vanishes (digest computation: first zero at z ≈ 7.341).",
"antecedent": "None cited; alternating-series bounds are used directly. (Digest's identification, not the manuscript's: f0(z) = J1(2√t)/√t and f0 + zf0' = J0(2√t) with t = z/2, Bessel functions of the first kind.)",
"cost": "Caps the stress-free analytic region at Y ≤ 4.1 and places the stress activation at Y = 4 (X0 = 4/Λ, which is Xa of Proposition 4.10); forces t̄ with 4e^{2t̄} < 4.1 and tc with 4e^{tc} < 4.1 so that later cutoffs stay inside the analytic region.",
"checkable": "Evaluate f0 by its series (or as J1(√(2z))/√(z/2)) on [0, 4.1] and confirm min > .265 (digest check: minimum .27111 at z = 4.1, maximum 1 at z = 0); confirm in exact arithmetic that the cubic partial sum at t = 41/20 equals 305719/1152000; confirm symbolically that f0 solves 2(zf'' + 2f') + f = 0 with f(0) = 1.",
"depends_on": [
"MB.2",
"M4.4",
"MB.3"
],
"constrains": [],
"reasons": {
"MB.2": "the large source ΛLχ from the steep axis datum reduces the angular equation to 2(YΦ_YY + 2Φ_Y) = -χΦ, solved by f0(Yχ).",
"M4.4": "that equation is the leading part of the angular zero-stress equation (4.13) in the variable Y = ΛX.",
"MB.3": "Φ0 = (1 + T)^{-1}1 is written with T = J_2χ/2, the radial inverse of Lemma B.1."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 146"
},
{
"id": "MB.5",
"kind": "move",
"name": "ns-mb-5-proposition-b-2-the-analytic-stress-free-axis-profile-by",
"title": "Proposition B.2, the analytic stress-free axis profile by contraction",
"section": "B",
"pages": "146-148",
"refs": [
"pp. 146 to 148, Proposition B.2, (B.12) to (B.16)",
"Theorem 4.6(i) to (ii), p. 33",
"Proposition 4.10(i), p. 36",
"(4.4) to (4.5), p. 25",
"Lemma 5.1, p. 47."
],
"statement": "With the axis data of Section B.1 there are Λ0 and, for each Λ ≥ Λ0, a threshold C0(Λ) such that every C ≥ C0(Λ) admits an analytic profile with vanishing leading residual stress on 0 ≤ Y = ΛX ≤ 4.1 of the form ϕ = ϕ∗Φ, U = U∗ + Λ^{−1}u, Π = Π0 + Λ^{−1}I(g²Φ²), g = ϕ∗/C (B.12), with Φ(0, η) = 1, u(0, η) = 0, analytic in Y and η on a common neighborhood of [0, 4.1] × I, and |∂Y^r ∂η^s (Φ − f0(Yχ), u + YZ∗/(2L))| ≤ Cr,s/Λ (B.13), uniformly in large Λ and C ≥ C0(Λ) (for X-derivatives the bound is.",
"description": "With the axis data of Section B.1 there are Λ0 and, for each Λ ≥ Λ0, a threshold C0(Λ) such that every C ≥ C0(Λ) admits an analytic profile with vanishing leading residual stress on 0 ≤ Y = ΛX ≤ 4.1 of the form ϕ = ϕ∗Φ, U = U∗ + Λ^{−1}u, Π = Π0 + Λ^{−1}I(g²Φ²), g = ϕ∗/C (B.12), with Φ(0, η) = 1, u(0, η) = 0, analytic in Y and η on a common neighborhood of [0, 4.1] × I, and |∂Y^r ∂η^s (Φ − f0(Yχ), u + YZ∗/(2L))| ≤ Cr,s/Λ (B.13), uniformly in large Λ and C ≥ C0(Λ) (for X-derivatives the bound is. OBLIGATION: This is the inner region of Theorem 4.6: (4.13) holds and T0 = 0 on 0 ≤ X ≤ Xa (Theorem 4.6(ii), Proposition 4.10(i)). ANTECEDENT: As cited in the text: a strict contraction and its unique fixed point, Cauchy's inequality, and Cauchy estimates, in the norm of Lemma B.1. The inversion of 1 + T is a Neumann series, not named as such. (Digest's identification, not the manuscript's: the resolvent series has Volterra-type factorial decay.) REFS: pp. 146 to 148, Proposition B.2, (B.12) to (B.16); Theorem 4.6(i) to (ii), p. 33; Proposition 4.10(i), p. 36; (4.4) to (4.5), p. 25; Lemma 5.1, p. 47.",
"obligation": "This is the inner region of Theorem 4.6: (4.13) holds and T0 = 0 on 0 ≤ X ≤ Xa (Theorem 4.6(ii), Proposition 4.10(i)). F = ϕ/C, U, Π and V0/X are analytic in X (power series in r²/(2q)), hence smooth at the axis, and with E = √(2X)ϕ/C and (4.4) to (4.5) the Cartesian field is smooth across r = 0 (Definition 3.2, Theorem 4.6(i)). The profiles are analytic in η on one complex neighborhood (Theorem 4.6(i), used by Lemma 5.1), and ϕ > 0 gives E > 0 for X > 0.",
"backward_question": "Can the same large parameter that steepens the swirl in η also rescale the radius so that the nonlinear stress-free system becomes a 1/Λ perturbation of an explicitly solvable linear problem, and can the pressure's coupling to an exponentially large swirl datum be neutralized by the still-free amplitude C?",
"mechanism": "In Y the stress-free system becomes 2(YΦYY + 2ΦY) = −χΦ + Λ^{−1}R1 and 2(YuYY + uY) = −Z∗/L + Λ^{−1}R2, where R1, R2 are explicit polynomials in Φ, u, their DX and η derivatives, W = W∗ + Λ^{−1}B, Hc = H∗ + Λ^{−1}du, and p = I(g²Φ²). The only products with both an unintegrated η-derivative and a DX derivative are (∂ηAX(u))DXΦ and (∂ηAX(u))DXu, controlled by (B.6); ∂ηp is bounded because ∂ηI is, and DXp = Yg²Φ². So (Φ, u) ↦ JνRi is bounded and locally Lipschitz on balls of Bρ². The angular term −χΦ is of order one, not small, but T = J2χ/2 raises the minimal radial degree by one and divides by (b + 1)(b + 2), so ‖T^k‖ ≤ (40Mχ)^k/(k!(k + 1)!) and Σ(−T)^k inverts 1 + T whatever the size of χ. The map (Φ, u) ↦ (Φ0 + (1 + T)^{−1}J2R1/(2Λ), u0 + J1R2/(2Λ)), with (Φ0, u0) = (f0(Yχ), −YZ∗/(2L)), is then a strict contraction on a fixed ball for large Λ, with fixed point within C/Λ of the center. The pressure couples to ϕ∗, which can be exponentially large in Λ; (B.16) gives |g| ≤ 1 on the complex neighborhood, so Cauchy's inequality bounds all η-derivatives of g uniformly in both large parameters (the manuscript stresses that this bound must hold on a complex neighborhood). Finally Σα C(α + β, β)(R/20)^α = (1 − R/20)^{−β−1} turns the coefficient norm into analyticity on |Y| ≤ R for any 4.1 < R < 20 with η-radius below ρ(1 − R/20); Cauchy estimates give (B.13); real data and uniqueness of the fixed point give a real solution; (B.11) gives Φ > 0.",
"antecedent": "As cited in the text: a strict contraction and its unique fixed point, Cauchy's inequality, and Cauchy estimates, in the norm of Lemma B.1. The inversion of 1 + T is a Neumann series, not named as such. (Digest's identification, not the manuscript's: the resolvent series has Volterra-type factorial decay.)",
"cost": "Λ ≥ Λ0; C ≥ C0(Λ) ≥ sup over Ω of |ϕ∗|, so C is chosen after Λ and may be exponentially large in Λ; ρ strictly below the distance to the boundary of Ω; the solution exists only for Y ≤ 4.1; the smaller common complex neighborhood fixed here is the one Corollary B.6 later preserves.",
"checkable": "Run the fixed-point iteration numerically on truncated Taylor coefficients in Y (coefficient rule (B.5) for J1, J2), with η discretized spectrally (Chebyshev), for several moderately large Λ and C ≥ max over a complex strip of |ϕ∗|. Check that sup|Φ − f0(Yχ)| and sup|u + YZ∗/(2L)| on [0, 4.1] × [−1, 1] scale like 1/Λ as in (B.13), that the Taylor coefficients decay at least like 20^{−α}(α + 1)^{−2} as membership in Bρ requires, and that Φ > 0.",
"depends_on": [
"MB.3",
"MB.4",
"MB.2",
"M4.4"
],
"constrains": [],
"reasons": {
"MB.3": "the fixed point is found in Lemma B.1's space B_ρ, whose radial inverses and product bound (B.6) absorb the η-derivatives of (4.13).",
"MB.4": "the contraction is centered at Φ0 = f0(Yχ), with 1 + T inverted by its factorially decaying series.",
"MB.2": "the axis data are ϕ(0, η) = ϕ*, and C ≥ sup|ϕ*| on Ω (B.16) tames the pressure coupling through g = ϕ*/C.",
"M4.4": "the system solved is the zero-stress equations (4.13), so T0 = 0 on the stress-free region."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 146-148"
},
{
"id": "MB.6",
"kind": "move",
"name": "ns-mb-6-proposition-b-3-positive-angular-source-and-the-two",
"title": "Proposition B.3, positive angular source and the two-branch endpoint inequality",
"section": "B",
"pages": "148-150",
"refs": [
"pp. 148 to 150, Proposition B.3, (B.17) to (B.21)",
"Proposition 4.10(ii), p. 37",
"Theorem 4.6(iii), p. 33",
"Section 2.1, p. 5."
],
"statement": "After increasing Λ and then C0(Λ): Φ ≥ c0 > 0 on [0, 4.1] × [−1, 1]; Sq ≥ 2.5 + .95ΛLχ (B.17); with p1 = ps,1 = XQs/L, p2 = ps,2 = XNs/(LE), ns = Ns/L, one has p1/X ≥ c1 > 0, 0 < p1 ≤ C1, ns = −2UX = Z∗/L + O(Λ^{−1}) on 0 < X ≤ 4.1/Λ (B.18); at X0 = 4/Λ, p1 + p2²/p1 > 2 + cex (B.19), for example with cex = .2; Φ, log Φ, u, p1, ns have η-derivative bounds of every fixed order uniform in C ≥ C0(Λ).",
"description": "After increasing Λ and then C0(Λ): Φ ≥ c0 > 0 on [0, 4.1] × [−1, 1]; Sq ≥ 2.5 + .95ΛLχ (B.17); with p1 = ps,1 = XQs/L, p2 = ps,2 = XNs/(LE), ns = Ns/L, one has p1/X ≥ c1 > 0, 0 < p1 ≤ C1, ns = −2UX = Z∗/L + O(Λ^{−1}) on 0 < X ≤ 4.1/Λ (B.18); at X0 = 4/Λ, p1 + p2²/p1 > 2 + cex (B.19), for example with cex = .2; Φ, log Φ, u, p1, ns have η-derivative bounds of every fixed order uniform in C ≥ C0(Λ). OBLIGATION: In the stress-free region ps = s = (a, −bs), so vs = a + bs²/a = p1 + p2²/p1, and (B.19) is exactly vs > 2 + cex at the inner annulus edge. Since the stress is born parallel to the shear there (Theorem 4.6(iii)), this is the viscous inequality of the admissible stress cone at the edge, stated in Proposition 4.10(ii) as a(Xa) > 0 and vs(Xa) > 2 + cex. The source bound gives p1 = a > 0 (so ts and vs are defined) and the lower bounds that Lemma B.4 propagates. ANTECEDENT: Young's inequality and alternating-series remainder bounds, used directly; nothing classical cited. REFS: pp. 148 to 150, Proposition B.3, (B.17) to (B.21); Proposition 4.10(ii), p. 37; Theorem 4.6(iii), p. 33; Section 2.1, p. 5.",
"obligation": "In the stress-free region ps = s = (a, −bs), so vs = a + bs²/a = p1 + p2²/p1, and (B.19) is exactly vs > 2 + cex at the inner annulus edge. Since the stress is born parallel to the shear there (Theorem 4.6(iii)), this is the viscous inequality of the admissible stress cone at the edge, stated in Proposition 4.10(ii) as a(Xa) > 0 and vs(Xa) > 2 + cex. The source bound gives p1 = a > 0 (so ts and vs are defined) and the lower bounds that Lemma B.4 propagates.",
"backward_question": "At the radius where the stress will be switched on, can vs > 2 be guaranteed for every η, and which free parameter enlarges the rotational part a, and which the axial part bs²/a, of vs?",
"mechanism": "For the source, (B.20) follows from Φ ≈ f0(Yχ) and |H∗χ'| ≤ 2‖H∗'‖∞χ; then −Hc(log ϕ)η ≈ ΛLχ with errors absorbed by Young's inequality (allocating .05ΛLχ), and with l = 1 + DX log Φ, −W∗ > 2.8 and |h(1 − 2ηU)| ≤ 10h ≤ .1 one gets (B.17) without dividing by χ near the zero of H∗. Qs > 0 follows from the positive representation Qs = ∫0^X X'Φ(ΛX')Sq dX'/(X²Φ(ΛX)). Integrating the stress-free equations from the axis gives p1 = a = −2YΦY/Φ and ns = −2uY. At Y = 4 there are two branches. If χ > .99, then t = 2χ ∈ (1.98, 2] and f0 + zf0' ≤ 1 − t + t²/4 − t³/36 + t⁴/576 < −.18 (the quartic equals −75535511/400000000 < −.188 at t = 1.98 and decreases on [1.98, 2]), so a = −2zf0'/f0 = 2 − 2(f0 + zf0')/f0 > 2.36 and p1 > 2.3 for large Λ: the rotational shear alone clears the threshold. If χ ≤ .99, then |Z∗| > δ∗ by (B.2), so |ns| ≥ δ∗/2, and at the endpoint |p2| = C(2/Λ)^{1/2}|ns|/(ϕ∗Φ) grows linearly in C for fixed Λ while p1 ≤ C1; enlarging C0(Λ) gives p2²/p1 > 2.3: a small swirl amplitude 1/C lets the axial shear dominate. This is the analytic form of Section 2.1's statement that the radial shear of axial velocity supplies the amplification near the middle plane while the rotational mechanism suffices farther away.",
"antecedent": "Young's inequality and alternating-series remainder bounds, used directly; nothing classical cited.",
"cost": "A further increase of Λ and of C0(Λ) (C must beat a Λ-dependent bound on ϕ∗Φ at the endpoint); the constants c0, c1, C1; the margin cex = .2, which reappears as vs > 2 + cex in Proposition 4.10(ii).",
"checkable": "Exact rational check that the quartic partial sum at t = 99/50 equals −75535511/400000000; evaluate a(z) = −2zf0'(z)/f0(z) on [3.96, 4] (digest check: 3.326 to 3.389, well above the proved 2.36); symbolic check that p2 = XNs/(LE) with E = √(2X)ϕ∗Φ/C equals C(X/2)^{1/2}ns/(ϕ∗Φ), which is C(2/Λ)^{1/2}ns/(ϕ∗Φ) at X = 4/Λ; with the numerical profile of MB.5, evaluate p1 + p2²/p1 at Y = 4 over η ∈ [−1, 1] for increasing C.",
"depends_on": [
"MB.5",
"MB.1",
"MB.4",
"M4.7"
],
"constrains": [],
"reasons": {
"MB.5": "reads all bounds off Proposition B.2's stress-free profile and its closeness (B.13) to f0(Yχ) and -YZ*/(2L).",
"MB.1": "the two branches at Y = 4 are the split χ > .99 (rotational) or |Z*| > δ* (axial shear), with -W* > 2.8 in the source.",
"MB.4": "on χ > .99 the bound on f0 + zf0' gives a = -2zf0'/f0 > 2.36 at Y = 4, and (B.11) gives Φ ≥ c0 > 0.",
"M4.7": "with p_s = s in the stress-free region, p1 + p2²/p1 is v_s of (4.20), so (B.19) is v_s > 2 + c_ex at the edge."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 148-150"
},
{
"id": "MB.7",
"kind": "move",
"name": "ns-mb-7-lemma-b-4-reference-continuation-with-frozen-logarithmic",
"title": "Lemma B.4, reference continuation with frozen logarithmic slopes",
"section": "B",
"pages": "150-151",
"refs": [
"pp. 150 to 151, Lemma B.4, (B.22) to (B.25)",
"(A.5), p. 129."
],
"statement": "Let X0 = 4/Λ, Xb = 100 (a local radius, not the annulus edge of Theorem 4.6), Xi = 110; fix t̄ > 0 with 4e^{2t̄} < 4.1; use the smooth step σ of (A.5); put y = log(X/X0) and 0 < t1 ≤ t̄. The reference (ϕr, Ur) equals the analytic profile for y ≤ t1; on t1 < y < 2t1, ∂y log ϕr = [1 − σ((y − t1)/t1)]DX log ϕnat and ∂yUr = [1 − σ((y − t1)/t1)]DXUnat (B.22); afterwards both are constant in log X; pressure, Qs and Ns are integrated from the axis with datum Π0.",
"description": "Let X0 = 4/Λ, Xb = 100 (a local radius, not the annulus edge of Theorem 4.6), Xi = 110; fix t̄ > 0 with 4e^{2t̄} < 4.1; use the smooth step σ of (A.5); put y = log(X/X0) and 0 < t1 ≤ t̄. The reference (ϕr, Ur) equals the analytic profile for y ≤ t1; on t1 < y < 2t1, ∂y log ϕr = [1 − σ((y − t1)/t1)]DX log ϕnat and ∂yUr = [1 − σ((y − t1)/t1)]DXUnat (B.22); afterwards both are constant in log X; pressure, Qs and Ns are integrated from the axis with datum Π0. OBLIGATION: The analytic solution exists only for Y ≤ 4.1, but the profile must reach X ≈ XRe^{−5}, a radius growing like C^{10}. The shear reduction of Proposition B.5 needs a comparison profile on the whole interval whose integrated coefficients ps,r are uniformly bounded and signed, with vr > 2 + c, so that the stress created by lowering the shear lies in the admissible cone. MECHANISM: Cutting the logarithmic slopes of ϕ and U to zero and then holding the fields constant in log X means nothing grows, however long the interval: Ur stays within O(Λ^{−1}) + o(1) of U∗ (radial averaging is a. ANTECEDENT: None cited; the smooth step (A.5) is the manuscript's own. REFS: pp. 150 to 151, Lemma B.4, (B.22) to (B.25); (A.5), p. 129.",
"obligation": "The analytic solution exists only for Y ≤ 4.1, but the profile must reach X ≈ XRe^{−5}, a radius growing like C^{10}. The shear reduction of Proposition B.5 needs a comparison profile on the whole interval whose integrated coefficients ps,r are uniformly bounded and signed, with vr > 2 + c, so that the stress created by lowering the shear lies in the admissible cone.",
"backward_question": "How can a profile known only on a short analytic interval be carried out to arbitrarily large radius with every quantity in the cone test bounded uniformly in the length of the interval and in the amplitude?",
"mechanism": "Cutting the logarithmic slopes of ϕ and U to zero and then holding the fields constant in log X means nothing grows, however long the interval: Ur stays within O(Λ^{−1}) + o(1) of U∗ (radial averaging is a contraction in sup norm, so AX(Ur) does too, independently of the interval length), log ϕr stays a bounded distance from log ϕ∗, and the pressure moves only by O(C^{−2}) because E ∝ 1/C. The source keeps its large gradient part LΛχ (replacing H∗ by Hc,r costs Cσ∗√χ + o(1), absorbed) and its constant part from −W∗ > 2.8. Because the analytic profile has p1 = a > 0, its ϕ slope is nonpositive, so freezing it gives lr ≤ 1. The equations (B.25) are linear with regular initial values; with lr ≤ 1 and either Sq,r ≥ .94LΛχ or Sq,r ≥ 2.4, integrating factors give the exponential and the linear lower bounds for p1,r, keeping p1,r above 2.3 on χ > .99 and above 3 from X = 100. On χ ≤ .99 the axial source keeps |ns,r| bounded below and p2,r = Xns,r/Er grows with C, so vr > 2 + c everywhere.",
"antecedent": "None cited; the smooth step (A.5) is the manuscript's own.",
"cost": "The width t1 (0 < t1 ≤ t̄) and t̄ with 4e^{2t̄} < 4.1; the fixed local radii X0, 100, 110; the order Λ, then C, then t1; the constant c in vr > 2 + c.",
"checkable": "From the numerical axis profile of MB.5, integrate (B.22) and then (B.25) in y up to log(110/X0); check Sq,r ≥ .94LΛχ + 2.4, lr ≤ 1, vr > 2 + c, and p1,r > 3 on [100, 110]; check the two comparison inequalities pointwise.",
"depends_on": [
"MB.6",
"MB.5",
"M4.4"
],
"constrains": [],
"reasons": {
"MB.6": "propagates Proposition B.3's source bound, p1 > 0, and the endpoint inequality v > 2 + c from X0 out to X_i = 110.",
"MB.5": "the reference equals the analytic profile for y ≤ t1 and then freezes its logarithmic slopes.",
"M4.4": "Q_s, N_s are integrated from the axis by (4.9), giving the linear equations (B.25) for p1,r and n_s,r."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 150-151"
},
{
"id": "MB.8",
"kind": "move",
"name": "ns-mb-8-proposition-b-5-first-part-flat-activation-of-the-stress",
"title": "Proposition B.5, first part: flat activation of the stress by shear reduction",
"section": "B",
"pages": "151-153",
"refs": [
"pp. 151 to 153, Proposition B.5, (B.26) to (B.31)",
"Lemma A.9, (A.47), pp. 141 to 142",
"Proposition 4.10(ii), (4.33), p. 37",
"Theorem 4.6(ii) to (iv), p. 33",
"Proposition C.3, (C.18) to (C.19), pp. 163 to 164."
],
"statement": "Fix a large C; take t∗ ≤ t̄ so that Lemma B.4 holds uniformly for 0 < t1 ≤ t∗, and let Vmax bound vr over this family. For 0 < κ0 < 1/2 set, on 0 < y < t1, ea = (1 − κ0)σ(y/t1), κ = 1 − ea, a = κp1,r, DXU = −κXns,r/2, ∂y log ϕ = −κp1,r/2 (B.26). Then exactly ∂y(log ϕ − log ϕr) = eap1,r/2 and ∂y(U − Ur) = eaXns,r/2 (B.27); ps − ps,r = O(yea) and Er/E = 1 + O(yea) in values and η-derivatives (B.28); ts = (p2,r/p1,r)(Er/E), vs = κvr + O(yea), Pc = vr + O(yea), Jc = O(yea) (B.29).",
"description": "Fix a large C; take t∗ ≤ t̄ so that Lemma B.4 holds uniformly for 0 < t1 ≤ t∗, and let Vmax bound vr over this family. For 0 < κ0 < 1/2 set, on 0 < y < t1, ea = (1 − κ0)σ(y/t1), κ = 1 − ea, a = κp1,r, DXU = −κXns,r/2, ∂y log ϕ = −κp1,r/2 (B.26). Then exactly ∂y(log ϕ − log ϕr) = eap1,r/2 and ∂y(U − Ur) = eaXns,r/2 (B.27); ps − ps,r = O(yea) and Er/E = 1 + O(yea) in values and η-derivatives (B.28); ts = (p2,r/p1,r)(Er/E), vs = κvr + O(yea), Pc = vr + O(yea), Jc = O(yea) (B.29). OBLIGATION: Theorem 4.6 at the inner edge Xa = X0: T0 = 0 up to Xa and nonzero just after (part (ii)); T0 flat at Xa, so its extension by zero is smooth; the unit direction n extends smoothly to Xa and is parallel to (a, −bs) there, with the directional margin (4.26) on the inner collar (part (iii)); ANTECEDENT: Lemma A.9 (pp. 141 to 142), the quadratic cone test of Lemma 4.5, and the moment formulas (4.16) of Lemma 4.3; nothing classical cited. REFS: pp. 151 to 153, Proposition B.5, (B.26) to (B.31); Lemma A.9, (A.47), pp. 141 to 142; Proposition 4.10(ii), (4.33), p. 37; Theorem 4.6(ii) to (iv), p. 33; Proposition C.3, (C.18) to (C.19), pp. 163 to 164.",
"obligation": "Theorem 4.6 at the inner edge Xa = X0: T0 = 0 up to Xa and nonzero just after (part (ii)); T0 flat at Xa, so its extension by zero is smooth; the unit direction n extends smoothly to Xa and is parallel to (a, −bs) there, with the directional margin (4.26) on the inner collar (part (iii)); the weighted bounds (4.27) with ζ comparable to e^{−t1²/ya²} (part (iv)); and the factorization (4.33) of Proposition 4.10(ii). Proposition C.3 derives these conclusions directly from (B.30) and (B.31).",
"backward_question": "How can the leading stress be switched on from zero smoothly, flatly, and already strictly inside the admissible cone, without disturbing the profile values and cumulative integrals on which the outer fields depend?",
"mechanism": "In the stress-free region the integrated inviscid vector equals the shear, ps = s, so T0 = F(ps − s) = 0. The stress is switched on by lowering the shear, not by changing the sources: the actual shear is prescribed as κ(p1,r, p2,rEr/E), a fraction κ = 1 − ea of the reference's integrated vector (which equals the reference shear while the reference is still stress-free). The vector ps depends only on profile values and cumulative radial integrals (the identities (4.16)), and the profile values differ from the reference by integrals of ea, which are O(yea); hence ps stays at ps,r up to O(yea) while s drops by the factor κ, and T0 = F·ea·ps,r + O(yea). The stress is therefore born along the old shear direction, where Jc = 0, the most interior direction for the quadratic cone test: the ratio of (vs − 2)+Jc² to (Pc − vs)² is at most Cy². The common factor κ cancels from ts = −bs/a, so no inverse power of κ0 enters the error constants. The flat step makes ea vanish to infinite order at X0, and Lemma A.9 (the substitution u = δ/(1 + δ²v)^{1/2}) shows that ea-weighted primitives are ea times y³ times smooth functions; all field differences lie in eay³C∞ (moments and pressure in eay⁶C∞), a class closed under products, smooth compositions and reciprocals of nonvanishing fields, so division by ea is smooth.",
"antecedent": "Lemma A.9 (pp. 141 to 142), the quadratic cone test of Lemma 4.5, and the moment formulas (4.16) of Lemma 4.3; nothing classical cited.",
"cost": "κ0 ∈ (0, 1/2) and the activation width t1, chosen in the order C, then κ0 (small relative to Vmax and the family constants), then t1; the same t1 becomes the inner exponent of the global weight ζ = exp(−t1²/ya² − 4/yb²) in (C.18); radial derivatives of the narrow cutoffs can be large (only η-derivatives are controlled uniformly).",
"checkable": "With numerical reference data at X0 (from MB.5 and MB.7), integrate (B.26) and (B.27) on a fine y-grid in (0, t1) using σ from (A.5); compute ps via (4.16), s via (4.11), and ts, vs, Pc, Jc via (4.20); verify T0/ea → F(X0)ps,r(X0), Pc − vs ≥ cea, and |Jc|/(yea) bounded. Verify Lemma A.9's factorization numerically: y^{−3}(1/ea(y))∫0^y ea(u)b(u)du → b(0)/(2t1²) as y → 0, a consequence of B(0, η) = b(0, η)/c in (A.47) (digest check with t1 = .3, κ0 = .25, b = 1 + 2u: 5.657 at y = .01 and 5.609 at y = .005, approaching 5.556 at rate O(y)); and σ(y/t1)e^{t1²/y²} → e as y → 0, so ga(0) = (1 − κ0)e.",
"depends_on": [
"MB.7",
"M4.5",
"MA.13",
"M4.7"
],
"constrains": [],
"reasons": {
"MB.7": "the shear is prescribed as the fraction κ = 1 - e_a of Lemma B.4's reference, whose p_s,r is bounded with v_r > 2 + c.",
"M4.5": "p_s depends only on values and cumulative integrals (4.16), so O(ye_a) value changes keep p_s = p_s,r + O(ye_a) while s drops by κ.",
"MA.13": "Lemma A.9 with c = t1², j = 0 makes e_a-weighted primitives e_a y³ times smooth factors, giving (B.30) and (B.31).",
"M4.7": "the stress is born along the shear, with J_c = O(ye_a) and P_c - v_s ≥ ce_a, inside Lemma 4.5's quadratic cone test."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 151-153"
},
{
"id": "MB.9",
"kind": "move",
"name": "ns-mb-9-proposition-b-5-second-part-small-shear-continuation-to",
"title": "Proposition B.5, second part: small-shear continuation to Xi with the barrier p1 > 2",
"section": "B",
"pages": "153",
"refs": [
"p. 153 (proof of Proposition B.5)",
"Proposition 4.10(ii) and its proof, p. 37."
],
"statement": "After the activation, keep (B.26) with κ = κ0 through the reference cutoff and the constant-slope interval; with κ0 small relative to Vmax and the family constants, then t1 small, (B.29) gives Pc > 2 + c/2 and vs < 1, so the strict relaxed cone holds regardless of the size of Jc. At X = 100, multiply the axial prescription for DXU by a smooth factor β decreasing from 1 to 0 on a short logarithmic interval (Pc = p1,r + βp2,r²/p1,r + o(1) > 2, vs < 1).",
"description": "After the activation, keep (B.26) with κ = κ0 through the reference cutoff and the constant-slope interval; with κ0 small relative to Vmax and the family constants, then t1 small, (B.29) gives Pc > 2 + c/2 and vs < 1, so the strict relaxed cone holds regardless of the size of Jc. At X = 100, multiply the axial prescription for DXU by a smooth factor β decreasing from 1 to 0 on a short logarithmic interval (Pc = p1,r + βp2,r²/p1,r + o(1) > 2, vs < 1). OBLIGATION: Proposition 4.10(ii) requires a > 0, Pc > 2 and vs < U(Pc, Jc) on all of (Xa, Xh]. The state at Xi (a = .8, so l = .6, the angular-momentum slope of the reference power law E ∝ X^{1/10}, and U constant in X) is the endpoint of the first continuation from Proposition B.5 as listed in the proof of Proposition 4.10, and it is the starting state from which (B.34) can reach the outer reference profile. ANTECEDENT: A barrier argument for a scalar ODE (the manuscript calls the same device a barrier on p. 155); nothing classical cited. REFS: p. 153 (proof of Proposition B.5); Proposition 4.10(ii) and its proof, p. 37.",
"obligation": "Proposition 4.10(ii) requires a > 0, Pc > 2 and vs < U(Pc, Jc) on all of (Xa, Xh]. The state at Xi (a = .8, so l = .6, the angular-momentum slope of the reference power law E ∝ X^{1/10}, and U constant in X) is the endpoint of the first continuation from Proposition B.5 as listed in the proof of Proposition 4.10, and it is the starting state from which (B.34) can reach the outer reference profile.",
"backward_question": "Once the stress exists, what is the weakest condition that can be maintained over a long radial interval, and to what normalized state must the profile be steered so that it can be glued to the outer power law?",
"mechanism": "With the shear held small (vs < 1), the relaxed cone (4.21) collapses to the single scalar inequality Pc > 2, because U(Pc, Jc) > 2 whenever Pc > 2. Pc stays large because it is essentially the reference's vr and the integrated angular coefficient p1 keeps growing under a positive source. The axial shear is then turned off (bs = 0, so ts = 0 and Pc = p1), and a is steered to .8 = 2 − 2(.6), where .6 = 1/2 + 1/10 is the slope l of the reference power law. The barrier uses the scalar equation DXp1 = XSq/L − lp1, which follows from (4.9) and p1 = XQs/L.",
"antecedent": "A barrier argument for a scalar ODE (the manuscript calls the same device a barrier on p. 155); nothing classical cited.",
"cost": "The condition κ0 sup p1,r < .8; the two final transitions, whose total logarithmic width ωfin enters the matching error through (B.32); the fixed radii 100 and 110.",
"checkable": "Continue the numerical integration of MB.8 through the κ = κ0 stage, the β cutoff at X = 100, and the interpolation of a to .8, up to X = 110, recomputing ps and the cone coordinates from (4.16), (4.11), (4.20); confirm Pc > 2 and vs < 1 throughout, and p1 > 2, a = .8, DXU = 0 at X = 110. Arithmetic: .6 × 2.8 = 1.68, and X − 1.2 > 0 on [100, 110].",
"depends_on": [
"MB.8",
"MB.7",
"M4.7",
"M4.4"
],
"constrains": [],
"reasons": {
"MB.8": "continues the prescription (B.26) with κ = κ0, whose estimates (B.29) give P_c > 2 + c/2 and v_s < 1.",
"MB.7": "Lemma B.4's reference gives v_r ≤ V_max and p1,r > 3 on 100 ≤ X ≤ 110 for the final transitions.",
"M4.7": "with v_s < 1 and P_c > 2 the relaxed cone (4.21) holds whatever J_c, since U(P_c, J_c) > 2 when P_c > 2.",
"M4.4": "the barrier p1 > 2 uses the scalar equation D_X p1 = XS_q/L - lp1 obtained from (4.9)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 153"
},
{
"id": "MB.10",
"kind": "move",
"name": "ns-mb-10-corollary-b-6-a-quarantined-analytic-collar",
"title": "Corollary B.6, a quarantined analytic collar",
"section": "B",
"pages": "153",
"refs": [
"p. 153, Corollary B.6",
"Theorem 4.6(i), p. 33",
"Appendix C opening, p. 158",
"Proposition C.3, p. 164",
"Lemma 5.1, p. 47."
],
"statement": "There is tc > 0 with tc < t1 and 4e^{tc} < 4.1 such that E/√(2X), U, V0/X, Π are smooth in (X, η) through X = 0 on [0, X0e^{tc}] × [−1, 1] and analytic in η on one complex neighborhood, every fixed radial derivative being analytic on the same neighborhood and bounded on a smaller one; on X0 < X ≤ X0e^{tc} the admissible stress cone and (B.30) hold; all later profile modifications are supported strictly to the right of X0e^{tc}.",
"description": "There is tc > 0 with tc < t1 and 4e^{tc} < 4.1 such that E/√(2X), U, V0/X, Π are smooth in (X, η) through X = 0 on [0, X0e^{tc}] × [−1, 1] and analytic in η on one complex neighborhood, every fixed radial derivative being analytic on the same neighborhood and bounded on a smaller one; on X0 < X ≤ X0e^{tc} the admissible stress cone and (B.30) hold; all later profile modifications are supported strictly to the right of X0e^{tc}. OBLIGATION: Theorem 4.6(i) requires a fixed Xan ∈ (Xa, Xb) with analyticity in η on [0, Xan] × [−1, 1], and an inner collar [Xa, Xan] carrying the directional margin; Proposition C.3 obtains this from Corollary B.6, and Appendix C chooses Xan inside this rectangle and modifies the profile only beyond it. Lemma 5.1 needs this analytic rectangle to solve the positive-order systems, which contain ∂η terms, on a fixed radial interval. MECHANISM: On the first collar every ingredient (the reference's Qs, Ns and the prescriptions (B.26)) is built from coefficients analytic in η, their η-derivatives, and forward radial. ANTECEDENT: None cited. REFS: p. 153, Corollary B.6; Theorem 4.6(i), p. 33; Appendix C opening, p. 158; Proposition C.3, p. 164; Lemma 5.1, p. 47.",
"obligation": "Theorem 4.6(i) requires a fixed Xan ∈ (Xa, Xb) with analyticity in η on [0, Xan] × [−1, 1], and an inner collar [Xa, Xan] carrying the directional margin; Proposition C.3 obtains this from Corollary B.6, and Appendix C chooses Xan inside this rectangle and modifies the profile only beyond it. Lemma 5.1 needs this analytic rectangle to solve the positive-order systems, which contain ∂η terms, on a fixed radial interval.",
"backward_question": "Which later edits could destroy analyticity in η near the axis, and can a rectangle be quarantined that no later edit or forward integral can reach?",
"mechanism": "On the first collar every ingredient (the reference's Qs, Ns and the prescriptions (B.26)) is built from coefficients analytic in η, their η-derivatives, and forward radial integrals, multiplied by cutoffs that depend on y alone, and cutoffs in y do not affect η-analyticity. Denominators stay nonzero on a small complex neighborhood (Φ has no zeros there), and ϕ is an exponential, hence nonvanishing. Because pressure and the cumulative moments are integrated forward from the axis, no edit supported at larger X can change anything on the rectangle.",
"antecedent": "None cited.",
"cost": "The width tc, strictly inside the first collar; neither tc nor the radial derivative bounds are uniform as C grows and the widths shrink (they are fixed once the finite choices are made).",
"checkable": "Structural bookkeeping only: in an implementation, assert that every later edit's support begins at X > X0e^{tc} and that recomputed forward integrals and fields on [0, X0e^{tc}] are unchanged. Otherwise none: pure argument.",
"depends_on": [
"MB.5",
"MB.8",
"M4.5"
],
"constrains": [],
"reasons": {
"MB.5": "on [0, X0] the profile is Proposition B.2's solution, analytic in Y and η on one common neighborhood.",
"MB.8": "on the first collar the activation (B.26) uses analytic coefficients times cutoffs in y alone and yields the admissible cone and (B.30).",
"M4.5": "pressure and the cumulative integrals are integrated forward from the axis, so edits farther out cannot reach the rectangle."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 153"
},
{
"id": "MB.11",
"kind": "move",
"name": "ns-mb-11-lemma-b-7-and-the-amplitude-independent-shape-transition",
"title": "Lemma B.7 and the amplitude-independent shape transition (B.33) to (B.34)",
"section": "B",
"pages": "154-155",
"refs": [
"pp. 154 to 155, Lemma B.7, (B.32) to (B.34)",
"Proposition 4.10 and its proof, pp. 36 to 38."
],
"statement": "Fix the outer and axis data, Λ, and an order k. With ℓi = log(CE(Xi, η)), Gi = U(Xi, η), and ωfin the total logarithmic width of the final axial cutoff and of the interpolation of a to .8, one has ‖ℓi‖ ≤ Bk and ‖Gi − U∗‖ ≤ Ck^nat/Λ + Ck^join(Λ)(t1 + κ0 + ωfin) in C^k-norms in η (B.32), with Ck^nat independent of Λ and of large C, and Bk, Ck^join(Λ) independent of large C and of smaller widths. Choose Tsh ≥ 20‖σ'‖∞(B0 + ‖log f‖∞) (B.33), where B0 is the k = 0 case of Bk.",
"description": "Fix the outer and axis data, Λ, and an order k. With ℓi = log(CE(Xi, η)), Gi = U(Xi, η), and ωfin the total logarithmic width of the final axial cutoff and of the interpolation of a to .8, one has ‖ℓi‖ ≤ Bk and ‖Gi − U∗‖ ≤ Ck^nat/Λ + Ck^join(Λ)(t1 + κ0 + ωfin) in C^k-norms in η (B.32), with Ck^nat independent of Λ and of large C, and Bk, Ck^join(Λ) independent of large C and of smaller widths. Choose Tsh ≥ 20‖σ'‖∞(B0 + ‖log f‖∞) (B.33), where B0 is the k = 0 case of Bk. OBLIGATION: The outer reference profile (A.7) has η-shape f = (1 + η²)^{−1}, while the axis profile's η-shape at Xi is exp(ℓi), which carries the steep factor ϕ∗. The shape must be changed over a logarithmic length Tsh that does not depend on the amplitude C chosen later; otherwise enlarging C to shrink the inner moment discrepancies (MB.12, MB.13) would lengthen the transition and undo the gain. Proposition 4.10 lists Tsh among the parameters fixed before C. MECHANISM: ℓi = log(√(2Xi)ϕ(Xi)) involves only the logarithmic slopes accumulated from the axis, and these are bounded independently of C. ANTECEDENT: None cited. REFS: pp. 154 to 155, Lemma B.7, (B.32) to (B.34); Proposition 4.10 and its proof, pp. 36 to 38.",
"obligation": "The outer reference profile (A.7) has η-shape f = (1 + η²)^{−1}, while the axis profile's η-shape at Xi is exp(ℓi), which carries the steep factor ϕ∗. The shape must be changed over a logarithmic length Tsh that does not depend on the amplitude C chosen later; otherwise enlarging C to shrink the inner moment discrepancies (MB.12, MB.13) would lengthen the transition and undo the gain. Proposition 4.10 lists Tsh among the parameters fixed before C.",
"backward_question": "Can the length of the shape-changing transition be bounded before the amplitude is chosen, so that the amplitude remains a free knob afterward?",
"mechanism": "ℓi = log(√(2Xi)ϕ(Xi)) involves only the logarithmic slopes accumulated from the axis, and these are bounded independently of C by Lemma B.4; only integrals of bounded cutoff values enter, so no inverse powers of the transition widths appear. A slow interpolation in log X between ℓi and log f, superposed on the fixed power 1/10, perturbs l = DX log H by at most ‖σ'‖∞(B0 + ‖log f‖∞)/Tsh ≤ .05, so the shear stays in a ∈ [.7, .9] with bs = 0. Positivity of Sq is checked term by term: the old gradient gives −Hcℓi' ≥ LΛχ minus absorbable errors (via (B.20)); the new gradient gives −Hc(log f)' = 2ηHc/(1 + η²) ≥ −Cj0² − C/Λ − o(1), after writing ηH∗ = (D + 4d)η² + dj0η and completing the square; the two are combined convexly; and −W ≈ −W∗ > 2.8 with l ≥ .55.",
"antecedent": "None cited.",
"cost": "Tsh (large, fixed before C, and dependent on Λ through Bk); the bounds Bk; the error term Ck^join(Λ)(t1 + κ0 + ωfin), which forces the order j0, Λ, then C, then κ0, t1, ωfin; the radius Xsep = Xie^{Tsh}.",
"checkable": "Compute ‖σ'‖∞ from (A.5) (digest check: ‖σ'‖∞ = 8, attained at y = 1/2) and use ‖log f‖∞ = log 2 on [−1, 1], so (B.33) reads Tsh ≥ 160(B0 + log 2); given a numerical ℓi from MB.9, evaluate l along (B.34) and confirm l ∈ [.55, .65]; evaluate Sq along the transition from (4.9).",
"depends_on": [
"MB.9",
"MB.7",
"MA.4",
"M4.4"
],
"constrains": [],
"reasons": {
"MB.9": "the transition starts from the state at X_i = 110 (a = .8, D_XU = 0, p1 > 2) reached by Proposition B.5.",
"MB.7": "ℓ_i involves only logarithmic slopes from the axis, bounded independently of C by Lemma B.4, which gives B_k in (B.32).",
"MA.4": "the target is the η-shape f = (1 + η²)^{-1} of the outer reference branch (A.7), interpolated with the step σ of (A.5).",
"M4.4": "along (B.34), l stays in [.55, .65], and the barrier D_X p1 = XS_q/L - lp1 with S_q > 1 keeps p1 > 2."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 154-155"
},
{
"id": "MB.12",
"kind": "move",
"name": "ns-mb-12-amplitude-radius-exchange-xr-xi-cp-10",
"title": "Amplitude-radius exchange, XR = Xi(CP∗)^{10}",
"section": "B",
"pages": "155-156",
"refs": [
"pp. 155 to 156, (B.38)",
"Proposition 4.10, pp. 36 to 37",
"section 4.6 Step 1, pp. 39 to 40."
],
"statement": "Set XR = Xi(CP∗)^{10} (Proposition 4.10 writes XR = 110(CP∗)^{10}), x = X/XR, and Xsep = Xie^{Tsh}. Beyond Xsep, (B.34) is exactly the ideal angular profile, because C^{−1}f(X/Xi)^{1/10} = P∗f x^{1/10}. In normalized coordinates the end of the transition sits at xsep = Xsep/XR = e^{Tsh}/(CP∗)^{10} (B.38), which tends to 0 as C → ∞ with Tsh fixed.",
"description": "Set XR = Xi(CP∗)^{10} (Proposition 4.10 writes XR = 110(CP∗)^{10}), x = X/XR, and Xsep = Xie^{Tsh}. Beyond Xsep, (B.34) is exactly the ideal angular profile, because C^{−1}f(X/Xi)^{1/10} = P∗f x^{1/10}. In normalized coordinates the end of the transition sits at xsep = Xsep/XR = e^{Tsh}/(CP∗)^{10} (B.38), which tends to 0 as C → ∞ with Tsh fixed. OBLIGATION: The inner profile's contribution to the five cumulative integrals, measured in units of the outer scale, must fall below a tolerance fixed by the outer data (B.36), so that a fixed-size bump correction can cancel it. The matching radius must also exceed R∗ (Lemma 4.8) and be large enough that Pc = XRxG/L > 2 on the correction patch (B.37). Proposition 4.10(iii) draws the consequence: XR can be pushed past any later lower bound while Λ and Tsh stay as already chosen. MECHANISM: The reference power law E ∝ X^{1/10} is scale covariant. The inner construction lives at swirl amplitude 1/C (E = √(2X)ϕ/C), and after the transition the profile follows C^{−1}f(X/Xi)^{1/10}, which reaches the outer amplitude P∗f. ANTECEDENT: None cited. REFS: pp. 155 to 156, (B.38); Proposition 4.10, pp. 36 to 37; section 4.6 Step 1, pp. 39 to 40.",
"obligation": "The inner profile's contribution to the five cumulative integrals, measured in units of the outer scale, must fall below a tolerance fixed by the outer data (B.36), so that a fixed-size bump correction can cancel it. The matching radius must also exceed R∗ (Lemma 4.8) and be large enough that Pc = XRxG/L > 2 on the correction patch (B.37). Proposition 4.10(iii) draws the consequence: XR can be pushed past any later lower bound while Λ and Tsh stay as already chosen.",
"backward_question": "Is there an exact scaling under which the inner region, fixed in X, looks arbitrarily small from the viewpoint of the outer profile, without redoing the inner construction?",
"mechanism": "The reference power law E ∝ X^{1/10} is scale covariant. The inner construction lives at swirl amplitude 1/C (E = √(2X)ϕ/C), and after the transition the profile follows C^{−1}f(X/Xi)^{1/10}, which reaches the outer amplitude P∗f x^{1/10} only after the radius is rescaled by (CP∗)^{10}. So the amplitude C, the last free parameter of the inner construction, is converted into radial separation: the inner structure, fixed in X up to Xsep before C is chosen, occupies [0, xsep] with xsep ∝ C^{−10} in outer units, and its moment contributions vanish as powers of xsep and of 1/C, as in (B.39).",
"antecedent": "None cited.",
"cost": "XR grows like C^{10}; C must be chosen after Tsh and Λ; section 4.6 imposes C ≥ max{C0, (R∗/110)^{1/10}/P∗} so that XR ≥ R∗.",
"checkable": "Symbolic check of C^{−1}(X/Xi)^{1/10} = P∗(X/XR)^{1/10} for XR = Xi(CP∗)^{10}; tabulate xsep = e^{Tsh}/(CP∗)^{10} against C for given Tsh and P∗ and find the least C with xsep < e^{−8}; check that the reference pressure increment at xsep is (5/2)P∗²f²xsep^{1/5} = (5/2)f²e^{Tsh/5}C^{−2}.",
"depends_on": [
"MB.11",
"MA.4"
],
"constrains": [],
"reasons": {
"MB.11": "beyond X_sep = X_i e^{T_sh} the transition (B.34) has reached C^{-1}f(X/X_i)^{1/10}, with T_sh fixed before C.",
"MA.4": "the target is the outer reference branch E = P*f x^{1/10} of (A.7), reached exactly when X_R = X_i(CP*)^{10}."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 155-156"
},
{
"id": "MB.13",
"kind": "move",
"name": "ns-mb-13-proposition-b-8-exact-matching-of-the-five-cumulative",
"title": "Proposition B.8, exact matching of the five cumulative radial integrals",
"section": "B",
"pages": "155-157",
"refs": [
"pp. 155 to 157, Proposition B.8, (B.35) to (B.39)",
"Lemma A.1, Lemma A.2, Corollary A.3, pp. 126 to 128",
"(A.7), p. 129",
"(A.25), p. 134",
"Lemmas 4.3 and 4.4, pp. 28 to 29",
"(4.34) and Proposition 4.10(iii), p. 37."
],
"statement": "For C sufficiently large and then the activation transitions sufficiently small, the profile of Proposition B.5 continued by (B.34) continues to log x = −5 with the strict relaxed cone preserved, and there its fields, pressure Π, and all five integrals M, I, J, S, Cp agree exactly with those of the reference inner profile (A.7); it then follows the outer radial profile without changing Π0 or the later Qs, Ns.",
"description": "For C sufficiently large and then the activation transitions sufficiently small, the profile of Proposition B.5 continued by (B.34) continues to log x = −5 with the strict relaxed cone preserved, and there its fields, pressure Π, and all five integrals M, I, J, S, Cp agree exactly with those of the reference inner profile (A.7); it then follows the outer radial profile without changing Π0 or the later Qs, Ns. OBLIGATION: Lemma 4.4(i): if two profiles agree beyond a radius and their five integrals agree there, with the same axis pressure datum, then pressure, V0, Qs, Ns, ps, a, bs and T0 agree at all larger radii. ANTECEDENT: Lemma A.1 (Rolle's theorem: a nonzero combination of m distinct powers has at most m − 1 positive zeros, plus multilinearity of the determinant), Lemma A.2 (a contraction plus the pointwise implicit function theorem), Corollary A.3 (the five-moment blocks with α = 1/10), and Lemmas 4.3 and 4.4. REFS: pp. 155 to 157, Proposition B.8, (B.35) to (B.39); Lemma A.1, Lemma A.2, Corollary A.3, pp. 126 to 128; (A.7), p. 129; (A.25), p. 134; Lemmas 4.3 and 4.4, pp. 28 to 29; (4.34) and Proposition 4.10(iii), p. 37.",
"obligation": "Lemma 4.4(i): if two profiles agree beyond a radius and their five integrals agree there, with the same axis pressure datum, then pressure, V0, Qs, Ns, ps, a, bs and T0 agree at all larger radii. This lets the regular axis profile replace the temporary inner branch (A.7) of the outer profile, which is not regular at the axis, without changing the exterior: the pressure normalization (4.25), the moment identities (4.28), the heat exterior (4.29), and hence Lemma 4.9 and Lemma A.8 (T0 = 0 for X ≥ Xb), whose hypotheses require a regular axis and exact moments. It is Proposition 4.10(iii) and the joining in Step 1 of the proof of Theorem 4.6.",
"backward_question": "Which finite set of integral invariants carries everything the outer fields need from the inner profile, and in what units does correcting them have bounds independent of the huge matching radius?",
"mechanism": "The stress at a radius depends on the profile inside that radius only through five cumulative integrals (Lemma 4.3), so a gluing must match those five functions of η as well as the fields. Normalizing them by powers of XR removes XR from (B.35), so the Lipschitz constants of the map from moments to (Qs, Ns) and the inverse bounds of the correction depend only on outer data: one fixed tolerance serves every large XR, and enlarging XR only helps, since Pc ∝ XR. The discrepancy entering the correction is at most Ck‖Gi − 4η‖ in C^{k+1} plus a term that is o(1) as C grows, because the inner region is tiny in x (MB.12) and Gi is close to 4η once j0, then Λ, then the transition widths are small ((B.32) and the proof of Proposition 4.10). After the row operations the linearization is block triangular: the U-bumps move M and J − 4ηI, and the E-bumps move I, S − 8ηM and Cp; each block is a matrix of distinct powers integrated against bumps on ordered disjoint intervals, invertible by the Rolle argument of Lemma A.1; the remainder is exactly quadratic, so the contraction of Lemma A.2 gives smooth coefficients with the prescribed finite set of η-derivative bounds.",
"antecedent": "Lemma A.1 (Rolle's theorem: a nonzero combination of m distinct powers has at most m − 1 positive zeros, plus multilinearity of the determinant), Lemma A.2 (a contraction plus the pointwise implicit function theorem), Corollary A.3 (the five-moment blocks with α = 1/10), and Lemmas 4.3 and 4.4.",
"cost": "The restoration patch (−8, −7) and the correction patch (−6, −5) in log x; five bump amplitudes; the tolerance εm fixed by outer data; one extra η-derivative on the inputs, because (B.35) contains η-derivatives of the moments; smallness only for a prescribed finite set of η-derivative orders.",
"checkable": "Assemble the 5 × 5 Jacobian of the normalized moment map at the ideal profile on (−6, −5) in log x, using bumps that are rescaled copies of σ' and the weights (1, f x^{3/5}) and (x^{1/2}, f x^{1/10}, f x^{−9/10}); compute its determinant and condition number for η ∈ [−1, 1]; run c ↦ B^{−1}(d − Q(c, c)) on synthetic discrepancies and confirm convergence when 8β0²κ0d0 ≤ 1 (Lemma A.2). Arithmetic: .9 + .01/.7 = .914 < 1, and 1 − (.1/(1 + w))w/.7 ≥ 6/7 for all w ≥ 0. Recompute the reference integrals (4.34) to confirm the target values.",
"depends_on": [
"MB.12",
"MA.3",
"M4.6",
"MA.2"
],
"constrains": [],
"reasons": {
"MB.12": "X_R = X_i(CP*)^{10} puts the inner structure at x ≤ x_sep → 0, so its moment contributions (B.39) fall below the tolerance.",
"MA.3": "Corollary A.3 at α = 1/10 makes the two U bumps and three E bumps on -6 < log x < -5 an invertible five-moment map.",
"M4.6": "once fields and all five integrals agree at log x = -5 with the same Π0, Lemma 4.4(i) makes every outer field agree beyond it.",
"MA.2": "the exactly quadratic five-moment system is solved by Lemma A.2's contraction, with bounds on finitely many η-derivatives."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 155-157"
},
{
"id": "MB.14",
"kind": "move",
"name": "ns-mb-14-remark-b-9-and-corollary-b-10-the-order-of-choices-and",
"title": "Remark B.9 and Corollary B.10, the order of choices and the completed connection",
"section": "B",
"pages": "157",
"refs": [
"p. 157, Remark B.9, (B.40), Corollary B.10",
"section 4.6, pp. 39 to 40",
"Definition 3.3, p. 18."
],
"statement": "For any finite list of η-derivative orders (including the extra derivative in (B.35)), the choices can be made in the order Md, Td, P∗, λ, h → tolerance for matching moments, j0 → δ∗, σ∗, Λ → (Bk), Tsh → C, XR → κ0, t1, widths of final transitions (B.40). The outer choices first make Cpre√λ(1 + log(1/λ)) small, and then h ≪ λ, h ≪ e^{−Td}; the radial frequency used in Appendix C is selected only after all of these.",
"description": "For any finite list of η-derivative orders (including the extra derivative in (B.35)), the choices can be made in the order Md, Td, P∗, λ, h → tolerance for matching moments, j0 → δ∗, σ∗, Λ → (Bk), Tsh → C, XR → κ0, t1, widths of final transitions (B.40). The outer choices first make Cpre√λ(1 + log(1/λ)) small, and then h ≪ λ, h ≪ e^{−Td}; the radial frequency used in Appendix C is selected only after all of these. OBLIGATION: Guarantees the construction is not circular: each smallness condition refers only to earlier choices. In particular C0(Λ) may be exponentially large in Λ, the moment tolerance depends only on outer data, and Tsh is fixed before C. Corollary B.10 is the deliverable consumed by Proposition 4.10 (hence by Step 1 of the proof of Theorem 4.6) and by Appendix C as its fixed input profile. MECHANISM: Every bound is arranged to be uniform in everything chosen later: the tolerance is uniform in XR by the normalization (B.35) to. ANTECEDENT: The smallness convention of Definition 3.3 (in a chain of constants the rightmost is fixed first); nothing classical cited. REFS: p. 157, Remark B.9, (B.40), Corollary B.10; section 4.6, pp. 39 to 40; Definition 3.3, p. 18.",
"obligation": "Guarantees the construction is not circular: each smallness condition refers only to earlier choices. In particular C0(Λ) may be exponentially large in Λ, the moment tolerance depends only on outer data, and Tsh is fixed before C. Corollary B.10 is the deliverable consumed by Proposition 4.10 (hence by Step 1 of the proof of Theorem 4.6) and by Appendix C as its fixed input profile.",
"backward_question": "Is there a single linear order of all parameter choices in which every smallness requirement refers only to quantities already fixed?",
"mechanism": "Every bound is arranged to be uniform in everything chosen later: the tolerance is uniform in XR by the normalization (B.35) to (B.37); the transition length is uniform in C by (B.32) to (B.33); the axis solution's η-bounds are uniform in C ≥ C0(Λ) by (B.13); the activation comparisons hold uniformly as κ0 and t1 decrease; the final widths enter only through small errors whose constants are fixed by earlier choices. Section 4.6 restates the same order as the hierarchy 0 < C^{−1} ≪ Tsh^{−1} ≪ Λ^{−1} ≪ σ∗ ≪ δ∗ ≪ j0 ≪ εm ≪ h ≪ λ ≪ P∗^{−1} ≪ Md^{−1} ≪ 1 and 0 < ωfin ≪ t1 ≪ κ0 ≪ C^{−1}, followed by N^{−1} ≪ ωfin.",
"antecedent": "The smallness convention of Definition 3.3 (in a chain of constants the rightmost is fixed first); nothing classical cited.",
"cost": "Constants may depend on all earlier choices; radial derivative bounds of cutoffs contain inverse powers of the final widths; only a prescribed finite set of η-derivative orders is made small (every other fixed order is merely finite).",
"checkable": "Encode the dependency graph of the constants (each condition's list of previously fixed quantities, read from (B.40), the proof of Proposition 4.10, and section 4.6) and check that it is acyclic and consistent with both stated orderings; the estimates themselves are pure estimates with unspecified constants.",
"depends_on": [
"MB.13",
"MB.10",
"MB.9",
"MA.4"
],
"constrains": [],
"reasons": {
"MB.13": "Corollary B.10's matching at log(X/X_R) = -5 with exact fields, pressure, and moment functions is Proposition B.8.",
"MB.10": "the inner collar, analytic in η, admissible, and carrying (B.30), is Corollary B.6.",
"MB.9": "the strict relaxed cone from the collar out to X_i is the small-shear continuation of Proposition B.5.",
"MA.4": "the order (B.40) begins with the outer parameters M_d, T_d, P*, λ, h of (A.6), fixed before any axis parameter."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 157"
},
{
"id": "MC.1",
"kind": "move",
"name": "ns-mc-1-target-and-obstruction-the-admissible-cone-on-a-relaxed",
"title": "Target and obstruction: the admissible cone on a relaxed-only interval",
"section": "C",
"pages": "157-158",
"refs": [
"pp. 157 to 158 (Appendix C preamble)",
"p. 27, (4.11)",
"pp. 30 to 32, (4.20) to (4.23), Lemma 4.5",
"p. 38, (4.35)",
"p. 74, (7.1) and the frame",
"pp. 80 to 81, (7.21), (7.22)",
"pp. 82 to 83, (7.23) to (7.29), Proposition 7.5",
"p. 2 (citations)."
],
"statement": "Notation from (4.11), (4.20), (4.21): shear s=(a,-b_s) with a=1-2D_X\\log E, b_s=2D_XU/E; integrated inviscid vector p_s=(XQ_s/L,\\ XN_s/(LE)); stress T_0=F(p_s-s); t_s=-b_s/a, v_s=a(1+t_s^2)=a+b_s^2/a, P_c=p_{s,1}+t_sp_{s,2}, J_c=p_{s,2}-t_sp_{s,1}, and the upper bound \\mathcal U(P_c,J_c)=P_c+J_c^2/4-|J_c|\\sqrt{(P_c-2)/2+J_c^2/16} (script U in the paper, distinct from the axial profile U). Relaxed cone (4.21): P_c>2, v_s<\\mathcal U. Admissible cone: (4.21) plus v_s>2.",
"description": "Notation from (4.11), (4.20), (4.21): shear s=(a,-b_s) with a=1-2D_X\\log E, b_s=2D_XU/E; integrated inviscid vector p_s=(XQ_s/L,\\ XN_s/(LE)); stress T_0=F(p_s-s); t_s=-b_s/a, v_s=a(1+t_s^2)=a+b_s^2/a, P_c=p_{s,1}+t_sp_{s,2}, J_c=p_{s,2}-t_sp_{s,1}, and the upper bound \\mathcal U(P_c,J_c)=P_c+J_c^2/4-|J_c|\\sqrt{(P_c-2)/2+J_c^2/16} (script U in the paper, distinct from the axial profile U). Relaxed cone (4.21): P_c>2, v_s<\\mathcal U. Admissible cone: (4.21) plus v_s>2. OBLIGATION: This move fixes what the waves can realize, and therefore what the profile must satisfy. ANTECEDENT: None cited in Appendix C. The introduction (p. 2) cites Leibovich and Stewartson [15] and Billant and Gallaire [2, 3] as centrifugal-instability precedents for the wave dynamics. It cites Lifschitz and Hameiri [17] and Friedlander and Vishik [14] for wavevector and polarization evolution. (Digest's note, not in the paper: put \\Omega=u_\\theta/r, W=u_z, \\Gamma=r^2\\Omega. Then (4.11) gives a=-r\\Omega'/\\Omega and b_s=W'/\\Omega, hence a(v_s-2)=(\\Omega'\\Gamma'+W'^2)/\\Omega^2.",
"obligation": "This move fixes what the waves can realize, and therefore what the profile must satisfy. In section 7.1 (p. 74) the chart shear is g_0=F_0(-a,b_s), with N=g_0/|g_0| and K=N^\\perp. The reference growth rate is \\lambda_0^2=2aF_0^2(1-2/v_s), and c_0^2=(v_s-2)/2 with c_0<0, so pulses grow only if v_s>2. A growing pulse has polarization y/x=c_0\\sqrt{1+s^2}+O(S_*^{-1}) (7.21). Its covariance column is therefore H_\\sigma=h_\\sigma(-A_cN-\\sigma u_*K+e_\\sigma) with A_c=-c_0\\sqrt{1+u_*^2}>0 (7.28). Positive squared amplitudes y=H^{-1}T_{0,*} (Proposition 7.5) exist exactly for targets with T_N<0 and |T_K|<(u_*/A_c)(-T_N). Since u_*/A_c increases to 1/|c_0| as u_*\\to\\infty, the union of these cones is (7.1): T\\cdot N<0 and |c_0\\,T\\cdot K|<|T\\cdot N|. That is a cone about the shear direction (1,t_s) with half-opening \\arctan\\sqrt{2/(v_s-2)}, and by (4.23) it is exactly (4.22). The first inequality is also the sign of energy extraction from the shear, -g_0\\cdot T=-|g_0|T_N>0 in (7.22). So the leading stress must lie in the cone for three reasons: amplitudes must be real (positive squared weights), only growing pulses carry the stress, and their polarization caps the ratio of transverse to along-shear flux at 1/|c_0|. Where v_s\\le2, \\lambda_0^2\\le0: there is no growing direction, c_0 is undefined, and Proposition 7.5 has nothing to work with. Without this appendix, Theorem 4.6(iii) (v_s-2 bounded below on the closed annulus) is unproved.",
"backward_question": "\"The waves realize only stresses in a cone about the shear direction, with opening set by v_s, and only where v_s>2. My joined profile satisfies P_c>2 and v_s<\\mathcal U but has v_s\\le2 somewhere in the annulus. Which profile data enter the cone test through radial derivatives and which through integrals, and can I change the first kind at order one while freezing the second?\"",
"mechanism": "The appendix exploits a split in how the profile enters the cone test. The shear s uses logarithmic radial derivatives (4.11). The vector p_s and the moments m=(M,I,J,S,C_p) use only profile values, cumulative radial integrals, and \\eta-derivatives ((4.15), (4.16)). So the shear can move at order one while p_s moves by O(N^{-1}). The construction freezes p_s pointwise and asks which shears are admissible for that p_s. It finds a loop of them averaging to the given shear (MC.2 to MC.4) and realizes the loop by fast radial modulation (MC.5 to MC.7). All changes live in I plus one reserved patch.",
"antecedent": "None cited in Appendix C. The introduction (p. 2) cites Leibovich and Stewartson [15] and Billant and Gallaire [2, 3] as centrifugal-instability precedents for the wave dynamics. It cites Lifschitz and Hameiri [17] and Friedlander and Vishik [14] for wavevector and polarization evolution. (Digest's note, not in the paper: put \\Omega=u_\\theta/r, W=u_z, \\Gamma=r^2\\Omega. Then (4.11) gives a=-r\\Omega'/\\Omega and b_s=W'/\\Omega, hence a(v_s-2)=(\\Omega'\\Gamma'+W'^2)/\\Omega^2. For a>0 (\\Omega'<0), the condition v_s>2 is exactly the Leibovich-Stewartson condition V\\Omega'(\\Omega'\\Gamma'+W'^2)<0, and with W'=0 it is Rayleigh's \\Gamma'<0.)",
"cost": "The input must satisfy the relaxed cone strictly, with a positive minimum on compact sets, and admissibility on neighborhoods of both ends of I. One unused reserved patch must remain downstream. This move fixes X_\\pm and X_{an}.",
"checkable": "This is a finite-dimensional check. For given (a,b_s,p_s), compute \\Psi of (4.35) and test all four entries >0. Equivalently, set N=(-a,b_s)/|(-a,b_s)|, K=(-N_z,N_\\theta), c_0=-\\sqrt{(v_s-2)/2}, T=p_s-(a,-b_s), and test T\\cdot N<0 and |c_0T\\cdot K/T\\cdot N|<1. Then pick u_* with u_*/\\sqrt{1+u_*^2}>|c_0T\\cdot K/T\\cdot N|, set A_c=-c_0\\sqrt{1+u_*^2} and H=[-A_cN-u_*K,\\ -A_cN+u_*K], and check H^{-1}T>0 componentwise. Symbolically, check -2F_0N_\\theta(2F_0N_\\theta+|g_0|)=2aF_0^2(1-2/v_s) and c_0^2=(v_s-2)/2. The digest ran these checks. Among about 2\\times10^5 random samples there were zero disagreements between (4.21) with v_s>2, (4.22), and (7.1). H^{-1}T>0 held in all 30,668 admissible samples. Sympy confirmed both identities and the Leibovich-Stewartson rewriting.",
"depends_on": [
"M4.7",
"M4.4",
"MB.14",
"MA.9"
],
"constrains": [],
"reasons": {
"M4.7": "the target is Lemma 4.5's admissible cone, the relaxed inequalities (4.21) plus v_s > 2, equivalently (4.22).",
"M4.4": "the cone is written through the shear s = (a, -b_s), the integrated vector p_s, and T0 = F(p_s - s) of (4.11).",
"MB.14": "the input is Corollary B.10's joined profile, admissible on the inner collar and only relaxed out to the matching point.",
"MA.9": "Proposition A.4 gives admissibility only from the intermediate power law onward, which leaves the relaxed-only interval I."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 157-158"
},
{
"id": "MC.2",
"kind": "move",
"name": "ns-mc-2-exponentially-tilted-ratio-family-mean-t-s-a-floor-on-p-c",
"title": "Exponentially tilted ratio family: mean t_s, a floor on P_c, unbounded variance",
"section": "C",
"pages": "159",
"refs": [
"p. 159, (C.4) to (C.7)",
"p. 31 (proof of Lemma 4.5: 2<v_-\\le P_c)."
],
"statement": "Proof of Lemma C.1, first part (p. 159). Write shear vectors as positive multiples of (1,t) and put P_c(t)=p_{s,1}+p_{s,2}t, J_c(t)=p_{s,2}-p_{s,1}t. Choose 0<d_0<\\tfrac12\\min(P_c(t_s)-2). Define M_e(z)=\\langle e^{z\\sin\\theta'}\\rangle_{\\theta'} (C.4) and t(\\theta';\\mu)=t_s+d_0\\,(e^{\\mu p_{s,2}\\sin\\theta'}/M_e(\\mu p_{s,2})-1)/p_{s,2} for \\mu\\ge0 (C.5). The singularity at p_{s,2}=0 is removable, and there t=t_s+d_0\\mu\\sin\\theta'.",
"description": "Proof of Lemma C.1, first part (p. 159). Write shear vectors as positive multiples of (1,t) and put P_c(t)=p_{s,1}+p_{s,2}t, J_c(t)=p_{s,2}-p_{s,1}t. Choose 0<d_0<\\tfrac12\\min(P_c(t_s)-2). Define M_e(z)=\\langle e^{z\\sin\\theta'}\\rangle_{\\theta'} (C.4) and t(\\theta';\\mu)=t_s+d_0\\,(e^{\\mu p_{s,2}\\sin\\theta'}/M_e(\\mu p_{s,2})-1)/p_{s,2} for \\mu\\ge0 (C.5). The singularity at p_{s,2}=0 is removable, and there t=t_s+d_0\\mu\\sin\\theta'. OBLIGATION: The loop must consist of shear directions t with mean t_s, so that the vectors can later average to (a,-b_s). It needs as much variance as required, because the variance is what lifts v above 2 (MC.3). Each member must also keep P_c(t)>2, since that is what makes the upper cone bound exceed 2 (2<\\mathcal U\\le P_c whenever P_c>2, proof of Lemma 4.5). A large symmetric oscillation of t would push P_c(t)=P_c(t_s)+p_{s,2}(t-t_s) below 2 on one side whenever p_{s,2}\\ne0. ANTECEDENT: None cited. (Digest's note: M_e(z) is the modified Bessel function I_0(z), and (C.5) is an exponential tilt. The paper names neither.) REFS: p. 159, (C.4) to (C.7); p. 31 (proof of Lemma 4.5: 2<v_-\\le P_c).",
"obligation": "The loop must consist of shear directions t with mean t_s, so that the vectors can later average to (a,-b_s). It needs as much variance as required, because the variance is what lifts v above 2 (MC.3). Each member must also keep P_c(t)>2, since that is what makes the upper cone bound exceed 2 (2<\\mathcal U\\le P_c whenever P_c>2, proof of Lemma 4.5). A large symmetric oscillation of t would push P_c(t)=P_c(t_s)+p_{s,2}(t-t_s) below 2 on one side whenever p_{s,2}\\ne0.",
"backward_question": "\"How can I oscillate the shear ratio t about t_s with arbitrarily large variance, without ever letting the along-shear inviscid coefficient P_c(t)=p_s\\cdot(1,t) fall to 2?\"",
"mechanism": "The weight w=e^{\\mu p_{s,2}\\sin\\theta'}/M_e(\\mu p_{s,2}) is positive with mean one. Setting p_{s,2}(t-t_s)=d_0(w-1) gives mean zero and bounds the change in P_c below by -d_0, while excursions that increase P_c are unbounded. So t is bounded on one side and free on the other, and every large excursion goes in the helpful direction. The variance is (d_0/p_{s,2})^2(\\langle w^2\\rangle-1) with \\langle w^2\\rangle=M_e(2z)/M_e(z)^2. Strict monotonicity comes from log-convexity of the moment generating function: g'' is the variance of \\sin\\theta' under the tilted density. Growth comes from Laplace's method at the maximum of \\sin. Joint smoothness through p_{s,2}=0 uses G(p)/p=\\int_0^1G'(up)\\,du.",
"antecedent": "None cited. (Digest's note: M_e(z) is the modified Bessel function I_0(z), and (C.5) is an exponential tilt. The paper names neither.)",
"cost": "New constants d_0 and \\mu_{\\max}. \\mu_{\\max} can be large, because V grows only like \\sqrt{\\mu|p_{s,2}|} when p_{s,2}\\ne0 (digest: M_e(2z)/M_e(z)^2\\sim\\sqrt{\\pi z}). The family is unbounded in t as \\mu\\to\\infty, which is why the next margin \\delta_L must be chosen after \\mu_{\\max}.",
"checkable": "Use scipy.special.i0 for M_e and quadrature in \\theta', on sample (a,b_s,p_s) with P_c(t_s)>2. Check \\langle t\\rangle=t_s and \\min_{\\theta'}P_c(t)\\ge P_c(t_s)-d_0. Check that \\langle(t-t_s)^2\\rangle equals the closed form V, that V increases in \\mu, that V/(d_0^2\\mu^2/2)\\to1 as \\mu\\to0, and that [M_e(2z)/M_e(z)^2]/\\sqrt{\\pi z}\\to1. The digest ran this at p_{s,2}=1,0,-1.5: all identities held to quadrature precision. The Bessel ratio was 0.980, 0.998, 0.9998 at z=10,100,1000. For p_{s,2}<0 the loop's t stayed below t_s+d_0/|p_{s,2}|, as predicted.",
"depends_on": [
"MC.1",
"M4.7"
],
"constrains": [],
"reasons": {
"MC.1": "works on the relaxed-only interval I with p_s frozen, where P_c(t_s) > 2 has a positive minimum.",
"M4.7": "P_c(t), J_c(t) are the cone coordinates (4.20) along the direction (1, t); keeping P_c > 2 keeps U(P_c, J_c) > 2 (Lemma 4.5)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 159"
},
{
"id": "MC.3",
"kind": "move",
"name": "ns-mc-3-target-instability-level-v-and-smooth-tilt-strength-mu-x",
"title": "Target instability level v and smooth tilt strength \\mu(X,\\eta)",
"section": "C",
"pages": "159-160",
"refs": [
"pp. 159 to 160, (C.8) to (C.10)",
"p. 74 (\\lambda_0^2)."
],
"statement": "Pp. 159 to 160. Choose 0<\\delta_L<1 with \\mathcal U(P_c(t),J_c(t))>2+\\delta_L for 0\\le\\mu\\le\\mu_{\\max} (C.8), then shrink \\delta_L below \\min(v_s-2) on neighborhoods of \\partial I. Let \\zeta_L be a smooth function of v_s with 0\\le\\zeta_L\\le1, \\zeta_L=1 for v_s\\le2+\\delta_L/8, and \\zeta_L=0 for v_s\\ge2+\\delta_L/4. Set v_*=2+\\delta_L/2, \\rho=\\zeta_L(v_s)^2(v_*-v_s), v=v_s+\\rho (C.9), and solve V(\\mu,p_{s,2})=\\rho/a with 0\\le\\mu<\\mu_{\\max} (C.10).",
"description": "Pp. 159 to 160. Choose 0<\\delta_L<1 with \\mathcal U(P_c(t),J_c(t))>2+\\delta_L for 0\\le\\mu\\le\\mu_{\\max} (C.8), then shrink \\delta_L below \\min(v_s-2) on neighborhoods of \\partial I. Let \\zeta_L be a smooth function of v_s with 0\\le\\zeta_L\\le1, \\zeta_L=1 for v_s\\le2+\\delta_L/8, and \\zeta_L=0 for v_s\\ge2+\\delta_L/4. Set v_*=2+\\delta_L/2, \\rho=\\zeta_L(v_s)^2(v_*-v_s), v=v_s+\\rho (C.9), and solve V(\\mu,p_{s,2})=\\rho/a with 0\\le\\mu<\\mu_{\\max} (C.10). OBLIGATION: This fixes how unstable each loop member is. It must exceed 2 (growth) and stay below \\mathcal U(P_c(t),J_c(t)) for every member (quadratic cone test). It must equal v_s, with no oscillation, wherever admissibility already holds, in particular near \\partial I, which gives (C.3). And it must be chosen so that \\mu depends smoothly on (X,\\eta), including where \\rho=0. MECHANISM: The loop vectors will be v(1,t)/(1+t^2), and the averaging identity of MC.4 forces v=a\\langle1+t^2\\rangle=v_s+aV. So each loop member's excess instability over the mean shear is exactly a times the variance, and (C.10) sets that variance. ANTECEDENT: None cited (implicit function theorem). REFS: pp. 159 to 160, (C.8) to (C.10); p. 74 (\\lambda_0^2).",
"obligation": "This fixes how unstable each loop member is. It must exceed 2 (growth) and stay below \\mathcal U(P_c(t),J_c(t)) for every member (quadratic cone test). It must equal v_s, with no oscillation, wherever admissibility already holds, in particular near \\partial I, which gives (C.3). And it must be chosen so that \\mu depends smoothly on (X,\\eta), including where \\rho=0.",
"backward_question": "\"If each loop vector is v(1,t)/(1+t^2) and their average must be (a,-b_s), what does that force on v? How do I place v strictly between 2 and the upper cone bound for every member, smoothly in (X,\\eta), with no change where nothing is broken?\"",
"mechanism": "The loop vectors will be v(1,t)/(1+t^2), and the averaging identity of MC.4 forces v=a\\langle1+t^2\\rangle=v_s+aV. So each loop member's excess instability over the mean shear is exactly a times the variance, and (C.10) sets that variance. The target v_* sits just above 2 because \\mathcal U can approach 2 along the unbounded direction of the family (digest: for p_{s,2}=0, \\mathcal U\\to2 as |t|\\to\\infty). So \\delta_L is fixed only after \\mu_{\\max} makes the family compact. Squaring the cutoff makes \\sqrt\\rho=\\zeta_L(v_s)\\sqrt{v_*-v_s} smooth, since v_*-v_s\\ge\\delta_L/4 on the support. V is even in \\mu with V=\\tfrac12d_0^2\\mu^2+O(\\mu^4p^2), so its signed square root is smooth and odd, with derivative d_0/\\sqrt2 at \\mu=0. The implicit function theorem applied to that square root and \\sqrt\\rho/\\sqrt a gives smooth \\mu through \\rho=0; (C.6) handles \\rho>0.",
"antecedent": "None cited (implicit function theorem).",
"cost": "New constants \\delta_L and v_* and the cutoff \\zeta_L, chosen in the order d_0\\to\\mu_{\\max}\\to\\delta_L. On the modulated set the instability margin is only about \\delta_L/2. Rewriting the p. 74 formula with a=v/(1+t^2) (digest's rewriting) gives \\lambda_0^2=2F_0^2(v-2)/(1+t^2)\\le F_0^2\\delta_L there. So the positive lower bound for \\lambda_0 used in section 7.1 is small, though fixed.",
"checkable": "Use sample data that violate only v_s>2. Take \\delta_L as a fraction of \\min_{\\theta',\\,\\mu\\le\\mu_{\\max}}[\\mathcal U(P_c(t),J_c(t))-2], form \\rho, and solve (C.10) by Brent's method. Check a\\langle1+t^2\\rangle=v and 2<v<\\mathcal U(P_c(t),J_c(t)) for all \\theta'. The digest ran this at three samples. For example, with a=1, b_s=0.3, p_s=(5,1) (v_s=1.09): \\min(\\mathcal U-2)=0.0564, \\delta_L=0.0282, v=2.0141, \\mu=1.274, and a\\langle1+t^2\\rangle=2.014093=v.",
"depends_on": [
"MC.2",
"M4.7",
"MC.1"
],
"constrains": [],
"reasons": {
"MC.2": "the variance ρ/a is reached by the tilted family, whose variance V increases strictly in μ and exceeds 3/min a at μ_max.",
"M4.7": "v must satisfy 2 < v < U(P_c(t), J_c(t)) for every loop member: the relaxed bound plus the viscous inequality.",
"MC.1": "δ_L is shrunk below min(v_s - 2) near ∂I, where the input is already admissible, so v = v_s there."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 159-160"
},
{
"id": "MC.4",
"kind": "move",
"name": "ns-mc-4-the-lift-varphi-exact-mean-a-b-s-and-uniform-admissible",
"title": "The lift \\varphi: exact mean (a,-b_s) and uniform admissible margins (Lemma C.1)",
"section": "C",
"pages": "158-160",
"refs": [
"pp. 158 to 160, Lemma C.1, (C.1) to (C.3)",
"pp. 38 to 39, Lemma 4.11, (4.36) to (4.37)."
],
"statement": "P. 160. Reparametrize \\theta' by \\varphi with \\varphi(0)=0 and d\\varphi/d\\theta'=a(1+t^2)/(2\\pi v), and set (a_L,-b_L)=v(1,t)/(1+t^2). Since a\\langle1+t^2\\rangle_{\\theta'}=v_s+aV=v, \\varphi(\\theta'+2\\pi)=\\varphi(\\theta')+1. Also \\int_0^1a_L\\,d\\varphi=a and \\int_0^1(-b_L)\\,d\\varphi=a\\langle t\\rangle=at_s=-b_s, which is (C.1). Since -b_L/a_L=t and a_L(1+t^2)=v, each member's own ratio and instability level are (t,v), and each is admissible with p_s fixed.",
"description": "P. 160. Reparametrize \\theta' by \\varphi with \\varphi(0)=0 and d\\varphi/d\\theta'=a(1+t^2)/(2\\pi v), and set (a_L,-b_L)=v(1,t)/(1+t^2). Since a\\langle1+t^2\\rangle_{\\theta'}=v_s+aV=v, \\varphi(\\theta'+2\\pi)=\\varphi(\\theta')+1. Also \\int_0^1a_L\\,d\\varphi=a and \\int_0^1(-b_L)\\,d\\varphi=a\\langle t\\rangle=at_s=-b_s, which is (C.1). Since -b_L/a_L=t and a_L(1+t^2)=v, each member's own ratio and instability level are (t,v), and each is admissible with p_s fixed. OBLIGATION: Proposition C.2 needs three things from the loop. It needs a period-one family whose \\varphi-mean is exactly the input shear, so that a_L-a and E(b_L-b_s) have zero mean and admit periodic antiderivatives (C.11). It needs a uniform margin \\kappa_L, so that O(N^{-1}) perturbations stay admissible. And it needs constancy near \\partial I, so that the modification is compactly supported inside I. MECHANISM: Directions with the right mean ratio are not yet vectors with the right mean. Weighting each direction by the time the loop spends there fixes both components at once. ANTECEDENT: None cited. REFS: pp. 158 to 160, Lemma C.1, (C.1) to (C.3); pp. 38 to 39, Lemma 4.11, (4.36) to (4.37).",
"obligation": "Proposition C.2 needs three things from the loop. It needs a period-one family whose \\varphi-mean is exactly the input shear, so that a_L-a and E(b_L-b_s) have zero mean and admit periodic antiderivatives (C.11). It needs a uniform margin \\kappa_L, so that O(N^{-1}) perturbations stay admissible. And it needs constancy near \\partial I, so that the modification is compactly supported inside I.",
"backward_question": "\"Given admissible directions t(\\theta') with mean t_s at a common level v, how do I make the vectors themselves, not just their ratios, average to exactly (a,-b_s)?\"",
"mechanism": "Directions with the right mean ratio are not yet vectors with the right mean. Weighting each direction by the time the loop spends there fixes both components at once. With speed proportional to (1+t^2)/v, the vectors v(1,t)/(1+t^2) integrate to (a/2\\pi)\\int_0^{2\\pi}(1,t)\\,d\\theta'=(a,at_s). Normalizing the period to one is exactly the identity a\\langle1+t^2\\rangle=v, which is why MC.3 set v=v_s+aV. The inverse reparametrization is smooth because d\\varphi/d\\theta' has a positive minimum on the compact family. (Digest's note: v_s=a+b_s^2/a is jointly convex in (a,b_s) on a>0, being the perspective of 1+t^2. By Jensen, a nonconstant loop with mean shear (a,-b_s) must contain shears with larger v_s; the construction puts every member at the same level v_s+a\\,\\mathrm{Var}(t).)",
"antecedent": "None cited.",
"cost": "Constants \\kappa_L and \\delta_\\partial, depending on a,b_s,p_s,I.",
"checkable": "By quadrature in \\theta', check \\int_0^{2\\pi}(d\\varphi/d\\theta')\\,d\\theta'=1, \\int a_L\\,(d\\varphi/d\\theta')\\,d\\theta'=a, \\int(-b_L)(d\\varphi/d\\theta')\\,d\\theta'=-b_s, and \\min_{\\theta'}\\Psi_j(a_L,b_L,p_s)>0 for j=1,\\dots,4. The digest ran this at three samples: the period was 1.000000, both means were exact to six digits, and all four minimal gaps were positive (for a=1, b_s=0.3, p_s=(5,1): 0.630, 0.0141, 1.706, 5.045).",
"depends_on": [
"MC.3",
"MC.2",
"M4.7"
],
"constrains": [],
"reasons": {
"MC.3": "the level v = v_s + aV of (C.9), (C.10) makes the reparametrized period exactly 1 and every member admissible.",
"MC.2": "the ratio family has mean t_s, so the φ-weighted vectors v(1, t)/(1 + t²) average to (a, at_s) = (a, -b_s).",
"M4.7": "each member (t, v) with 2 < v < U(P_c(t), J_c(t)) is admissible by Lemma 4.5, giving the margin (C.2)."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 158-160"
},
{
"id": "MC.5",
"kind": "move",
"name": "ns-mc-5-fast-radial-modulation-at-phase-n-log-x-with-exact-shear",
"title": "Fast radial modulation at phase N\\log X with exact shear identities",
"section": "C",
"pages": "161",
"refs": [
"p. 161, (C.11) to (C.13)",
"duplicated in section 4.6 Step 2, p. 41, (4.38)",
"outline p. 10, item 4."
],
"statement": "P. 161. Let \\mathcal A,\\mathcal B be the zero-mean periodic antiderivatives \\partial_\\varphi\\mathcal A=-\\tfrac12(a_L-a) and \\partial_\\varphi\\mathcal B=\\tfrac12E(b_L-b_s) (C.11). They exist by (C.1), vanish near \\partial I, and are extended by zero. Set E_N=E\\exp(\\mathcal A(X,\\eta,N\\log X)/N) and U_N=U+\\mathcal B(X,\\eta,N\\log X)/N (C.12). Then, exactly, a_N=a_L-2D_X\\mathcal A/N and b_N=e^{-\\mathcal A/N}(b_L+2D_X\\mathcal B/(NE)) (C.13).",
"description": "P. 161. Let \\mathcal A,\\mathcal B be the zero-mean periodic antiderivatives \\partial_\\varphi\\mathcal A=-\\tfrac12(a_L-a) and \\partial_\\varphi\\mathcal B=\\tfrac12E(b_L-b_s) (C.11). They exist by (C.1), vanish near \\partial I, and are extended by zero. Set E_N=E\\exp(\\mathcal A(X,\\eta,N\\log X)/N) and U_N=U+\\mathcal B(X,\\eta,N\\log X)/N (C.12). Then, exactly, a_N=a_L-2D_X\\mathcal A/N and b_N=e^{-\\mathcal A/N}(b_L+2D_X\\mathcal B/(NE)) (C.13). OBLIGATION: It turns the loop, a function of an extra variable \\varphi, into actual radial profiles. Their shear (4.11) at radius X equals the loop shear at phase N\\log X, up to O(N^{-1}). MECHANISM: After substituting \\varphi=N\\log X, X\\partial_X=D_X+N\\partial_\\varphi. The prefactor 1/N cancels the N from N\\partial_\\varphi, so the order-one part of the shear is \\partial_\\varphi\\mathcal A and \\partial_\\varphi\\mathcal B, which were defined to be. ANTECEDENT: None cited. (Digest's note: this is a one-dimensional fast-oscillation device, in which a small, rapidly varying function has a derivative that follows a prescribed loop with prescribed mean.) REFS: p. 161, (C.11) to (C.13); duplicated in section 4.6 Step 2, p. 41, (4.38); outline p. 10, item 4.",
"obligation": "It turns the loop, a function of an extra variable \\varphi, into actual radial profiles. Their shear (4.11) at radius X equals the loop shear at phase N\\log X, up to O(N^{-1}).",
"backward_question": "\"The shear is a logarithmic radial derivative of the profiles. Can I make that derivative trace a prescribed periodic loop by adding a small, rapidly oscillating term whose own derivative carries the deviation?\"",
"mechanism": "After substituting \\varphi=N\\log X, X\\partial_X=D_X+N\\partial_\\varphi. The prefactor 1/N cancels the N from N\\partial_\\varphi, so the order-one part of the shear is \\partial_\\varphi\\mathcal A and \\partial_\\varphi\\mathcal B, which were defined to be the loop deviations. What remains is D_X(\\cdot)/N. Modulating \\log E additively makes a_N linear in \\mathcal A. The axial shear picks up only the factor e^{-\\mathcal A/N}, which is why \\mathcal B carries the factor E. The phase is logarithmic because the shear is defined with D_X. Across I the shear traverses the loop N\\log(X_+/X_-) times.",
"antecedent": "None cited. (Digest's note: this is a one-dimensional fast-oscillation device, in which a small, rapidly varying function has a derivative that follows a prescribed loop with prescribed mean.)",
"cost": "The large integer N. Mixed derivatives of the profile change with r\\ge1 radial derivatives are only O(N^{r-1}). So X\\partial_X(E_N-E) is order one, and the new profile is not C^1-close in X to the input. All later profile derivative bounds carry N-dependent constants.",
"checkable": "Symbolic: differentiate (C.12) with \\varphi=N\\log X and substitute (C.11) to recover (C.13). The digest ran this in sympy and obtained a_N=a-2\\partial_\\varphi\\mathcal A-2D_X\\mathcal A/N and b_Ne^{\\mathcal A/N}=2(XU_X+\\partial_\\varphi\\mathcal B+X\\partial_X\\mathcal B/N)/E. Inserting (C.11) gives (C.13).",
"depends_on": [
"MC.4",
"M4.4"
],
"constrains": [],
"reasons": {
"MC.4": "the zero-mean antiderivatives (C.11) exist because the loop's φ-mean is exactly (a, -b_s) (C.1), and vanish near ∂I by (C.3).",
"M4.4": "the shear formulas a = 1 - 2D_X log E and b_s = 2D_XU/E of (4.11) give (C.13) once φ = N log X."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 161"
},
{
"id": "MC.6",
"kind": "move",
"name": "ns-mc-6-values-not-derivatives-o-n-1-control-of-moments-pressure",
"title": "Values, not derivatives: O(N^{-1}) control of moments, pressure, and p_s, and persistence of the cone",
"section": "C",
"pages": "161-162",
"refs": [
"pp. 161 to 162, (C.14) to (C.16)",
"pp. 28 to 30, (4.15) to (4.17), Lemma 4.4(ii) and the remark on p. 30",
"section 4.6, pp. 41 to 42, (4.39) to (4.41)."
],
"statement": "Pp. 161 to 162. The estimates hold on the fixed range from X_- through the first correction interval, where X,E,H,L are bounded below. (C.14) gives \\sup_X\\sum_{j\\le m}(|\\partial_\\eta^j(E_N-E)|+|\\partial_\\eta^j(U_N-U)|)\\le C_mN^{-1}. The same bound holds for the shears (C.13) minus their loop values, while mixed derivatives with r\\ge1 radial derivatives are only C_{r,m}N^{r-1}. The axis pressure \\Pi_0(\\eta) is kept, so \\Pi_N=\\Pi_0+C_{p,N}.",
"description": "Pp. 161 to 162. The estimates hold on the fixed range from X_- through the first correction interval, where X,E,H,L are bounded below. (C.14) gives \\sup_X\\sum_{j\\le m}(|\\partial_\\eta^j(E_N-E)|+|\\partial_\\eta^j(U_N-U)|)\\le C_mN^{-1}. The same bound holds for the shears (C.13) minus their loop values, while mixed derivatives with r\\ge1 radial derivatives are only C_{r,m}N^{r-1}. The axis pressure \\Pi_0(\\eta) is kept, so \\Pi_N=\\Pi_0+C_{p,N}. OBLIGATION: The cone test (4.35) involves p_s as well as the shear, and the loop was built with p_s frozen. So the modulated profile's p_s must stay within the margin \\kappa_L. The estimates also secure E_N>0 and the hypotheses of Lemma 4.4(ii). MECHANISM: The phase N\\log X does not depend on \\eta, so \\eta-derivatives never hit it and produce no powers of N. Every parameter derivative of the profile change therefore stays O(N^{-1}). The moments (4.15) integrate values. ANTECEDENT: Lemma 4.4(ii) (internal). No external citation. REFS: pp. 161 to 162, (C.14) to (C.16); pp. 28 to 30, (4.15) to (4.17), Lemma 4.4(ii) and the remark on p. 30; section 4.6, pp. 41 to 42, (4.39) to (4.41).",
"obligation": "The cone test (4.35) involves p_s as well as the shear, and the loop was built with p_s frozen. So the modulated profile's p_s must stay within the margin \\kappa_L. The estimates also secure E_N>0 and the hypotheses of Lemma 4.4(ii).",
"backward_question": "\"Does the integrated inviscid vector p_s, which enters the cone test, see the fast oscillation at all? Which terms of (4.16) contain radial derivatives, and do \\eta-derivatives of the oscillation cost powers of N?\"",
"mechanism": "The phase N\\log X does not depend on \\eta, so \\eta-derivatives never hit it and produce no powers of N. Every parameter derivative of the profile change therefore stays O(N^{-1}). The moments (4.15) integrate values. Q_s and N_s in (4.16) involve only values, moments, and first \\eta-derivatives of moments, divided by XH and X. So p_s is Lipschitz in these data (Lemma 4.4(ii), (4.17), whose estimate contains no radial derivative of a difference). Between I and the patch, the profile values and shear are unchanged, but p_s still moves by O(N^{-1}) through the cumulative moments from the axis. The input's strict admissibility absorbs that.",
"antecedent": "Lemma 4.4(ii) (internal). No external citation.",
"cost": "It uses positive lower bounds for X,E,H,L on the fixed range and one extra \\eta-derivative for p_s. N must exceed thresholds set by \\kappa_L and the Lipschitz constant of \\Psi on a compact neighborhood. Section 4.6 makes this explicit in (4.41): \\Psi_i\\ge\\mu_L-C_\\Psi(B_0+P_0)/N\\ge\\mu_L/2 on I, and \\ge\\mu_R/2 on [X_+,Y_1].",
"checkable": "Take a smooth test profile on a compact X-interval and any smooth zero-mean periodic \\mathcal A,\\mathcal B, and build E_N,U_N for N=10,20,40,80. Compute the moments (4.15) by cumulative quadrature, Q_s,N_s by (4.16), and p_s by (4.11). Confirm that \\sup|E_N-E|, \\sup|\\partial_\\eta(E_N-E)|, \\sup|m_N-m|, and \\sup|p_{s,N}-p_s| scale like N^{-1}, while \\sup|X\\partial_X(E_N-E)| stays order one. (Not run by the digest.)",
"depends_on": [
"MC.5",
"M4.6",
"MC.4"
],
"constrains": [],
"reasons": {
"MC.5": "estimates the modulated profiles (C.12), whose values move by O(N^{-1}) because the phase N log X carries no η-dependence.",
"M4.6": "Lemma 4.4(ii) bounds Δp_s by value and moment changes with no radial derivative (4.17), so p_s moves only O(N^{-1}).",
"MC.4": "the loop's uniform margin κ_L (C.2) absorbs the O(N^{-1}) errors, so the admissible cone persists on I."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 161-162"
},
{
"id": "MC.7",
"kind": "move",
"name": "ns-mc-7-exact-restoration-of-the-five-cumulative-moments-on-the",
"title": "Exact restoration of the five cumulative moments on the first reserved patch",
"section": "C",
"pages": "162-163",
"refs": [
"pp. 162 to 163",
"pp. 126 to 128, Lemma A.1, (A.1), Lemma A.2, (A.2) to (A.3), Corollary A.3, (A.4)",
"p. 129, (A.5), (A.9)",
"section 4.6 Step 3, pp. 42 to 43, (4.42)."
],
"statement": "Pp. 162 to 163. The correction sits on the first patch listed after (A.9). In the local log coordinate of the intermediate power-law interval this is (T_w-25,T_w-20) with T_w=60\\log(1/\\lambda), reserved on p. 129 for the correction that follows cone realization. There the input has U=0 and E=K(\\eta)X^{-1/2-\\lambda}, with K smooth and bounded below. Add two fixed compact bumps to U and three to E, with \\eta-dependent coefficients. Order the moments at the right endpoint as (M,J;I,S,C_p).",
"description": "Pp. 162 to 163. The correction sits on the first patch listed after (A.9). In the local log coordinate of the intermediate power-law interval this is (T_w-25,T_w-20) with T_w=60\\log(1/\\lambda), reserved on p. 129 for the correction that follows cone realization. There the input has U=0 and E=K(\\eta)X^{-1/2-\\lambda}, with K smooth and bounded below. Add two fixed compact bumps to U and three to E, with \\eta-dependent coefficients. Order the moments at the right endpoint as (M,J;I,S,C_p). OBLIGATION: Every larger radius sees the cumulative integrals from the axis ((4.10), (4.16)). An uncorrected O(N^{-1}) moment error would propagate outward. The total moment identities (4.28) would fail, so the exterior stress would acquire the r^{-2} and r^{-1} tails described on p. 30 and would not vanish beyond X_b. ANTECEDENT: Lemmas A.1 and A.2 and Corollary A.3 (internal). The proof of Lemma A.1 is a Rolle's theorem induction; no external source is cited. REFS: pp. 162 to 163; pp. 126 to 128, Lemma A.1, (A.1), Lemma A.2, (A.2) to (A.3), Corollary A.3, (A.4); p. 129, (A.5), (A.9); section 4.6 Step 3, pp. 42 to 43, (4.42).",
"obligation": "Every larger radius sees the cumulative integrals from the axis ((4.10), (4.16)). An uncorrected O(N^{-1}) moment error would propagate outward. The total moment identities (4.28) would fail, so the exterior stress would acquire the r^{-2} and r^{-1} tails described on p. 30 and would not vanish beyond X_b. The pressure normalization (4.25), the terminal compensation, and the heat exterior would all shift.",
"backward_question": "\"The modulation leaves O(N^{-1}) errors in five integrals that control everything farther out. Is there a place where the base profile is a pure power law with U=0, so that five bumps give an invertible, nearly linear map onto those integrals without disturbing the cone?\"",
"mechanism": "Because the base has U=0 on the patch, the linearization decouples: U-bumps move only (M,J), and E-bumps move only (I,S,C_p). Each block is a moment matrix B_{ij}=\\int X^{\\alpha_i}\\beta_j\\,dX. By multilinearity, its determinant integrates the generalized Vandermonde determinant \\det[x_j^{\\alpha_i}] against the bumps. That determinant has constant sign on ordered points, because a nonzero combination of m distinct powers has at most m-1 positive zeros (Rolle induction, p. 127). The quadratic part is absorbed by the contraction c\\mapsto B^{-1}(d-Q(c,c)) on the ball of radius 2\\beta_0d_0, valid when 8\\beta_0^2\\kappa_0d_0\\le1 (Lemma A.2). Taking N large makes d_0=O(N^{-1}) small enough.",
"antecedent": "Lemmas A.1 and A.2 and Corollary A.3 (internal). The proof of Lemma A.1 is a Rolle's theorem induction; no external source is cited.",
"cost": "It consumes the first reserved patch. The U-block inverse degenerates like \\lambda^{-1} as the weights 1 and X^{-\\lambda} coalesce (pp. 127 to 128; the paper claims no uniformity in that limit), so \\lambda must be fixed before N. N is chosen after \\lambda, the patch scales, and all input choices. Smallness is needed only for finitely many \\eta-orders.",
"checkable": "Compute B_{ij}=\\int X^{\\alpha_i}\\beta_j(X)\\,dX for \\alpha=(0,-\\lambda) and \\alpha=(1/2,-1/2-\\lambda,-3/2-\\lambda), with rescaled \\sigma' bumps ((A.5)) on ordered disjoint log-intervals. Confirm \\det\\ne0, that \\lambda\\,\\mathrm{cond}(B_U) stays bounded as \\lambda\\to0, and that \\mathrm{cond}(B_E) stays bounded. Then iterate c\\mapsto B^{-1}(d-Q(c,c)) with |d|\\sim N^{-1} and verify convergence with \\|c\\|\\le2\\beta_0\\|d\\|. The digest computed the conditioning: \\lambda\\,\\mathrm{cond}(B_U)\\approx5.9,6.1,6.1 at \\lambda=0.1,0.01,0.001, and \\mathrm{cond}(B_E)\\approx2\\times10^4, flat in \\lambda, for its bump placement.",
"depends_on": [
"MC.6",
"MA.3",
"MA.4",
"MA.2"
],
"constrains": [],
"reasons": {
"MC.6": "cancels the O_m(N^{-1}) discrepancy (C.15) that the modulation leaves in the five cumulative moments.",
"MA.3": "at α = -1/2 - λ, two U bumps and three E bumps give block-diagonal distinct-power Jacobians, invertible by Corollary A.3.",
"MA.4": "the bumps sit on the schedule's first reserved patch (T_w - 25, T_w - 20), where U = 0 and E = K(η)X^{-1/2-λ}.",
"MA.2": "the exactly quadratic system is solved by Lemma A.2 with O_m(N^{-1}) coefficients in each fixed η-order."
},
"statement_leaks_reason": false,
"statement_leaks_answer": false,
"verified": true,
"source": "OpenAI 2026, Finite Time Blowup for Navier-Stokes, pp. 162-163"
},