[proofplan] Introduce the linear contraction $H: U \times [0,1] \to U$, $H(x,t) = a + t(x - a)$, which joins the constant map $c_a$ at $t = 0$ to the identity at $t = 1$. The pullback $H^*\omega$ on $U \times [0,1]$ splits uniquely into a "horizontal" $k$-form and a $dt$-component whose $U$-fibre integral over $t \in [0,1]$ is precisely $K_k\omega$. Applying $d$ to both sides of this decomposition and using naturality of the [exterior derivative](/theorems/1525) ($d \circ H^* = H^* \circ d$) yields an identity whose $dt$-component, after integrating from $0$ to $1$ via the [Fundamental Theorem of Calculus](/theorems/632), is exactly $dK\omega + Kd\omega = \omega - c_a^*\omega$. The vanishing of $c_a^*\omega$ for $k \ge 1$ follows from the fact that the differential of a constant map is zero. [/proofplan]

[step:Introduce the straight-line homotopy from $c_a$ to the identity]Because $U$ is star-shaped with centre $a$, the map \begin{align*} H: U \times [0,1] &\to U \\ (x, t) &\mapsto a + t(x - a) \end{align*} is well-defined and smooth. Its boundary values are \begin{align*} H(x, 0) = a = c_a(x), \qquad H(x, 1) = x. \end{align*} Equivalently, with $\iota_s: U \to U \times [0,1]$, $\iota_s(x) = (x, s)$, we have $H \circ \iota_0 = c_a$ and $H \circ \iota_1 = \operatorname{id}_U$.[/step]

[guided]The geometric picture is a deformation retract: at $t = 1$ every point $x \in U$ sits at itself; as $t$ decreases to $0$ every point slides along the line segment $\{a + t(x - a) : t \in [0,1]\}$ to the centre $a$. Star-shapedness is exactly what guarantees this segment never leaves $U$, so $H$ takes values in $U$ and is smooth (it is even affine in each variable separately). The two slice maps $\iota_0, \iota_1: U \hookrightarrow U \times [0,1]$ are smooth embeddings, and the compositions $H \circ \iota_0$ and $H \circ \iota_1$ recover the two endpoint maps $c_a$ and $\operatorname{id}_U$ between which we wish to compare. Pullback by the homotopy is therefore the natural tool to relate $\omega = \operatorname{id}_U^*\omega$ and $c_a^*\omega$ via a $1$-parameter family on $U \times [0,1]$.[/guided]

[step:Decompose $H^*\omega$ into its horizontal and $dt$ components]The smooth $k$-form $H^*\omega \in \Omega^k(U \times [0,1])$ admits a unique decomposition \begin{align*} H^*\omega = \alpha + dt \wedge \beta, \end{align*} where $\alpha \in \Omega^k(U \times [0,1])$ satisfies $\iota_{\partial_t}\alpha = 0$ and $\beta \in \Omega^{k-1}(U \times [0,1])$ satisfies $\iota_{\partial_t}\beta = 0$. Here $\partial_t$ denotes the standard coordinate vector field $(0, 1)$ on $U \times [0,1]$, and $\iota_{\partial_t}$ is the interior product. Concretely, $\alpha$ and $\beta$ are the parts of $H^*\omega$ in which $dt$ does, respectively does not, appear. For each fixed $t \in [0,1]$, the pullback $\iota_t^* \alpha \in \Omega^k(U)$ equals $\iota_t^*(H^*\omega) = (H \circ \iota_t)^*\omega$, because $\iota_t^*(dt) = 0$ kills the $dt \wedge \beta$ summand. In particular, \begin{align*} \iota_0^*(H^*\omega) = c_a^*\omega, \qquad \iota_1^*(H^*\omega) = \omega. \end{align*}[/step]

[guided]On $U \times [0,1]$ we have coordinates $(x_1, \dots, x_n, t)$, so a basis of $1$-forms is $\{dx_1, \dots, dx_n, dt\}$. Any $k$-form decomposes uniquely into a sum of wedge products of these basis $1$-forms; collecting terms by whether or not the factor $dt$ appears partitions $H^*\omega$ into \begin{align*} H^*\omega = \underbrace{\sum_{|I|=k} f_I(x,t)\, dx_I}_{= \alpha} \;+\; dt \wedge \underbrace{\sum_{|J|=k-1} g_J(x,t)\, dx_J}_{= \beta}. \end{align*} The condition $\iota_{\partial_t} \alpha = 0$ is equivalent to the statement that $\alpha$ has no $dt$ factor, since interior product with $\partial_t$ extracts the $dt$-coefficient: $\iota_{\partial_t}(dt) = 1$, $\iota_{\partial_t}(dx_i) = 0$. So the decomposition is unique. Evaluating at $t = 0, 1$ via the slice maps $\iota_t$: the pullback $\iota_t^*$ acts on a $1$-form $dt$ by $\iota_t^* dt = d(t) = 0$ (since $t$ is constant on the image of $\iota_t$). Hence $\iota_t^*(dt \wedge \beta) = 0$, leaving $\iota_t^*(H^*\omega) = \iota_t^*\alpha = (H \circ \iota_t)^*\omega$. With $H \circ \iota_0 = c_a$ and $H \circ \iota_1 = \operatorname{id}_U$, we get the asserted endpoint values.[/guided]

