TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10

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.

Poincare lemma for differential forms on star shaped domains

Statement

Every closed smooth $k$ -form on a star-shaped open domain is exact for $k \geq 1$ . For centre $0$ , one primitive is $η_{x} (v_{1}, \dots, v_{k - 1}) = \int_{0}^{1} t^{k - 1} ω_{t x} (x, v_{1}, \dots, v_{k - 1}) d t$ .

Facts & Assumptions

Given: A domain $U$ star-shaped about $c$ , and a closed $k$ -form $ω$ with $k \geq 1$ .

[F1]

Radial contraction of a star shaped domain: For an open $U \subseteq R^{n}$ star-shaped about a specified $c \in U$ , the radial contraction is $F : U \times [0, 1] \to U$ , $F (x, t) = c + t (x - c)$ . def-star-shaped-open-subset-of-rn says exactly that each displayed value lies in $U$ . The coordinate expression is polynomial, so its restriction is smooth up to both endpoints; $F (x, 0) = c$ and $F (x, 1) = x$ . The centre is part of the data, so $U$ is nonempty. For $n = 0$ the unique nonempty domain is a point and the formula is constant.

[F2]

De rham homotopy formula for a smooth homotopy: If $F : M \times [0, 1] \to N$ is smooth up to the endpoints and $F_{t} (x) = F (x, t)$ , then $F_{1}^{*} - F_{0}^{*} = d (K F^{*}) + (K F^{*}) d$ .

Proof

technique · direct

1.1F1F2given

Take the radial homotopy from the constant map to the identity. Its time-zero pullback on positive-degree forms vanishes because the differential of the constant map is zero. The homotopy formula and $d ω = 0$ give $ω = d (K F^{*} ω)$ , so $η = K F^{*} ω$ is a smooth primitive.

2.1F2step 1.1∎

For $c = 0$ , $d F_{(x, t)} \partial_{t} = x$ and $d F_{(x, t)} (v, 0) = t v$ . The contraction coefficient therefore equals $t^{k - 1} ω_{t x} (x, v_{1}, \dots, v_{k - 1})$ . Integrating gives the displayed formula. When $k = 1$ the factor is $1$ , including $t = 0$ ; for $k > 1$ the integrand is smooth and vanishes there. Degrees exceeding the dimension have zero form and zero primitive.

Source locator

Lee, Theorem 17.14, p.447; the explicit primitive follows by evaluating the interval operator.

Poincare lemma for differential forms on star shaped domains

Statement

Facts & Assumptions

Proof

Source locator

Depends on

Dependency tree · 2 levels

Sources