[proofplan] Translating coordinates, we may assume $U$ is star-shaped with respect to the origin. The straight-line contraction $F: [0,1] \times U \to U$, $(t,x) \mapsto tx$, is a smooth homotopy from the constant map at $0$ (recovered at $t=0$) to the identity (recovered at $t=1$). Pulling $\omega$ back along $F$ and isolating its $dt$-component produces a $(k-1)$-form on $U$ for each $t$; integrating in $t$ defines a chain-homotopy operator $H: \Omega^k(U) \to \Omega^{k-1}(U)$ satisfying $dH + Hd = \mathrm{id}$ on $\Omega^k(U)$ for $k \ge 1$. The identity $dH + Hd = \mathrm{id}$ is verified by decomposing $F^*\omega$ into its purely-spatial and $dt$-containing parts, computing $d_{[0,1]\times U}$ on each, and applying the [Fundamental Theorem of Calculus](/theorems/632) in $t$ together with the [Leibniz Integral Rule](/theorems/831) to interchange spatial $d$ with $\int_0^1$. Closedness of $\omega$ then forces $\omega = d(H\omega)$, so $\eta := H\omega$ is the desired primitive. [/proofplan]

[step:Reduce to the case where $U$ is star-shaped with respect to the origin]Let $x_0 \in U$ be a star-center of $U$, so that for every $x \in U$ and every $t \in [0,1]$ the point $x_0 + t(x - x_0)$ lies in $U$. Define the translation \begin{align*} T: \mathbb{R}^n &\to \mathbb{R}^n \\ y &\mapsto y + x_0, \end{align*} and put $V := T^{-1}(U) = \{y \in \mathbb{R}^n : y + x_0 \in U\}$. Then $V$ is open, $0 \in V$, and for $y \in V$, $t \in [0,1]$ we have $ty + x_0 = x_0 + t((y + x_0) - x_0) \in U$, so $ty \in V$. Thus $V$ is star-shaped with respect to $0$. The diffeomorphism $T: V \to U$ pulls back to an isomorphism of complexes $T^*: \Omega^\bullet(U) \to \Omega^\bullet(V)$ commuting with $d$ by the [Naturality of the Pullback: Compatibility with Wedge Product and Exterior Derivative](/theorems/3574). Hence $\omega_V := T^*\omega \in \Omega^k(V)$ is closed. If we produce $\eta_V \in \Omega^{k-1}(V)$ with $d\eta_V = \omega_V$, then $\eta := (T^{-1})^* \eta_V \in \Omega^{k-1}(U)$ satisfies $d\eta = (T^{-1})^*(d\eta_V) = (T^{-1})^* T^* \omega = \omega$. For the remainder of the proof we therefore assume $0 \in U$ and $U$ is star-shaped with respect to $0$, so that \begin{align*} F: [0,1] \times U &\to U \\ (t, x) &\mapsto tx \end{align*} is well-defined and smooth.[/step]

[guided]The Poincaré lemma is a statement that does not see the location of the star-center, only its existence. To make formulas cleaner — in particular so that the contracting homotopy is simply $(t,x) \mapsto tx$ rather than $(t,x) \mapsto x_0 + t(x - x_0)$ — we first move the star-center to the origin. Translation is a diffeomorphism of $\mathbb{R}^n$, it preserves star-shapedness (translating both the center and every point by $-x_0$ moves the center to $0$ and preserves the property that every segment from $0$ to a point of $V$ lies in $V$), and the pullback $T^*$ commutes with $d$ (Theorem 3574: naturality of $d$ under smooth maps). The translation step is reversible: a primitive on $V$ pulls back through $(T^{-1})^*$ to a primitive on $U$. Concretely, if $d\eta_V = T^*\omega$, then \begin{align*} d((T^{-1})^* \eta_V) = (T^{-1})^* (d\eta_V) = (T^{-1})^* T^* \omega = (T \circ T^{-1})^* \omega = \omega. \end{align*} So nothing is lost by assuming $0$ is the star-center. Why does $F(t,x) = tx$ stay inside $U$? Because $U$ star-shaped with respect to $0$ means: for $x \in U$ and $t \in [0,1]$, the segment $\{tx : t \in [0,1]\}$ lies in $U$. That is exactly what we need for $F$ to be well-defined as a map into $U$, not just into $\mathbb{R}^n$.[/guided]

[step:Decompose $F^*\omega$ into a purely spatial part and a $dt$-part]Write \begin{align*} \omega = \sum_{\substack{I = (i_1 < \cdots < i_k) \\ 1 \le i_j \le n}} \omega_I \, dx_{i_1} \wedge \cdots \wedge dx_{i_k}, \end{align*} where the sum is over strictly increasing multi-indices $I$ of length $k$ in $\{1, \dots, n\}$ and each component $\omega_I \in C^\infty(U)$. Applying $F^*$ and using $F^* x_j = t x_j$, hence $F^*(dx_j) = d(tx_j) = x_j \, dt + t \, dx_j$, we obtain \begin{align*} F^*\omega = \sum_I \omega_I(tx) \, \bigwedge_{a=1}^k \bigl(x_{i_a}\, dt + t\, dx_{i_a}\bigr). \end{align*} Expanding the wedge product and using $dt \wedge dt = 0$, each factor contributes either $x_{i_a}\, dt$ to a single position or $t\, dx_{i_a}$, so \begin{align*} \bigwedge_{a=1}^k \bigl(x_{i_a}\, dt + t\, dx_{i_a}\bigr) = t^k\, dx_{i_1} \wedge \cdots \wedge dx_{i_k} + dt \wedge \sum_{a=1}^k (-1)^{a-1}\, t^{k-1}\, x_{i_a}\, dx_{i_1} \wedge \cdots \wedge \widehat{dx_{i_a}} \wedge \cdots \wedge dx_{i_k}, \end{align*} where the hat denotes omission of the $a$-th factor. Setting \begin{align*} \alpha(t, x) &:= t^k \sum_I \omega_I(tx) \, dx_{i_1} \wedge \cdots \wedge dx_{i_k}, \\ \beta(t, x) &:= t^{k-1} \sum_I \sum_{a=1}^k (-1)^{a-1} x_{i_a}\, \omega_I(tx) \, dx_{i_1} \wedge \cdots \wedge \widehat{dx_{i_a}} \wedge \cdots \wedge dx_{i_k}, \end{align*} we obtain the decomposition \begin{align*} F^*\omega = \alpha + dt \wedge \beta, \end{align*} where for each $t \in [0,1]$ the forms $\alpha(t, \cdot) \in \Omega^k(U)$ and $\beta(t, \cdot) \in \Omega^{k-1}(U)$ depend smoothly on $t$ and contain no $dt$.[/step]

[guided]The pullback $F^*\omega$ is a $k$-form on the $(n+1)$-dimensional manifold-with-boundary $[0,1] \times U$, so its expansion in the basis $\{dt, dx_1, \dots, dx_n\}$ has two kinds of terms: those that contain the symbol $dt$ exactly once, and those that do not contain $dt$ at all. (No term can contain $dt$ twice, because $dt \wedge dt = 0$.) Writing \begin{align*} F^*\omega = \alpha + dt \wedge \beta \end{align*} makes this split explicit: $\alpha$ collects the terms with no $dt$, and $dt \wedge \beta$ collects the rest, with $\beta$ a $(k-1)$-form in the spatial variables. To get explicit formulas, we expand $\bigwedge_a (x_{i_a} dt + t \, dx_{i_a})$. Distributing the wedge, each of the $k$ binomials contributes either the "$x_{i_a} dt$" term or the "$t\, dx_{i_a}$" term, giving $2^k$ summands a priori. But $dt \wedge dt = 0$ forces at most one factor to contribute the $dt$-term, leaving only $k+1$ surviving contributions: - All factors choose $t\, dx_{i_a}$: gives $t^k\, dx_{i_1} \wedge \cdots \wedge dx_{i_k}$. This is the $\alpha$ contribution. - Exactly one factor (the $a$-th) chooses $x_{i_a}\, dt$, all others choose $t\, dx$: gives $t^{k-1}\, x_{i_a}\, dt \wedge dx_{i_1} \wedge \cdots \widehat{dx_{i_a}} \cdots \wedge dx_{i_k}$. Pulling the $dt$ to the front through $a-1$ wedge factors introduces a sign $(-1)^{a-1}$. Collecting these gives the formulas for $\alpha$ and $\beta$ stated above. The key features for what follows: - At $t = 1$: $\alpha(1, x) = \sum_I \omega_I(x)\, dx_{i_1} \wedge \cdots \wedge dx_{i_k} = \omega$. - At $t = 0$: since $k \ge 1$, the leading factor $t^k$ vanishes, so $\alpha(0, x) = 0$. - The form $\beta$ carries the factor $t^{k-1}$, so it is smooth in $t \in [0,1]$ even at $t = 0$ (and at $t = 0$ it vanishes if $k \ge 2$, equals $\sum_a (-1)^{a-1} x_{i_a} \omega(0)\,\widehat{\cdot}$-stuff if $k = 1$ — but the value at $t = 0$ is not used). These are precisely the boundary values that will produce $\omega$ on the right-hand side of the chain-homotopy formula.[/guided]

