Physics theoremStatement: AI-adaptedProof: AI-adapted

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Cutoff maximum principle and uniform collar regularity

PDF p. 19: Proof of Lemma 3.4, cutoff calculation

Statement

Fix $δ > 0$ in the supplied regular mass-one stationary vacuum/Harrison construction, with $T ∣_{S} \equiv̸ 0$ , and its existing smooth spacelike maximal sections $Σ_{q}$ , $q \in [δ, 1]$ , with the complete preceding boundary height and barrier hypotheses. On the common Gaussian graph collar let $R_{q} = ρ_{q} \circ π_{q}^{⊥}$ and $∣ τ_{q} ∣ \leq θ_{δ} R_{q}$ , where $θ_{δ} < 1$ . Choose $θ_{δ} < c < 1$ . Let $r_{δ} > 0$ be the common normal-graph radius supplied by the boundary-angle result. Fix $0 < ρ_{δ} < r_{δ}$ small enough that the closed cone region $0 \leq R_{q} \leq ρ_{δ}$ , $∣ τ_{q} ∣ \leq θ_{δ} R_{q}$ lies in a fixed compact common Gaussian tube, after the uniform shrinking in Proof 1.1, and in the collar of the full-range angle inequality. Choose $0 < d < \frac{1}{2} (c - θ_{δ}) ρ_{δ}$ and set $χ = (1 + (τ_{q} - c R_{q}) / d)_{+}$ . Then $χ = 1$ on $S$ , $χ = 0$ on $R_{q} = ρ_{δ} / 2$ , and $0 \leq χ \leq 1$ on the candidate collar. On $χ > 0$ , $∣ \nabla χ ∣_{h_{q}}^{2} \geq c_{δ} v_{q}^{2} - C_{δ}$ and $∣ Δ_{h_{q}} χ ∣ \leq C_{δ} v_{q}^{2}$ , where $v_{q} = - g_{q} (n_{q}, - {grad}_{g_{q}} τ_{q}) \geq 1$ . At an interior positive maximum of $χ^{m} v_{q}$ , $\nabla \log v_{q} = - m \nabla χ / χ$ and $0 \geq Δ \log (χ^{m} v_{q}) \geq (m^{2} / 4 - m) ∣ \nabla χ ∣^{2} / χ^{2} - C_{δ} v_{q}^{2} (1 + m / χ)$ . A common sufficiently large integer $m$ gives $\sup_{χ \geq 1 / 2} v_{q} \leq C_{δ}$ . This region contains a fixed positive-width reference collar of $S$ . On a smaller common collar the normal graph heights have uniform $C^{k, α}$ bounds for every finite $k$ and $0 < α < 1$ , including up to $S$ , and the graphs are uniformly spacelike. Constants may depend on $δ, k, α$ and the fixed background but not on the candidate or on $q \in [δ, 1]$ .

Facts & Assumptions

[A1]

Adopt the stationary vacuum model, regular data, mass-one normalization, with $T ∣_{S} \equiv̸ 0$ , and the existing maximal sections with their preceding height/barrier premises. Stationary vacuum model and asymptotic normalization Regular non-degenerate stationary vacuum spacetime Mass-one convention and Harrison denominator Stationary maximal graphs and normalized graph heights Work in ZFC, including The Axiom of Choice.

[F1]

Under the nonzero stationary-field hypothesis in [A1], the authored reference collar is a smooth compact background family; the completed boundary theorem supplies the common one-to-one Gaussian graph domain of radius $r_{δ} > 0$ , the strict cone, zero height on $S$ and the boundary angle bound. Lemma 3.3: common spacelike reference collar Boundary angle bound and normal-graph cone The full logarithmic angle inequality holds through all $v_{q} \geq 1$ . Angle differential inequality near S

[F2]

The induced metric, maximality and scalar-operator conventions are Spacelike sections, maximality and lapse–shift data, and Holder norms are Hölder spaces C^k,α, closure and interior scaled norms, and C^k,α domains.

[F3]

The five helpers give the ambient cutoff estimates, weighted maximum argument, Gaussian graph equation, uniform extension/flattening and bootstrap from a boundary C1-Holder seed. Projection estimates for a Gaussian collar cutoff Weighted cutoff maximum gives a uniform normal angle Gaussian maximal graph equation on a compact spacelike slope cone Uniform elliptic extension and flattening before the boundary gradient estimate Uniform boundary Schauder bootstrap after a C1-Holder seed.

[F4]

Import Simon Lecture18 Theorems1–2, pp.216–217, for the local interior and homogeneous-Dirichlet boundary $C^{1, β}$ seed, with exact coefficient-box, forcing, gradient and flattening hypotheses recorded in the source entry. No interior-only estimate is used as a boundary estimate.

[F5]

The complete preceding height/barrier premises in the Statement retain maximality on the actual original $C = Σ_{0} \cap E$ and the selected-end access required for those height estimates. Use $Σ_{1} = C \cup S$ as the reference section of the common-collar contract; its topological spherical identification remains independent of the physical stationary end chart. The boundary-angle input is used only for its candidate graph, cone and boundary-angle conclusions under those full hypotheses. Lemma 3.3: common spacelike reference collar Boundary angle bound and normal-graph cone

Proof

Given: The existing candidate family and supplied common collar, cone and full-range angle inequality. Goal: Establish the cutoff angle bound and all uniform higher collar estimates.

1.1A1F1F2F3F5

