Local Smoothing for the Euclidean Wave Equation

Local Smoothing for the Euclidean Wave Equation

OpenAI's claim

Wave local smoothing: OpenAI claims the critical $L^3$ spacetime estimate for the wave equation in three dimensions with any positive Sobolev loss. This is the Euclidean three-dimensional smoothing assertion at that exponent.

Mathematical statement of the claimed result

Mathematical claim 1.

Let $Uf(x,t)=(2\pi)^{-3}\int e^{i(x\cdot\xi+t|\xi|)}\widehat f(\xi)\,d\xi$ and $J^\epsilon=(1-\Delta)^{\epsilon/2}$. The claimed three-dimensional critical local-smoothing estimate is \[\|Uf\|_{L^3(\mathbb R^3\times[1,2])}\le C_\epsilon\|J^\epsilon f\|_{L^3(\mathbb R^3)}\quad(\epsilon>0,\ f\in\mathcal S(\mathbb R^3)).\] Every positive Sobolev loss is allowed, but zero loss is not asserted.

Outline of the argument

Wave local smoothing: Null coordinates put light rays into a quadratic velocity model, and packet synthesis reduces the physical estimate to a cubic mass sum. Entropy records retain changing shear frames as well as direction and time. Planar Furstenberg and cone-envelope inputs constrain those records, giving a frequency-annulus estimate that can be summed with arbitrarily small loss.

Formal verification

Wave local smoothing: The pinned catalogue lists no Lean formalization for this result.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

• OpenAI, Critical local smoothing for the three-dimensional wave equation, 2026-09-24; citation key OAI:Critical-local-smoothing-for-the-three-dimensional-wave-equation-September-24-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• OpenAI catalogue entry.

Local Smoothing for the Euclidean Wave Equation

Definitions and mathematical statement

For a Schwartz function on ${\mathbb{R}}^n$, the half-wave propagator is the Fourier multiplier $\widehat{e^{it\sqrt{-\Delta}}f}(\xi)=e^{it|\xi|}\widehat f(\xi)$, using the Fourier convention in which $-\Delta$ has symbol $|\xi|^2$. Define the Bessel-potential norm $\|f\|_{W^{s,p}}=\|(1-\Delta)^{s/2}f\|_{L^p}$ and put $s_p=(n-1)(1/2-1/p)$. The assertion is \[ \left(\int_1^2\int_{{\mathbb{R}}^n}|e^{it\sqrt{-\Delta}}f(x)|^p\,\mathrm d x\,\mathrm d t\right)^{1/p} \le C_{n,p,\varepsilon}\|f\|_{W^{s_p-1/p+\varepsilon,p}} \] for $n\ge3$, $p>2n/(n-1)$, and every $\varepsilon>0$. Constants are independent of $f$. This is a spacetime estimate with an arbitrarily small derivative loss; the excluded endpoint and a zero-loss bound are not asserted.

Formulation and concept references: [S1].

Short English statement

Does averaging the wave evolution over time save almost one-over-p derivatives throughout the conjectured range of exponents?

Sources

• S1 Formal statement, Introduction, local smoothing conjecture. https://www.sciencedirect.com/science/article/pii/S0022123623003786. Catalogue formulation source.
• E1 J. Bourgain and C. Demeter, The proof of the $\ell^2$ Decoupling Conjecture, Annals of Mathematics $2$ 182 $2015$, no. 1, 351--389, Theorem 1.2 (cone decoupling) and the discussion immediately following it. https://annals.math.princeton.edu/2015/182-1/p09; author manuscript https://arxiv.org/pdf/1403.5335v3. Published result; consulted 24 September 2026.
• E2 S. Gan, D. He, X. Li, and S. Wu, On local smoothing estimates for wave equations, arXiv:2502.05973v2, 4 January 2026, Theorem 1.3, equation $1.4$, and Sections 1.1, 1.3, and 5.1. https://arxiv.org/html/2502.05973v2. Recent manuscript theorem, not independently audited here; version 2 has four authors and an improved main result. Consulted 24 September 2026.
• E3 D. Beltran, J. Roos, A. Rutar, and A. Seeger, A fractal local smoothing problem for the wave equation, Bulletin of the London Mathematical Society 57 $2025$, no. 12, 3667--3690; author manuscript arXiv:2501.12805v1, 22 January 2025, Theorem 1.1, equation $1.6$, and Section 5 (radial inputs). https://arxiv.org/html/2501.12805v1. The radial theorem, not its January 2025 general-frontier summary, is used here. Consulted 24 September 2026.

Local Smoothing for the Euclidean Wave Equation

Definitions and mathematical statement

For a Schwartz function on ${\mathbb{R}}^n$, the half-wave propagator is the Fourier multiplier $\widehat{e^{it\sqrt{-\Delta}}f}(\xi)=e^{it|\xi|}\widehat f(\xi)$, using the Fourier convention in which $-\Delta$ has symbol $|\xi|^2$. Define the Bessel-potential norm $\|f\|_{W^{s,p}}=\|(1-\Delta)^{s/2}f\|_{L^p}$ and put $s_p=(n-1)(1/2-1/p)$. The assertion is \[ \left(\int_1^2\int_{{\mathbb{R}}^n}|e^{it\sqrt{-\Delta}}f(x)|^p\,\mathrm d x\,\mathrm d t\right)^{1/p} \le C_{n,p,\varepsilon}\|f\|_{W^{s_p-1/p+\varepsilon,p}} \] for $n\ge3$, $p>2n/(n-1)$, and every $\varepsilon>0$. Constants are independent of $f$. This is a spacetime estimate with an arbitrarily small derivative loss; the excluded endpoint and a zero-loss bound are not asserted.

Formulation and concept references: [S1].

Short English statement

Does averaging the wave evolution over time save almost one-over-p derivatives throughout the conjectured range of exponents?

Research attempt

Current frontier and source audit (24 September 2026).

The published cone decoupling theorem of Bourgain--Demeter gives the desired almost-$1/p$ gain in the range $p\geq 2(n+1)/(n-1)$; this is not the full range in this entry. [E1] The more recent manuscript of Gan--He--Li--Wu, version 2 of 4 January 2026, states the improved range $p\geq P_n$, where \begin{equation}\label{wsref-0-72-61-33-30-30-30-34-38-34-34-3a-66-72-6f-6e-74-69-65-72} P_n=\begin{cases} 2+\dfrac{8}{3n-3},&n\text{ odd},\\[4pt] 2+\dfrac{8}{3n-2-\omega(n)},&n\text{ even}, \end{cases} \qquad \omega(n)=\frac{4(7n-2)}{3n^2+5n+14}. \end{equation} Its Theorem 1.3 treats both flat and compact-manifold problems. In particular, $P_3=10/3$, whereas the present flat-space target begins at $p>3$. The manuscript's sharp odd-dimensional manifold result must not be read as a resolution of the stronger Euclidean range. This notebook uses its stated theorem as recent frontier information, not as an independently refereed proof supplied here. [E2] Radial inputs are a genuinely easier, already studied subcase; the 2025 paper of Beltran--Roos--Rutar--Seeger proves even a fractal-time radial extension. [E3] The attack below rederives a radial estimate by an elementary one-dimensional calculation, and then tries to remove the radial hypothesis. That calculation is not claimed as a new theorem. The publisher text at the original [S1] was not retrievable in this session. No missing definition is filled in from it: the displayed, self-contained target in the supplied document is used verbatim.

Attack map.

Write $U_t=e^{it\sqrt{-\Delta}}$ and \[ p_* =\frac{2n}{n-1},\qquad a_n(p)=s_p-\frac1p=\frac{n-1}{2}-\frac np. \] Three possible routes were considered. Interpolation from an available large-$p$ theorem would need a better low-$p$ input; the exact loss is computed below. A second route transports each narrow angular cap almost without distortion and then tries to exploit time averaging when the caps are recombined; its missing ingredient is a deterministic, phase-sensitive synthesis estimate, not an estimate for an individual cap. The route pursued most fully is to solve the radial dynamics exactly in dimension three and then expand in spherical harmonics. It would need uniform control of the angular-momentum barrier and the summation of angular modes. Bounds for one fixed spherical harmonic do not supply those two uniformities.

Attempt A: make the frequency and interpolation losses explicit.

Fix smooth dyadic annular projections $P_\lambda$, $\lambda=2^k\geq2$, with slightly larger annular cutoffs available. The sufficient frequency-localized statement is \begin{equation}\label{wsref-0-72-61-33-30-30-30-34-38-34-34-3a-64-79-61-64-69-63} \|U_t g\|_{L^p({\mathbb{R}}^n\times[1,2])} \leq C_{n,p,\eta}\lambda^{a_n(p)+\eta}\|g\|_p, \qquad \operatorname{supp}\widehat g\subset \{\lambda/2\leq|\xi|\leq2\lambda\}, \end{equation} for every $\eta>0$, with harmless changes of the fixed annulus. To see that this suffices for the stated assertion, take $\eta=\varepsilon/2$ and put $s=a_n(p)+\varepsilon$. Annular multiplier bounds give \[ \|P_{2^k}f\|_p\leq C_s2^{-ks}\|(1-\Delta)^{s/2}f\|_p. \] The triangle inequality and $\sum_{k\geq1}2^{-k\varepsilon/2}<\infty$ prove the assertion. The low-frequency term is uniformly bounded for $1<p<\infty$ by the multiplier theorem; $e^{it|\xi|}$ need not be declared smooth at $\xi=0$ to use that theorem. One first applies the argument to finite dyadic sums and then passes in $L^p$ to the limit. Conversely, the requested Sobolev estimate implies (ra30004844:dyadic), with the same arbitrarily small loss, by applying the Bessel multiplier on an annulus. Thus no summability problem is being hidden in the notation. Here is an obstruction to the first attack route. Suppose the sharp frequency exponent $a_n(q)$ is available at some $q>p_*$. Interpolating that estimate with the exact $L^2$ identity on the time interval of length one gives, for $2<p<q$, \[ \vartheta=\frac{\frac12-\frac1p}{\frac12-\frac1q},\qquad b(p)=\vartheta a_n(q). \] An elementary subtraction yields \begin{equation}\label{wsref-0-72-61-33-30-30-30-34-38-34-34-3a-69-6e-74-65-72-70-6f-6c-61-74-69-6f-6e-6c-6f-73-73} b(p)-a_n(p)=\frac{1-\vartheta}{2}>0. \end{equation} The arbitrarily small losses at $q$ do not remove this fixed positive loss. For example, $n=3$, $q=10/3$, $p=3$ give $\vartheta=5/6$ and a loss of $1/12$ derivatives. Here $p=3$ is only a boundary diagnostic; (ra30004844:interpolationloss) is also positive throughout the unproved open interval $3<p<10/3$. Supplying a negative power of $\lambda$ at $L^2$ to repair the interpolation is impossible: unitarity gives $\|U_tg\|_{L^2_{x,t}}=\|g\|_2$ exactly.

Attempt B: an exact radial calculation, including its critical logarithm.

Lemma 201.1 (radial benchmark, independently derived). Let $n=3$, let $f$ be radial and Schwartz, and suppose its Fourier support lies in $\{\lambda/2\leq|\xi|\leq2\lambda\}$, $\lambda\geq2$. For $2\leq p<\infty$, \begin{equation}\label{wsref-0-72-61-33-30-30-30-34-38-34-34-3a-72-61-64-69-61-6c-62-6f-75-6e-64} \|U_tf\|_{L^p({\mathbb{R}}^3\times[1,2])} \leq C_p B_p(\lambda)\|f\|_p, \quad B_p(\lambda)= \begin{cases} 1,&2\leq p<3,\\ (1+\log\lambda)^{1/3},&p=3,\\ \lambda^{1-3/p},&p>3. \end{cases} \end{equation} The implication for the target is only the radial three-dimensional subcase. Its relationship with the established radial theory is discussed in [E3], Theorem 1.1 and Section 5. Proof. Write $f(x)=F(|x|)$ and extend $v(r)=rF(|r|)$ as an odd Schwartz function on ${\mathbb{R}}$. The three-dimensional radial Fourier formula shows that $\widehat v$ is supported where $\lambda/2\leq|\rho|\leq2\lambda$. Equivalently, conjugating the radial Laplacian by multiplication by $r$ gives the one-dimensional Dirichlet Laplacian, or the ordinary Laplacian on odd functions. Let $g$ be the positive-frequency part of $v$. Since the Fourier support avoids zero, this part can be obtained using a fixed smooth multiplier $m(\rho/\lambda)$ which is one on the positive annulus and zero on the negative annulus. Oddness implies $v(r)=g(r)-g(-r)$, hence exactly \begin{equation}\label{wsref-0-72-61-33-30-30-30-34-38-34-34-3a-72-61-64-69-61-6c-69-64-65-6e-74-69-74-79} rU_tf(r)=g(r+t)-g(t-r),\qquad r>0. \end{equation} This is an identity for the half-wave, not a replacement of it by the cosine propagator. For $p\geq2$ put $W(r)=(1+|r|)^{2-p}$. The kernel of the smooth positive-frequency cutoff is $K_\lambda(r)=\lambda K(\lambda r)$, where $K$ is Schwartz. The elementary weight comparison \[ \frac{W(x)^{1/p}}{W(y)^{1/p}} \leq (1+|x-y|)^{(p-2)/p} \] and Young's inequality prove \begin{equation}\label{wsref-0-72-61-33-30-30-30-34-38-34-34-3a-77-65-69-67-68-74-65-64-63-75-74-6f-66-66} \|g\|_{L^p(W\,\,\mathrm d r)}+ \lambda^{-1}\|g'\|_{L^p(W\,\,\mathrm d r)} \leq C_p\|v\|_{L^p(W\,\,\mathrm d r)} \leq C_p\|v\|_{L^p(|r|^{2-p}\,\,\mathrm d r)}. \end{equation} Indeed the required weighted $L^1$ norm of $K_\lambda$ is uniformly bounded, and that of $K_\lambda'$ is $O(\lambda)$. The last norm to the $p$th power is $2\int_0^\infty |F(r)|^p r^2\,\mathrm d r$, a fixed multiple of $\|f\|_p^p$. This argument deliberately uses the inhomogeneous weight $W$; claiming a Hilbert-transform bound on $L^p(|r|^{2-p}\,\mathrm d r)$ at $p\geq3$ would be an unjustified shortcut. For $0<r\leq1/2$, all the arguments $t\pm r$ lie in $[1/2,5/2]$. The triangle inequality and then the fundamental theorem of calculus, applied separately, give \[ \|g(t+r)-g(t-r)\|_{L^p_t([1,2])} \leq C_p\min\{1,\lambda r\}\|f\|_p. \] For $r\geq1/2$, substitute $s=t+r$ and $s=t-r$ in the two terms. Since $r^{2-p}\leq C_p(1+|s|)^{2-p}$ on these substitutions, (ra30004844:weightedcutoff) gives \[ \int_1^2\int_{1/2}^{\infty} |g(t+r)-g(t-r)|^p r^{2-p}\,\mathrm d r\,\mathrm d t \leq C_p\|f\|_p^p. \] Using polar coordinates in (ra30004844:radialidentity), the remaining factor is bounded by \begin{equation}\label{wsref-0-72-61-33-30-30-30-34-38-34-34-3a-72-61-64-69-61-6c-69-6e-74-65-67-72-61-6c} 1+\int_0^{1/2}r^{2-p}\min\{1,(\lambda r)^p\}\,\mathrm d r \leq C_p \begin{cases} 1,&p<3,\\ 1+\log\lambda,&p=3,\\ \lambda^{p-3},&p>3. \end{cases} \end{equation} For example, the part $r<\lambda^{-1}$ is $\lambda^{p-3}/3$; the other part is the elementary integral of $r^{2-p}$. Tonelli applies to the nonnegative integrands. This proves the lemma.$\square$ In particular, the radial estimate has the desired power $a_3(p)=1-3/p$ for every $p>3$ without a dyadic power loss, and has only a logarithm at $p=3$. The dyadic summation already proved converts this to the radial version of the original Sobolev assertion. It does not prove an unrestricted zero-loss Sobolev estimate after summing all frequencies.

Attempt C: remove radial symmetry without discarding its cancellation.

The exact identity above suggests expanding \[ f(r\omega)=\sum_{\ell=0}^{\infty}\sum_{m=-\ell}^{\ell} F_{\ell m}(r)Y_{\ell m}(\omega), \qquad -\Delta_{S^2}Y_{\ell m}=\ell(\ell+1)Y_{\ell m}. \] For $w_{\ell m}(r)=rF_{\ell m}(r)$, the radial operator is now \begin{equation}\label{wsref-0-72-61-33-30-30-30-34-38-34-34-3a-61-6e-67-75-6c-61-72-62-61-72-72-69-65-72} L_\ell=-\frac{\mathrm d^2}{\mathrm dr^2} +\frac{\ell(\ell+1)}{r^2} \end{equation} with the regular, Friedrichs boundary condition at zero. The corresponding half-wave is $e^{it\sqrt{L_\ell}}$, not the translated function in (ra30004844:radialidentity). On $r\asymp1$, modes $\ell\asymp\lambda$ have a potential of order $\lambda^2$, comparable to the spectral energy. They cannot be treated as a uniformly small perturbation of $L_0$. Positivity of the potential does not imply pointwise domination of this oscillatory half-wave by the free half-wave. The missing step has two parts: a weighted spacetime estimate for $e^{it\sqrt{L_\ell}}$ which remains controlled through the turning region $r\asymp\ell/\lambda$, and an estimate for the coupled angular sum with the $L^p$ norm of the original sum on the right. A fixed-$\ell$ constant, however finite, is insufficient. There are $(M+1)^2$ modes up to degree $M$; a polynomial loss in $M$ cannot simply be absorbed into $\lambda^\eta$ when $M$ grows on the scale of $\lambda$. No uniform turning-region estimate or cancellation-preserving angular summation bound is established here. This is the precise point at which this extension stops. A complementary localization check helps to locate rather than remove that difficulty. For a cap around $e_n$ of angular width $O(\lambda^{-1/2})$, write $\xi_n=\lambda\rho$ and $\xi'=\sqrt\lambda\,\zeta$, where $\rho$ stays in a fixed compact subset of $(0,\infty)$ and $\zeta$ stays bounded. After removing the translation multiplier $e^{it\xi_n}$, the phase is exactly \begin{equation}\label{wsref-0-72-61-33-30-30-30-34-38-34-34-3a-63-61-70-70-68-61-73-65} t(|\xi|-\xi_n)= \frac{t|\zeta|^2}{\sqrt{\rho^2+\lambda^{-1}|\zeta|^2}+\rho}. \end{equation} All derivatives of this phase times a fixed smooth cap cutoff are uniformly bounded for $1\leq t\leq2$. Its inverse Fourier transform in $(\zeta,\rho)$ has uniformly bounded $L^1$ norm, by integration by parts to order greater than $n$. Anisotropic dilation preserves the kernel's $L^1$ norm. Consequently \[ \sup_{1\leq t\leq2}\|U_tf\|_p\leq C_p\|f\|_p \] for input supported in a slightly smaller such cap. This proves that an individual cap is controllable, but there are $O(\lambda^{(n-1)/2})$ caps. Summing their norms discards exactly the angular information the full conjecture asks us to preserve. The wave-packet and anisotropic-rescaling perspective is also central to [E2], Sections 1.3 and 5.1; no new decoupling inequality is being inferred from the elementary cap calculation.

Stress test: focusing, fake dephasing, and quantifiers.