[step:Define the chain-homotopy operator $H$ by integrating $\beta$ in $t$] Define \begin{align*} H: \Omega^k(U) &\to \Omega^{k-1}(U) \\ \omega &\mapsto \int_0^1 \beta(t, \cdot) \, d\mathcal{L}^1(t), \end{align*} where the integral is taken componentwise in the coefficient basis $\{dx_{i_1} \wedge \cdots \widehat{dx_{i_a}} \cdots \wedge dx_{i_k}\}$. Explicitly, \begin{align*} (H\omega)(x) = \sum_I \sum_{a=1}^k (-1)^{a-1} \left(\int_0^1 t^{k-1}\, \omega_I(tx) \, d\mathcal{L}^1(t)\right) x_{i_a}\, dx_{i_1} \wedge \cdots \wedge \widehat{dx_{i_a}} \wedge \cdots \wedge dx_{i_k}. \end{align*} For fixed $x \in U$ the segment $\{tx : t \in [0,1]\}$ is a compact subset of $U$, hence each $\omega_I(t \cdot)$ is smooth on $[0,1]$, and the integrand $t \mapsto t^{k-1} \omega_I(tx)$ is continuous on $[0,1]$. Smoothness of $H\omega$ in $x$ follows from the [Leibniz Integral Rule](/theorems/831): for each multi-index $\gamma$ of partial derivatives in $x$, the integrand $t^{k-1} \omega_I(tx)$ has $\partial^\gamma$ in $x$ equal to $t^{k-1 + |\gamma|} (\partial^\gamma \omega_I)(tx)$, which is jointly continuous in $(t, x)$ on $[0,1] \times K$ for any compact $K \subset U$, so differentiation in $x$ commutes with $\int_0^1 \cdots \, d\mathcal{L}^1(t)$. Therefore $H\omega \in C^\infty(U)$ and $H\omega \in \Omega^{k-1}(U)$. [/step]

[step:Express $d_{[0,1]\times U}(F^*\omega)$ in terms of $\alpha$, $\beta$ and their derivatives] Decompose the [exterior derivative](/theorems/1525) on $[0,1] \times U$ as \begin{align*} d_{[0,1] \times U} = dt \wedge \partial_t + d_U, \end{align*} where $d_U$ acts in the $x$-variables only (treating $t$ as a parameter) and $\partial_t$ is the partial derivative in $t$ applied to coefficient functions. This notation means the following: for a form whose coefficients depend on $(t,x)$ and whose basis factors are built from $dt, dx_1, \dots, dx_n$, the term $dt \wedge \partial_t$ differentiates only the coefficients in $t$ and then wedges a new $dt$ on the left, while $d_U$ differentiates only the coefficients in the $x$-variables. This follows from the formula on coefficient functions $g(t, x)$, namely $dg = \partial_t g \, dt + \sum_j \partial_{x_j} g \, dx_j$, together with the derivation rule for $d$ and the identities $d(dt)=0$ and $d(dx_j)=0$ for $1 \le j \le n$; in particular, when a term already contains $dt$, the temporal contribution contains $dt \wedge dt$ and therefore vanishes. Apply this to $\alpha$ (a form with no $dt$): \begin{align*} d\alpha = dt \wedge \partial_t \alpha + d_U \alpha. \end{align*} Apply it to $dt \wedge \beta$, using the graded Leibniz rule $d(dt \wedge \beta) = d(dt) \wedge \beta - dt \wedge d\beta = -dt \wedge d\beta$ (since $d(dt) = 0$): \begin{align*} d(dt \wedge \beta) = -dt \wedge (dt \wedge \partial_t \beta + d_U \beta) = -dt \wedge d_U \beta, \end{align*} using $dt \wedge dt = 0$. Summing, \begin{align*} d(F^*\omega) = d(\alpha + dt \wedge \beta) = d_U \alpha + dt \wedge \bigl(\partial_t \alpha - d_U \beta\bigr). \end{align*} On the other hand, by [Naturality of the Pullback](/theorems/3574) ($F^*$ commutes with $d$), \begin{align*} d(F^*\omega) = F^*(d\omega). \end{align*} Applying the decomposition of Step 2 to $d\omega \in \Omega^{k+1}(U)$, write \begin{align*} F^*(d\omega) = \alpha' + dt \wedge \beta' \end{align*} with $\alpha' \in \Omega^{k+1}([0,1] \times U)$ and $\beta' \in \Omega^k([0,1] \times U)$ both free of $dt$. The decomposition into a $dt$-free part and a part of the form $dt \wedge (\cdot)$ is unique. Indeed, let $\iota_{\partial_t}$ denote interior product with the coordinate vector field $\partial_t$ on $[0,1] \times U$. If $\theta = \theta_0 + dt \wedge \theta_1$ with $\theta_0$ and $\theta_1$ free of $dt$, then $\iota_{\partial_t}\theta_0 = 0$ and $\iota_{\partial_t}(dt \wedge \theta_1) = \theta_1$, so $\theta_1 = \iota_{\partial_t}\theta$ and $\theta_0 = \theta - dt \wedge \theta_1$. Therefore comparing the $dt$-free and $dt$-containing parts of the two expressions for $d(F^*\omega) = F^*(d\omega)$ yields \begin{align*} \alpha' = d_U \alpha, \qquad \beta' = \partial_t \alpha - d_U \beta. \end{align*}[/step]

[guided]On the product $[0,1] \times U$, the de Rham complex splits according to the number of $dt$-factors. Any smooth form $\theta$ on $[0,1] \times U$ decomposes uniquely as $\theta = \theta_0 + dt \wedge \theta_1$ with $\theta_0, \theta_1$ free of $dt$. To see uniqueness, let $\iota_{\partial_t}$ denote interior product with the coordinate vector field $\partial_t$; then $\iota_{\partial_t}\theta_0 = 0$ and $\iota_{\partial_t}(dt \wedge \theta_1) = \theta_1$, so $\theta_1 = \iota_{\partial_t}\theta$ and $\theta_0 = \theta - dt \wedge \theta_1$. The [exterior derivative](/theorems/1525) splits compatibly: it has a "spatial" part $d_U$ (differentiating in $x$ only, leaving $t$ as a parameter) and a "temporal" part $dt \wedge \partial_t$ (differentiating in $t$ and prepending $dt$). Computing $d(\alpha + dt \wedge \beta)$: - $d\alpha = dt \wedge \partial_t \alpha + d_U \alpha$ contributes $d_U \alpha$ to the $dt$-free part and $\partial_t \alpha$ to the $dt$-coefficient. - $d(dt \wedge \beta)$: by Leibniz, $d(dt) \wedge \beta - dt \wedge d\beta = 0 - dt \wedge d\beta = -dt \wedge (dt \wedge \partial_t \beta + d_U \beta) = -dt \wedge d_U \beta$. So this contributes $-d_U \beta$ to the $dt$-coefficient. Total: $dt$-free part is $d_U \alpha$, $dt$-coefficient is $\partial_t \alpha - d_U \beta$. Why apply naturality $d \circ F^* = F^* \circ d$? Because we already wrote $F^*\omega$ in the decomposed form $\alpha + dt \wedge \beta$. To leverage closedness of $\omega$ (or, more generally, to express $H(d\omega)$ in terms of $\alpha, \beta$), we need to identify the components of $F^*(d\omega)$. Naturality (Theorem 3574) says these are the components of $d(F^*\omega)$. Uniqueness of the decomposition of forms on $[0,1] \times U$ then forces $\alpha' = d_U \alpha$ and $\beta' = \partial_t \alpha - d_U \beta$.[/guided]