Use the actual original reference section and complete inherited hypotheses in [F5]. The compact smooth Gaussian background in [F1] has uniformly bounded reference distance derivatives. Since $c < 1$ and $∣ d R_{q} ∣_{h_{q, 0}} = 1$ , shrink the tube to make $c ∣ d R_{q} ∣_{h_{q, τ_{q}}} \leq γ < 1$ for all parameters. Choose the fixed radius $0 < ρ_{δ} < r_{δ}$ in the Statement after this shrinking, so its closed cone region lies in this compact common tube and the collar of the full-range angle inequality. Smoothness and compactness of the reference family and the strict cone permit a positive choice independent of $q$ and of the candidates. The first helper in [F3] gives exactly the cutoff values, its positive-set gradient/Laplacian bounds and a fixed collar $R_{q} \leq d / [2 (c + θ_{δ})]$ on which $χ \geq 1 / 2$ . These facts concern fixed background derivatives and use only maximality for the Laplacian trace.

2.1F1F2F3step 1.1

Restrict the common normal graph to the closed reference collar $0 \leq R_{q} \leq ρ_{δ} / 2$ . It is compact and individually smooth through $S$ , so $χ^{m} v_{q}$ attains a maximum there. Its outer value is zero and its value on $S$ has the uniform bound in [F1]. Apply the second helper in [F3] and the full-range differential inequality in [F1]. It supplies the displayed maximum-point formula and a common integer $m$ yielding $v_{q} \leq C_{δ}$ on $χ \geq 1 / 2$ . The nonsmooth zero set of $χ$ cannot contain a positive interior maximum, so differentiation across that set is unnecessary.

3.1A1F1F2F3F4step 2.1

On a smaller fixed reference collar inside that region, the Gaussian graph equation in [F3] identifies $v_{q} = (1 - ∣ D u_{q} ∣_{h_{q, u_{q}}}^{2})^{- 1 / 2}$ . The bound in step 2.1 gives a compact common spacelike slope cone and a uniform Euclidean gradient bound; the original cone gives a height bound. The third and fourth helpers in [F3] therefore provide smooth joint coefficients and a uniformly elliptic extension on a full containing jet box. Flatten the compact smooth fixed boundary with a finite common family of charts. The actual graph height is zero there. The forcing is bounded without any derivative of $D u_{q}$ , so every hypothesis of [F4] is satisfied uniformly, including near $S$ . Apply its boundary theorem and its interior counterpart to obtain a uniform $C^{1, β}$ bound on a smaller collar for some common $β > 0$ .

4.1F1F2F3step 3.1∎

Use the fifth helper in [F3], now with the genuine boundary seed from step 3.1. Freeze the realized coefficients for the initial boundary Schauder gain and then differentiate tangentially and recover the remaining normal derivatives by the uniformly elliptic equation. This gives every finite uniform higher bound on a common smaller collar; one extra derivative yields any prescribed exponent $α < 1$ . The angle bound already supplies uniform spacelikeness. This proves all the stated estimates, without assuming an initial uniform C4 norm or invoking a theorem restricted to interior patches.

Source notes

The cutoff argument follows the original method with its positive-set qualification made explicit. The higher-order step uses an independently sourced boundary C1-Holder estimate before applying local boundary Schauder estimates; individual smoothness alone is not substituted for a uniform estimate. The global weighted temporal theorem and exterior lapse maximum principles are not needed for this local collar argument. No original-article defect is asserted.

External input

The local nonlinear boundary C1-Holder estimate is an imported input. Use Simon Lecture18 Theorem2, printed p.217 with (P), (*) and (**) on pp.216–217 (PDF sheet111): a classical C2 solution with zero Dirichlet trace, bounded height and gradient, bounded forcing, C1 joint coefficient bounds on a containing full jet box, positive uniform ellipticity and a uniformly C2-flattenable boundary has a controlled C1-beta norm on smaller patches for some beta in (0,1). Theorem1 is the interior counterpart. Exact hypotheses and reading limits are recorded in the source metadata. The fifth local helper supplies the subsequent boundary Schauder bootstrap; it does not stand in for this initial estimate.

Depends on

Used by · 1

Lemma 3.4: uniform graph regularity at the bifurcation sphere

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

External dependencies

Leon Simon, Lectures on PDE · Lecture 18, Theorem 2 (C^{1,beta} estimate, boundary), printed p.217, assumptions (P), (*) and (**) on pp.216–217; PDF sheet111

Let u be a C2 solution of a^{ij}(x,u,Du)u_ij=f on a boundary patch, with u=0 on the actual boundary, bounded |u|+R|Du|, bounded f, C1 joint bounds on a^{ij} in a containing position/height/slope box, positive uniform ellipticity on that box, and a C2 boundary-flattening diffeomorphism and inverse with bounded norms. On every smaller patch there is a uniform C^{1,beta} bound, for some beta in (0,1), with constants controlled by dimension, shrinking factor, the height/gradient bound, structural coefficient/ellipticity constants and the flattening constants. The analogous interior statement is Theorem 1 on the same page.

Hypotheses: Classical C2 solution, C1 joint principal coefficients, bounded RHS, uniform positive ellipticity on the containing slope/height box, a common finite height/gradient bound and uniformly C2 flattenable boundary; homogeneous Dirichlet trace on the actual boundary portion. Bounds are local and do not require any condition at the remote spherical edge of the patch.

Reading limits: Retained independent source-input/background reading record: Read the actual retained Simon PDF sheet111, printed pp.216–217, including (P), (*), (**), Theorems1–2 and all stated dependencies. No full proof reconstruction is claimed. This is an imported a priori estimate, not a claimed local proof of boundary gradient Holder regularity. Current maintenance checks the stated contract and its local application, without claiming new external-proof or PDF reading.

Sources

The uniqueness of smooth stationary black holes · PDF p.19, proof of Lemma3.4, cutoff calculation and final Schauder sentence
Leon Simon, Lectures on PDE · Lecture 18, Theorem 2 (C^{1,beta} estimate, boundary), printed p.217, assumptions (P), (*) and (**) on pp.216–217; PDF sheet111