Pipeline-generated

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.

Smooth null screen and KN parameter family — Examples

1 · Prerequisites

2 · Summary

The example computes the Schwarzschild and nonrotating charged specializations of the exact family identities and records the extremal Reissner–Nordström endpoint as a boundary value. The counterexample computes a flat ingoing null cone with zero Ricci curvature and strictly decreasing area before its finite-affine-parameter vertex. That cone fails the future-complete persistent-cut assumption, so it refutes a weaker local claim without contradicting the restricted area theorem.

The diagram is the $(t, r)$ orbit-space section of the Minkowski example. A point on the cone represents a round two-sphere; the marked points show the sample cuts $(t, r) = (- 2, 2)$ and $(- 1, 1)$ . The generator direction is future-directed along $k = \partial_{t} - \partial_{r}$ , toward the excluded vertex. The proof uses the equations and area calculation, not the drawing.

\begin{tikzpicture}[scale=0.95]
  \draw[->] (0,0.2) -- (3.1,0.2) node[right] {$r$};
  \draw[->] (0,-2.7) -- (0,0.55) node[above] {$t$};
  \draw[thick] (0,0) -- (2.55,-2.55) node[pos=0.78,below right] {$t+r=0$};
  \draw[dashed] (0,-2) -- (2,-2);
  \draw[dashed] (0,-1) -- (1,-1);
  \fill (2,-2) circle (1.7pt);
  \fill (1,-1) circle (1.7pt);
  \fill (0,0) circle (1.7pt);
  \node[anchor=west] at (2.02,-2.02) {$S_{\lambda_0}$, $r_0=2$};
  \node[anchor=west] at (1.02,-1.02) {$S_{\lambda_0+1}$, $r=1$};
  \node[anchor=south west] at (0.06,0.02) {vertex excluded};
  \draw[->,very thick] (1.65,-1.65) -- (0.42,-0.42);
  \node[anchor=south east] at (1.15,-1.08) {$k=\partial_t-\partial_r$};
\end{tikzpicture}

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck pendingOpen item page →

Schwarzschild and charged endpoint algebra

Example

Take the nonrotating slice $a = 0$ of the parameter family in Smooth null screen and subextremal Kerr–Newman parameter family.

If $q = 0$ and $m > 0$ , then $r_{+} = 2 m$ , $D = 4 m^{2}$ , $A = 16 π m^{2}$ , $κ_{K N} = 1 / (4 m)$ , and $j = Ω_{K N} = Φ_{K N} = 0$ . The local horizon data are exactly those proved in Exact Schwarzschild horizon data at the zero-rotation KN point. The first-law identity becomes $d m = κ_{K N} d A / (8 π)$ , and the Smarr identity becomes $m = κ_{K N} A / (4 π)$ .
If $q^{2} < m^{2}$ , put $s = \sqrt{m^{2} - q^{2}}$ and $r_{+} = m + s$ . Then $D = r_{+}^{2}$ , $A = 4 π r_{+}^{2}$ , $κ_{K N} = s / r_{+}^{2}$ , $Φ_{K N} = q / r_{+}$ , and $j = Ω_{K N} = 0$ . The family identities reduce to $d m = κ_{K N} d A / (8 π) + Φ_{K N} d q$ and $m = κ_{K N} A / (4 π) + Φ_{K N} q$ .
At the boundary $q^{2} = m^{2}$ with $m > 0$ , the exact double-root supplier gives $r_{+} = m$ , $D = m^{2}$ , $A = 4 π m^{2}$ , $κ_{K N} = 0$ , and $Φ_{K N} = q / m$ . This is a boundary value, not an assertion about attaining the extremal parameter in a physical process.

Facts & Assumptions

Given: The real parameter family and its strict subextremal formulas, the separately checked zero-rotation zero-charge point, and the exact double-root geometric supplier.

[F1]

Smooth null screen and subextremal Kerr–Newman parameter family: $r_{+} = m + \sqrt{m^{2} - a^{2} - q^{2}}$ , $D = r_{+}^{2} + a^{2}$ , $A = 4 π D$ , $j = m a$ , $κ_{K N} = (r_{+} - m) / D$ , $Ω_{K N} = a / D$ , and $Φ_{K N} = q r_{+} / D$ on $m^{2} > a^{2} + q^{2}$ .

[F2]

Verified Kerr-Newman family first law and Smarr identity: on the strict parameter domain, $d m = \frac{κ_{K N}}{8 π} d A + Ω_{K N} d j + Φ_{K N} d q, m = \frac{κ_{K N} A}{4 π} + 2 Ω_{K N} j + Φ_{K N} q .$

[F3]

KN Killing generators, surface gravity, area and potential: for $M > 0$ and $M^{2} \geq a^{2} + q^{2} > 0$ , the selected outer horizon has $r_{H} = M + \sqrt{M^{2} - a^{2} - q^{2}}$ , area $4 π (r_{H}^{2} + a^{2})$ , $κ_{H} = \sqrt{M^{2} - a^{2} - q^{2}} / (r_{H}^{2} + a^{2})$ , and constant potential $q r_{H} / (r_{H}^{2} + a^{2})$ ; the equality case is the double root with $κ_{H} = 0$ .

[F4]

Exact Schwarzschild horizon data at the zero-rotation KN point: at $a = q = 0$ , the smooth ingoing KN specialization has the null Killing horizon $r = 2 m$ , area $16 π m^{2}$ and signed surface gravity $1 / (4 m)$ .

Verification

1.1F1F4givenalgebra

On $a = q = 0$ , $s = \sqrt{m^{2}} = m$ because $m > 0$ , so $r_{+} = 2 m$ and $D = 4 m^{2}$ . Substitution in [F1] gives $A = 16 π m^{2}$ , $κ_{K N} = 1 / (4 m)$ , and $j = Ω_{K N} = Φ_{K N} = 0$ ; [F4] independently verifies the geometric horizon data at this point.

2.1step 1.1F2algebra

Differentiating $A = 16 π m^{2}$ gives $d A = 32 π m d m$ , whence $κ_{K N} d A / (8 π) = d m$ and $κ_{K N} A / (4 π) = m$ . Thus both family identities in [F2] reduce to the stated Schwarzschild formulas.

2.2F1F2step 1.1algebra

On $a = 0$ with $q^{2} < m^{2}$ , $s = \sqrt{m^{2} - q^{2}} > 0$ , so [F1] gives $r_{+} = m + s$ , $D = r_{+}^{2}$ , $A = 4 π r_{+}^{2}$ , $κ_{K N} = s / r_{+}^{2}$ , $Φ_{K N} = q / r_{+}$ and $j = Ω_{K N} = 0$ . For Smarr, $κ_{K N} A / (4 π) + Φ_{K N} q = s + q^{2} / r_{+} = s + (m^{2} - s^{2}) / (m + s) = s + (m - s) = m$ . For the first law, differentiate $s^{2} = m^{2} - q^{2}$ to obtain $s d s = m d m - q d q$ , and hence $d r_{+} = d m + d s = (r_{+} / s) d m - (q / s) d q$ . Therefore $κ_{K N} d A / (8 π) + Φ_{K N} d q = (s / r_{+}^{2}) (8 π r_{+} d r_{+}) / (8 π) + (q / r_{+}) d q = (s / r_{+}) d r_{+} + (q / r_{+}) d q = d m$ .

3.1F1F3step 2.2algebra∎

At $q^{2} = m^{2}$ and $m > 0$ , the strict parameter formula has the continuous boundary values $s \to 0$ , $r_{+} \to m$ , $D \to m^{2}$ , $A \to 4 π m^{2}$ , $κ_{K N} \to 0$ , and $Φ_{K N} \to q / m$ . Independently, [F3] supplies this selected-model double-root data exactly, since $M = m > 0$ and $M^{2} = a^{2} + q^{2} > 0$ . This verifies the boundary formula without extending the open-family differential identity or making a process claim.

