ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated

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.

Transport of a translating rigid region: the rate integral vanishes for a travelling profile

Example

Assume ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )) for the actual Lebesgue transport and change-of-variables suppliers.

Let $B : = B_{1} (0) \subseteq R^{3}$ be the open unit ball (Open ball, closed ball and sphere in a metric space), a nonempty bounded open set and hence a material region in the sense of Material regions, densities and their mass; let $v \in R^{3}$ be fixed, and let

$ψ (t, X) : = X + t v (t \in R, X \in R^{3})$

be the uniform translation motion of Continuum motions, spatial velocity, material acceleration and swept regions (each $ψ_{t}$ is the identity plus a translation, a $C^{\infty}$ diffeomorphism with $D_{X} ψ_{t} = I_{3}$ ). Let $h : R^{3} \to R$ be $C^{1}$ ( $C^{k}$ Euclidean maps and diffeomorphisms) and define the travelling profile

$f (t, x) : = h (x - t v) ((t, x) \in R \times R^{3}) .$

Then $\int_{ψ_{t} (B)} f (t, x) d x$ is independent of $t$ , while the transport integrand vanishes pointwise:

$\partial_{t} f + div (f v) = 0,$

so the transport theorem reproduces the constant rate $0$ .

Facts & Assumptions

Given: Countable choice. The unit ball $B$ , the velocity $v$ , the motion $ψ (t, X) = X + t v$ , the $C^{1}$ profile $h$ and $f (t, x) = h (x - t v)$ .

[L1]

Transport theorem: for the motion $ψ$ with spatial velocity $w$ and a $C^{1}$ $f$ on a neighbourhood of the swept compact region, $\frac{d}{d t} \int_{ψ_{t} (B)} f = \int_{ψ_{t} (B)} (\partial_{t} f + div (f w))$ ; here $w (t, ψ (t, X)) = \partial_{t} ψ (t, X) = v$ , so $w \equiv v$ (The transport theorem for a $C^{2}$ family of diffeomorphisms: $\frac{d}{d t} \int_{ψ_{t} (B)} f = \int_{ψ_{t} (B)} (\partial_{t} f + div (f w))$ , Continuum motions, spatial velocity, material acceleration and swept regions).

[L2]

Change of variables: for the translation $ψ_{t}$ (a $C^{1}$ diffeomorphism with $∣ \det D ψ_{t} ∣ = 1$ ), $\int_{ψ_{t} (B)} f (t, x) d x = \int_{B} f (t, X + t v) d X = \int_{B} h (X) d X$ (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions, The Axiom of Countable Choice ( ${A C}_{ω}$ ), Integral over a measurable subset).

[L3]

The affine map $A (t, x) : = x - t v$ has total derivative $D A (t, x) (τ, z) = z - τ v$ , directly from its exact increment. Since $h$ is $C^{1}$ , The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ gives $f = h \circ A$ of class $C^{1}$ and $D f (t, x) (τ, z) = D h (x - t v) (z - τ v)$ . Derivatives: $\partial_{t} f (t, x) = - D h (x - t v) v$ and $\nabla f (t, x) = (\nabla h) (x - t v)$ , hence $\partial_{t} f + ⟨ \nabla f, v ⟩_{2} = 0$ ; moreover $div (f v) = ⟨ \nabla f, v ⟩_{2} + f div v = ⟨ \nabla f, v ⟩_{2}$ because $v$ is constant (Euclidean spatial calculus: gradient, divergence and material derivative, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , A total derivative computes every directional derivative, and its matrix is the Jacobian, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The Lebesgue integral is linear on $L^{1} (μ)$ ).

Verification

technique · direct; evaluate both sides of the transport identity for the explicit translating flow

1.1givenL2algebra

By [L2], $\int_{ψ_{t} (B)} f (t, x) d x = \int_{B} h (X) d X$ for every $t$ ; the right-hand side does not depend on $t$ , so the derivative is $0$ .

1.2givenL3algebra

By [L3], $\partial_{t} f + div (f v) = (\partial_{t} f + ⟨ \nabla f, v ⟩_{2}) + f div v = 0$ , and the same conclusion holds for every point of the swept region.

2.1step 1.1step 1.2L1algebra∎

The transport theorem [L1] gives $\frac{d}{d t} \int_{ψ_{t} (B)} f = \int_{ψ_{t} (B)} (\partial_{t} f + div (f v)) = 0$ , in agreement with step 1.1: both computations produce the constant rate.

Remarks

This example verifies the transport identity on a flow with constant velocity and non-constant density-like profile; it exercises the change-of-variables and material-derivative pieces without any physical claim.

Depends on

Dependency tree · 2 levels

Sources

R. Abeyaratne, Continuum Mechanics, Volume II of Lecture Notes on the Mechanics of Solids (MIT, 1988, revised 2020), Sections 3.7, 4.2 and 4.4 (transport equations; mass and momentum balance in integral form)