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.

A mixed tensor field: components in two charts and the invariance of its trace

Example

Let $M = R^{4}$ carry the flat Lorentzian metric $g = diag (- 1, 1, 1, 1)$ and the time orientation $N = \partial_{0}$ , so that $(M, g, N)$ is a time-oriented smooth Lorentzian four-manifold (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model); here $g$ and $N$ enter only to place the charts and the tensor field in the setting of the cited definition and take no part in the computation. Let $x = (x^{0}, x^{1}, x^{2}, x^{3})$ be the identity chart and let the chart $y = (y^{0}, y^{1}, y^{2}, y^{3})$ be defined by

$y^{0} = x^{0}, y^{1} = x^{1} + x^{0}, y^{2} = x^{2}, y^{3} = x^{3} .$

Define a type $(1, 1)$ tensor field $T$ on $M$ by its components in the $x$ chart,

$T^{0}_{1} : = 1, T^{2}_{3} : = x^{1}, T^{a}_{b} : = 0 otherwise .$

Then $T$ is a smooth type $(1, 1)$ tensor field. Its components in the chart $y$ are

$T^{' 0}_{0} = - 1, T^{' 0}_{1} = 1, T^{' 1}_{0} = - 1, T^{' 1}_{1} = 1, T^{' 2}_{3} = y^{1} - y^{0}, others 0,$

and its trace computed in the two charts agrees: it is $0$ in both, as the chart-independence of contraction requires.

Facts & Assumptions

Given: The flat Lorentzian four-manifold $(R^{4}, g, N)$ with time orientation $N = \partial_{0}$ , the charts $x$ and $y$ on $R^{4}$ , and the component data $T^{0}_{1} = 1$ , $T^{2}_{3} = x^{1}$ , all other $T^{a}_{b} = 0$ .

[L1]

A smooth type $(1, 1)$ tensor field has component functions $T^{a}_{b} (q) = T_{q} (d x^{a} ∣_{q}, \partial_{b} ∣_{q})$ in each chart, and it is smooth exactly when these components are $C^{\infty}$ in every smooth chart (Tensor fields of type (r,s) on a Lorentzian four-manifold and their components).

[L2]

In overlapping charts the components of a smooth type $(r, s)$ tensor field satisfy $T^{' a_{1} \dots a_{r}}_{b_{1} \dots b_{s}} (y (q)) = \sum_{c, d} (\prod_{i} \frac{\partial y^{a_{i}}}{\partial x^{c_{i}}}) (\prod_{j} \frac{\partial x^{d_{j}}}{\partial y^{b_{j}}}) T^{c_{1} \dots c_{r}}_{d_{1} \dots d_{s}} (x (q))$ (The component transformation law of a smooth tensor field).

[L3]

The trace $tr T$ of a smooth type $(1, 1)$ field is a smooth function whose value in every smooth chart is $\sum_{a} T^{a}_{a}$ (Contraction of a smooth tensor field is a smooth tensor field).

Verification

technique · direct

1.1givenalgebra

The two maps $y$ and $x = (y^{0}, y^{1} - y^{0}, y^{2}, y^{3})$ are mutually inverse smooth maps between open subsets of $R^{4}$ , so $x$ and $y$ are smooth charts on $R^{4}$ . Their Jacobians are constant: $\frac{\partial y^{a}}{\partial x^{c}}$ is $1$ for $(a, c) \in {(0, 0), (1, 0), (1, 1), (2, 2), (3, 3)}$ and $0$ otherwise, while $\frac{\partial x^{d}}{\partial y^{b}}$ is $1$ for $(d, b) \in {(0, 0), (1, 1), (2, 2), (3, 3)}$ and $- 1$ for $(d, b) = (1, 0)$ , and $0$ otherwise.

1.2givenL1

The components $T^{a}_{b}$ are $1$ , $x^{1}$ and $0$ , hence $C^{\infty}$ on $R^{4}$ ; by [L1] the field $T$ is a smooth type $(1, 1)$ tensor field.

2.1step 1.1L2algebra

By [L2] and step 1.1, $T^{' a}_{b} = \sum_{c, d} \frac{\partial y^{a}}{\partial x^{c}} \frac{\partial x^{d}}{\partial y^{b}} T^{c}_{d} = \frac{\partial y^{a}}{\partial x^{0}} \frac{\partial x^{1}}{\partial y^{b}} + (y^{1} - y^{0}) \frac{\partial y^{a}}{\partial x^{2}} \frac{\partial x^{3}}{\partial y^{b}}$ , where $x^{1} = y^{1} - y^{0}$ . Evaluating the two terms: at $(a, b) = (0, 0)$ we get $1 \cdot (- 1) + 0 = - 1$ ; at $(a, b) = (0, 1)$ we get $1 \cdot 1 + 0 = 1$ ; at $(a, b) = (1, 0)$ we get $1 \cdot (- 1) + 0 = - 1$ ; at $(a, b) = (1, 1)$ we get $1 \cdot 1 + 0 = 1$ ; at $(a, b) = (2, 3)$ we get $0 + (y^{1} - y^{0}) \cdot 1 \cdot 1 = y^{1} - y^{0}$ ; all other entries vanish because the corresponding Jacobian entries are $0$ .

3.1step 2.1L3algebra∎

In the $x$ chart the diagonal components are $T^{0}_{0} = T^{1}_{1} = T^{2}_{2} = T^{3}_{3} = 0$ , so $\sum_{a} T^{a}_{a} = 0$ ; in the $y$ chart, step 2.1 gives diagonal entries $T^{' 0}_{0} = - 1$ and $T^{' 1}_{1} = 1$ with $T^{' 2}_{2} = T^{' 3}_{3} = 0$ , so $\sum_{a} T^{' a}_{a} = - 1 + 1 + 0 + 0 = 0$ . The two values agree, as required by [L3].

Remarks

The example also shows that the diagonal components individually are not invariant: the trace is the chart-independent quantity. The mixed field $T$ has both contravariant and covariant slots, and step 2.1 uses one Jacobian factor of each kind, in contrast to the purely covariant case.

A mixed tensor field: components in two charts and the invariance of its trace

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources