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 scalar field with null-or-zero gradient in flat space: equation of motion and conservation

Example

Let $M = R^{4}$ carry the identity chart, the flat metric $g = diag (- 1, 1, 1, 1)$ and the chart orientation, with metric-selected connection $\nabla$ (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model, Metric compatibility, torsion freedom and the metric-selected connection class, Oriented smooth manifolds and oriented charts). Let $f : R \to R$ be a smooth function, let

$φ (x) : = f (x^{0} + x^{1}),$

and let $(φ, V, K)$ be the scalar-field matter model with $V \equiv 0$ and $K > 0$ (The scalar-field matter model of the classical gravitational framework). Then:

$\partial^{c} φ \partial_{c} φ = 0$ : the metric dual of $d φ$ is null wherever $d φ \neq 0$ and is zero wherever $d φ = 0$ .
$□_{g} φ = \nabla^{a} \partial_{a} φ = 0$ : $φ$ satisfies the scalar equation of motion, and its stress-energy tensor is $T_{a b} = K \partial_{a} φ \partial_{b} φ$ .
$\nabla^{a} T_{a b} = 0$ : the tensor is divergence-free, and $T (v, v) = K (\partial_{a} φ v^{a})^{2} \geq 0$ for every $v \in T_{p} M$ , with equality exactly on the kernel $\partial_{a} φ v^{a} = 0$ ; this is a hyperplane where $d φ \neq 0$ and the full tangent space where $d φ = 0$ .

Facts & Assumptions

Given: The flat Lorentzian four-manifold $(R^{4}, g)$ with identity chart and $g = diag (- 1, 1, 1, 1)$ ; the smooth function $φ = f (x^{0} + x^{1})$ ; and the scalar-field matter model $(φ, V, K)$ with $V \equiv 0$ , $K > 0$ .

[L1]

For the flat metric in the identity chart, the inverse-metric components are $diag (- 1, 1, 1, 1)$ and $□_{g} φ = g^{a b} \partial_{a} \partial_{b} φ = - \partial_{0}^{2} φ + \partial_{1}^{2} φ + \partial_{2}^{2} φ + \partial_{3}^{2} φ$ (The inverse metric, musical isomorphisms and index raising, Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields).

[L2]

The scalar-field model has equation of motion $□_{g} φ - V^{'} (φ) = 0$ and candidate tensor $T_{a b} = K [\partial_{a} φ \partial_{b} φ - g_{a b} (\frac{1}{2} \partial^{c} φ \partial_{c} φ + V (φ))]$ ; it satisfies $\nabla^{a} T_{a b} = K (□_{g} φ - V^{'} (φ)) \partial_{b} φ$ (The scalar-field matter model of the classical gravitational framework, First variation, Hilbert tensor and conservation of the scalar-field model clause (c)).

[L3]

For a smooth function of $u = x^{0} + x^{1}$ , the chain rule gives $\partial_{0} φ = \partial_{1} φ = f^{'} (u)$ and $\partial_{2} φ = \partial_{3} φ = 0$ ( $C^{r}$ and smooth maps between smooth manifolds).

Verification

technique · direct; apply the chain rule and evaluate the flat-space expressions

1.1L1L3algebra

(Null or zero gradient.) By [L3], $\partial_{a} φ = (f^{'} (u), f^{'} (u), 0, 0)$ in the identity chart. By [L1], $\partial^{a} φ \partial_{a} φ = g^{a b} \partial_{a} φ \partial_{b} φ = - (f^{'})^{2} + (f^{'})^{2} + 0 + 0 = 0$ . Thus the metric dual of $d φ$ is null where $f^{'} (u) \neq 0$ and is the zero vector where $f^{'} (u) = 0$ .

2.1step 1.1L1L2L3algebra

(Equation of motion.) Again by [L3], $\partial_{0}^{2} φ = f^{''} (u)$ and $\partial_{1}^{2} φ = f^{''} (u)$ , while $\partial_{2}^{2} φ = \partial_{3}^{2} φ = 0$ ; hence $□_{g} φ = - f^{''} + f^{''} = 0$ . Since $V \equiv 0$ , the scalar equation $□_{g} φ = V^{'} (φ) = 0$ holds. Using step 1.1 in the tensor formula of [L2], the metric bracket vanishes and $T_{a b} = K \partial_{a} φ \partial_{b} φ$ .

3.1step 2.1L2algebra∎

(Conservation and positivity.) By the conservation identity of [L2] and step 2.1, $\nabla^{a} T_{a b} = K \cdot 0 \cdot \partial_{b} φ = 0$ . For any $v \in T_{p} M$ , $T (v, v) = K \partial_{a} φ \partial_{b} φ v^{a} v^{b} = K (\partial_{a} φ v^{a})^{2} \geq 0$ because $K > 0$ and the square is nonnegative; equality holds exactly when the linear functional $\partial_{a} φ v^{a}$ vanishes, i.e. on its kernel ${v : \partial_{a} φ v^{a} = 0}$ , a hyperplane at nonzero gradient and the whole tangent space at zero gradient, containing the gradient direction itself. This completes the verification.

Remarks

Reading. The example is the flat-space plane-wave branch of the scalar model: the kinetic bracket vanishes identically on a null gradient, so the stress-energy tensor is a nonnegative tensor of rank at most one, with rank one wherever the gradient is nonzero. It illustrates the conservation identity of the proposition without any physical claim about the model's realization.

A scalar field with null-or-zero gradient in flat space: equation of motion and conservation

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources