Pipeline-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.

✓ 12 results · all verified · 11 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Exterior Derivative and Cartan Calculus — Examples

1 · Prerequisites

2 · Summary

This draft page develops the exterior derivative intrinsically, its Cartan-calculus identities, and the Pfaffian Frobenius criterion. Its examples record coordinate calculations and the direct angular-period obstruction.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-09-06Open item page →

Exterior derivatives of coordinate one-forms

Statement

On a coordinate domain, $d x^{i} = d x^{i}$ and $d (d x^{i}) = 0$ .

Facts & Assumptions

Given: The manifolds, forms, vector fields, maps, and coordinates explicitly named in the statement.

[F1]

The preceding result states that On a chart, if $ω = \sum_{I} ω_{I} d x^{I}$ , then $d ω = \sum_{I} d ω_{I} \land d x^{I} .$ (The local coordinate formula for the exterior derivative).

Verification

technique · direct

1.1F1given

The coordinate formula applied to the function $x^{i}$ gives $d x^{i} = d x^{i}$ .

2.1F1step 1.1∎

Applying the same coordinate formula to $d x^{i} = 1 d x^{i}$ gives $d (d x^{i}) = d (1) \land d x^{i} = 0$ .

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

The Euclidean area form is closed

Statement

On $R^{2}$ , the area form $d x \land d y$ is closed.

Facts & Assumptions

Given: The manifolds, forms, vector fields, maps, and coordinates explicitly named in the statement.

[F1]

The preceding result states that On a chart, if $ω = \sum_{I} ω_{I} d x^{I}$ , then $d ω = \sum_{I} d ω_{I} \land d x^{I} .$ (The local coordinate formula for the exterior derivative).

Verification

technique · direct

1.1F1given

The coordinate formula gives $d (d x \land d y) = d (1) \land d x \land d y$ .

2.1step 1.1∎

Because $d (1) = 0$ , the area form is closed.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

The angular one-form on the punctured plane is closed

Statement

On $R^{2} ∖ {0}$ , the angular form $ω = (- y d x + x d y) / (x^{2} + y^{2})$ is closed.

Facts & Assumptions

Given: The manifolds, forms, vector fields, maps, and coordinates explicitly named in the statement.

[F1]

The preceding result states that On a chart, if $ω = \sum_{I} ω_{I} d x^{I}$ , then $d ω = \sum_{I} d ω_{I} \land d x^{I} .$ (The local coordinate formula for the exterior derivative).

Verification

technique · direct

1.1F1given

Write $r^{2} = x^{2} + y^{2}$ . Differentiating $- y / r^{2}$ and $x / r^{2}$ gives the coefficient $\partial_{x} (x / r^{2}) - \partial_{y} (- y / r^{2}) = 0$ .

2.1step 1.1∎

The coordinate formula therefore gives $d ω = 0$ on the punctured plane.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

The angular one-form has no global potential

Statement

The angular form has local primitives $atan2 (y, x)$ on angular charts and no global potential on $R^{2} ∖ {0}$ .

Facts & Assumptions

Given: The manifolds, forms, vector fields, maps, and coordinates explicitly named in the statement.

[F1]

The form under consideration is $ω = (- y d x + x d y) / (x^{2} + y^{2})$ on $R^{2} ∖ {0}$ (The angular one-form on the punctured plane is closed).

Verification

technique · direct

1.1F1given

On any angular chart avoiding a ray, a smooth branch $θ$ of the angle satisfies $d θ = (- y d x + x d y) / (x^{2} + y^{2})$ .

2.1step 1.1∎

If $d F = ω$ globally, then along $γ (t) = (\cos t, \sin t)$ one has $(F \circ γ)^{'} = ω (γ^{'}) = 1$ . Thus $0 = F (γ (2 π)) - F (γ (0)) = 2 π$ , a contradiction; so the local primitives cannot patch globally.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Curl and divergence encoded by the exterior derivative

Statement

For $P, Q, R, A, B, C \in C^{\infty} (R^{3})$ , $d (P d x + Q d y + R d z)$ has the usual curl coefficients, and $d (A d y \land d z + B d z \land d x + C d x \land d y) = (\partial_{x} A + \partial_{y} B + \partial_{z} C) d x \land d y \land d z .$

Facts & Assumptions

Given: The manifolds, forms, vector fields, maps, and coordinates explicitly named in the statement.

[F1]

The preceding result states that On a chart, if $ω = \sum_{I} ω_{I} d x^{I}$ , then $d ω = \sum_{I} d ω_{I} \land d x^{I} .$ (The local coordinate formula for the exterior derivative).

Verification

technique · direct

1.1F1given

Apply the coordinate formula to $P d x + Q d y + R d z$ and collect the $d y \land d z$ , $d z \land d x$ , and $d x \land d y$ coefficients.

2.1step 1.1∎

Applying it to $A d y \land d z + B d z \land d x + C d x \land d y$ leaves the coefficient $\partial_{x} A + \partial_{y} B + \partial_{z} C$ of $d x \land d y \land d z$ .

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Lie derivative of the Euclidean metric under dilations

Statement

For $X = x \partial_{x} + y \partial_{y}$ and $g = d x^{2} + d y^{2}$ on $R^{2}$ , $L_{X} g = 2 g$ .

Facts & Assumptions

Given: The manifolds, forms, vector fields, maps, and coordinates explicitly named in the statement.

[F1]

The preceding result states that For a covariant $k$ -tensor $T = T_{i_{1} \dots i_{k}} d x^{i_{1}} \otimes \dots \otimes d x^{i_{k}}$ , $(L_{X} T)_{i_{1} \dots i_{k}} = X^{j} \partial_{j} T_{i_{1} \dots i_{k}} + \sum_{a} (\partial_{i_{a}} X^{j}) T_{i_{1} \dots j \dots i_{k}} .$ (The coordinate formula for the Lie derivative of a covariant tensor).

Verification

technique · direct

1.1F1given

The coefficients of $g$ are constant and $\partial_{i} X^{j} = δ_{i}^{j}$ .

2.1step 1.1∎

The covariant tensor formula therefore adds two copies of each metric component, giving $L_{X} g = 2 g$ .

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Lie derivative of an area form and planar divergence

Statement

For $X = P \partial_{x} + Q \partial_{y}$ on $R^{2}$ , $L_{X} (d x \land d y) = (\partial_{x} P + \partial_{y} Q) d x \land d y$ .

Facts & Assumptions

Given: The manifolds, forms, vector fields, maps, and coordinates explicitly named in the statement.

[F1]

The preceding result states that For every vector field $X$ and differential form $ω$ , $L_{X} ω = d (ι_{X} ω) + ι_{X} (d ω) .$ (Cartan's magic formula).

Verification

technique · direct

1.1F1given

Cartan's formula gives $L_{X} (d x \land d y) = d (P d y - Q d x)$ because the area form is closed.

2.1step 1.1∎

Differentiating yields $(\partial_{x} P + \partial_{y} Q) d x \land d y$ .

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Cartan's formula for a coordinate vector field

Statement

For $X = \partial_{x^{1}}$ and $ω = \sum_{I} a_{I} d x^{I}$ on a coordinate chart, both sides of Cartan's formula equal $\sum_{I} (\partial_{x^{1}} a_{I}) d x^{I}$ .

Facts & Assumptions

Given: The manifolds, forms, vector fields, maps, and coordinates explicitly named in the statement.

[F1]

The preceding result states that For every vector field $X$ and differential form $ω$ , $L_{X} ω = d (ι_{X} ω) + ι_{X} (d ω) .$ (Cartan's magic formula).

Verification

technique · direct

1.1F1given

For $ω = \sum_{I} a_{I} d x^{I}$ , contraction and the coordinate formula give $d ι_{X} ω + ι_{X} d ω = \sum_{I} (\partial_{x^{1}} a_{I}) d x^{I}$ .

2.1step 1.1∎

This is also the coefficientwise Lie derivative under the translation flow of $\partial_{x^{1}}$ .

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

A contact form on three-space

Statement

For $α = d z - x d y$ on $R^{3}$ , $α \land d α = - d x \land d y \land d z \neq 0$ , so $\ker α$ is not integrable.

Facts & Assumptions

Given: The manifolds, forms, vector fields, maps, and coordinates explicitly named in the statement.

[F1]

The preceding result states that For a nowhere-zero one-form $α$ , the hyperplane distribution $\ker α$ is integrable if and only if $α \land d α = 0$ . (The codimension-one Frobenius criterion).

Verification

technique · direct

1.1F1given

For $α = d z - x d y$ , $d α = - d x \land d y$ .

2.1step 1.1∎

Thus $α \land d α = - d x \land d y \land d z \neq 0$ , and the codimension-one criterion says $\ker α$ is not integrable.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

An integrable Pfaffian equation with a local first integral

Statement

On $R^{2}$ , the nowhere-zero form $α = d y$ defines the integrable Pfaffian equation $d y = 0$ , with first integral $y$ .

Facts & Assumptions

Given: The manifolds, forms, vector fields, maps, and coordinates explicitly named in the statement.

[F1]

The preceding result states that If $θ^{1}, \dots, θ^{n - k}$ locally frame $D^{\circ}$ , then $D$ is involutive if and only if $d θ^{a} = \sum_{b} η_{b}^{a} \land θ^{b}$ locally for every $a$ ; equivalently, its annihilator ideal is differential. (The Pfaffian Frobenius criterion).

Verification

technique · direct

1.1F1given

The form $d y$ is nowhere zero and $d (d y) = 0$ , so it satisfies the Pfaffian criterion.

2.1step 1.1∎

Its kernel consists of vectors tangent to the lines $y = c o n s t a n t$ , and $y$ is the displayed local first integral.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

A nonproper pullback destroys compact support

Statement

There are a compactly supported form $ω$ and a nonproper smooth map $F$ for which $F^{*} ω$ has noncompact support.

Facts & Assumptions

Given: The manifolds, forms, vector fields, maps, and coordinates explicitly named in the statement.

Counterexample

technique · direct

1.1given

Let $ρ \in C_{c}^{\infty} (R)$ satisfy $ρ (0) = 1$ and take the constant nonproper map $F : R \to R$ , $F (t) = 0$ .

2.1step 1.1∎

Then $F^{*} ρ = 1$ has support $R$ , which is noncompact despite $ρ$ having compact support.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Time-dependent pullback differentiation for a translation

Statement

For $X_{t} = \partial_{x}$ , $Φ_{t, s} (x) = x + t - s$ , and $ω_{t} = t d x$ , the time-dependent pullback identity holds.

Facts & Assumptions

Given: The manifolds, forms, vector fields, maps, and coordinates explicitly named in the statement.

[F1]

The preceding result states that If $Φ_{t, s}$ is the local evolution of $X_{t}$ and $ω_{t}$ is a smooth time-dependent form, then $\frac{d}{d t} Φ_{t, s}^{*} ω_{t} = Φ_{t, s}^{*} ({\dot{ω}}_{t} + L_{X_{t}} ω_{t}) .$ (Differentiation of a pulled-back form along a time-dependent flow).

Verification

technique · direct

1.1F1given

Here $Φ_{t, s}^{*} (t d x) = t d x$ , so the left side is $d x$ .

2.1step 1.1∎

Since ${\dot{ω}}_{t} = d x$ and $L_{\partial_{x}} (t d x) = 0$ , the right side is also $d x$ .

Sources

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