Theorem 4.1: limiting horizon area upper bound

The primitive in [F7] is chosen with the potential and pole of its construction, not independently for different suppliers. The actual original exterior section in [A1] is the section on which its maximality and ADM normalization are imposed; [F8] gives the required coefficient $M_0=1$ in that section's physical stationary end chart. First verify the one-form conditions locally. By [F13], torsion freeness and the Killing equation give $(d{T}^{\mathrm{♭}}{)}_{ab}={\mathrm{\nabla }}_a{T}_b-{\mathrm{\nabla }}_b{T}_a=2F_{ab}$. Stationarity of $g$ and $T$ gives ${\mathcal{L}}_T{T}^{\mathrm{♭}}=0$, so the stationarity of $W_0$ in [F7] implies ${\mathcal{L}}_T{W}_q=0$. Differentiating its polynomial definition and using the primitive equation in [F7] yields $d{W}_q=4(1-q)(((1-q)f-(1+q))F+(1-q)\psi {\star }_{g}F)$. The denominator in the one-form definition expands as $D_q=(1-q{)}^2{D}_0+4q(1-(1-q)f)$. Since $f(p)=0$, $d_q=D_q(p)=(1-q{)}^2{D}_0(p)+4q$. Consequently $W_q(T)=(1-q{)}^2(D_0(p)-D_0)+4q(1-q)f=d_q-D_q$. These are precisely the Harrison one-form conditions of [A1]. The electrovacuum supplier in [F3] applies to this smooth stationary normalized primitive and its polynomial family and gives joint smoothness. The local $K$ invariance of both the primitive and the normalized potential in [F7] matches the horizon-preservation input in [F3], so the fixed compact sphere is spacelike for these same metrics, including $q=0$. For the end estimates in [F9], the original section and ADM limit are [A1], the original mass coefficient is [F8], and the potential, pole and five differentiated spatial decay bounds are [F7]; the one-form conditions were verified above. Thus [F9] applies to this very family. These are the end estimates inherited by the comparison-sphere result in [F2]. No equality of independent gauges or of the physical end chart with an adapted spherical chart is assumed.

Fix any sufficiently small $q>0$. The regular vacuum, actual original-section maximality, mass-one normalization and $T{\mathrm{\mid }}_S\equiv ̸0$ hypotheses of [F10] are exactly [A1] and [F8]. Use the single smooth Harrison family matched in step 1.1, and take the lower parameter bound $\delta =q\mathrm{/}2$. The maximal-slice result supplies a complete smooth spacelike $g_q$-maximal stationary graph section ${\mathrm{\Sigma }}_q$ with included boundary $S$. Its induced metric $h=g_q{\mathrm{\mid }}_{T{\mathrm{\Sigma }}_q}$ is smooth and positive definite up to that compact boundary. This is the section denoted ${\mathrm{\Sigma }}_{q,0}$ in the comparison and cut suppliers; use this same selected section in each application.

Let $h_q=g_q{\mathrm{\mid }}_{TS}$. By [F3], $h_q$ is a jointly smooth family of positive-definite metrics on the compact sphere, including at $q=0$. Orient $S$ and write ${\omega }_q$ for the positive area density of $h_q$. The adopted model in [A1] works in ZFC, so countable choice is available. By [F6], ${\omega }_0$ defines a Radon Borel measure ${\mu }_0$ on $S$, and ${\mu }_0(S)<\mathrm{\infty }$ because $S$ is compact. In a positive chart, [F4] gives ${\omega }_q=a_q{\omega }_0$, where $a_q=\sqrt{\det (h_q)\mathrm{/}\det (h_0)}$. The coordinate-independent densities make this ratio globally defined; it is smooth on $S$ for each $q$, jointly continuous in $(x,q)$, and tends pointwise to $1$ as $q\downarrow 0$. Each $a_q$ has compact support on the compact sphere, so the integration agreement in [F6] identifies $\mathrm{\mid }S{\mathrm{\mid }}_{g_q}={\int }_S{\omega }_q={\int }_S{a}_{q}d{\mu }_0$. The functions $a_q$ are Borel measurable, and compactness of $S\times [0,1]$ bounds them by one finite constant, integrable against ${\mu }_0$. Thus [F5], applied to any sequence $q_n\in (0,1]$ tending to zero, gives $\mathrm{\mid }S{\mathrm{\mid }}_{g_{q_n}}={\int }_S{a}_{q_n}d{\mu }_0\to {\int }_{S}1d{\mu }_0=\mathrm{\mid }S{\mathrm{\mid }}_{g_0}$. The sequential criterion yields the same one-sided limit as $q\downarrow 0$.

Apply the two collar results in [F11] to $({\mathrm{\Sigma }}_q,h)$ from step 2.1. Their smoothness, positivity and compact-boundary hypotheses hold by that step, and their ZFC convention is inherited from [A1]. They supply a smooth intrinsic boundary-distance collar, with $\rho$ equal to its inward normal coordinate even when the distance infimum allows paths outside the collar. Choose a closed smaller collar $\{0\le \rho \le \eta \}$, with a larger smooth collar still available. Thus the intrinsic distance, smooth collar and boundary conventions required by [F1] and [F12] refer to this same section and induced metric.

The standing regular-vacuum, mass-one, actual original maximal-section and nontrivial-$T$ hypotheses for [F12] are [A1] and [F8]; its supplied transformed maximal section and intrinsic collar are steps 2.1 and 3.1. Use the comparison cylinder of the same spheres as [F2], with their fixed radius constant chosen sufficiently large for these suppliers. For every sufficiently small $\eta$, localization in [F12] supplies a sufficiently late stationary target $C_t$ and the localized causal cut. Fix that target before choosing $ϵ$. The smooth-cut result in [F12] then supplies, for every $ϵ>0$, smooth compact regions in the section, with boundary $S\bigsqcup D_{ϵ}$, $D_{ϵ}$ between $S$ and $S_{\eta }$, and $\mathrm{\mid }{D}_{ϵ}\mathrm{\mid }\le \mathrm{\mid }{C}_t{\mathrm{\mid }}_{g_q}+ϵ$. For the divergence argument, use the collar-contained smooth comparison regions supplied by [F1] for this same localized construction; its interface gives their boundary and area bound as well as its uniform fixed-collar estimate. All these objects use the same $g_q$, section, collar and target as the comparison supplier; the lateness threshold may depend on $q$ and $\eta$.

The fixed-$q$ comparison in [F1] now has its complete maximal section, smooth intrinsic distance collar and localized smooth comparison regions from steps 2.1, 3.1 and 4.1. Its uniform fixed-collar estimate sends $ϵ\downarrow 0$ and then $\eta \downarrow 0$ with $q$ fixed, giving $\mathrm{\mid }S{\mathrm{\mid }}_{g_q}\le \mathrm{\mid }{C}_q{\mathrm{\mid }}_{g_q}$ for every sufficiently small positive $q$. The comparison-sphere result applies to the same family and gives $\mathrm{\mid }{C}_q{\mathrm{\mid }}_{g_q}\to 4\pi$. No collar width, late-target threshold or section estimate uniform as $q\downarrow 0$ is used.

Pass to the limit in the inequality of step 5.1 using step 2.2 and the comparison-sphere limit in [F2]. This gives $\mathrm{\mid }S{\mathrm{\mid }}_{g_0}\le 4\pi$.