# Spacetime Penrose inequalities: enclosing area, charge, rotation, and anti-de Sitter extensions

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Area-controlled end replacement and the Bondi–Penrose inequality in the CKS class](../../preprints/Area-controlled-end-replacement-and-the-Bondi-Penrose-inequality-in-the-CKS-class-September-27-2026/paper.pdf)

## Scope

The formalization replaces a three-dimensional Cha–Khuri–Sakovich hyperboloidal end by asymptotically flat ends while preserving each fixed compact interior, completeness, and the dominant energy condition. For strictly future-timelike initial-data charge, the ADM masses approach the invariant Bondi mass and the loss of enclosing area tends to zero.

The Comparator also includes canonical Schwarzschild equality examples at every positive mass, with $m_{\mathrm{Bondi}}=m$ and enclosing area $16\pi m^2$. The paper's general Bondi–Penrose inequality for possibly disconnected weakly trapped boundaries remains unformalized.

The implementation retains a conditional inequality for the connected marginal-boundary case, assuming the asymptotically flat exterior Penrose inequality. This supporting result is not selected as a substitute for the paper's main inequality.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Area-controlled end replacement and Schwarzschild equality examples | [CKSBondiPenrose.lean](../ComparatorChallenges/CKSBondiPenrose.lean) |