A counterexample search should first challenge the proposed exponent. Fix $t_0=3/2$ and a nonzero, nonnegative smooth radial $\psi$ supported in $1<|\eta|<2$, and define \[ f_\lambda(x)=\int_{{\mathbb{R}}^n} e^{i\lambda(x\cdot\eta-t_0|\eta|)}\psi(\eta)\,\mathrm d\eta. \] At $|x|,|t-t_0|\leq c/\lambda$, continuity of the phase and positivity of $\int\psi$ give $|U_tf_\lambda(x)|\geq c'>0$, uniformly in $\lambda$. Hence \[ \|U_tf_\lambda\|_{L^p_{x,t}}\gtrsim\lambda^{-(n+1)/p}. \] For completeness, the input estimate is obtained by stationary phase in the angular variables near the two directions parallel to $x$, followed by integration by parts in the radial frequency. On $t_0/2<|x|<2t_0$ this gives, to arbitrarily high order, \[ |f_\lambda(x)|\leq C_N\lambda^{-(n-1)/2} (1+\lambda\,||x|-t_0|)^{-N}+O_N(\lambda^{-N}). \] Outside that bounded annulus the phase gradient does not vanish and integration by parts gives integrable rapid decay, with arbitrary powers of $\lambda^{-1}$. Thus, for fixed finite $p$, \[ \|f_\lambda\|_p\lesssim \lambda^{-(n-1)/2-1/p},\qquad \frac{\|U_tf_\lambda\|_{L^p_{x,t}}}{\|f_\lambda\|_p} \gtrsim\lambda^{a_n(p)}. \] The attempt to beat the proposed power fails: this is a sharpness test, not a counterexample to the stated estimate. For $n=3$ it agrees with the radial upper bound just proved. Another attempted shortcut was to treat radial-frequency pieces as if time averaging provided arbitrary-$L^p$ orthogonality. The proposed scalar ingredient \[ \Big\|\sum_{j=1}^{N}a_je^{ij(t-t_0)}\Big\|_{L^p([1,2])} \leq C_\eta N^\eta\Big(\sum_{j=1}^{N}|a_j|^2\Big)^{1/2} \] is false for $p>2$ and $\eta<1/2-1/p$. Set every $a_j=1$: on $|t-t_0|\leq c/N$ the sum has modulus at least $c'N$, so the left side is at least $c''N^{1-1/p}$, whereas the right side is $C_\eta N^{1/2+\eta}$. This refutes that intermediate lemma, not local smoothing. A successful time-frequency argument must retain the spatial constraints and cannot use this scalar assertion. The radial proof controls the region $r=0$ through the difference in (ra30004844:radialidentity), rather than estimating its two summands separately in a singular weight. The cap proof uses a smooth cutoff supported away from $\rho=0$. Constants may depend on the fixed exponent $p$, which is allowed; they may not depend on angular momentum or the number of caps in a claimed unrestricted estimate. Finally, an endpoint bound at $p_*$ with arbitrarily small loss would be a useful stronger sufficient goal, but the supplied problem excludes that endpoint and it is not silently added to the target.

Outcome.

Outcome: Exploratory approach with unresolved gap. The notebook establishes the dyadic reduction, the exact interpolation loss, the radial three-dimensional estimate with its critical logarithm, and uniform transport for one narrow angular cap. It also supplies explicit tests that defeat a better-than-allowed exponent and a proposed scalar dephasing lemma. The radial estimate belongs to an already known special-case theory; these calculations are not advertised as a new advance in the unrestricted frontier. The unresolved step is uniform angular-momentum control together with cancellation-preserving synthesis, or a genuinely different argument that supplies (ra30004844:dyadic) throughout $p_*<p<P_n$. Neither this interval for arbitrary inputs in dimension three nor the all-dimensional target has been proved or disproved. No numerical experiment has been used as a substitute for either claim.

Sources

• S1 Formal statement, Introduction, local smoothing conjecture. https://www.sciencedirect.com/science/article/pii/S0022123623003786. Catalogue formulation source.
• E1 J. Bourgain and C. Demeter, The proof of the $\ell^2$ Decoupling Conjecture, Annals of Mathematics $2$ 182 $2015$, no. 1, 351--389, Theorem 1.2 (cone decoupling) and the discussion immediately following it. https://annals.math.princeton.edu/2015/182-1/p09; author manuscript https://arxiv.org/pdf/1403.5335v3. Published result; consulted 24 September 2026.
• E2 S. Gan, D. He, X. Li, and S. Wu, On local smoothing estimates for wave equations, arXiv:2502.05973v2, 4 January 2026, Theorem 1.3, equation $1.4$, and Sections 1.1, 1.3, and 5.1. https://arxiv.org/html/2502.05973v2. Recent manuscript theorem, not independently audited here; version 2 has four authors and an improved main result. Consulted 24 September 2026.
• E3 D. Beltran, J. Roos, A. Rutar, and A. Seeger, A fractal local smoothing problem for the wave equation, Bulletin of the London Mathematical Society 57 $2025$, no. 12, 3667--3690; author manuscript arXiv:2501.12805v1, 22 January 2025, Theorem 1.1, equation $1.6$, and Section 5 (radial inputs). https://arxiv.org/html/2501.12805v1. The radial theorem, not its January 2025 general-frontier summary, is used here. Consulted 24 September 2026.