[step:Identify $\beta$ with the integrand of $K_k\omega$]We claim that for all $(x,t) \in U \times [0,1]$ and $v_1, \dots, v_{k-1} \in \mathbb{R}^n$, \begin{align*} \beta_{(x,t)}(v_1, \dots, v_{k-1}) = t^{k-1}\, \omega_{a + t(x - a)}(x - a,\, v_1,\, \dots,\, v_{k-1}). \end{align*} Since $\iota_{\partial_t}(dt \wedge \beta) = \beta$ and $\iota_{\partial_t}\alpha = 0$, we have $\beta = \iota_{\partial_t}(H^*\omega)$. Evaluating at the tangent vectors $(v_i, 0)$ at $(x,t)$: \begin{align*} \beta_{(x,t)}(v_1, \dots, v_{k-1}) = (H^*\omega)_{(x,t)}\bigl(\partial_t,\, (v_1, 0),\, \dots,\, (v_{k-1}, 0)\bigr) = \omega_{H(x,t)}\bigl(dH_{(x,t)}\partial_t,\, dH_{(x,t)}(v_1,0),\, \dots,\, dH_{(x,t)}(v_{k-1},0)\bigr). \end{align*} From $H(x,t) = a + t(x - a)$ we compute \begin{align*} dH_{(x,t)}(0, 1) &= \partial_t H(x,t) = x - a, \\ dH_{(x,t)}(v_i, 0) &= \partial_{x}H(x,t)\, v_i = t\, v_i. \end{align*} Multilinearity of $\omega$ in its $k - 1$ trailing arguments extracts the factor $t^{k-1}$, yielding the claimed formula. Defining $K_k\omega$ via the fibre integral \begin{align*} (K_k\omega)_x(v_1, \dots, v_{k-1}) = \int_0^1 \beta_{(x,t)}(v_1, \dots, v_{k-1})\, d\mathcal{L}^1(t) \end{align*} therefore agrees with the formula in the statement.[/step]

[guided]This step is the computational heart of the construction: the $t^{k-1}$ factor that appears in the definition of $K_k$ is not arbitrary — it is dictated by the geometry of the homotopy $H$. Why does each spatial input $v_i$ produce a factor of $t$? Because $H$ is the linear contraction by factor $t$ in the directions transverse to time, so its spatial differential is $t \cdot I_n$. A $k$-form eats $k$ vectors; one slot is consumed by $\partial_t \mapsto x - a$, and the remaining $k - 1$ slots each contribute a $t$, giving $t^{k-1}$ overall. By contrast, the time direction contributes $x - a$ rather than a power of $t$: this is precisely the displacement vector from the centre to $x$, and it is what couples the form to the geometry of the star-shaped domain. The interior-product identity $\iota_{\partial_t}(H^*\omega) = \beta$ is purely algebraic: $\iota_{\partial_t}\alpha = 0$ by construction, and $\iota_{\partial_t}(dt \wedge \beta) = (\iota_{\partial_t} dt) \cdot \beta - dt \wedge \iota_{\partial_t}\beta = 1 \cdot \beta - 0 = \beta$.[/guided]

