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.
Selected ingoing RN extension and time orientation
Definition
Let be length parameters. Set and The selected ingoing RN manifold is where have units of metres, has unit round metric and outward area form , and the signature is . Orient the product by . Define These are smooth on every , including every positive root of ; the domain excludes . This is an extension of the static RN metric and field, not a maximal extension or a specification of a source at the excluded centre.
For the time orientation, define the global smooth fields The chosen future timelike field is ; the future cone is the component of the timelike cone containing it. The well-definedness proof shows that is timelike and that are future null. On , the substitution with identifies the metric and two-form with the static dyonic RN formulas of Dyonic Reissner-Nordström metric and field domains. This coordinate identification does not assert agreement of time orientations on the interior static components: on the selected orientation agrees with , while on it is the opposite of the separate choice made by that static definition.
Facts & Assumptions
Given: Real length parameters , the unit round oriented sphere, and signature .
Dyonic Reissner-Nordström metric and field domains: on each open where , the static metric is and the two-form is ; its independently selected time orientation is on and on . This is a current draft definition, used only through these exact formulas.
Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model: a smooth Lorentzian metric together with a smooth everywhere timelike vector field specifies a time orientation. Time orientation, future and past timelike/null/causal vectors, and the closed cones defines the future cone as the closure of the timelike component containing that field.
Classification of future and past causal vectors by a timelike field: for a nonzero causal vector , future-directedness is equivalent to for the chosen future timelike field .
The coordinate domain is . No positive-mass or nonzero-charge hypothesis is imposed. The finite component calculations below use no choice principle.
Proof
In product coordinates the block is with determinant and inverse Its eigenvalues have opposite signs because their product is negative. The sphere block is positive definite for , so is a smooth nondegenerate Lorentzian metric on the stated product. The two-form is smooth since is smooth on and is global.
The product fields are global and smooth, hence so are . Direct contraction gives , , , and . Thus is an everywhere timelike field and fixes the asserted time orientation; [F3] then makes both nonzero null fields future-directed.
On any component where , substitute into . The mixed terms cancel and the radial coefficient is , giving . Also , so becomes the static two-form in [F1]. The substitution is defined separately on each component where ; it does not extend through a root.
On , and , so the exterior orientations agree. On , the static-coordinate vector is , and ; hence the static definition's is past-directed under the selected ingoing orientation. This proves the stated convention boundary and makes no identification of the two interior time orientations.
Remarks
The future orientation is chosen by the smooth global field . The static metric and field formulas agree on every component, while their separate interior time-orientation convention is not inherited across the ingoing extension. No global event-horizon or maximal-extension conclusion is part of this definition.