ExampleConstruction: AI-adaptedVerification: AI-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 metric-selected connection of a conformal metric, verified by the defining identities

Example

Let $U \subseteq R^{4}$ be open, let $φ : U \to R$ be smooth, put $Ω : = e^{φ} > 0$ and consider the conformal metric

$g_{a b} = Ω^{2} η_{a b} = e^{2 φ} η_{a b}, η = diag (- 1, 1, 1, 1),$

on $U$ , with the identity chart and the time orientation $N = \partial_{0}$ (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model). Define, in this chart,

$Γ^{a}_{b c} : = δ^{a}_{b} \partial_{c} φ + δ^{a}_{c} \partial_{b} φ - η_{b c} η^{a d} \partial_{d} φ .$

Then:

$Γ^{a}_{b c} = Γ^{a}_{c b}$ , so the resulting connection is torsion-free.
The compatibility identity $\partial_{a} g_{b c} = \sum_{d} (Γ^{d}_{a b} g_{d c} + Γ^{d}_{a c} g_{b d})$ holds identically on $U$ .
By the uniqueness part of Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields, this connection is the metric-selected connection of $g$ on $U$ ; hence the displayed formula is the Levi–Civita connection of every conformally flat metric in these coordinates.

As a finite check, for the special choice $φ (x) = λ x^{1}$ and $λ \neq 0$ the nonzero symbols are $Γ^{0}_{01} = Γ^{0}_{10} = λ, Γ^{1}_{00} = Γ^{1}_{11} = λ, Γ^{1}_{22} = Γ^{1}_{33} = - λ, Γ^{2}_{12} = Γ^{2}_{21} = Γ^{3}_{13} = Γ^{3}_{31} = λ .$ For $λ = 0$ all symbols vanish. The identity of claim 2 is verified on the components $(a, b, c) = (1, 0, 0)$ and $(0, 0, 0)$ below.

Facts & Assumptions

Given: An open set $U \subseteq R^{4}$ with the identity chart, a smooth $φ : U \to R$ , the metric $g_{a b} = e^{2 φ} η_{a b}$ , and the coefficients $Γ^{a}_{b c} = δ^{a}_{b} \partial_{c} φ + δ^{a}_{c} \partial_{b} φ - η_{b c} η^{a d} \partial_{d} φ$ .

[L1]

The metric $g = e^{2 φ} η$ with $e^{2 φ} > 0$ is a smooth Lorentzian metric of signature $(-, +, +, +)$ on $U$ , and its inverse-metric components are $g^{a b} = e^{- 2 φ} η^{a b}$ with $η^{a d} η_{d b} = δ^{a}_{b}$ (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model, The inverse metric, musical isomorphisms and index raising, Smoothness and transformation of the inverse-metric components).

[L2]

Torsion freedom of a connection in a chart is the symmetry $Γ^{a}_{b c} = Γ^{a}_{c b}$ , and metric compatibility is the identity $\partial_{a} g_{b c} = \sum_{d} (Γ^{d}_{a b} g_{d c} + Γ^{d}_{a c} g_{b d})$ , both in the sense of Torsion freedom and metric compatibility in chart components and Metric compatibility, torsion freedom and the metric-selected connection class.

[L3]

A smooth symmetric nondegenerate metric has exactly one metric-selected connection, characterized by torsion freedom and metric compatibility (Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields, Christoffel symbols of an affine connection).

Verification

technique · direct

1.1givenL2algebra

The coefficients are smooth functions of $x$ because $φ$ is smooth, and they satisfy $Γ^{a}_{b c} - Γ^{a}_{c b} = (δ^{a}_{b} \partial_{c} φ + δ^{a}_{c} \partial_{b} φ) - (δ^{a}_{c} \partial_{b} φ + δ^{a}_{b} \partial_{c} φ) - (η_{b c} - η_{c b}) η^{a d} \partial_{d} φ = 0$ by symmetry of $η$ . Hence the connection they define is torsion-free by [L2].

2.1step 1.1L1L2algebra

For the compatibility identity, multiply the candidate by the metric: $\sum_{d} Γ^{d}_{a b} g_{d c} = e^{2 φ} \sum_{d} Γ^{d}_{a b} η_{d c} = e^{2 φ} (\partial_{b} φ η_{a c} + \partial_{a} φ η_{b c} - η_{a b} \partial_{c} φ)$ , using $δ^{d}_{a} η_{d c} = η_{a c}$ , $δ^{d}_{b} η_{d c} = η_{b c}$ and $η^{d e} η_{d c} = δ^{e}_{c}$ . Adding the analogous expression with $b$ and $c$ interchanged gives $e^{2 φ} (2 \partial_{a} φ η_{b c} + \partial_{b} φ η_{a c} - \partial_{b} φ η_{a c} + η_{a b} \partial_{c} φ - η_{a b} \partial_{c} φ) = 2 \partial_{a} φ e^{2 φ} η_{b c} = \partial_{a} (e^{2 φ} η_{b c}) = \partial_{a} g_{b c}$ , since $\partial_{a} η_{b c} = 0$ and $\partial_{a} e^{2 φ} = 2 \partial_{a} φ e^{2 φ}$ .

3.1step 1.1step 2.1L3algebra

Steps 1.1 and 2.1 verify the two hypotheses of [L3] for the connection with coefficients $Γ$ ; hence this connection is the unique metric-selected connection of $g$ on the chart domain, and since the identity chart covers $U$ it is that connection on $U$ .

4.1step 2.1algebra∎

(Finite check for $φ = λ x^{1}$ .) Here $\partial_{d} φ = λ δ^{1}_{d}$ , so $Γ^{a}_{b c} = λ (δ^{a}_{b} δ^{1}_{c} + δ^{a}_{c} δ^{1}_{b} - η_{b c} η^{a 1})$ . Substitution gives exactly the symbols listed in the Example: the first two arise from the Kronecker-delta terms with $a = 0$ ; for $a = 1$ the diagonal cases $(b, c) = (0, 0), (1, 1), (2, 2), (3, 3)$ give respectively $λ, λ, - λ, - λ$ ; and for $a = 2, 3$ the delta terms give respectively the symmetric pairs $(1, 2), (1, 3)$ with value $λ$ . All other cases vanish by the displayed formula. If $λ = 0$ every coefficient is zero. For $(a, b, c) = (1, 0, 0)$ the identity of claim 2 reads $\partial_{1} g_{00} = 2 Γ^{0}_{10} g_{00} = 2 λ (- e^{2 λ x^{1}}) = - 2 λ e^{2 λ x^{1}}$ , which equals $\partial_{1} (- e^{2 λ x^{1}})$ ; for $(a, b, c) = (0, 0, 0)$ both sides vanish.

Remarks

The example shows that the Koszul construction of Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields is effective: the two defining identities alone identify the connection, with no frame field or curvature computation. Nothing here is a statement about the curvature of $g = e^{2 φ} η$ ; the conformal factor is an arbitrary positive smooth function and may or may not come from a coordinate transformation of the flat metric.

The metric-selected connection of a conformal metric, verified by the defining identities

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources