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.

SI and geometric solution parameter identifications — Examples

1 · Prerequisites

2 · Summary

Scope

These examples calculate the outer equatorial circular null-orbit radius in the selected dyonic RN exterior and exhibit a fixed-angular-coordinate spacelike curve in a selected rotating KN ergoregion. The first uses the adopted geometric-optics rule to interpret a null geodesic as an ideal light ray; neither example reports an observation. The rotating example concerns only the specified stationary Killing field and does not claim an extraction process or rule out trajectories with angular motion.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

Thought experimentStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-6-luna)Open item page →

RN circular null orbit example

Physical scope

A conditional calculation of equatorial circular null geodesic radii in the selected dyonic RN exterior. Under the adopted geometric-optics rule, these are ideal-light-ray orbit radii; the result makes no stability, photon-mass, observation, or measurement claim.

Statement

Let $m_{*} > 0$ and $Q_{e}, Φ_{B} \in R$ be SI mass, electric-charge and magnetic-flux inputs, and define the dyonic RN lengths by SI and geometric solution parameter identifications and Dyonic Reissner-Nordström metric and field domains. Write $Q^{2} : = q_{e}^{2} + q_{m}^{2}$ and assume $0 \leq Q^{2} \leq M^{2}$ . In the static exterior $r > r_{+} : = M + \sqrt{M^{2} - Q^{2}}$ , let $γ$ be a future affine null geodesic in the equatorial plane $θ = π / 2$ , with constants $E : = f {\dot{x}}^{0} > 0$ and $ℓ : = r^{2} \dot{ϕ} \neq 0$ . Its radial equation is ${\dot{r}}^{2} = E^{2} - ℓ^{2} V (r), V (r) : = \frac{f (r)}{r^{2}} .$ An exterior circular null orbit exists at and only at the outer radius $r_{γ}^{+} = \frac{3 M + \sqrt{9 M^{2} - 8 Q^{2}}}{2} > r_{+} .$ The second algebraic stationary radius $r_{γ}^{-} = (3 M - \sqrt{9 M^{2} - 8 Q^{2}}) / 2$ lies at or inside $r_{+}$ and is not a second exterior circular orbit. Radii are in metres. By the adopted geometric-optics assumption of Adopted clock, free-fall and light-ray assumptions of the classical gravitational framework, the exhibited null geodesic is an ideal-light-ray orbit within that model approximation. The result says nothing about orbital stability or an observed photon trajectory.

Facts & Assumptions

Given: The conditional dyonic RN model with $M > 0$ and $0 \leq Q^{2} \leq M^{2}$ , the static exterior, and the adopted ideal-light-ray geometric-optics rule.

[F1]

SI and geometric solution parameter identifications and Dyonic Reissner-Nordström metric and field domains: $M = G_{N} m_{*} / c^{2}$ , $q_{e} = \sqrt{G_{N} / (4 π ε_{0} c^{4})} Q_{e}$ , $q_{m} = α Φ_{B} / (4 π)$ , and the static metric is $g = - f (d x^{0})^{2} + f^{- 1} d r^{2} + r^{2} (d θ^{2} + \sin^{2} θ d ϕ^{2})$ with $f = 1 - 2 M / r + Q^{2} / r^{2}$ .

[F2]

Dyonic RN as adopted Einstein–Maxwell model: this dyonic RN datum on $r > 0$ , $f \neq 0$ is a conditional solution of the adopted source-free equation-based model; the field-equation proof is draft and not independently accepted.

[A1]

Adopted clock, free-fall and light-ray assumptions of the classical gravitational framework: in geometric optics an ideal light ray is assumed to be a future null geodesic of the metric-selected connection. This is an adopted model postulate, not an equation derived from the RN field solution.

[F3]

Metric compatibility, torsion freedom and the metric-selected connection class and Geodesic of an affine connection: the selected connection is torsion-free and metric-compatible, and an affine geodesic satisfies $D_{t} γ^{'} = 0$ .

[F4]

Killing fields of a Lorentzian metric and Killing fields and conserved currents, and on-shell conservation of the Hilbert stress-energy tensor: a Killing field has zero metric Lie derivative, and its metric pairing with an affine geodesic tangent is constant.

[F5]

SI unit and coordinate conventions of the classical gravitational framework: $x^{0} = c t$ and $r$ have units of metres; affine constants below are coordinate-geometric constants and are not assigned particle-energy measurements.

[F6]

Classification of future and past causal vectors by a timelike field: a nonzero causal vector whose metric pairing with the selected future timelike field is negative is future-directed.

[A2]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): the inherited RN metric and geometric-flux conventions use only ${A C}_{ω}$ . The finite root and geodesic calculation makes no new selections from families and uses no full AC.

Proof

1.1F1F4F5A1

On the static exterior $f > 0$ , the fields $\partial_{x^{0}}$ and $\partial_{ϕ}$ are Killing because the metric in [F1] is independent of $x^{0}$ and $ϕ$ . Therefore [F4] makes $E = f {\dot{x}}^{0} = - g (\partial_{x^{0}}, γ^{'})$ and $ℓ = r^{2} \dot{ϕ} = g (\partial_{ϕ}, γ^{'})$ constant along the affine geodesic. Restrict to its equatorial plane, as in the Statement.

2.1F1step 1.1algebra

Substituting $θ = π / 2$ , $\dot{θ} = 0$ and these constants into $g (γ^{'}, γ^{'}) = 0$ gives $- f {\dot{x}}^{0, 2} + f^{- 1} {\dot{r}}^{2} + r^{2} {\dot{ϕ}}^{2} = 0.$ Multiplying by $f > 0$ and using $E = f {\dot{x}}^{0}$ , $ℓ = r^{2} \dot{ϕ}$ yields ${\dot{r}}^{2} = E^{2} - f ℓ^{2} / r^{2}$ .

3.1F1F3step 2.1algebra

The metric-selected Christoffel formula from [F3] gives $Γ^{r}_{00} = f f^{'} / 2$ and $Γ^{r}_{ϕ ϕ} = - f r$ on the equator. At a circular point, $\dot{r} = \ddot{r} = 0$ and the radial geodesic equation becomes $f f^{'} {\dot{x}}^{0, 2} / 2 - f r {\dot{ϕ}}^{2} = 0$ . The null condition gives $f {\dot{x}}^{0, 2} = r^{2} {\dot{ϕ}}^{2}$ , so the radial equation is equivalent to $V^{'} (r) = \frac{f^{'}}{r^{2}} - \frac{2 f}{r^{3}} = 0.$ Conversely, at an equatorial point with $f > 0$ and $V^{'} = 0$ , the same connection coefficients make the radial equation hold for the null circular tangent; the $x^{0}$ and $ϕ$ equations have only terms proportional to $\dot{r}$ , and the $θ$ equation vanishes at $θ = π / 2$ by reflection symmetry. Thus solving $V^{'} = 0$ is necessary and sufficient for an equatorial circular null geodesic in the static region.

4.1step 3.1algebra

Expanding $V = r^{- 2} - 2 M r^{- 3} + Q^{2} r^{- 4}$ gives $V^{'} (r) = - \frac{2}{r^{5}} (r^{2} - 3 M r + 2 Q^{2}) .$ The discriminant is $9 M^{2} - 8 Q^{2} \geq M^{2} > 0$ , so its real roots are $r_{γ}^{\pm} = (3 M \pm \sqrt{9 M^{2} - 8 Q^{2}}) / 2$ . Set $x = \sqrt{M^{2} - Q^{2}} \in [0, M]$ and $s = \sqrt{M^{2} + 8 x^{2}} = \sqrt{9 M^{2} - 8 Q^{2}}$ . Then $r_{γ}^{+} - r_{+} = \frac{M + s - 2 x}{2} > 0,$ because $s^{2} - (2 x)^{2} = M^{2} + 4 x^{2} > 0$ , while $r_{γ}^{-} - r_{+} = \frac{M - s - 2 x}{2} \leq 0$ because $s \geq M$ and $x \geq 0$ . Thus exactly the outer root is in $r > r_{+}$ , and there $f > 0$ .

5.1F1F6A1step 3.1step 4.1algebra

At $r = r_{γ}^{+}$ choose any $ℓ \neq 0$ and set $E = ∣ ℓ ∣ \sqrt{f (r_{γ}^{+})} / r_{γ}^{+} > 0$ . Then the null condition and $V^{'} (r_{γ}^{+}) = 0$ make the radial geodesic equation hold with constant $r$ . Taking ${\dot{x}}^{0} = E / f > 0$ and $\dot{ϕ} = ℓ / r^{2}$ makes the tangent nonzero and null; its pairing with the selected future timelike static field $ξ = \partial_{x^{0}}$ is $g (ξ, γ^{'}) = - E < 0$ , so [F6] makes it future-directed. The equatorial angular equation also holds as shown in step 3.1. This constructs the outer circular null geodesic, rather than only a formal root of an effective potential.