[step:Apply the exterior derivative and use $d \circ H^* = H^* \circ d$]The [exterior derivative](/theorems/1525) on $U \times [0,1]$ splits according to the product structure: for any smooth form $\gamma$ on $U \times [0,1]$, \begin{align*} d\gamma = d_U \gamma + dt \wedge \partial_t \gamma, \end{align*} where $d_U$ is the [exterior derivative](/theorems/1525) in the $U$-variables (treating $t$ as a parameter) and $\partial_t$ acts on coefficient functions. Apply this to $H^*\omega = \alpha + dt \wedge \beta$: \begin{align*} d(H^*\omega) = d_U\alpha + dt \wedge \partial_t \alpha + d(dt \wedge \beta) = d_U\alpha + dt \wedge \partial_t\alpha - dt \wedge d_U\beta, \end{align*} using $d(dt) = 0$ and the Leibniz rule $d(dt \wedge \beta) = -dt \wedge d\beta$ (since $dt$ is a $1$-form), together with $dt \wedge dt \wedge \partial_t \beta = 0$. By naturality of the [exterior derivative](/theorems/1525) under smooth pullback, $d(H^*\omega) = H^*(d\omega)$. Now write the analogous decomposition for $d\omega \in \Omega^{k+1}(U)$ pulled back via $H$: \begin{align*} H^*(d\omega) = \alpha' + dt \wedge \beta', \end{align*} where $\alpha'$ has no $dt$ factor and $\beta'$ has no $dt$ factor. Comparing the $dt$-parts of $d(H^*\omega) = H^*(d\omega)$ yields the identity in $\Omega^k(U \times [0,1])$: \begin{align*} \partial_t \alpha - d_U \beta = \beta'. \end{align*}[/step]

[guided]The split $d = d_U + dt \wedge \partial_t$ is just bookkeeping: write the [exterior derivative](/theorems/1525) on $U \times [0,1]$ in coordinates, and separate the terms containing $dt$ from those that do not. The terms that do not contain $dt$ are exactly $d_U$ applied to the $U$-coefficient functions; the ones that do are $dt \wedge \partial_t$ applied to those same coefficients. Why expand $d(H^*\omega)$ via this split? Because the original decomposition $H^*\omega = \alpha + dt \wedge \beta$ is also organised by whether $dt$ appears, so we can read off the $dt$-component of $d(H^*\omega)$ cleanly. We use: \begin{align*} d(dt \wedge \beta) &= d(dt) \wedge \beta - dt \wedge d\beta \\ &= 0 - dt \wedge (d_U\beta + dt \wedge \partial_t \beta) \\ &= -dt \wedge d_U\beta, \end{align*} since $dt \wedge dt = 0$. The $dt$-part of $d(H^*\omega)$ is therefore $dt \wedge (\partial_t \alpha - d_U \beta)$. Naturality $d \circ H^* = H^* \circ d$ is a defining property of the [exterior derivative](/theorems/1525) under smooth pullback. The $dt$-part of $H^*(d\omega)$ is by definition $dt \wedge \beta'$. Equating the two $dt$-coefficients (which are uniquely determined by the decomposition in Step 2) gives $\partial_t\alpha - d_U\beta = \beta'$.[/guided]

[step:Integrate the $dt$-component from $0$ to $1$]The identity $\partial_t \alpha - d_U \beta = \beta'$ holds in $\Omega^k(U \times [0,1])$ at every $t \in [0,1]$. Pull back along $\iota_t: x \mapsto (x,t)$ — which simply substitutes the value of $t$ into the $U$-coefficients of these horizontal $k$-forms — and integrate in $t$: \begin{align*} \int_0^1 \iota_t^*(\partial_t \alpha)\, d\mathcal{L}^1(t) - \int_0^1 \iota_t^*(d_U \beta)\, d\mathcal{L}^1(t) = \int_0^1 \iota_t^*\beta'\, d\mathcal{L}^1(t). \end{align*} The right-hand side equals $K_{k+1}(d\omega)$ by definition. We evaluate the two terms on the left. For the first term, apply the [Fundamental Theorem of Calculus](/theorems/632) componentwise (each component of $\iota_t^*\alpha$ is a smooth function of $t$ with values in $C^\infty(U)$): \begin{align*} \int_0^1 \iota_t^*(\partial_t \alpha)\, d\mathcal{L}^1(t) = \iota_1^*\alpha - \iota_0^*\alpha = \omega - c_a^*\omega, \end{align*} using the endpoint identifications $\iota_1^*\alpha = \iota_1^*(H^*\omega) = \omega$ and $\iota_0^*\alpha = c_a^*\omega$ from Step 2. For the second term, the [exterior derivative](/theorems/1525) $d_U$ on $U$ does not act on $t$, so by the [Leibniz Integral Rule](/theorems/831) — which applies because $\beta$ is smooth, in particular jointly continuous together with all its $x$-derivatives on the compact parameter interval $[0,1]$ — we may interchange $d_U$ with the $t$-integral: \begin{align*} \int_0^1 \iota_t^*(d_U\beta)\, d\mathcal{L}^1(t) = d\left(\int_0^1 \iota_t^*\beta\, d\mathcal{L}^1(t)\right) = d(K_k\omega). \end{align*} Combining, \begin{align*} \omega - c_a^*\omega - d(K_k\omega) = K_{k+1}(d\omega), \end{align*} which rearranges to the claimed identity $d(K_k\omega) + K_{k+1}(d\omega) = \omega - c_a^*\omega$.[/step]

[guided]This is where the formula assembles itself. We have an identity of horizontal $k$-forms on $U \times [0,1]$, and we want an identity of $k$-forms on $U$. The bridge is integration of the $t$-parameter from $0$ to $1$, which collapses a horizontal $k$-form $\gamma(x, t)$ on $U \times [0,1]$ to the $k$-form $\int_0^1 \iota_t^*\gamma\, d\mathcal{L}^1(t)$ on $U$. Why does the integral of $\partial_t \alpha$ give a boundary term? Because we are integrating an exact $t$-derivative over $[0,1]$, the [Fundamental Theorem of Calculus](/theorems/632) applies. We verify its hypotheses: the components of $\iota_t^*\alpha$ are smooth functions of $(x, t)$ on $U \times [0,1]$, so for each fixed $x \in U$ the map $t \mapsto (\iota_t^*\alpha)_x$ is $C^1$ on $[0,1]$, and the FTC gives $\int_0^1 \partial_t (\iota_t^*\alpha)_x\, d\mathcal{L}^1(t) = (\iota_1^*\alpha)_x - (\iota_0^*\alpha)_x$. Why can we swap $d_U$ with the $t$-integral? We invoke the [Leibniz Integral Rule](/theorems/831) (theorem 831). Its hypotheses require that the integrand and its required $x$-derivatives be jointly continuous in $(x, t)$ and that $[0,1]$ be a fixed (parameter-independent) interval. Smoothness of $\beta$ on $U \times [0,1]$ gives joint continuity of all required derivatives, and the interval $[0,1]$ is fixed, so the rule applies and we may pass $d_U$ inside the integral. The right-hand side $\int_0^1 \iota_t^*\beta'\, d\mathcal{L}^1(t)$ is, by the very definition of $K_{k+1}$ applied to the $(k+1)$-form $d\omega$, equal to $K_{k+1}(d\omega)$ — for $K_{k+1}$ is built from the $dt$-component of $H^*(d\omega)$ in the same way $K_k$ is built from the $dt$-component of $H^*\omega$. Rearranging the resulting equation gives $d(K_k\omega) + K_{k+1}(d\omega) = \omega - c_a^*\omega$, which is the homotopy operator identity.[/guided]

[step:Show $c_a^*\omega = 0$ for $k \ge 1$]The constant map $c_a: U \to U$ has differential $(dc_a)_x = 0: \mathbb{R}^n \to \mathbb{R}^n$ at every $x \in U$, because $c_a$ is constant. For $\omega \in \Omega^k(U)$ with $k \ge 1$ and tangent vectors $v_1, \dots, v_k \in \mathbb{R}^n$, \begin{align*} (c_a^*\omega)_x(v_1, \dots, v_k) = \omega_{c_a(x)}\bigl((dc_a)_x v_1, \dots, (dc_a)_x v_k\bigr) = \omega_a(0, \dots, 0) = 0, \end{align*} by multilinearity of $\omega_a$ on its $k \ge 1$ arguments. Hence $c_a^*\omega \equiv 0$ on $U$, and the identity from Step 5 reduces to $d(K_k\omega) + K_{k+1}(d\omega) = \omega$.[/step]

[guided]The pullback of a differential form along a smooth map $f$ at a point $x$ is built from the differential $df_x$ acting on each input vector. When $f = c_a$ is constant, $df_x \equiv 0$, so every input slot of the pulled-back form receives the zero vector. A $k$-form with $k \ge 1$ is multilinear and alternating, so any input slot being zero forces the whole evaluation to be zero. The exception is $k = 0$: a $0$-form is a function $\omega: U \to \mathbb{R}$, and the pullback is $c_a^*\omega = \omega \circ c_a$, which is the constant function $\omega(a)$. This is generally nonzero, which is why the full identity in Step 5 retains the $c_a^*\omega$ term — that term carries the constant-mode information lost by $K$. For $k \ge 1$ the constant-mode obstruction disappears, and the homotopy operator inverts $d$ in the sense that $d K + K d = \operatorname{id}$ on $\Omega^k(U)$. This is the algebraic content underlying the Poincaré lemma for star-shaped domains: if $d\omega = 0$ and $k \ge 1$, then $\omega = d(K_k\omega)$ is exact, with an explicit primitive given by the formula in the statement.[/guided]