we-solve (beta)

Phys-80 · physics · mathematics · Physics

The Riemannian Penrose bound with minimizing frontiers in every dimension

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
In every $n\geq 3$, let a complete connected one-ended Euclidean exterior have smooth metric through a compact outer-minimizing locally perimeter-minimizing frontier, whose regular part is minimal and whose singular set has dimension at most $n-8$. Assume nonnegative integrable scalar curvature decaying as $O(r^{-n-\beta })$, $\beta >0$, and $g-\delta =O_2(r^{-\tau })$, $\tau >(n-2)/2$. Is $m_ADM\geq (1/2)(H^{n-1}(frontier)/\omega _{n-1})^((n-2)/(n-1))$?

Short English statement

In every $n\geq 3$, let a complete connected one-ended Euclidean exterior have smooth metric through a compact outer-minimizing locally perimeter-minimizing frontier, whose regular part is minimal and whose singular set has dimension at most $n-8$. Assume nonnegative integrable scalar curvature decaying as $O(r^{-n-\beta })$, $\beta >0$, and $g-\delta =O_2(r^{-\tau })$, $\tau >(n-2)/2$. Is $m_ADM\geq (1/2)(H^{n-1}(frontier)/\omega _{n-1})^((n-2)/(n-1))$?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Phys-80-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Phys-80

The numerical Riemannian mass-area inequality is claimed in every dimension for full outer-minimizing, locally perimeter-minimizing frontiers, including singular and disconnected ones. The question retains these same parameters and conventions. Within these assumptions, this is a claimed affirmative answer to the stated question.

The Riemannian Penrose bound with minimizing frontiers in every dimension

OpenAI's claim

OpenAI presents a proof in the selected manuscript. The numerical Riemannian mass-area inequality is claimed in every dimension for full outer-minimizing, locally perimeter-minimizing frontiers, including singular and disconnected ones.

Mathematical statement of the claimed result

Result 1.
For $n\ge3$, let $(E,h)$ be a connected complete exterior with one Euclidean end and compact complement, including its complete possibly singular frontier $\Sigma$. Completeness is measured within each finite-distance class of its intrinsic length metric. The metric extends smoothly through the frontier and satisfies \[ R_h\ge0,\quad R_h\in L^1(E,dV_h),\quad R_h=O(r^{-n-\beta})\ (\beta>0),\qquad h-\delta=O_2(r^{-\tau})\ (\tau>(n-2)/2). \] The full frontier is the perimeter support of a filled side, outer minimizing and locally perimeter minimizing on both sides. Its regular part is smooth, embedded and minimal; its singular part satisfies $\dim_{\mathrm H}\Sigma_{\mathrm{sing}}\le n-8$. With $\omega_{n-1}=|\mathbb S^{n-1}|$ and the usual ADM energy normalization $[2(n-1)\omega_{n-1}]^{-1}$, \[ m_{\mathrm{ADM}}(h)\ge\frac12\left(\frac{\mathcal H_h^{n-1}(\Sigma)}{\omega_{n-1}}\right)^{(n-2)/(n-1)}. \] Every frontier component contributes to the area; no spin or frontier-connectedness hypothesis is imposed.

Outline of the argument

A conformal flow is built from smooth obstacles while preserving frontier area. Regular-patch estimates control forcing, and distance-median separation handles the singular region; mass monotonicity and the limiting comparison give the stated numerical 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. No Comparator is assigned to the selected manuscript here; the family page selects other papers or supporting statements. 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

Go to contribution →