LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Moser pullback differentiation equation

Statement

Assume ${A C}_{ω}$ . If $ϕ_{t} = Φ_{t, 0}$ is the evolution of a smooth time-dependent vector field $X_{t}$ and $ω_{t}$ is a smooth family of forms, then

$\frac{d}{d t} (ϕ_{t}^{*} ω_{t}) = ϕ_{t}^{*} ({\dot{ω}}_{t} + L_{X_{t}} ω_{t}) .$

If the $ω_{t}$ are closed two-forms and $σ_{t}$ is a smooth family of one-forms satisfying ${\dot{ω}}_{t} = d σ_{t}$ , then any solution of $ι_{X_{t}} ω_{t} = - σ_{t}$ satisfies $\frac{d}{d t} (ϕ_{t}^{*} ω_{t}) = 0$ . When $ω_{t}$ is nondegenerate, that contraction equation has a unique smooth solution $X_{t}$ .

Facts & Assumptions

Given: ${A C}_{ω}$ , a smooth family $ω_{t}$ , a smooth family $σ_{t}$ when the second assertion is used, and a local evolution $ϕ_{t}$ generated by $X_{t}$ .

[F1]

Differentiation along a time-dependent evolution gives the displayed pullback derivative. The supplier's definition of such fields assumes ${A C}_{ω}$ . Differentiation of a pulled-back form along a time-dependent flow.

[F2]

Cartan's formula is $L_{X} η = d (ι_{X} η) + ι_{X} d η$ . Cartan's magic formula.

Proof

technique · direct

1.1

The first formula is [F1] with initial time zero. If $d ω_{t} = 0$ , [F2] turns its parenthesis into $d σ_{t} + d (ι_{X_{t}} ω_{t})$ . Thus the Moser equation $ι_{X_{t}} ω_{t} = - σ_{t}$ makes the derivative zero.

F1F2givenalgebra

2.1

For nondegenerate $ω_{t}$ , the smooth bundle map $ω_{t}^{♭} : T M \to T^{*} M$ is invertible, so the unique solution is $X_{t} = - (ω_{t}^{♭})^{- 1} σ_{t}$ . Matrix inversion in local coordinates proves joint smoothness in $(t, p)$ .

step 1.1givenalgebra∎

Depends on

Used by

Compact-support Moser stability on a noncompact manifold Theorem
Moser stability theorem Theorem
Relative Moser theorem Theorem
Symplectic neighborhood theorem Theorem

Dependency tree · two levels

17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Ana Cannas da Silva, Lectures on Symplectic Geometry (standard reference, not scraped)