TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-06

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.

The local coordinate formula for the exterior derivative

Statement

Let $(U, x^{1}, \dots, x^{n})$ be a smooth chart on a smooth manifold and $ω$ a smooth $k$ -form on $U$ , with $k \geq 0$ . Summing over increasing $k$ -tuples $I$ , and writing $d x^{I} = d x^{i_{1}} \land \dots \land d x^{i_{k}}$ , if $ω = \sum_{I} ω_{I} d x^{I}$ , then $d ω = \sum_{I} d ω_{I} \land d x^{I} .$

Facts & Assumptions

Given: The chart and smooth form in the statement; for k=0 the empty wedge is 1.

[F2]

The exterior derivative is given by the invariant vector-field formula (The exterior derivative by the invariant vector-field formula).

[F3]

Coordinate vector fields commute (Coordinate vector fields commute).

[F4]

The increasing coordinate wedges give a unique expansion of each smooth differential form (Local coordinate expression for a differential form).

Proof

technique · direct

1.1F2F3F4given

Evaluate the invariant formula on coordinate vector fields. By [F3] their brackets vanish. On an increasing $(k + 1)$ -tuple $J = (j_{0}, \dots, j_{k})$ the resulting value is $\sum_{a = 0}^{k} (- 1)^{a} \partial_{j_{a}} ω_{J ∖ j_{a}}$ .

2.1F2F4step 1.1algebra∎

For a function $f$ , [F2] in degree zero gives $d f (\partial_{j}) = \partial_{j} f$ , hence $d f = \sum_{j} \partial_{j} f d x^{j}$ . Evaluating $\sum_{I} d ω_{I} \land d x^{I}$ on $J$ gives exactly the alternating sum in step 1.1. Uniqueness in [F4] proves the formula. For $k \geq n$ both sides vanish in degree $k + 1$ ; for $k = 0$ it is the function formula just established.

Depends on

Dependency tree · 2 levels

Sources

John M. Lee, Introduction to Smooth Manifolds, 2nd ed.