Papers With

← All papers
First page of Finite Mass Response to Vanishing Perturbations at Cauchy Horizons

Finite Mass Response to Vanishing Perturbations at Cauchy Horizons

Yi-kun Li

gr-qc Oct 20, 2026 · v1
formalization analysis physics
Read PDF arXiv abstract Code
TL;DR
The paper's mathematical results and proofs on mass response at Cauchy horizons are formalized in Lean 4, with a public repository and verification instructions.
Abstract
Smooth transverse perturbations with vanishing $L^p$ norm, for fixed finite $p\ge4$, can leave a finite positive mass increment at a Cauchy horizon. We prove this at a critical surface-gravity relation in the spherical Einstein–Maxwell–scalar system with positive cosmological constant. Each solution has bounded mass and local finite-energy weak extensions. The response escapes every fixed time window. An analytic law determines its delay and duration, and resolves enhancement or cancellation for overlapping packets.
Problem

Whether smooth transverse perturbations with vanishing L^p norm (fixed finite p≥4) can still produce a finite positive mass increment at a Cauchy horizon, in the spherically symmetric Einstein–Maxwell–scalar system with positive cosmological constant.

Approach

The proof first constructs a common nonlinear characteristic interior that exists uniformly for a whole sequence of perturbations. It works at a critical surface-gravity relation b=k/a=1-1/p. The radiation is compared with an explicit positive radial mode, and the exact mass flux is integrated to obtain an analytic law for the mass increment. The results and proofs are formalized in Lean 4.

Results

Perturbations with vanishing L^p norm leave a finite positive mass increment that escapes every fixed time window. An explicit law gives the response's delay and duration and determines enhancement or cancellation for overlapping signed packets. Each solution has bounded mass and a local finite-energy weak extension across the horizon.