LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

The positive-scalar conformastatic chart tensor is Lorentzian

Statement

For every $D, H, g_{H}$ in Positive-scalar conformastatic chart data, the coordinate tensor $g_{H}$ is a C3 nondegenerate Lorentzian metric of signature $(-, +, +, +)$ . Its inverse components are $g^{00} = - H^{2}$ and $g^{i j} = H^{- 2} δ_{i j}$ , its determinant is $- H^{4}$ , and $\sqrt{∣ \det g ∣} = H^{2}$ . The vector fields $n : = H \partial_{0}$ and $e_{i} : = H^{- 1} \partial_{i}$ form a global orthonormal frame with $g (n, n) = - 1$ , $g (n, e_{i}) = 0$ , and $g (e_{i}, e_{j}) = δ_{i j}$ . The chosen time orientation makes $n$ future-directed, and the frame $(n, e_{1}, e_{2}, e_{3})$ is positively oriented.

Facts & Assumptions

Given: An open set $D \subseteq R^{3}$ , a positive C3 function $H$ independent of $x^{0}$ , and the coordinate tensor $g_{H}$ .

[F1]

Positive-scalar conformastatic chart data defines the coordinate matrix $diag (- H^{- 2}, H^{2}, H^{2}, H^{2})$ , with $H > 0$ . It fixes the coordinate orientation $d x^{0} \land d x^{1} \land d x^{2} \land d x^{3}$ and the future timelike cone $C_{p}^{+} = {v : g_{H} (v, v) < 0, v^{0} > 0}$ . Thus a timelike vector is future-directed exactly when its zeroth coordinate is positive; for $n = H \partial_{0}$ , that coordinate is $H > 0$ .

Proof

1.1givenF1algebra

The coordinate matrix is diagonal and symmetric. Since $H > 0$ , all entries are nonzero, its inverse is $diag (- H^{2}, H^{- 2}, H^{- 2}, H^{- 2})$ , and multiplying the two diagonal matrices gives the identity. The determinant is $(- H^{- 2}) (H^{2})^{3} = - H^{4} < 0$ , so the matrix has exactly one negative and three positive diagonal entries and no zero eigenvalue. Thus it is nondegenerate of signature $(-, +, +, +)$ at every point. Its coefficients and inverse are C3 because $H$ is C3 and the reciprocal map $u \mapsto 1 / u$ is smooth on $(0, \infty)$ .

2.1givenF1step 1.1algebra∎

With the frame fields defined in the Statement, direct contraction against the diagonal matrix gives $g (n, n) = H^{2} (- H^{- 2}) = - 1$ , $g (n, e_{i}) = 0$ , and $g (e_{i}, e_{j}) = H^{- 2} H^{2} δ_{i j} = δ_{i j}$ . Each frame vector is a nonzero multiple of a distinct coordinate vector, so the four vectors form a basis. Their coordinate change matrix is $diag (H, H^{- 1}, H^{- 1}, H^{- 1})$ , with positive determinant $H^{- 2}$ ; hence the frame is positively oriented. The time orientation is the one specified in [F1], so $n$ is future-directed. The already computed metric determinant gives $\sqrt{∣ \det g ∣} = H^{2}$ .

Remarks

The result is pointwise and coordinate-local. It does not assert geodesic completeness, asymptotic flatness, or any Einstein–Maxwell equation.

Depends on

Positive-scalar conformastatic chart data