OpenAI claim summary for Phys-52

A Bondi enclosing-area inequality for CKS hyperboloidal ends

OpenAI's claim

OpenAI presents a proof in the selected manuscript. CKS hyperboloidal ends are claimed replaceable by asymptotically flat ends with asymptotically unchanged enclosing area and ADM mass tending to invariant Bondi mass.

Mathematical statement of the claimed result

Result 1.

Let a smooth connected orientable three-dimensional exterior be complete including its nonempty compact boundary $S$, with one hyperboloidal end. Use $16\pi\mu=R_g+(\operatorname{tr}_gK)^2-|K|^2$, $8\pi J=\operatorname{div}_g(K-(\operatorname{tr}_gK)g)$ and $\mu\ge|J|$. Put $h=(1+r^2)^{-1}dr^2+r^2\sigma$, $g=h+a$, $K=h+b$. The precise CKS asymptotics are \[ a_{rr}=r^{-5}m^r+O_3(r^{-6}),\quad a_{rA}=O_3(r^{-3}),\quad a_{AB}=r^{-1}m^g_{AB}+O_3(r^{-2}), \] \[ b_{rr}=O_2(r^{-5}),\quad b_{rA}=O_2(r^{-3}),\quad b_{AB}=r^{-1}m^K_{AB}+O_2(r^{-2}), \] with smooth angular leading fields and differentiated component bounds using angular derivatives and $r\partial_r$. For the sphere inclusion $n:\mathbb S^2\to\mathbb R^3$, define \[ M=\operatorname{tr}_\sigma(m^g+2m^K)+2m^r,\quad (E_B,P_B)=\frac1{16\pi}\int_{\mathbb S^2}(1,n)M\,dA_\sigma,\quad E_B>|P_B|. \] These are the initial-data CKS charges, without assuming a spacetime development. Choose a connected smooth end-side region $D\subset\Omega$, closed in $\Omega$, containing the distant end and having its manifold interior in $\operatorname{int}\Omega$. A full cut consists of all of its intrinsic boundary $\Gamma=\partial D$; require this boundary to be compact, smoothly embedded and two-sided. All components and portions coinciding with $S=\partial\Omega$ count. Put $a_g(S)=\inf_\Gamma\operatorname{Area}_g(\Gamma)$. There is a balanced end chart, with $P_B=0$, in which for every sufficiently large $R$ there are complete DEC-preserving asymptotically flat replacements $(G_R,k_R)$ agreeing with $(g,K)$ on the compact side of $r=R$, satisfying $G_R\ge(1-\varepsilon_R)g$, $\varepsilon_R\to0$, and having $P_R=0$, $E_R=m_B+\eta_R$, $0\le\eta_R\le2R^{-1/2}$, where $m_B=\sqrt{E_B^2-|P_B|^2}$. They preserve every cut area up to $1-\varepsilon_R$. If additionally $H+\operatorname{tr}_SK\le0$ and $a_g(S)>0$, the corollary gives \[ m_B\ge\sqrt{a_g(S)/(16\pi)}. \] The boundary may be disconnected. For each $m>0$, horizon-regular Schwarzschild hyperboloidal data attain $m_B=m$, $a_g(S)=16\pi m^2$.

Outline of the argument

Constraint balancing and a rounded collar separate compact interior data from the end replacement. Radial bending preserves the energy condition, and angular and charge estimates show both mass convergence and protection of enclosing cuts; the neutral companion then supplies the Bondi inequality.

Formal verification

For family 260, the only selected family entry is the CKS end-replacement construction and Schwarzschild equality examples. A connected-boundary inequality is conditional on the flat Penrose input; the general Bondi or spacetime inequalities are not formalized there. The listed Comparator files are CKSBondiPenrose.lean. The inventory does not supply a named declaration for these Comparator entries. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

• OpenAI, Area-controlled end replacement and the Bondi–Penrose inequality in the CKS class, 2026-09-27; citation key OAI:Area-controlled-end-replacement-and-the-Bondi-Penrose-inequality-in-the-CKS-class-September-27-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: cor:cks-inequality.
• Family 260: Lean scope.
• Comparator CKSBondiPenrose.json.
• Comparator CKSBondiPenrose.lean.
• OpenAI catalogue entry.