6.1A1F2step 5.1A2∎

The outer orbit is therefore a conditional null-geodesic prediction of the selected dyonic RN model. The geometric-optics postulate interprets such a curve as an ideal light ray within its scope; no stability or empirical claim follows.

Thought experimentStatement: AI-adaptedProof: AI-adaptedOpen item page →

Fixed-coordinate curve is spacelike in the rotating ergoregion

Physical scope

Conditional demonstration that a fixed-angular-coordinate stationary curve is spacelike in a chosen exterior region of the rotating KN model. It supplies no energy-extraction argument, maximum-extension result, or observation and does not rule out timelike trajectories with angular motion.

Statement

Take the zero-magnetic-flux KN model with SI mass, angular-momentum and electric-charge inputs $m_{*} > 0, J, Q_{e}$ , mapped by SI and geometric solution parameter identifications to lengths $M, a, q$ . Assume $M > 0$ , $a \neq 0$ , and $M^{2} \geq a^{2} + q^{2} > 0$ . Use the selected ingoing product and its future orientation from Regular ingoing KN metric, field and sphere axes, and write $N$ for that product's designated smooth future timelike field. Let $r_{+} = M + \sqrt{M^{2} - a^{2} - q^{2}}, r_{E +} = M + \sqrt{M^{2} - q^{2}} .$ At the equator, choose any $r$ with $r_{+} < r < r_{E +}$ and fixed azimuth $ψ_{0}$ , and set $ω_{0} = (\cos ψ_{0}, \sin ψ_{0}, 0) \in S^{2}$ . The candidate fixed-coordinate curve is the smooth map $γ : R \to M_{i n}, v \mapsto (v, r, ω_{0}) .$ Its tangent is $T = \partial_{v} \neq 0$ and, by Specified time Killing stationary-limit set and geodesic constants, $g (T, T) > 0$ , so it is a regular spacelike curve. The exact definition Timelike worldlines, proper time, length and four-velocity on a Lorentzian four-manifold makes a future timelike worldline a $C^{1}$ map $η : I \to M_{i n}$ on an interval $I$ with nonempty interior whose tangent satisfies $g (η^{'}, η^{'}) < 0$ and $g (η^{'}, N) < 0$ at every parameter value; its tangent is therefore nonzero. Thus $γ$ is not a worldline of a massive observer and cannot represent one at rest in these stationary coordinates. For ideal freely falling massive test bodies, Adopted clock, free-fall and light-ray assumptions of the classical gravitational framework separately adopts a future timelike geodesic worldline. The ergoregion here means the positive-norm set of the specified stationary Killing field, as defined in Causal solutions, Killing horizons, escape and metric extensions. Curves with angular motion require a separate norm calculation; no energy-extraction or empirical claim follows.

Facts & Assumptions

Given: The pure-electric KN SI inputs, $M > 0$ , $a \neq 0$ , $M^{2} \geq a^{2} + q^{2} > 0$ , the selected ingoing model, and the adopted massive-test-body interpretation.

[F1]

SI and geometric solution parameter identifications: $M = G_{N} m_{*} / c^{2}$ , $a = J / (m_{*} c)$ , $q_{e} = \sqrt{G_{N} / (4 π ε_{0} c^{4})} Q_{e}$ , and $ε_{0} μ_{0} c^{2} = 1$ ; zero magnetic flux makes the KN seed parameter $q = q_{e}$ .

[F2]

Verified rotating electric KN physical model: on the stated electric KN domains with $Δ \neq 0$ , the SI-rescaled datum is a conditional source-free equation-based model solution; its field-equation proof is draft and not independently accepted.

[F3]

Regular ingoing KN metric, field and sphere axes: $M_{i n} = R_{v} \times (0, \infty)_{r} \times S^{2}$ carries the smooth selected ingoing metric and future timelike field $N = \partial_{v} - \frac{1}{2} (1 + f_{0}^{2}) \partial_{r}$ , where $f_{0} = 1 - (2 M r - q^{2}) / Σ$ ; $T = \partial_{v}$ is defined on the full product. Its field-equation continuation remains conditional on the current verification draft.

[L1]

Specified time Killing stationary-limit set and geodesic constants: $g (T, T) = - (r^{2} - 2 M r + q^{2} + a^{2} \cos^{2} θ) / Σ$ ; at the equator the outer stationary-limit radius is $r_{E +} = M + \sqrt{M^{2} - q^{2}}$ , it strictly exceeds $r_{+}$ when $a \neq 0$ , and the norm is positive between the roots. Its proof remains draft and is used conditionally.

[F4]

Causal solutions, Killing horizons, escape and metric extensions: for a specified stationary Killing field, the ergoregion is its positive-norm set; this definition alone does not identify a null horizon.

[A1]

Adopted clock, free-fall and light-ray assumptions of the classical gravitational framework adopts a future timelike geodesic worldline for an ideal freely falling massive test body; it does not derive that physical rule from the KN equations. The exact mathematical worldline condition from Timelike worldlines, proper time, length and four-velocity on a Lorentzian four-manifold is a $C^{1}$ map on an interval with nonempty interior whose tangent satisfies $g (η^{'}, η^{'}) < 0$ and $g (η^{'}, N) < 0$ for the selected future timelike field $N$ .

[A2]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): the inherited geometric metric convention uses only ${A C}_{ω}$ . The finite choice of a radius between two explicit real roots uses no family selection or full AC.

Proof

1.1givenF1F3algebra

From $a \neq 0$ and $M^{2} \geq a^{2} + q^{2}$ , we have $M^{2} - q^{2} \geq a^{2} > 0$ . Therefore $r_{E +} - r_{+} = \sqrt{M^{2} - q^{2}} - \sqrt{M^{2} - a^{2} - q^{2}} > 0,$ since the first radicand exceeds the second and both square roots are nonnegative. Both radii are positive, so the stated open interval is nonempty. Retain the arbitrary radius $r$ of the Statement with $r_{+} < r < r_{E +}$ . In particular $r > 0$ , which places every point of $γ$ in the selected product.

2.1L1step 1.1algebra

On the equator, [L1] gives $g (T, T) = - (r^{2} - 2 M r + q^{2}) / r^{2}$ . The numerator factors as $(r - r_{E -}) (r - r_{E +})$ , where $r_{E -} = M - \sqrt{M^{2} - q^{2}} < M \leq r_{+}$ ; the chosen radius satisfies $r_{E -} < r < r_{E +}$ , so the numerator is strictly negative. Thus $g (T, T) > 0$ . The fixed-coordinate curve has derivative $T$ and is spacelike at every point.

3.1A1step 2.1

By the future timelike worldline condition in [A1], a curve representing a massive observer must have a future timelike tangent. Since the curve in step 2.1 has a spacelike tangent, it cannot be such an observer at rest in the chosen stationary coordinates. This conclusion concerns only tangent $T$ ; an angularly moving curve has a different tangent and needs its own causal-norm check.

4.1F2F3F4A1step 3.1A2∎

The result uses the conditional KN solution and ergoregion geometry only as specified in [F2]-[L1]. It establishes no extraction process, horizon maximality, observation, or measured property.

SI and geometric solution parameter identifications — Examples

1 · Prerequisites

2 · Summary

Scope

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

5 · Examples, experiments and counterexamples

RN circular null orbit example

Statement

Facts & Assumptions

Proof

Fixed-coordinate curve is spacelike in the rotating ergoregion

Statement

Facts & Assumptions

Proof

Sources