[proofplan]
We regard the radial contraction $H(t,x)=a+t(x-a)$ as a smooth homotopy from the constant map $x\mapsto a$ to the identity map on $U$. Pulling $\omega$ back to $[0,1]\times U$, we decompose the [exterior derivative](/theorems/1525) into the $t$-direction and the $U$-directions and prove the needed Cartan-type identity for the vector field $\partial_t$ directly in coordinates. Integrating this identity in $t$ gives the difference between the endpoint pullbacks $H_1^*\omega$ and $H_0^*\omega$. The endpoint at $t=1$ is $\omega$, while the endpoint at $t=0$ vanishes because $\omega$ has positive degree and the map $H_0$ is constant.
[/proofplan]
[step:Define the radial homotopy and identify the operator obtained by contraction]
Define the smooth map
\begin{align*}
H:[0,1]\times U &\to U \\
(t,x) &\mapsto a+t(x-a).
\end{align*}
This map is well-defined because $U$ is star-shaped with respect to $a$. For each $t \in [0,1]$, define
\begin{align*}
H_t:U &\to U \\
x &\mapsto H(t,x)=a+t(x-a).
\end{align*}
Then $H_1=\operatorname{id}_U$ and $H_0$ is the constant map $x\mapsto a$.
Let $\partial_t$ denote the coordinate vector field on $[0,1]\times U$ in the interval direction. For $\omega \in \Omega^k(U)$, define the $(k-1)$-form
\begin{align*}
\widetilde K\omega \in \Omega^{k-1}(U)
\end{align*}
by
\begin{align*}
(\widetilde K\omega)_x(v_1,\dots,v_{k-1})
=
\int_0^1
(\iota_{\partial_t}H^*\omega)_{(t,x)}
(v_1,\dots,v_{k-1})
\,d\mathcal{L}^1(t),
\end{align*}
where $v_1,\dots,v_{k-1}\in \mathbb{R}^n$ are viewed as tangent vectors in the $U$-directions at $(t,x)$.
For every $j \in \{1,\dots,k-1\}$,
\begin{align*}
dH_{(t,x)}(v_j)=t v_j,
\end{align*}
and
\begin{align*}
dH_{(t,x)}(\partial_t)=x-a.
\end{align*}
Therefore
\begin{align*}
(\iota_{\partial_t}H^*\omega)_{(t,x)}(v_1,\dots,v_{k-1})
&=
(H^*\omega)_{(t,x)}(\partial_t,v_1,\dots,v_{k-1})\\
&=
\omega_{a+t(x-a)}(x-a,tv_1,\dots,tv_{k-1})\\
&=
t^{k-1}\omega_{a+t(x-a)}(x-a,v_1,\dots,v_{k-1}).
\end{align*}
Thus $\widetilde K=K$ by the defining formula in the statement.
[guided]
The point of this step is to connect the explicit radial formula for $K$ with the homotopy expression obtained by contracting $H^*\omega$ against the interval direction.
We define
\begin{align*}
H:[0,1]\times U &\to U \\
(t,x) &\mapsto a+t(x-a).
\end{align*}
The star-shaped hypothesis says exactly that $a+t(x-a)\in U$ for every $x\in U$ and $t\in[0,1]$, so $H$ maps into $U$. For fixed $t$, define
\begin{align*}
H_t:U &\to U \\
x &\mapsto a+t(x-a).
\end{align*}
Then $H_1(x)=x$, so $H_1=\operatorname{id}_U$, and $H_0(x)=a$, so $H_0$ is constant.
Let $\partial_t$ be the coordinate vector field in the $[0,1]$ direction. The contraction $\iota_{\partial_t}H^*\omega$ is a $(k-1)$-form on $[0,1]\times U$. Integrating it in $t$ gives a $(k-1)$-form on $U$:
\begin{align*}
(\widetilde K\omega)_x(v_1,\dots,v_{k-1})
=
\int_0^1
(\iota_{\partial_t}H^*\omega)_{(t,x)}
(v_1,\dots,v_{k-1})
\,d\mathcal{L}^1(t).
\end{align*}
Now compute the differential of $H$. If $v\in\mathbb{R}^n$ is a tangent vector in the $U$ direction, then changing $x$ by $sv$ changes $H(t,x)$ by $stv$, hence
\begin{align*}
dH_{(t,x)}(v)=tv.
\end{align*}
Changing $t$ by $s$ changes $H(t,x)$ by $s(x-a)$, hence
\begin{align*}
dH_{(t,x)}(\partial_t)=x-a.
\end{align*}
Therefore
\begin{align*}
(\iota_{\partial_t}H^*\omega)_{(t,x)}(v_1,\dots,v_{k-1})
&=
(H^*\omega)_{(t,x)}(\partial_t,v_1,\dots,v_{k-1})\\
&=
\omega_{H(t,x)}(dH_{(t,x)}(\partial_t),dH_{(t,x)}(v_1),\dots,dH_{(t,x)}(v_{k-1}))\\
&=
\omega_{a+t(x-a)}(x-a,tv_1,\dots,tv_{k-1})\\
&=
t^{k-1}\omega_{a+t(x-a)}(x-a,v_1,\dots,v_{k-1}).
\end{align*}
This is precisely the formula defining $K\omega$, so the contraction-and-integration construction agrees with the stated radial operator.
[/guided]
[/step]
[step:Differentiate the pulled-back form in the interval direction]
Let $\eta:=H^*\omega\in\Omega^k([0,1]\times U)$. We prove the identity
\begin{align*}
\partial_t\eta=d(\iota_{\partial_t}\eta)+\iota_{\partial_t}(d\eta),
\end{align*}
where $\partial_t\eta$ denotes coefficientwise differentiation of $\eta$ in the $t$ variable.
Write local coordinates on $[0,1]\times U$ as $(t,x_1,\dots,x_n)$. Every $k$-form $\eta$ decomposes uniquely as
\begin{align*}
\eta=dt\wedge \alpha+\beta,
\end{align*}
where $\alpha\in\Omega^{k-1}([0,1]\times U)$ and $\beta\in\Omega^k([0,1]\times U)$ contain only the differentials $dx_1,\dots,dx_n$. Since $\iota_{\partial_t}\eta=\alpha$, and since the exterior derivative decomposes as
\begin{align*}
d=dt\wedge \partial_t+d_x,
\end{align*}
where $d_x$ is the exterior derivative in the $x$ variables, we compute
\begin{align*}
d\eta
&=
d(dt\wedge\alpha+\beta)\\
&=
-dt\wedge d\alpha+dt\wedge\partial_t\beta+d_x\beta\\
&=
-dt\wedge d_x\alpha+dt\wedge\partial_t\beta+d_x\beta.
\end{align*}
Contracting with $\partial_t$ gives
\begin{align*}
\iota_{\partial_t}(d\eta)
=
-d_x\alpha+\partial_t\beta.
\end{align*}
Also
\begin{align*}
d(\iota_{\partial_t}\eta)
=
d\alpha
=
dt\wedge\partial_t\alpha+d_x\alpha.
\end{align*}
Adding these two identities yields
\begin{align*}
d(\iota_{\partial_t}\eta)+\iota_{\partial_t}(d\eta)
=
dt\wedge\partial_t\alpha+\partial_t\beta
=
\partial_t(dt\wedge\alpha+\beta)
=
\partial_t\eta.
\end{align*}
[guided]
We need the usual Cartan identity only for the special vector field $\partial_t$, so we prove that special case directly. This avoids hiding the main computation inside a named theorem.
Let
\begin{align*}
\eta:=H^*\omega\in\Omega^k([0,1]\times U).
\end{align*}
In the product coordinates $(t,x_1,\dots,x_n)$, every form splits into the part containing $dt$ and the part containing no $dt$. Thus there are unique forms $\alpha\in\Omega^{k-1}([0,1]\times U)$ and $\beta\in\Omega^k([0,1]\times U)$, both involving only $dx_1,\dots,dx_n$, such that
\begin{align*}
\eta=dt\wedge\alpha+\beta.
\end{align*}
Because contraction with $\partial_t$ removes the leading $dt$ and kills forms with no $dt$, we have
\begin{align*}
\iota_{\partial_t}\eta=\alpha.
\end{align*}
The exterior derivative on the product decomposes into the $t$ part and the $x$ part:
\begin{align*}
d=dt\wedge\partial_t+d_x,
\end{align*}
where $d_x$ differentiates only with respect to the variables $x_1,\dots,x_n$. Applying this to $\eta=dt\wedge\alpha+\beta$ gives
\begin{align*}
d\eta
&=
d(dt\wedge\alpha)+d\beta\\
&=
-dt\wedge d\alpha+dt\wedge\partial_t\beta+d_x\beta\\
&=
-dt\wedge d_x\alpha+dt\wedge\partial_t\beta+d_x\beta.
\end{align*}
The term $dt\wedge dt\wedge\partial_t\alpha$ vanishes because $dt\wedge dt=0$.
Now contract this identity with $\partial_t$. Since $\alpha,\beta,d_x\alpha,d_x\beta$ contain no $dt$, we obtain
\begin{align*}
\iota_{\partial_t}(d\eta)
=
-d_x\alpha+\partial_t\beta.
\end{align*}
On the other hand,
\begin{align*}
d(\iota_{\partial_t}\eta)
=
d\alpha
=
dt\wedge\partial_t\alpha+d_x\alpha.
\end{align*}
Adding the two expressions cancels the $d_x\alpha$ terms:
\begin{align*}
d(\iota_{\partial_t}\eta)+\iota_{\partial_t}(d\eta)
=
dt\wedge\partial_t\alpha+\partial_t\beta.
\end{align*}
But coefficientwise differentiation of $\eta=dt\wedge\alpha+\beta$ in the $t$ direction is
\begin{align*}
\partial_t\eta
=
dt\wedge\partial_t\alpha+\partial_t\beta.
\end{align*}
Therefore
\begin{align*}
\partial_t\eta=d(\iota_{\partial_t}\eta)+\iota_{\partial_t}(d\eta).
\end{align*}
[/guided]
[/step]
[step:Integrate the interval derivative to obtain the endpoint difference]
For $v_1,\dots,v_k\in\mathbb{R}^n$, evaluating the identity from the previous step on the $U$-direction tangent vectors $v_1,\dots,v_k$ gives
\begin{align*}
\frac{\partial}{\partial t}
\bigl[(H_t^*\omega)_x(v_1,\dots,v_k)\bigr]
=
\bigl(d(\iota_{\partial_t}H^*\omega)+\iota_{\partial_t}d(H^*\omega)\bigr)_{(t,x)}(v_1,\dots,v_k).
\end{align*}
Since $H$ and $\omega$ are smooth, the integrand is continuous in $t$. Integrating with respect to $\mathcal{L}^1$ on $[0,1]$ and applying the [fundamental theorem of calculus](/theorems/632) for the real-valued function
\begin{align*}
t\mapsto (H_t^*\omega)_x(v_1,\dots,v_k)
\end{align*}
yields
\begin{align*}
(H_1^*\omega)_x(v_1,\dots,v_k)-(H_0^*\omega)_x(v_1,\dots,v_k)
=
\int_0^1
\bigl(d(\iota_{\partial_t}H^*\omega)+\iota_{\partial_t}d(H^*\omega)\bigr)_{(t,x)}(v_1,\dots,v_k)
\,d\mathcal{L}^1(t).
\end{align*}
The exterior derivative commutes with pullback, so
\begin{align*}
d(H^*\omega)=H^*(d\omega).
\end{align*}
Also, differentiation in the $x$ variables commutes with integration over the compact interval $[0,1]$, because the coefficients of $\iota_{\partial_t}H^*\omega$ are smooth in $(t,x)$. Hence
\begin{align*}
\int_0^1
d(\iota_{\partial_t}H^*\omega)_{(t,x)}(v_1,\dots,v_k)
\,d\mathcal{L}^1(t)
=
(dK\omega)_x(v_1,\dots,v_k),
\end{align*}
and
\begin{align*}
\int_0^1
(\iota_{\partial_t}H^*(d\omega))_{(t,x)}(v_1,\dots,v_k)
\,d\mathcal{L}^1(t)
=
(Kd\omega)_x(v_1,\dots,v_k).
\end{align*}
Therefore
\begin{align*}
H_1^*\omega-H_0^*\omega=dK\omega+Kd\omega.
\end{align*}
[guided]
We now turn the infinitesimal identity in $t$ into a global identity between forms on $U$.
Fix $x\in U$ and tangent vectors $v_1,\dots,v_k\in\mathbb{R}^n$. The coefficient
\begin{align*}
t\mapsto (H_t^*\omega)_x(v_1,\dots,v_k)
\end{align*}
is a smooth real-valued function on $[0,1]$, because $H$ and $\omega$ are smooth. Evaluating
\begin{align*}
\partial_t(H^*\omega)
=
d(\iota_{\partial_t}H^*\omega)+\iota_{\partial_t}d(H^*\omega)
\end{align*}
on the $U$-direction vectors $v_1,\dots,v_k$ gives
\begin{align*}
\frac{\partial}{\partial t}
\bigl[(H_t^*\omega)_x(v_1,\dots,v_k)\bigr]
=
\bigl(d(\iota_{\partial_t}H^*\omega)+\iota_{\partial_t}d(H^*\omega)\bigr)_{(t,x)}(v_1,\dots,v_k).
\end{align*}
The ordinary fundamental theorem of calculus applies to this smooth real-valued function, so
\begin{align*}
(H_1^*\omega)_x(v_1,\dots,v_k)-(H_0^*\omega)_x(v_1,\dots,v_k)
=
\int_0^1
\bigl(d(\iota_{\partial_t}H^*\omega)+\iota_{\partial_t}d(H^*\omega)\bigr)_{(t,x)}(v_1,\dots,v_k)
\,d\mathcal{L}^1(t).
\end{align*}
We now identify the two terms on the right. First, the exterior derivative commutes with pullback, hence
\begin{align*}
d(H^*\omega)=H^*(d\omega).
\end{align*}
Second, the operation $d$ in the $x$ variables commutes with integration over $[0,1]$: the coefficients of $\iota_{\partial_t}H^*\omega$ are smooth functions of $(t,x)$, and the interval of integration is compact. Therefore differentiating the coefficient of
\begin{align*}
\int_0^1 \iota_{\partial_t}H^*\omega\,d\mathcal{L}^1(t)
\end{align*}
is the same as integrating the differentiated coefficient. Since this integrated contraction is exactly $K\omega$, we get
\begin{align*}
\int_0^1
d(\iota_{\partial_t}H^*\omega)_{(t,x)}(v_1,\dots,v_k)
\,d\mathcal{L}^1(t)
=
(dK\omega)_x(v_1,\dots,v_k).
\end{align*}
Similarly, replacing $\omega$ by $d\omega$ in the defining formula for $K$ gives
\begin{align*}
\int_0^1
(\iota_{\partial_t}H^*(d\omega))_{(t,x)}(v_1,\dots,v_k)
\,d\mathcal{L}^1(t)
=
(Kd\omega)_x(v_1,\dots,v_k).
\end{align*}
Since the equality holds for every $x\in U$ and every $v_1,\dots,v_k\in\mathbb{R}^n$, it is an equality of $k$-forms:
\begin{align*}
H_1^*\omega-H_0^*\omega=dK\omega+Kd\omega.
\end{align*}
[/guided]
[/step]
[step:Evaluate the endpoint pullbacks and conclude the formula]
Since $H_1=\operatorname{id}_U$,
\begin{align*}
H_1^*\omega=\omega.
\end{align*}
Since $H_0:U\to U$ is the constant map $x\mapsto a$, its differential satisfies
\begin{align*}
d(H_0)_x(v)=0
\end{align*}
for every $x\in U$ and every $v\in\mathbb{R}^n$. Because $k\geq 1$, for every $v_1,\dots,v_k\in\mathbb{R}^n$,
\begin{align*}
(H_0^*\omega)_x(v_1,\dots,v_k)
=
\omega_a(0,\dots,0)
=
0.
\end{align*}
Thus $H_0^*\omega=0$. Substituting the endpoint values into
\begin{align*}
H_1^*\omega-H_0^*\omega=dK\omega+Kd\omega
\end{align*}
gives
\begin{align*}
\omega=dK\omega+Kd\omega.
\end{align*}
This is the desired homotopy formula.
[/step]
