LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05

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.

Commuting independent vector fields give a coordinate system

Statement

Let $X_{1}, \dots, X_{k}$ be smooth vector fields on an $n$ -manifold $M$ , defined near $p$ , pointwise linearly independent there, and satisfying $[X_{i}, X_{j}] = 0$ for all $i, j$ . Then there are local coordinates $(x^{1}, \dots, x^{n})$ near $p$ such that

$X_{i} = \frac{\partial}{\partial x^{i}} (1 \leq i \leq k) .$

Facts & Assumptions

Given: Commuting smooth vector fields $X_{1}, \dots, X_{k}$ near $p$ that are linearly independent at $p$ .

[A1]

Choose a local submanifold $S$ through $p$ transverse to the span of the $X_{i}$ .

Proof

technique · direct

1.1

Let $Φ^{i}$ be the local flow of $X_{i}$ . Because the fields commute, their [given] local flows commute pairwise. Define $F (t_{1}, \dots, t_{k}, s) : = Φ_{t_{1}}^{1} \circ \dots \circ Φ_{t_{k}}^{k} (s)$ for $(t, s)$ near $(0, p)$ with $s \in S$ . This map is smooth.

givenconstruct

1.2

The differential of $F$ at $(0, p)$ sends the coordinate vector [given] $\partial_{t_{i}}$ to $X_{i} (p)$ and the tangent space of $S$ identically into a complement of their span. Hence $d F_{(0, p)}$ is an isomorphism. By the inverse function theorem, after shrinking domains, $F$ is a local diffeomorphism.

given

2.1

In the resulting coordinates, changing only $t_{i}$ applies the $X_{i}$ -flow, [given] so the pushforward of $\partial_{t_{i}}$ is exactly $X_{i}$ . Renaming the source coordinates as $(x^{1}, \dots, x^{n})$ gives the desired chart.

given∎

Depends on

Used by

Frobenius local coordinate theorem Theorem

Dependency tree · two levels

14 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

Will J. Merry, Differential Geometry (standard reference, not scraped)