[step:Verify the chain-homotopy identity $dH + Hd = \mathrm{id}$ on $\Omega^k(U)$]By the definition of $H$ applied to $d\omega$: \begin{align*} H(d\omega) = \int_0^1 \beta'(t, \cdot)\, d\mathcal{L}^1(t) = \int_0^1 \bigl(\partial_t \alpha(t, \cdot) - d_U \beta(t, \cdot)\bigr)\, d\mathcal{L}^1(t). \end{align*} Split the integral. For the $\partial_t \alpha$ term, the [Fundamental Theorem of Calculus](/theorems/632) applied componentwise gives \begin{align*} \int_0^1 \partial_t \alpha(t, \cdot)\, d\mathcal{L}^1(t) = \alpha(1, \cdot) - \alpha(0, \cdot). \end{align*} For the $d_U \beta$ term, $d_U$ involves only $x$-derivatives and the integration is over $t \in [0,1]$; for each fixed $x \in U$ the coefficients of $\beta(\cdot, \cdot)$ and their $x$-derivatives are jointly continuous on the compact set $[0,1] \times K$ for any compact $K \subset U$, so the [Leibniz Integral Rule](/theorems/831) gives \begin{align*} \int_0^1 d_U \beta(t, \cdot)\, d\mathcal{L}^1(t) = d_U \int_0^1 \beta(t, \cdot)\, d\mathcal{L}^1(t) = d(H\omega). \end{align*} (Here $d_U$ acting on a form on $U$ is just the [exterior derivative](/theorems/1525) $d$ on $U$.) Combining, \begin{align*} H(d\omega) = \alpha(1, \cdot) - \alpha(0, \cdot) - d(H\omega). \end{align*} It remains to evaluate the boundary terms. From the explicit formula for $\alpha$ in Step 2: \begin{align*} \alpha(1, x) &= 1^k \sum_I \omega_I(x)\, dx_{i_1} \wedge \cdots \wedge dx_{i_k} = \omega(x), \\ \alpha(0, x) &= 0^k \sum_I \omega_I(0)\, dx_{i_1} \wedge \cdots \wedge dx_{i_k} = 0, \end{align*} where in the second line we used $k \ge 1$ so that $0^k = 0$. Therefore \begin{align*} d(H\omega) + H(d\omega) = \omega \qquad \text{for every } \omega \in \Omega^k(U) \text{ with } k \ge 1. \end{align*}[/step]

[guided]This is the central identity of the proof: $H$ is a *chain homotopy* between the identity and the zero map on $\Omega^k(U)$ for $k \ge 1$. Geometrically, it is the algebraic shadow of the fact that the straight-line contraction $F(t,x) = tx$ deforms the identity ($t=1$) to the constant map at $0$ ($t=0$). Reading the computation: we know $\beta' = \partial_t \alpha - d_U \beta$ from Step 4, and $H(d\omega) = \int_0^1 \beta' \, dt$ from the definition of $H$. The integral splits into two pieces. The $\int_0^1 \partial_t \alpha \, dt$ piece is handled by FTC in $t$: for each fixed $x$, the coefficient functions of $\alpha$ are smooth in $t$, so $\int_0^1 \partial_t \alpha_I(t, x)\, d\mathcal{L}^1(t) = \alpha_I(1, x) - \alpha_I(0, x)$. We then read off the boundary values from the explicit formula: - $t = 1$: the factor $t^k$ is $1$, the argument $tx$ is $x$, so we recover exactly $\omega$. - $t = 0$: the factor $t^k$ is $0$ (using $k \ge 1$), so $\alpha(0, \cdot) = 0$. This last step is where the hypothesis $k \ge 1$ is consumed. For $k = 0$ (functions), $0^0 = 1$ would give $\alpha(0, x) = \omega(0)$ (a constant), and the lemma would fail in the form stated: closed $0$-forms are locally constant functions, which need not be in the image of $d$ (which lands in $\Omega^1$, not $\Omega^0$). The hypothesis $k \ge 1$ is therefore essential. The $\int_0^1 d_U \beta \, dt$ piece is handled by the [Leibniz integral rule](/theorems/831) (Theorem 831). Its hypotheses — joint continuity of the integrand and its $x$-derivatives on a compact rectangle — are met because $\beta(t, x)$ has smooth coefficients in $(t, x)$ on $[0,1] \times U$, so on any compact subset $K \subset U$ the integrand is uniformly bounded along with all its $x$-derivatives. Pulling $d_U$ out of $\int_0^1$ gives $d(H\omega)$. Putting the pieces together with the right signs: \begin{align*} H(d\omega) = [\alpha(1, \cdot) - \alpha(0, \cdot)] - d(H\omega) = \omega - 0 - d(H\omega), \end{align*} which rearranges to $dH\omega + H d\omega = \omega$.[/guided]

[step:Conclude that $\eta := H\omega$ is a primitive of $\omega$] Let $\omega \in \Omega^k(U)$ with $d\omega = 0$ and $k \ge 1$. Applying the chain-homotopy identity from Step 5, \begin{align*} \omega = d(H\omega) + H(d\omega) = d(H\omega) + H(0) = d(H\omega). \end{align*} Set $\eta := H\omega \in \Omega^{k-1}(U)$ (smoothness was verified in Step 3). Then $d\eta = \omega$, completing the proof. [/step]