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.

Metric density, volume form and current flux of the flat metric in the identity chart

Example

Let $M = R^{4}$ carry the identity chart $x = (x^{0}, x^{1}, x^{2}, x^{3})$ , the flat Lorentzian metric $g = diag (- 1, 1, 1, 1)$ , the time orientation $N = \partial_{0}$ and the orientation for which the identity chart is oriented (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model, Oriented smooth manifolds and oriented charts); let $\nabla$ be the metric-selected connection of $g$ and ${v o l}_{g}$ the metric volume form (The metric volume form, current flux through 3-faces and finite-chain charges). Then:

The metric density and the volume form are $w = 1$ and ${v o l}_{g} = d x^{0} \land d x^{1} \land d x^{2} \land d x^{3}$ in the identity chart, and ${v o l}_{g} (\partial_{0}, \partial_{1}, \partial_{2}, \partial_{3}) = 1$ .
The connection is the coordinate connection, $Γ \equiv 0$ , so that $\nabla_{a} J^{a} = \partial_{a} J^{a}$ for every smooth vector field $J$ and the divergence formula $w^{- 1} \partial_{a} (w J^{a})$ reduces to the coordinate divergence.
For $J = x^{1} \partial_{1}$ the divergence is $\nabla_{a} J^{a} = 1$ , the current form is $ι_{J} {v o l}_{g} = - x^{1} d x^{0} \land d x^{2} \land d x^{3}$ , and $d (ι_{J} {v o l}_{g}) = {v o l}_{g}$ , in accordance with Divergence, Stokes flux balance and the non-null face formula for a Lorentzian current clause (a).
Let $Δ^{3} = {(t_{1}, t_{2}, t_{3}) : t_{i} \geq 0, t_{1} + t_{2} + t_{3} \leq 1}$ with its coordinate orientation and coordinate volume $1 / 6$ . The affine simplex $σ_{-} (t) = (t_{1}, 0, t_{2}, t_{3})$ has adapted normal $- \partial_{1}$ , so the flux of $J = \partial_{1}$ through it is $- 1 / 6$ . The affine simplex $σ_{+} (t) = (t_{2}, a, t_{1}, t_{3})$ on the parallel plane $x^{1} = a$ has adapted normal $+ \partial_{1}$ , so its flux is $+ 1 / 6$ . Both induced metric densities on the parameter simplex equal $1$ ; the signs follow from the stated parameter orientations and the ambient chart orientation.

Facts & Assumptions

Given: The flat Lorentzian four-manifold $(R^{4}, g)$ with the identity chart $x$ , $g = diag (- 1, 1, 1, 1)$ , the metric-selected connection $\nabla$ of Metric compatibility, torsion freedom and the metric-selected connection class, the vector fields $J = x^{1} \partial_{1}$ and $J_{0} = \partial_{1}$ of A smooth vector field is a smooth section of the tangent bundle, and the affine simplices $σ_{-} (t) = (t_{1}, 0, t_{2}, t_{3})$ and $σ_{+} (t) = (t_{2}, a, t_{1}, t_{3})$ on $Δ^{3} = {t_{i} \geq 0, t_{1} + t_{2} + t_{3} \leq 1}$ .

[L1]

The metric density is $w = \sqrt{∣ \det (g_{a b}) ∣}$ and the local volume form is $w d x^{0} \land d x^{1} \land d x^{2} \land d x^{3}$ in every oriented chart; for the flat metric both are constant (The metric volume form, current flux through 3-faces and finite-chain charges, Chart independence of the metric volume form, its value on orthonormal frames, and the unit normal and density of a non-null hyperplane).

[L2]

On the identity chart the Christoffel symbols vanish, so $\nabla$ is the coordinate connection and $\nabla_{a} J^{a} = \partial_{a} J^{a}$ ; this is the unique metric-selected connection (Metric compatibility, torsion freedom and the metric-selected connection class, Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields, The derivative of the metric density and the chart formula for the divergence of a vector field).

[L3]

The interior product inserts the vector in the first slot: $(ι_{J} ω) (X_{1}, \dots) = ω (J, X_{1}, \dots)$ ; consequently $ι_{\partial_{a}} (d x^{0} \land \dots \land d x^{3}) = (- 1)^{a} d x^{0} \land \dots \hat{d x^{a}} \dots \land d x^{3}$ (Interior product of a form by a vector field, The wedge product of differential forms).

[L4]

The exterior derivative of a $3$ -form is computed in coordinates by the alternating sum of partial derivatives, and $d (ι_{J} {v o l}_{g}) = (\nabla_{a} J^{a}) {v o l}_{g}$ (Divergence, Stokes flux balance and the non-null face formula for a Lorentzian current clause (a)).

[L5]

For a non-null $3$ -face with adapted unit normal $ν^{*}$ the pullback of $ι_{J} {v o l}_{g}$ on the ordered velocity basis $(v_{1}, v_{2}, v_{3})$ equals $ε g (J, ν^{*}) \sqrt{∣ \det (g (v_{i}, v_{j})) ∣}$ with $ε = g (ν^{*}, ν^{*})$ (Divergence, Stokes flux balance and the non-null face formula for a Lorentzian current clause (c), Chart independence of the metric volume form, its value on orthonormal frames, and the unit normal and density of a non-null hyperplane).

[L6]

The simplex coefficient integral uses zero extension to $[0, 1]^{3}$ . Each successive indicator section is an integrable interval indicator, so Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections reduces its volume to $\int_{0}^{1} \int_{0}^{1 - t_{1}} \int_{0}^{1 - t_{1} - t_{2}} 1 d t_{3} d t_{2} d t_{1} = \int_{0}^{1} (1 - t_{1})^{2} / 2 d t_{1} = 1 / 6$ by The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ and the simplex-integral convention of Integral of a form over a smooth singular simplex.

Verification

technique · direct; evaluate the definitions on the constant-coefficient flat data

1.1L1algebra

(Density and volume form.) Since $g_{a b} = diag (- 1, 1, 1, 1)$ is constant, $w = \sqrt{∣ \det g ∣} = \sqrt{∣ - 1 ∣} = 1$ , and [L1] gives ${v o l}_{g} = d x^{0} \land d x^{1} \land d x^{2} \land d x^{3}$ . Evaluating on the coordinate frame, ${v o l}_{g} (\partial_{0}, \partial_{1}, \partial_{2}, \partial_{3}) = w \det (δ^{a}_{b}) = 1$ .

1.2L2algebra

(Connection and divergence.) The Christoffel symbols of the constant metric vanish: $Γ^{a}_{b c} = \frac{1}{2} g^{a d} (\partial_{b} g_{d c} + \partial_{c} g_{b d} - \partial_{d} g_{b c}) = 0$ . By [L2], $\nabla$ is the coordinate connection, so for $J = x^{1} \partial_{1}$ (components $J^{0} = 0$ , $J^{1} = x^{1}$ , $J^{2} = J^{3} = 0$ ) the divergence is $\nabla_{a} J^{a} = \partial_{0} 0 + \partial_{1} x^{1} + \partial_{2} 0 + \partial_{3} 0 = 1$ .

2.1step 1.1step 1.2L3L4algebra

(Current form and its derivative.) By [L3], $ι_{J} {v o l}_{g} = (- 1)^{1} J^{1} d x^{0} \land d x^{2} \land d x^{3} = - x^{1} d x^{0} \land d x^{2} \land d x^{3}$ . Differentiating by [L4], $d (ι_{J} {v o l}_{g}) = - \partial_{1} x^{1} d x^{1} \land d x^{0} \land d x^{2} \land d x^{3} = d x^{0} \land d x^{1} \land d x^{2} \land d x^{3} = {v o l}_{g}$ , which equals $(\nabla_{a} J^{a}) {v o l}_{g}$ by step 1.2.

3.1step 2.1L5L6algebra∎

(Two flux orientations.) On the affine simplex $σ_{-}$ , the ordered velocities are $(v_{1}, v_{2}, v_{3}) = (\partial_{0}, \partial_{2}, \partial_{3})$ and their Gram matrix is $diag (- 1, 1, 1)$ , so its determinant is $- 1$ and the induced density is $1$ . The ambient ordered basis $(\partial_{1}, \partial_{0}, \partial_{2}, \partial_{3})$ is negatively oriented; therefore the adapted normal is $ν_{-}^{*} = - \partial_{1}$ . The face is non-null, $ε = 1$ , and $ε g (J_{0}, ν_{-}^{*}) = - 1$ . Hence $σ_{-}^{*} (ι_{J_{0}} {v o l}_{g}) = - d t_{1} \land d t_{2} \land d t_{3}$ and $Φ_{J_{0}} (σ_{-}) = - 1 / 6$ . On $σ_{+}$ , the ordered velocities are $(\partial_{2}, \partial_{0}, \partial_{3})$ with the same Gram determinant $- 1$ and density $1$ ; now $(\partial_{1}, \partial_{2}, \partial_{0}, \partial_{3})$ is positively oriented, so $ν_{+}^{*} = + \partial_{1}$ and $ε g (J_{0}, ν_{+}^{*}) = 1$ . Thus $σ_{+}^{*} (ι_{J_{0}} {v o l}_{g}) = d t_{1} \land d t_{2} \land d t_{3}$ and $Φ_{J_{0}} (σ_{+}) = 1 / 6$ , since the coordinate volume of $Δ^{3}$ is $1 / 6$ . This verifies clause 4 with consistent orientations and the induced area densities.

Metric density, volume form and current flux of the flat metric in the identity chart

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources