Theorem 4.2: charged horizon area lower bound

The model, regularity, original maximal section and mass-one normalization are those in the Statement. A spacelike section has positive-definite induced metric; maximal means that its second fundamental form has zero trace. Stationary vacuum model and asymptotic normalization Regular non-degenerate stationary vacuum spacetime Spacelike sections, maximality and lapse–shift data Mass-one convention and Harrison denominator

Work in ZFC, including the axiom of choice. The Axiom of Choice

The global one-form construction supplies the single smooth stationary primitive used in the Harrison family under these hypotheses. Closedness, periods and smooth global choice of W0

For each $q\in (0,1]$, the bifurcation-stability result supplies an individually admissible smooth spacelike maximal section with boundary $S$. Its Statement also supplies a smooth spacelike extension agreeing with the section on its original side near $S$, an outward normal-graph tube of radius allowed to depend on $q$, and nonnegative principal eigenvalue in the future/outward gauge. Nonnegative principal eigenvalue of the horizon stability operator

For such a section and its extension and graph tube, the stable-horizon inequality gives $\mathrm{\mid }S{\mathrm{\mid }}_{g_q}\ge (4\pi {)}^{-1}({\int }_S{e}_{q}d{\mu }_q{)}^2$. The horizon notation fixes the induced area form and the two flux-density identities in the Statement. Stable-horizon flux-energy and area-charge inequalities Horizon null frame, flux densities and stability operator notation

With the mass-one stationary end expansion $g_{00}=-1+2\mathrm{/}r+O_6(r^{-2})$ established in [F8], the supplied primitive and the inherited orientation, the Harrison flux result gives $(4\pi {)}^{-1}{\int }_S{\star }_{g_q}{F}_q=\sqrt{1-q^2}$ and $(4\pi {)}^{-1}{\int }_S{F}_q=0$ for $0\le q\le 1$. Proposition 2.1: electric and magnetic fluxes

The single-primitive family is $W_q=(1-q{)}^2{W}_0-4q(1-q)T^{\mathrm{♭}}$. For the normalized Ernst potential $\sigma =f+i\psi$, the Harrison definitions specify $B_q=q(1+\sigma )+(1-\sigma )$, $D_q=\mathrm{\mid }{B}_q{\mathrm{\mid }}^2$, the metric $g_q$ and the electromagnetic form $F_q$ on their positive-denominator domain, using the same $W_q$, spacetime orientation and Hodge convention. The definitions require a supplied zero $p$ of $T$ and $d_q=D_q(p)>0$; they do not themselves supply the primitive. Single-potential construction of the Harrison one-form family Stationary Harrison one-form and metric Harrison electromagnetic form Mass-one convention and Harrison denominator

Under [A1], the denominator-positivity result applies to the smooth normalized Ernst data supplied by the global construction. It gives $D_q>0$ on the exterior and on one open neighborhood of $S$ for $q\in [0,1]$, with $D_q\ge (1+q{)}^2$ on $S$. Positivity of the Harrison denominator and horizon bound Closedness, periods and smooth global choice of W0

For this same $W_0$ and polynomial family, the regular electrovacuum result supplies the Harrison metric and real electromagnetic form on the exterior and an open neighborhood of $S$, where they are smooth in spacetime and satisfy the source-free Einstein–Maxwell equations. The orientations and fields are the same ones used by the flux and stability results. Proposition 2.1: Einstein–Maxwell equations and regularity

Under the regular stationary-vacuum hypotheses, the stationary-mass lemma gives $M_0=m_K=E$, where $E$ is the ADM energy of the original exterior section. Thus [A1]'s ADM mass-one convention gives $M_0=E=1$, and the regular end expansion becomes $g_{00}=-1+2\mathrm{/}r+O_6(r^{-2})$; the bounds $g_{0i}=O_6(r^{-2})$ and $g_{ij}={\delta }_{ij}+O_6(r^{-1})$ are unchanged. Positive stationary mass from the bifurcate vacuum boundary Regular non-degenerate stationary vacuum spacetime Mass-one convention and Harrison denominator