we-solve (beta)

Math-2670 · mathematics · Geometry

Nonnegative Einstein curvature classification in dimension four

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
If a connected closed smooth Riemannian four-manifold has $Ric=3g$ and sectional curvature $\geq 0$, is its universal Riemannian cover isometric to the round $S^{4}$ of curvature 1, the Fubini–Study $CP^{2}$ normalized to $Ric=3g$, or $S^{2}(1/\surd 3)×S^{2}(1/\surd 3)$?

Short English statement

If a connected closed smooth Riemannian four-manifold has $Ric=3g$ and sectional curvature $\geq 0$, is its universal Riemannian cover isometric to the round $S^{4}$ of curvature 1, the Fubini–Study $CP^{2}$ normalized to $Ric=3g$, or $S^{2}(1/\surd 3)×S^{2}(1/\surd 3)$?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2670-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2670

The nonnegative-classification corollary includes both the strictly positive case and the zero-plane case. With the same normalization $\operatorname{Ric}=3g$, it lists exactly the three universal covers required by this question. The main zero-plane theorem supplies one branch of that corollary rather than imposing an additional hypothesis on the full classification.

Nonnegative Einstein curvature classification in dimension four

OpenAI's claim

For closed Einstein four-manifolds with $\operatorname{Ric}=3g$ and nonnegative sectional curvature, OpenAI claims that one zero-curvature plane forces the universal cover to be the product of two round two-spheres of radius $1/\sqrt3$. Its classification corollary claims that every such universal cover is this product, the round four-sphere, or normalized Fubini--Study projective two-space.

Mathematical statement of the claimed result

Mathematical claim 1.
For a connected smooth closed four-manifold with $\operatorname{Ric}_g=3g$ and sectional curvature $\ge0$, the existence of one zero-curvature tangent two-plane is claimed to force its universal Riemannian cover to be \[S^2(1/\sqrt3)\times S^2(1/\sqrt3).\] Its corollary classifies every such universal cover as this product, round $S^4$ of curvature $1$, or Fubini--Study $\mathbb{CP}^2$ with $\operatorname{Ric}=3g$. This is an Einstein four-dimensional assertion, not a classification of all nonnegatively curved manifolds.

Outline of the argument

Zero-plane Einstein rigidity: Bonnet--Myers reduces the analysis to the compact simply connected cover. The two Weyl blocks satisfy a sharp coupled spectral constraint at the boundary of the curvature cone. Extending the weighted comparisons to this boundary and tracking equality forces the product geometry rather than merely a weaker norm bound.

Formal verification

Family 348 describes Lean coverage for the strict-positive-curvature Einstein classification; zero-plane rigidity and the small-energy gap are separate.

Zero-plane Einstein rigidity: No manuscript-specific Comparator is listed in the pinned inventory.

The documented selection does not cover the entire manuscript assertion relevant here.

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

Go to contribution →