Future-complete horizon focusing proof of the area theorem (source code)

= Future-complete horizon focusing proof of the area theorem

For future-complete generators of an <event horizon>, the <null convergence condition> and hypersurface orthogonality reduce the <Null Raychaudhuri equation> to $\theta'\leq-\theta^2/2$. If $\theta_0<0$, integration gives focusing within affine distance $2/|\theta_0|$. The <null focusing theorem> identifies this with a <conjugate point to a spacelike surface>. A null generator cannot remain on an <achronal boundary> beyond such a focal point, contradicting future completeness on the horizon. Thus $\theta\geq0$, and $dA/d\lambda=\theta A\geq0$ gives the <second law of black-hole mechanics>. New horizon generators may join toward the future at crease sets, adding area, but generators have no future endpoints on a regular event horizon under these assumptions.

// Target: quantum-field-theory.bigb