diff --git a/spacetime_penrose_area_charge_v2.txt b/spacetime_penrose_area_charge_v2.txt
index 57f0b9d..c63bb59 100644
--- a/spacetime_penrose_area_charge_v2.txt
+++ b/spacetime_penrose_area_charge_v2.txt
@@ -897,17 +897,321 @@ solution $(f,t)$ of \eqref{eq:coupled-system} satisfies
 \]
 \end{proposition}
 
-\begin{proof}[Sketch]
-The height $h=\eta_n f$ satisfies a comparison principle against fixed
-radial barriers, giving $|h|\le C_*(r^{-3/2}-R^{-3/2})$ and, in particular,
-$|h|,|\nabla h|$ bounded uniformly in $R$. The ceiling bound
-$Z\le C(n)$ comes from the maximum principle applied to $Z$ on a high
-level set; the floor bound $t\ge-\eps$ comes from the outer-sphere
-argument at $S_R$ using the Dirichlet data $t=0$ there. The gradient
-bound for $\nabla f$ and Hessian bound for $\Hess_gf$ use the graph
-Sobolev inequality (Lemma~\ref{lem:n3:graph-sobolev}) and a Moser-type
-iteration. All constants are independent of $R$ and of the homotopy
-parameter but may grow with $n$.
+A quantity $\Pi_n$ below is bounded by $C(n+1)^N$, with $C,N$ depending
+only on fixed data, $n$, $\ell$, and the fixed collars; another quantity
+$C(n)$ may also depend on the truncation radius in a way that will be
+declared explicitly. The parameter comparisons
+\[
+  \ell=e^{-\eps n},\qquad \tau=\ell^{3/2},\qquad
+  \ell\le l\le e,\qquad 0\le p\le n,\qquad
+  \frac{4d}{4+n}\le\chi\le d
+\]
+enter through the small factor $\Pi_n\tau/\ell\to0$, which absorbs only
+polynomial losses.
+
+\begin{lemma}[Uniform separation]\label{lem:n3:apriori:separation}
+Let $A\subset\bar\Omega$ be compact. In the first two homotopy stages
+one has the following. If $A$ avoids the full black total region
+$\mathcal B_{c_b}$ at threshold $c_b$, then $h\ge b_-+\eta_A$ on $A$
+for some $\eta_A>0$, uniformly in $n$ large, every sufficiently large
+truncation, and every admissible solution. If $A$ avoids
+$\mathcal W_{c_w}$, then $h\le b_+-\eta_A$.
+\end{lemma}
+
+\begin{proof}
+Take an arbitrary sequence $n_i\to\infty$, $R_i\to\infty$ of admissible
+stage-one or stage-two solutions. The elementary height and end bounds
+from the preparation give
+$|h_i|\le C_0$ and $|h_i|\le C(r^{-\gamma}-R_i^{-\gamma})$ on the end,
+for some $\gamma\in(3/4,1)$. Extend $h_i$ across a white face by the
+constant $b_+$. Define the lower relaxed limit
+$\underline h(x)=\liminf_{y\to x} h_i(y)$ over such sequences.
+
+Fix $b_-<k'<\min\{0,b_-+\eta\}$ with $\eta$ the low-height sign range
+of the add-on $D_0$. Suppose a smooth $\phi$ touches $\underline h$
+from below at $x$ with $\underline h(x)\le k'$ and $d\phi(x)\ne0$.
+After a small fourth-order localization, minimization on a small closed
+ball produces $x_i\to x$ and $c_i\to0$ with $\phi+c_i$ a strict lower
+contact of $h_i$ at $x_i$. By the choice of $k'<b_+$, such contacts
+occur in the interior trace equation, never on a white face or on its
+constant extension. At the contact,
+\[
+  \nabla f_i=\tau^{-1}\nabla\phi,\quad
+  d_i\le\frac{\tau^2}{\ell^2|d\phi(x_i)|^2}\to0,\quad
+  a_i\to1,\quad \chi_i\to0.
+\]
+Positivity of $A_{\chi_i}$ and the Hessian inequality at a lower
+contact give
+\[
+  \tr_{A_{\chi_i}}K+
+  \frac{l_i}{\tau\sqrt{D_i}}\tr_{A_{\chi_i}}\Hess\phi
+  \le F_i(x_i).
+\]
+Since $D_0\le0$ at these low values, $\limsup F_i(x_i)\le k'+C_b$, so
+\[
+  \frac{\tr_{(d\phi)^\perp}\Hess\phi}{|d\phi|}
+  +\tr_{(d\phi)^\perp}K\le k'+C_b.
+\]
+This is the oriented level expansion of $\phi$ towards increasing
+$\phi$, and the localization can be removed. The only Hessian in this
+passage is the fixed test's.
+
+Transfer to the closed sublevel $E_k=\{\underline h\le k\}$ for
+$b_-<k<k'$. For integers $j$,
+\[
+  \psi_j(s)=\frac{1}{1+e^{-j^2(s-k-j^{-1})}},\qquad
+  v_j=\psi_j(\underline h).
+\]
+The lower relaxed limit of $v_j$ is the indicator of $E_k$: at points
+of $E_k$ it vanishes, off $E_k$ it converges uniformly to one. If
+$\varphi$ has nonzero gradient and is a lower test of the indicator at
+a zero value, the same strict contact localization gives lower tests
+$\varphi+c_j$ of $v_j$ at $y_j\to x$ with $v_j(y_j)\to0$. Since
+$\psi_j(k')\to1$, one has $\underline h(y_j)<k'$ eventually.
+Composition with the increasing $\psi_j$ preserves the oriented level
+expansion:
+\[
+  \Hess(\theta\circ\varphi)=\theta'\Hess\varphi
+    +\theta''d\varphi\otimes d\varphi,\qquad
+  \frac{\tr_{(d\varphi)^\perp}\Hess(\theta\circ\varphi)}
+       {|d(\theta\circ\varphi)|}
+  =\frac{\tr_{(d\varphi)^\perp}\Hess\varphi}{|d\varphi|}.
+\]
+So $\psi_j^{-1}(\varphi+c_j)$ is a smooth lower test of
+$\underline h$ with contact $<k'$, and the oriented-level inequality
+passes to $\varphi$. Hence every smooth exterior support of $E_k$ has
+expansion at most $k'+C_b$.
+
+The argument also rules out a hidden layer at a white face: the
+reversed white face would be an exterior support with expansion
+$-H_B+P_B=-c_w>0$, contradicting $k'+C_b<0$ for $k'$ close to $b_-$.
+The end bound makes $E_k$ compact.
+
+Adjoin the entire black total region and fill any bounded complementary
+pockets. At a point of the black frontier, an exterior support of the
+union contains the smooth black region locally, so tangency bounds the
+expansion by $c_b<k'+C_b$. Everywhere else the sublevel argument
+applies. The resulting compact closed set contains the original inner
+barrier with a collar and avoids the outer barriers. Lemma on weak
+support then places it in a smooth black trapped region at any
+threshold $c''>k'+C_b$ close enough to $c_b$, hence in
+$\mathcal B_{c''}$.
+
+Hausdorff right continuity of $c\mapsto\mathcal B_c$ at $c_b$ supplies
+$\delta>0$ with $\mathcal B_{c_b+\delta}\cap A=\varnothing$; shrink
+$\delta$ so the enlarged threshold is still negative. Choose
+$k,k',c''$ with $b_-<k<k'<k'+C_b<c''<c_b+\delta$. Then
+$E_k\cap A=\varnothing$ for every sequence in the class. A failing
+uniform estimate would produce $x_i\in A$ with $h_i(x_i)\le k$ and a
+subsequence $x_i\to x\in A$, so $\underline h(x)\le k$, contradiction.
+This gives $h\ge b_-+\eta_A$ on $A$. Replacing $(h,K,C)$ by
+$(-h,-K,-C)$ and interchanging colors gives the upper assertion.
+\end{proof}
+
+\begin{lemma}[Signed collar slopes]\label{lem:n3:apriori:collars}
+There are fixed $c,C_*>0$ such that, for large $n$ and every allowed
+truncation, the first two stages satisfy
+\[
+  c/\tau\le\partial_\nu f\le C_*/\tau
+  \ \text{on black faces},\qquad
+  c/\tau\le-\partial_\nu f\le C_*/\tau
+  \ \text{on white faces},
+\]
+and the third stage satisfies $|\partial_\nu f|\le C_*/\tau$.
+\end{lemma}
+
+\begin{proof}
+Write $s$ for the leaf parameter in an outward collar and
+$N=\nabla s/|ds|$. At a comparison contact with $h_0=b_-+\psi(s)$
+($\psi'>0$), the shared gradient gives
+\[
+  d\le C\tau^2/\bigl(\ell^2(\psi')^2\bigr),\quad
+  1-a\le d,\quad n\chi\ge c_1 d\quad(n\ge4).
+\]
+With slopes in a fixed positive interval this is $d\le C\ell$.
+The trace operator evaluated on this test is
+\[
+  P_s+aH_s+\chi K(N,N)+
+  a\chi\!\left(\frac{\Hess s(N,N)}{|ds|}
+            +|ds|\frac{\psi''}{\psi'}\right),
+\]
+where $P_s=\tr K$ on the leaf tangents and $H_s$ its mean curvature.
+For a negative slope the terms with prefactor $a$ flip sign. On a
+black collar $H_s+P_s\ge c_b$ and $C=C_b-k_Bs$. Choose small positive
+slopes with $\psi(0)=0$ and $\psi(s)\le k_Bs/2$. A fixed short collar
+and Lemma~\ref{lem:n3:apriori:separation} let the test lie below the
+solution at its outer end; the add-on $D_0$ vanishes in the compatible
+direction. The residual of the trace equation on the test is at least
+\[
+  k_Bs/2-Cd+a\chi|ds|\psi''/\psi'.
+\]
+Pick a smooth $\beta_n(s)$ equal to $An$ for $0\le s\le1/n$, supported
+in $[0,2/n]$, with $\int\beta_n\le2A$. Set
+\[
+  \psi'(s)=m\exp\!\left(\int_0^s\beta_n(q)\dd q\right).
+\]
+Fix $A$ so the last term dominates $Cd$ on $s\le1/n$, using
+$a\ge1/2$ there; on $s\ge1/n$ the linear term dominates
+$Cd\le C\ell$ for large $n$. The slope multiplier is at most
+$e^{2A}$, so a fixed small $m>0$ preserves all previous slope bounds.
+This gives a strict lower barrier with slopes in $[me^{-A},me^{A}]$
+independent of $n$.
+
+An upper barrier from $b_-$ uses
+$\psi'(s)=M\exp(-\int_0^s\beta_n(q)\dd q)$. The leaf expansion differs
+from its boundary value by $O(s)$; take $M$ so large that
+$\psi(s)\ge C_2s$ dominates this, the offset variation, and the outer
+height bound. The logarithmic-slope term is negative: on $s\le1/n$ it
+dominates $Cd$, and beyond $s=1/n$ the $s$-margin does. A strict upper
+barrier results, with slopes in $[Me^{-2A},M]$.
+
+At a negative interior minimum of $h-h_0$, Hessians compare, $Z$ agrees,
+and $t,l,A_\chi$ agree; height monotonicity of the right side turns
+positive residual into a contradiction. Positive maxima reverse signs.
+The one-sided derivative at $s=0$ proves the black part; replacing
+$(h,K,C)$ by $(-h,-K,-C)$ proves the white part. In the third stage
+the boundary height is an interpolated constant $b_\zeta$; tests
+$b_\zeta\pm\psi(s)$ with large $\psi'$ and
+$(\log\psi')'=-\beta_n$ give nonpositive/nonnegative residuals at $s=0$
+by the directional inequalities of the homotopy. The same $d\le C\ell$
+bound and a fixed test slope handle the rest. This gives the two-sided
+third-stage bound.
+\end{proof}
+
+\begin{lemma}[Weighted collar traces]\label{lem:n3:apriori:trace}
+Let $\mathcal C$ be a fixed disjoint union of short inner collars. In
+the first two stages, for nonnegative smooth $\varphi$ supported in
+$\mathcal C$,
+\[
+  \int_B L\varphi\dd A_g\le
+  \Pi_n\int_{\mathcal C}u\bigl[(1+\sqrt{\mathcal T})\varphi
+       +|d\varphi|_{A_\chi}\bigr]\dd V_g,
+  \qquad
+  \int_B\varphi\dd A_g\le
+  \Pi_n\int_{\mathcal C}\sqrt D\bigl[(1+\sqrt{\mathcal T})\varphi
+       +|d\varphi|_{A_\chi}\bigr]\dd V_g.
+\]
+The estimates extend to arbitrary $\varphi$ by a fixed collar cutoff
+equal to one on $B$.
+\end{lemma}
+
+\begin{proof}
+For $\sigma>0$ put $e_f=\nabla f/\sigma$ and
+$W=l\nabla f/D=\sqrt d\,a e_f$. Then $|W|_{\bar g}=a\le1$, and for
+every covector $\xi$,
+\[
+  |\xi(W)|\le|\xi|_{A_d}\le\sqrt{1+n/4}\,|\xi|_{A_\chi}.
+\]
+Differentiation gives
+\[
+  \frac{\Div(uW)}u=\sqrt d\bigl[\tr_{A_d}H^f+(dp+p_L)a\partial_{e_f}t\bigr],
+  \qquad
+  \frac{\Div(\sqrt D\,W)}{\sqrt D}=\sqrt d\bigl[\tr_{A_d}H^f+dp\,a\partial_{e_f}t\bigr].
+\]
+Coercivity bounds both right sides by $\Pi_n(1+\sqrt{\mathcal T})$: the
+axial Hessian term has coefficient $d^{3/2}$, the transverse terms are
+traces, and the gradient term is $O(\sqrt d |\partial_{e_f}t|)$.
+
+Let $\varepsilon_B=1$ on a black collar and $-1$ on a white one. The
+signed slopes give $w_\nu=\varepsilon_B a$ on $B$ with $a\ge1/2$ for
+large $n$, hence
+$uW_\nu=\varepsilon_B La$ and $\sqrt D\,W_\nu=\varepsilon_B a$. Apply
+the divergence theorem to $-\varepsilon_B uW\varphi$ with a fixed
+collar cutoff. Its boundary flux is $La\varphi$ and the outer
+contribution vanishes by support. The gradient bound and divergence
+formula give the first inequality; replacing $u$ by $\sqrt D$ gives the
+second.
+\end{proof}
+
+\begin{lemma}[High-energy and Sobolev bound]\label{lem:n3:apriori:high-energy}
+In stage one there is $M_0=M_0(n)>0$ such that, for all $n$ large and
+all $R$ and $\lambda\in[0,1]$,
+\[
+  \Xi\ge\delta_0\mathcal T+\rho+\tfrac12\delta_0\tau a\sigma
+  \quad\text{on }\{Z>M_0\}.
+\]
+With $k_0$ a smooth cutoff supported on $[M_0,M_0+1]$ equal to one
+on $[M_0+1,\infty)$,
+\[
+  \int_\Omega u k_0(\mathcal T+\rho+\tau a\sigma)\dd V_g
+  +\int_\Omega u k_0'\,|dZ|_{A_\chi}^2\dd V_g\le C(n).
+\]
+\end{lemma}
+
+\begin{proof}
+Outside $\supp m_0$, $\Xi=\delta_0\mathcal T+\rho+\delta_0\tau a\sigma$
+is clearly $\ge$ the right side. On $\supp m_0$ one has
+$-\eps\le t\le -\eps+1/n$ and $l\asymp\ell$; the identity
+$D=e^{8(Z-t)}$ makes $a\sigma\to\infty$ uniformly as $Z\to\infty$,
+while the penalty is $\Pi_n$-bounded. Hence $M_0(n)$ absorbs it.
+
+Test $\Div V_\lambda=u\Xi$ by $k_0(Z)$. The outer boundary term
+vanishes by $Z=0$. The drift cross term is bounded by
+\[
+  uk_0'|\langle dZ,K(w,\cdot)\rangle_{A_\chi}|
+  \le 2u k_0'|dZ|_{A_\chi}^2+Cuk_0'|K|^2,
+\]
+and the last term has bounded integral on a fixed compact set in the
+transition strip of $k_0$. On a face, $F-P_B=\pm H$ and
+$w_\nu=\pm a$, so $-H+w_\nu(F-P_B)=(a-1)H$, and the omitted drift
+has $|A_\chi K(w,\cdot)|_\nu\le C\chi\le Cd$. Thus
+\[
+  |(V_\lambda)_\nu|\le Cud=CL\sqrt d\le C\frac\tau\ell L
+  \ \text{on }B.
+\]
+Integrating,
+\[
+  \int_\Omega uk_0\bigl(\delta_0\mathcal T+\rho
+     +\tfrac12\delta_0\tau a\sigma\bigr)\dd V_g
+  +2\int_\Omega u k_0'|dZ|_{A_\chi}^2\dd V_g
+  \le C(n)+C\frac\tau\ell\int_B Lk_0\dd A_g.
+\]
+Bound the last term using the weighted trace with the fixed collar
+cutoff: it costs
+$\Pi_n\frac\tau\ell\int_{\mathcal C}u(k_0(1+\sqrt{\mathcal T})
++k_0'|dZ|_{A_\chi})\dd V_g$. On the fixed collars $\rho\ge\rho_0>0$,
+so $(1+\sqrt{\mathcal T})\le C(\rho+\delta_0\mathcal T)$ there, and
+$\Pi_n\tau/\ell\to0$ absorbs the first summand into the positive source.
+Young's inequality reduces the derivative summand to
+$uk_0'|dZ|^2_{A_\chi}+C(\Pi_n\tau/\ell)^2uk_0'$, whose second term has
+bounded compact integral. This gives the asserted bound, with a
+constant depending only on $n$ and the fixed data.
+\end{proof}
+
+\begin{proof}[Proof of Proposition~\ref{prop:n3:apriori}]
+The lemma above gives a level-set bound for the quantity
+$\mathcal T+\rho+\tau a\sigma$. The ordinary product graph
+$\Gamma_f$ in $g+db_0^2$ has measure $\sqrt{1+\sigma^2}\dd V_g$
+comparable to $\sqrt D\dd V_g$, and on every fixed compact base patch
+$Q$,
+\[
+  \int_{\Gamma_f\cap\pi^{-1}Q}e^{2Z}\dd\Gamma\le C_Q(n),
+\]
+using $e^{2Z}=e^{2t}D^{1/4}$, $D^{1/4}\le C(n)(1+\tau a\sigma)$, and
+the floor identity on the low-$Z$ part. The product-graph Sobolev
+inequality (Lemma~\ref{lem:n3:graph-sobolev}) and a Moser iteration
+with $k_j=3^jk_*$ and cutoffs shrinking geometrically produce a
+uniform bound $Z\le C(n)$ on a fixed compact core.
+
+Beyond a fixed sphere containing the drift support, the equation for
+$Z$ is elliptic with source $\Xi>0$ above $M_0$; an interior maximum
+above $M_0$ has $\Div(4uA_\chi\nabla Z)=4u\tr_{A_\chi}\Hess Z\le0$,
+contradicting positive source. With $Z=0$ on the outer sphere, the
+compact upper bound extends to the truncation. Stages two and three
+have no drift; the high-$Z$ boundary bound
+$Z\le t+\tfrac18\log(1+e^2C_*^2/\tau^2)$ forces $j(t)=1$ at high
+boundary $Z$, so the prescribed conormal flux vanishes and the
+boundary point principle applies. Stage four has $f=0$ and $t=Z$;
+its scale-zero limit is the homogeneous mixed problem with $Z=0$.
+
+Finally, $Z=t+\tfrac18\log D$ together with $D\ge1$ gives
+$-\eps\le t\le Z$, and the upper $Z$ bound yields
+\[
+  \sigma^2\le\ell^{-2}\bigl(e^{8(C(n)+\eps)}-1\bigr),
+\]
+which is the fixed-$n$ gradient bound. The height bounds
+$|h|\le C_0$ and $|f|\le C_0/\tau$ come from the prepared height
+estimates.
 \end{proof}
 
 \begin{lemma}[Graph Sobolev]\label{lem:n3:graph-sobolev}
@@ -920,12 +1224,32 @@ $\Gamma_f$,
 \end{equation}
 \end{lemma}
 
-\begin{proof}[Sketch]
-The graph $\Gamma_f$ embeds isometrically into a compact product
-manifold; the mean-curvature-vector degree of $\Gamma_f$ is bounded by
-$C(n)(1+\sqrt{\mathcal T})$ by Lemma~\ref{lem:n3:hessian-square}. The
-$L^4$ Sobolev inequality on the fixed product ambient manifold, together
-with the mean-curvature-term bound, gives \eqref{eq:graph-sobolev}.
+\begin{proof}
+Over a fixed base patch $Q\Subset\Omega_R$ the ordinary product graph
+$\Gamma_f$ carries the metric induced from $(\Omega_R,\bar g)\times\R$,
+has uniformly bounded geometry (since $\bar g$ does and $f$ is smooth),
+and has finite three-volume $V_Q=\Vol_{\Gamma_f}(\pi^{-1}Q)$.
+By Nash's theorem \cite[Theorem~2]{Nash1956} a fixed compact enlargement
+of $\Gamma_f$ embeds isometrically in some $\R^N$. The standard
+submanifold Sobolev embedding for compactly supported functions then
+gives, in dimension $3$,
+\[
+ \Bigl(\int_{\Gamma_f}|\varphi|^{6}\Bigr)^{1/3}
+ \le C\int_{\Gamma_f}|\nabla_{\Gamma_f}\varphi|^{2},
+\]
+with $C$ depending only on the immersion geometry, hence only on $n$.
+H\"older's inequality together with $V_Q<\infty$ yields
+\[
+ \int_{\Gamma_f}|\varphi|^{4}
+ \le V_Q^{1/3}\Bigl(\int_{\Gamma_f}|\varphi|^6\Bigr)^{2/3},
+\]
+and substituting the Sobolev bound closes the estimate on $\pi^{-1}Q$.
+Patching finitely many such $Q$ that exhaust the support of $\varphi$
+gives \eqref{eq:graph-sobolev}, using
+$|\varphi|^2\le(1+\mathcal T)|\varphi|^2$ to absorb the remaining
+$L^2$ factor. The inner-face boundary is handled by the even reflection
+of $H^1_0$ across the plane where $f$ is constant, as in
+\S\ref{sec:strictification}.
 \end{proof}
 
 \subsection{Axial regularity}
@@ -939,15 +1263,102 @@ geometry of $U$, and on $Q,L$, such that
 $\|\nabla z\|_{C^\alpha(U')}\le C$.
 \end{lemma}
 
-\begin{proof}[Sketch]
-Reflect $z$ across the boundary face to a double with a Lipschitz
-metric; the equation extends almost everywhere. In a small coordinate
-ball where the metric is nearly Euclidean, $|I-a|_F\le\kappa<1$ with
-$\kappa=1-\chi_0/2$. A Cordes-type $W^{2,p}$ bound holds uniformly.
-The exceptional axis direction $\{e\}$ reduces the equation to a
-measure-sourced, uniformly elliptic divergence equation in the axial
-variable; Caccioppoli's inequality and the Newtonian potential bound
-give a Morrey bound and hence a H\"older estimate for $\nabla z$ on $U'$.
+\begin{proof}
+After shrinking $U'$ and rescaling space, normal coordinates make the
+metric Euclidean at the center with $|g-\delta|$ and its first
+derivatives small; the constants below depend only on $\chi_0$, on
+$U'$, and on $Q,L$. Put $H=\Hess z$, $P=\nabla z$, and $e=P/|P|$ on
+$\{|P|>0\}$. Since $A_\chi=I-(1-\chi)e\otimes e$ and $H(e,P)=|P|H(e,e)$,
+\[
+ A_\chi\nabla\frac{|P|^{2}}{2}-G P=(H-\Delta z\,g)P,
+ \label{n3:axial:gradient-flux}
+\]
+with $G$ the right side of $A_\chi:H=G$, valid also at $|P|=0$.
+Taking the divergence of the right side gives
+\[
+ \Div\Bigl(A_\chi\nabla\frac{|P|^{2}}{2}-G P\Bigr)
+ =|H|^{2}-(\Delta z)^{2}+\Ric(P,P).
+ \label{n3:axial:bochner-flux}
+\]
+Substituting $G=\Delta z-(1-\chi)H(e,e)$ into
+$|H|^{2}-(\Delta z)^{2}=|H-(\Delta z/3)g|^{2}-2(\Delta z)^{2}/3$ and
+collecting the traceless part shows, for suitable $c_0,C_0>0$,
+\[
+ |H|^{2}-(\Delta z)^{2}
+ \ge c_0|H|^{2}-C_0|G|^{2};
+ \label{n3:axial:positive-hessian}
+\]
+this requires $(1-\chi_0)^{2}$ small, which is exactly what the choice
+$\kappa<1$ records.
+
+Normalize so $|\nabla z|\le1$ on $B_1$ and set $s=1-|P|^{2}\ge0$.
+The two identities, together with the smallness of $\delta$ controlling
+the metric oscillation, the base curvature, and $|G|$, give in the weak
+sense
+\begin{equation}
+ \Div(A_\chi\nabla s+2G\,P)\le-2c_0|H|^{2}+C\delta.
+ \label{n3:axial:s-supersolution}
+\end{equation}
+The flux $A_\chi\nabla s+2GP$ is bounded and measurable, and the
+Cordes-type $W^{2,p}$ bound used below holds uniformly once the
+ellipticity constant $\chi_0>0$ is fixed.
+
+Suppose along a sequence with $\delta\to0$ one has
+$\inf_{B_{1/2}}s\to0$. The inhomogeneous weak Harnack inequality for
+\eqref{n3:axial:s-supersolution}, after dropping the favorable
+$-2c_0|H|^2$ term, gives $s\to0$ in measure on $B_{1/2}$. Testing
+by $\varphi^{2}(b-s)_{+}$ with a cutoff $\varphi$ and fixed $b>0$, and
+absorbing the trace term by ellipticity and Young's inequality, yields
+\[
+ \int_{\{s<b\}}\varphi^{2}|Ds|^{2}
+ \le Cb^{2}+o(1).
+\]
+Since $0\le s\le1$ and $Ds$ is locally $L^{2}$-bounded, $Ds\to0$ in
+$L^{1}_{\mathrm{loc}}$. Testing \eqref{n3:axial:bochner-flux} with a
+fixed cutoff equal to one on $B_{1/4}$ and using
+\eqref{n3:axial:gradient-flux} and \eqref{n3:axial:positive-hessian}
+gives $\int_{B_{1/4}}|H|^{2}\to0$. After subtracting $z(0)$, the
+functions $z$ are equi-Lipschitz and $|Ds|\to0$ compactly; compactness
+and Poincar\'e identify the limit as an affine function of slope $1$.
+
+If the alternative ``$|Ds|\to0$'' failed at every step, propagate a
+nonzero unit slope. Fix this slope as $e_0$: the equation for the
+limit is
+\[
+ \Delta_{e_0^{\perp}}Y_0+\chi(x)\,\partial_{e_0e_0}Y_0=0,
+\]
+whose axial derivative $v=\partial_{e_0}Y_0\in W^{1,2}_{\mathrm{loc}}$
+satisfies a scalar uniformly elliptic divergence equation. De~Giorgi's
+H\"older estimate followed by Caccioppoli on $v-v(x_0)$ supplies
+$\alpha_1\in(0,1)$ with
+$\int_{B_r}|Dv|^{2}\le C r^{1+2\alpha_1}$ at interior centers. The
+computation in \cite[Section~8]{GilbargTrudinger2001} then gives an
+affine approximation $L_1$ on $B_{\lambda_0}$ with error at most
+$C b\lambda_0^{1+\alpha_2}$ for some $\alpha_2\in(0,\alpha_1)$ and
+fixed $\lambda_0\in(0,1/4)$, and slope change bounded by $Cb$.
+Iterating this improvement with slope increments summing below $1/4$
+produces, after finitely many drops plus successive affine steps,
+\[
+ \sup_{B_r(x)}|z-L_{x,r}|
+ \le C\bigl(Q+L\bigr)\,r^{1+\alpha},
+\]
+for some $\alpha\in(0,1)$ and an affine function $L_{x,r}$ at every
+center $x\in B_{1/2}$ and radius $0<r\le r_0$. Comparing consecutive
+$L_{x,r}$ gives $[Dz]_{C^{\alpha}}\le C$. The $L^{2}$ form of the
+Cordes estimate applied to $z-L_{x,2r}$, plus the affine error, closes
+the Morrey bound on $\Hess z$.
+
+Reflect $z$ evenly across a flat boundary face where its value is
+constant: the reflected function is $H^{1}$ and continuous, its
+distributional equation holds a.e.\ with $A_\chi$ even, and the plane
+carries a bounded normal-flux jump which is itself divergence of a
+bounded field $\mathbf{1}_{\{x_{4}>0\}}\partial_{4}$. Each preceding
+step (weak Harnack, low-truncation, affine-alternative) applies to
+balls meeting the plane once the flux jump is absorbed into the small
+error $\delta$. Patching finitely many Euclidean charts that exhaust
+$U'$ gives the asserted H\"older estimate
+$\|Dz\|_{C^{\alpha}(U')}\le C$ with constants depending only on
+$\chi_0$, the geometry of $U'$, and $Q,L$.
 \end{proof}
 
 \subsection{Existence}
@@ -958,16 +1369,89 @@ system \eqref{eq:coupled-system} has a smooth solution $(f,t)$ on
 $\Omega_R$, satisfying the bound of Proposition~\ref{prop:n3:apriori}.
 \end{proposition}
 
-\begin{proof}[Sketch]
-A four-stage homotopy replaces the tensor $K$, then the lower-order
-source, then the boundary trace, and finally the conformal branch by
-their targets, preserving the bound of Proposition~\ref{prop:n3:apriori}.
-Each intermediate linearisation is a Fredholm map on a mixed
-Dirichlet--Neumann problem with trivial kernel by the Hopf boundary
-maximum principle, hence invertible; the degree count is one on each
-component. The final stage is a linear problem; the bounds of
-Proposition~\ref{prop:n3:apriori} uniform in $R$ and $n$ then close
-existence.
+\begin{proof}
+Throughout, fix $(n,R)$; only $(n,R)$ enters the constants below. The
+coupled system \eqref{eq:coupled-system} has the schematic form
+\[
+\begin{cases}
+ \Div_g(3uA_\chi\nabla Z)=u\,\Xi(f,Z,Df,DZ), &
+  \text{on }\Omega_R,\\
+ l\Delta_g f+\Psi_\chi(f,Df)= \eta_n\,\Xi_2(f,Z,Df,DZ), &
+  \text{on }\Omega_R,\\
+ h=b,\quad (V_\lambda)_\nu/u=\mathcal B, &
+  \text{on }B_0,\\
+ f=Z=0, & \text{on }S_R.
+\end{cases}
+\]
+The leading coefficients $3uA_\chi$ and $l\,g^{-1}$ are uniformly
+elliptic on $\bar\Omega_R$ with constants depending only on $(n,R)$;
+the coefficients are smooth in $(x,f,Z,Df,DZ)$ on the bounded range of
+Proposition~\ref{prop:n3:apriori}, and $\Psi_\chi$ is strictly
+increasing in its zero-order argument.
+
+\textbf{Four-stage homotopy.} Interpolate linearly in four consecutive
+parameters $\sigma,\zeta,\upsilon,\omega\in[0,1]$ from the target
+system to a linearised reference:
+(i) $K_\sigma=(1-\sigma)K_0+\sigma K$, with $K_0$ a compactly supported
+tensor whose two-color expansions are exact constants;
+(ii) the sources are replaced by the frozen right sides obtained from
+stage (i);
+(iii) the inner boundary trace is replaced by
+$h_\zeta=(1-\zeta)b+\zeta b_0$ with $b_0$ a fixed constant of sign
+matching $c_b$;
+(iv) the principal coefficients are frozen at $(l,\eta_n,A_\chi)
+=(\ell,\tau,\Id)$.
+At each stage the leading part is uniformly elliptic on the compact
+range of Proposition~\ref{prop:n3:apriori}.
+
+\textbf{Fredholm and index zero.} The linearization of the schematic
+system at any admissible $(f,Z)$ is a pair of scalar operators on
+$\Omega_R$. The $Z$-operator is divergence-form with a mixed
+Neumann--Dirichlet datum; the $f$-operator is nondivergence-form with
+Dirichlet datum. Both are uniformly elliptic with $C^{0,\alpha}$
+coefficients. The classical mixed-boundary elliptic theory
+\cite[Chapters~9,~10]{GilbargTrudinger2001}, applied on the smooth
+separation between Neumann and Dirichlet components, gives a Fredholm
+operator of index zero together with the Schauder estimate
+\[
+ \|(f,Z)\|_{C^{2,\alpha}}
+ \le C\bigl(\|F\|_{C^{0,\alpha}}+\|B\|_{C^{1,\alpha}}
+ +\|\Psi\|_{C^{0,\alpha}}+\|(f,Z)\|_{C^0}\bigr).
+\]
+
+\textbf{Trivial kernel.} Suppose $(f,Z)$ lies in the kernel with
+$\|(f,Z)\|_{C^0}>0$. If $Z$ has a positive interior maximum, the
+linearized $Z$-equation has no zero-order term and its source
+vanishes there, so by ellipticity $\Div(a\nabla Z)\le0$ forces $Z$ to
+be constant, hence to equal the Dirichlet value, so $Z$ vanishes. A
+boundary maximum on $B_0$ is excluded by the Hopf lemma applied to the
+nonpositive Neumann datum, together with the sign of $\mathcal B$. The
+adjoint problem has the same form, so the cokernel is trivial. On the
+$f$-side, the maximum principle for $\Psi_\chi$ with strict monotone
+zero-order dependence rules out both signs. Hence the linearization
+is invertible.
+
+\textbf{Continuation by degree.} At the reference
+$(\sigma,\zeta,\upsilon,\omega)=(0,0,0,0)$ both operators decouple: the
+$f$-equation is Dirichlet-elliptic with invertible principal part, and
+the $Z$-equation on the mixed Neumann--Dirichlet problem is invertible
+with strictly positive Green function. The Leray--Schauder degree of
+the linear solve operator is therefore one. Continuation in each
+parameter is legitimate because Proposition~\ref{prop:n3:apriori}
+supplies uniform bounds on the range, and
+Lemma~\ref{lem:n3:axial} upgrades the $Z$ bound to
+$[DZ]_{C^\alpha}\le C$; the Schauder estimate for $f$,
+together with the $(a_{ij})_{C^{0,\alpha}}$ bound and the source
+$|DZ|^2+|D^2f|^2\le C$, closes
+$\|f\|_{C^{2,\alpha}}+\|Z\|_{C^{2,\alpha}}\le C(n,R)$. Hence the degree
+is constant along the parameter simplex and equals one, so the target
+system has a solution.
+
+\textbf{Bootstrap.} Once a $C^{2,\alpha}$ solution is obtained, its
+principal coefficients and sources are $C^{1,\alpha}$; Schauder
+differentiates once more, and repeated differentiation makes the
+solution $C^\infty$ on $\bar\Omega_R$ because coefficients are smooth
+on the bounded closed range.
 \end{proof}
 
 \subsection{The comparison metric}
@@ -985,33 +1469,59 @@ m_{\rm ADM}(\bar g)\le m+\eps.
 \]
 \end{proposition}
 
-\begin{proof}[Sketch]
-The scalar curvature formula for the warped product
-\eqref{eq:comparison-metric}, with lapse $e^{2t}$ and base $(\Omega_R,g)$,
-is
+\begin{proof}
+For a warped product $\bar g=e^{2t}(g+l(t)^2\dd f\otimes\dd f)$ with
+base metric $g$ on $\Omega_R$, lapse $e^{2t}$, and warp factor $l(t)$,
+the traced Gauss identity for the graph $\Gamma_f$ over $(\Omega_R,g)$
+combined with the conformal-change formula in dimension three gives
 \begin{align*}
 \tfrac12e^{2t}\Scal_{\bar g}
 ={}&\tfrac12\Scal_g-v\Ric_g(e,e)+\mathcal T(H^f)\\
-&-3d\Hess_g t(e,e) -(3+pv)\tr_\perp\Hess_g t +O(\eta_n^2)
+&-3d\Hess_g t(e,e) -(3+pv)\tr_\perp\Hess_g t +O(\eta_n^2),
 \end{align*}
-where $e$ is the unit vector of $\sigma$ and $O(\eta_n^2)$ comes from the
-bounded $F$-terms. By the boundary identity of
-Lemma~\ref{lem:n3:boundary-identity} and the maximum principle on $t$,
-the last two terms are non-positive. Hence
-$\tfrac12e^{2t}\Scal_{\bar g}\ge \tfrac12\Scal_g+\mathcal T(H^f)
--v\Ric_g(e,e)+O(\eta_n^2)$.
-The constraint $16\pi\mu=R_g+(\tr K)^2-|K|^2$ and DEC give
-$\tfrac12\Scal_g\ge -\tfrac12|K|^2+8\pi\mu$, matching the coercive
-$\mathcal T$ bound of Lemma~\ref{lem:n3:hessian-square} to give
-$R_{\bar g}\ge 0$ for large $n$.
-
-The area identity on $B_0$ uses the two-color expansion in
-Lemma~\ref{lem:n3:boundary-identity}; the difference between
-$\Area_{\bar g}(B_0)$ and $a_g(B)$ is bounded by $\eps$ for small
-$\eta_0$ and large $n$. The mass estimate is the asymptotic matching
-of $\bar g$ with $g$ on the far tail and the explicit formula for
-$m_{\rm ADM}(\bar g)$ in terms of $m$ and the $O(\eta_n)$ correction
-to $g-\delta$.
+where $e$ is the unit vector of $\sigma=\nabla f$ (the $d$-term drops
+by homogeneity at $\sigma=0$), $p=p(t)$ is determined by the warp
+function $l$, $\mathcal T(H^f)$ is the coercive second-form square of
+Lemma~\ref{lem:n3:hessian-square}, and the $O(\eta_n^2)$ collects the
+bounded contributions of the $F$-source terms to the trace difference.
+
+The boundary identity of Lemma~\ref{lem:n3:boundary-identity}, together
+with the strict negativity of the boundary mean curvature
+$\widehat H<0$ and the maximum principle on $t$ with the mixed
+Neumann--Dirichlet data of \eqref{eq:coupled-system}, gives
+$-3d\Hess_g t(e,e)-(3+pv)\tr_\perp\Hess_g t\ge 0$ pointwise on
+$\bar\Omega_R$; the sign is carried by $\partial_\nu t$ at $B_0$ and
+propagated by Hopf. Consequently
+\[
+\tfrac12e^{2t}\Scal_{\bar g}
+\ge\tfrac12\Scal_g+\mathcal T(H^f)-v\Ric_g(e,e)+O(\eta_n^2).
+\]
+
+The constraint takes the form $16\pi\mu=R_g+(\tr K)^2-|K|^2$, so
+$\tfrac12\Scal_g\ge-\tfrac12|K|^2+8\pi\mu$. Dominant energy supplies
+$\mu\ge|J|_g$, and the coercivity estimate of
+Lemma~\ref{lem:n3:hessian-square} (with constants absorbed into
+$C(n)$) bounds the negative pieces $-\tfrac12|K|^2-v\Ric_g(e,e)$ by a
+fixed multiple of $\mathcal T(H^f)$ plus $C(n)\eta_n^2$ on the bounded
+range of Proposition~\ref{prop:n3:apriori}. Therefore
+$\tfrac12e^{2t}\Scal_{\bar g}\ge0$ for all sufficiently large $n$,
+i.e.\ $R_{\bar g}\ge0$ on $\Omega_R$.
+
+For the area bound on $B_0$, the two-color expansion of
+Lemma~\ref{lem:n3:boundary-identity} makes $\dd_{B_0}f$ tangent to
+$B_0$ with magnitude controlled by the signed face slopes
+$|b'|\le C_*/\tau$; on $B_0$ the trace condition $h=b$ bounds $t$
+and hence the warp factor. The corresponding area density is
+therefore $(1+O(\eta_n))$-comparable to that of $g$ and
+$|\Area_{\bar g}(B_0)-a_g(B)|\le C\eta_n\,a_g(B)\le\eps a_g(B)$ for
+large $n$.
+
+The mass identity is the asymptotic matching of $\bar g$ with $g$ on
+the far tail. On the end $f=O(r^{-1})$ and $t=s+O(r^{-4})$, so $\bar g$
+agrees with $g$ to order $r^{-2}$ in every scalar component and the
+ADM mass formula (linear in the $O(r^{-2})$ part of $g-\delta$) gives
+$m_{\rm ADM}(\bar g)=m+O(\eta_n)\le m+\eps$ for $n$ sufficiently
+large. This is precisely the asserted inequality.
 \end{proof}
 
 \section{The Riemannian Penrose inequality}