Relativistic initial-data inequality audit

Family 260: Spacetime Penrose inequalities: enclosing area, charge, rotation, and anti-de Sitter extensions. First application triage, 9 October 2026 Australia/Brisbane.

Problem and potential new use

Relativity researchers can compare a numerical initial-data model with the specified mass, enclosing-area, charge and asymptotic assumptions.

Applicability and commercial boundary

The inequality does not compute an astrophysical mass from arbitrary observations. Dominant energy, trapping, decay and equality-rigidity assumptions need independent evidence.

Initial business decision

Research infrastructure. Buyer budget, commercial novelty and profitability are unvalidated.

Next verification action

Extract computable mass/area expressions for one known exact initial-data family.

Evidence scope

The catalog statement was individually reviewed. This record does not imply a manuscript proof review or formal-scope comparison. No independent Lean check was run. Source revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. See source metadata.

Main source

The spacetime Penrose inequality with charge and original-data rigidity.