LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Jacobian identity for a specified smooth diffeomorphic flow

Statement

Let $n \geq 1$ , let $I \subseteq R$ be an open interval containing $0$ , and let $U \subseteq R^{n}$ be open. Suppose $χ : I \times U \to R^{n}$ is jointly $C^{2}$ , each $χ_{t} (a) : = χ (t, a)$ is a $C^{2}$ diffeomorphism from $U$ onto an open set $U_{t}$ , and $χ_{0} (a) = a$ . Let $D : = {(t, x) : t \in I, x \in U_{t}}$ be open and let $b : D \to R^{n}$ be $C^{1}$ with $\partial_{t} χ (t, a) = b (t, χ (t, a))$ . Define $F (t, a) : = D_{a} χ (t, a)$ , $J (t, a) : = \det F (t, a)$ , and $div b : = \sum_{i = 1}^{n} \partial_{x_{i}} b_{i}$ . Then

$\partial_{t} F = (D_{x} b) (t, χ) F, \partial_{t} J = J (div b) (t, χ), J (0, a) = 1.$

In particular $J (t, a) > 0$ for all $(t, a) \in I \times U$ , and if $div b = 0$ on $D$ , then $J (t, a) = 1$ . The same identities hold on the flat torus $T^{n} : = R^{n} / Λ$ , where $Λ = Z ℓ_{1} + \dots + Z ℓ_{n}$ for a linearly independent basis $ℓ_{1}, \dots, ℓ_{n}$ and the smooth structure and Euclidean metric descend from $R^{n}$ . In that clause, let $χ : I \times T^{n} \to T^{n}$ be jointly $C^{2}$ , with each $χ_{t}$ a diffeomorphism and $χ_{0} = id$ . Let $π : T T^{n} \to T^{n}$ be the tangent-bundle projection, and let $b : I \times T^{n} \to T T^{n}$ have $C^{1}$ chart coefficients and satisfy $π (b (t, a)) = a$ and $\partial_{t} χ (t, a) = b (t, χ (t, a))$ . In every translation chart write $b = \sum_{i} b^{i} \partial_{x^{i}}$ and define $div b : = \sum_{i} \partial_{x^{i}} b^{i}$ . Define $F (t, a)$ to be the matrix of $D_{a} χ_{t} : T_{a} T^{n} \to T_{χ_{t} (a)} T^{n}$ in the translation frames and $J (t, a) : = \det F (t, a)$ . Translation-chart changes have derivative $I$ , so these matrices, determinants and divergences agree on overlaps. These are identities for supplied flow data; no existence or global-flow theorem is asserted.

Facts & Assumptions

Given: The interval $I$ , open set $U$ , jointly $C^{2}$ family $χ$ , diffeomorphism and initial-identity hypotheses, and $C^{1}$ velocity field $b$ in the Statement.

[F1]

Clairaut--Schwarz theorem for continuous second partial derivatives: the two mixed second partial derivatives of a $C^{2}$ scalar function on an open Euclidean set agree.

[F2]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : for totally differentiable maps, the derivative of a composite is the composite of the derivatives.

[F3]

The derivative of the determinant along an invertible C¹ matrix curve: $(\det A)^{'} = \det A tr (A^{- 1} A^{'})$ : if $A (t)$ is a differentiable invertible real square-matrix curve, then $(\det A)^{'} = \det A tr (A^{- 1} A^{'})$ .

[F4]

For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ : for matching finite real square matrices, $tr (A B) = tr (B A)$ .

[F5]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : a function continuous on a closed interval and differentiable on its interior has an interior point where its derivative equals the interval's average slope.

[F6]

Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ : a continuous real function on a closed interval takes every value between its endpoint values.

Proof

1.1givenF1F2algebra

For each component $χ_{i}$ , joint $C^{2}$ regularity and [F1] give $\partial_{t} \partial_{a_{j}} χ_{i} = \partial_{a_{j}} \partial_{t} χ_{i}$ . Differentiating the given velocity equation in $a$ and applying [F2] yields $\partial_{t} F = L F$ , where $L (t, a) : = (D_{x} b) (t, χ (t, a))$ .

2.1givenF2F3step 1.1

Each $F (t, a)$ is invertible: differentiating $χ_{t}^{- 1} \circ χ_{t} = id$ by [F2] gives $D χ_{t}^{- 1} (χ_{t} (a)) F (t, a) = I$ . Thus [F3] applies to the $C^{1}$ matrix curve $t \mapsto F (t, a)$ and gives $\partial_{t} J = J tr (F^{- 1} L F)$ .

3.1F4step 1.1step 2.1algebra

By [F4], $tr (F^{- 1} L F) = tr (F F^{- 1} L) = tr L = \sum_{i} \partial_{x_{i}} b_{i} (t, χ (t, a))$ . Also $F (0, a) = I$ , so $J (0, a) = 1$ .

4.1givenF6step 2.1step 3.1

The determinant $J (t, a)$ is continuous and nonzero on $I$ by step 2.1. If it were negative for some $t$ , [F6] on the closed segment with endpoints $0$ and $t$ would give a point where $J = 0$ , contradicting invertibility. Hence $J > 0$ .

4.2givenF5step 3.1algebra

If $div b = 0$ , step 3.1 gives $\partial_{t} J = 0$ . For each fixed $a$ , the case $t = 0$ is already $J (0, a) = 1$ . For $t \neq 0$ , apply [F5] to $J (\cdot, a)$ on $[\min (0, t), \max (0, t)]$ , whose endpoints are distinct; since its derivative is zero, its endpoint difference is zero, so $J (t, a) = J (0, a) = 1$ .

5.1givenstep 1.1step 2.1step 3.1step 4.1step 4.2∎

For the torus clause, fix $a \in T^{n}$ and $t_{0} \in I$ . By continuity, choose a time neighborhood of $t_{0}$ on which $a$ and $χ_{t} (a)$ stay in translation charts. Their transition maps are translations, so the coordinate matrices of $D_{a} χ_{t}$ , their determinants, and the coordinate divergence of $b$ agree on overlaps. In these charts the Euclidean calculations in steps 1.1–3.1 prove both differential identities, and $χ_{0} = id$ gives $J (0, a) = 1$ . Since $t_{0}$ was arbitrary, the identities hold throughout $I$ ; applying steps 4.1 and 4.2 on the closed segment between $0$ and any $t \in I$ gives positivity and the divergence-free conclusion.

Remarks

The hypotheses describe an already supplied family of diffeomorphisms and its velocity field. This lemma does not prove that an ODE generates such a family, that a trajectory is global, or that any physical fluid or Hamiltonian model satisfies the hypotheses.

Jacobian identity for a specified smooth diffeomorphic flow

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources