The de Rham homotopy formula extends to boundary manifolds

At a point $(x,t)$ choose source and target coordinates and local Euclidean extensions of the map and the finitely many form coefficients. Shrink the map domain so it lies in the domain of the extended coefficients. The ordinary Euclidean pullback then restricts to a locally extendible form $\theta =H^{\ast }\omega$ on the parameter product. Derivatives are uniquely determined there: they agree on the dense set where the spatial half-space coordinate and the time coordinate are both interior, hence everywhere by continuity. The Euclidean formula for $d$ and naturality restrict to this product just as in [F1], giving $d\theta =H^{\ast }d\omega$.

Fix a spatial chart point $x_0$. Each coefficient of $\theta$ has smooth extensions on product neighbourhoods of $(x_0,t)$. There are finitely many coefficients; intersect their neighbourhoods at one $t$. Consider the family of all nested time intervals $J⋐I$ for which a coefficient extension exists on $W\times I$ for some Euclidean neighbourhood $W$ of $x_0$. These inner intervals cover $[0,1]$, by the local extension property at each one time; no interval or extension is chosen as a function of time. By [F6], finitely many $J_i$ cover $[0,1]$. For these finitely many members only, take corresponding $I_i,W_i$ and extensions. For each, take numbers $a_i<b_i<c_i<d_i$ inside $I_i$ with $J_i\cap [0,1]\subseteq [b_i,c_i]$ and put ${\rho }_i(t)=s\text{\hspace{0.17em}⁣}\left(\frac{t-a_i}{b_i-a_i}\right)s\text{\hspace{0.17em}⁣}\left(\frac{d_i-t}{d_i-c_i}\right)\mathrm{.}$ It is one on $[b_i,c_i]$, zero off $[a_i,d_i]$ and smooth by [F5]. Thus $R={\sum }_i{\rho }_i$ is positive on an open neighbourhood $J$ of $[0,1]$. Put ${\psi }_i={\rho }_i\mathrm{/}R$ on $J$. Their sum is one and each is supported away from the endpoints of $I_i$.

On the finite intersection $W={\bigcap }_i{W}_i$, multiply the $i$th coefficient extension by ${\psi }_i(t)$ and extend that product by zero outside $I_i$. Its support condition makes the extension smooth on $W\times J$. Summing the finitely many products gives a smooth coefficient extension on $W\times J$ of the original coefficient on $(W\cap M)\times [0,1]$, since every original coefficient equals each extension there and ${\sum }_i{\psi }_i=1$. This construction is used only to prove local smoothness at the one point $x_0$; it selects no families over all points of $M$.

Decompose $\theta ={\alpha }_t+dt\wedge {\beta }_t$ as in [F2]. Integrate each extended coefficient of $\beta$ from step 3.1 over $[0,1]$. On any smaller closed spatial rectangle in $W$, repeated use of [F3] gives ${\mathrm{\partial }}_x^I{\int }_0^{1}b(x,t)dt={\int }_0^1{\mathrm{\partial }}_x^{I}b(x,t)dt\mathrm{.}$ Each right side is continuous: [F7] bounds its change by the uniform change of the integrand times the interval length. Thus these integrals define a smooth Euclidean extension near $x_0$. A spatial coordinate change multiplies the coefficient vector of ${\beta }_t$ by an exterior-power transition matrix depending on $x$ only; moving this finite matrix through the integral proves that the restrictions patch as a form. Consequently $K\theta =L_H\omega$ is well defined and smooth, including at $\mathrm{\partial }M$.

The coordinate formula of [F1], applied on the extensions and restricted back, gives $d\theta =d_M{\alpha }_t+dt\wedge ({\mathrm{\partial }}_t{\alpha }_t-d_M{\beta }_t)\mathrm{.}$ The minus sign comes from moving $d_M$ past $dt$. By [F4], ${\int }_0^1{\mathrm{\partial }}_t{\alpha }_{t}dt={\alpha }_1-{\alpha }_0$ coefficientwise. Step 4.1 also gives $d_{M}K\theta ={\int }_0^1{d}_M{\beta }_{t}dt$. Therefore $d_{M}K\theta +Kd\theta ={\alpha }_1-{\alpha }_0\mathrm{.}$ Using $d\theta =H^{\ast }d\omega$ from step 1.1 and ${\alpha }_t=H_t^{\ast }\omega$, this is the asserted homotopy identity.

For a closed form, step 5.1 says $H_1^{\ast }\omega -H_0^{\ast }\omega =d(L_H\omega )$, so the endpoint classes agree in the quotient of [F1]. In degree zero $\beta =0$ and $K\theta =0$, while $Kd\theta$ is the integral of the time derivative; [F4] gives the same identity. In degree one $L_H\omega$ is an ordinary smooth function, including at the spatial boundary. Zero forms, negative degrees, constant homotopies and empty source or target cases satisfy the same formula with the appropriate zero spaces. Both time endpoints were included in steps 2.1–5.1. Only finitely many extensions at one specified point and explicit interval cutoffs were used, so no choice axiom is needed.