Remarks

The open-family first law and Smarr formula concern exact parameter identities. The extremal line is a boundary of that open family; the example makes no statement about how, or whether, a physical process can reach it.

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck pendingjudge pass (gpt-6-luna)Open item page →

Flat focusing cone without future smooth completeness

Statement refuted

Let $(M, g, N)$ be a time-oriented smooth Lorentzian four-manifold, let $H \subset M$ be a smooth null hypersurface, and let $k$ be a smooth nowhere-zero future-directed section of the radical of $g ∣_{T H}$ with $\nabla_{k} k = 0$ , as in Smooth null screen and subextremal Kerr–Newman parameter family. Use the Ricci tensor defined by contraction of the curvature operator in The Riemann curvature operator and the derived Ricci, scalar and Einstein tensors. Let $S_{0} \subset H$ be a compact smooth embedded two-dimensional submanifold with positive-definite induced metric and $T_{x} H = T_{x} S_{0} \oplus R k_{x}$ . For finite $λ_{*} > λ_{0}$ , suppose $Φ : [λ_{0}, λ_{*}) \times S_{0} \to H$ is smooth, $Φ (λ_{0}, x) = x$ , $\partial_{λ} Φ = k \circ Φ$ , and every $Φ_{λ}$ is an embedding with compact image and positive-definite induced metric. Assume ${A C}_{ω}$ for intrinsic density integration, as in Null focusing and a restricted smooth future area theorem, and use that theorem's definitions $q_{λ} : = Φ_{λ}^{*} g$ , $μ_{q_{λ}}$ , and $A (λ) : = \int_{S_{0}} μ_{q_{λ}}$ . The claim that ${Ric}_{Φ (λ, x)} (k, k) \geq 0$ throughout this finite future flow implies that $A$ is nondecreasing is false. Thus null convergence alone does not guarantee area monotonicity when the affine flow is given only up to a finite future parameter.

Facts & Assumptions

Given: Four-dimensional Minkowski space $R^{1, 3}$ with metric $- d t^{2} + \sum_{i = 1}^{3} d x_{i}^{2}$ , equipped with the time orientation selected by $N = \partial_{t}$ , and the definitions of null screen, expansion and area in Smooth null screen and subextremal Kerr–Newman parameter family.

[F1]

Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model fixes the signature $(-, +, +, +)$ and defines a nonzero causal vector $v$ as future-directed when $g (v, N) < 0$ for the specified smooth timelike time-orientation field $N$ .

[F2]

The Riemann curvature operator and the derived Ricci, scalar and Einstein tensors defines curvature and Ricci by contraction of the curvature operator; Tensoriality of the curvature, its coordinate formula and its point-normal metric formula supplies its coordinate expression.

[F3]

Smooth null screen and subextremal Kerr–Newman parameter family defines affine null generators, $B$ , $θ$ , and the screen metric.

[F4]

Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields supplies the metric-compatible connection and its Christoffel formula; constant Cartesian metric components therefore give zero Christoffel symbols.

[F5]

Null focusing and a restricted smooth future area theorem requires the initial cut to have positive-definite induced metric and satisfy $T_{x} H = T_{x} S_{0} \oplus R k_{x}$ , and every future cut to persist as a smooth embedded surface with positive-definite induced metric on the full future half-line; finite affine endpoints/caustics are excluded by the persistence hypothesis.

[F6]

Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model, Facts [F2]: the positive square root is smooth by repeated differentiation on $(0, \infty)$ , so $r = \sqrt{x_{1}^{2} + x_{2}^{2} + x_{3}^{2}}$ is smooth where $r > 0$ .

Counterexample

1.1F1F3F6givenalgebra

On $R^{1, 3} ∖ {x = 0}$ put $r = \sqrt{x_{1}^{2} + x_{2}^{2} + x_{3}^{2}}$ , $n_{i} = x_{i} / r$ , $H = {t + r = 0, r > 0}$ , and $k = \partial_{t} - \sum_{i} n_{i} \partial_{x_{i}}$ . By [F6], $r$ is smooth for $r > 0$ , so $H$ is a smooth embedded hypersurface. Its normal covector is $d (t + r) = d t + d r$ , whose Minkowski dual is $- \partial_{t} + \partial_{r} = - k$ and whose squared norm is zero; hence $H$ is null and $k$ is a null normal tangent to $H$ . Moreover $g (k, N) = - 1 < 0$ , so $k$ is future-directed by [F1].

1.2F1F2F3F4algebra

The components of the Minkowski metric are constant in the global Cartesian chart, so [F4]'s Christoffel formula gives zero Christoffel symbols. The coordinate curvature formula in [F2] then gives $R^{a}_{b c d} = 0$ and hence $Ric (k, k) = 0$ . Also $k (r) = - 1$ and $k (n_{i}) = k (x_{i} / r) = (- n_{i} r + x_{i}) / r^{2} = 0$ , so the Cartesian components of $k$ are constant along each integral curve and $\nabla_{k} k = 0$ . Choose $r_{0} > 0$ and set $λ_{0} : = - r_{0}$ ; then the initial round cut $S_{λ_{0}} : = {t = λ_{0}, r = r_{0}}$ lies on $H$ . Along each generator from this cut, $λ = t$ is affine and $r (λ) = r_{0} - (λ - λ_{0}) > 0$ for $λ_{0} \leq λ < λ_{*} : = λ_{0} + r_{0} = 0$ .

2.1F3F5step 1.2algebra

For $λ_{0} \leq λ < λ_{*} = 0$ , the cut $S_{λ} : = {t = λ, r = r (λ)}$ lies in $H$ because $λ + r (λ) = λ_{0} + r_{0} = 0$ . It is a round two-sphere of radius $r (λ) > 0$ with induced metric $r (λ)^{2} (d ϑ^{2} + \sin^{2} ϑ d φ^{2})$ and area $A (λ) = \int_{0}^{2 π} \int_{0}^{π} r (λ)^{2} \sin ϑ d ϑ d φ = 4 π r (λ)^{2}$ . The metric is positive definite on each cut. Since $H$ is spanned by the radial generator $k = \partial_{t} - \partial_{r}$ and the two angular tangent directions, $T_{p} H = T_{p} S_{λ} \oplus R k_{p}$ at every prevertex point; in particular the initial cut satisfies the positive-definite and transversality conditions of [F5]. In a screen-orthonormal basis, for any screen vector $X$ one has $\nabla_{X} k = - X (n_{i}) \partial_{x_{i}} = - X / r$ , because $X (r) = 0$ and $X (x_{i}) = X_{i}$ ; hence $B = - \overset{ˉ}{g} / r$ , $θ = - 2 / r$ , and directly $A^{'} (λ) = - 8 π r (λ) < 0$ .

3.1F5step 1.1step 1.2step 2.1givenalgebra∎

At the finite future parameter $λ_{*} = λ_{0} + r_{0} = 0$ , every generator from the initial sphere reaches the common vertex $r = 0$ . The cone ceases to be a smooth embedded null hypersurface there and the flow map collapses the two-sphere to one point, so the future-persistent embedded-cut hypothesis [F5] fails. The strict area decrease on each smooth pre-vertex interval therefore refutes the stated weaker claim without contradicting Null focusing and a restricted smooth future area theorem.

Remarks

The example has zero Ricci contraction and negative expansion on a finite smooth segment. Its future affine incompleteness at the cone vertex is the exact missing hypothesis; it makes no claim about an event horizon.

Smooth null screen and KN parameter family — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

5 · Examples, experiments and counterexamples

Schwarzschild and charged endpoint algebra

Example

Facts & Assumptions

Verification

Remarks

Flat focusing cone without future smooth completeness

Statement refuted

Facts & Assumptions

Counterexample

Remarks

Sources