The de Rham Theorem and Degree

The affine parametrization $x\mapsto v_0+{\sum }_{j=1}^k{x}_j{E}_j$ identifies the simplex with $x_j\ge 0$ and ${\sum }_j{x}_j\le 1$. The $E_j$ are independent: their coordinates in positions $1,\dots ,k$ form the identity matrix. Swapping two vertices other than $v_0$ swaps two basis columns and changes the wedge sign. Swapping $v_0,v_1$ replaces the basis by $-E_1,E_2-E_1,\dots ,E_k-E_1$, whose wedge is $-\mathrm{\Omega }$. These swaps generate the vertex permutations, so a permutation changes the ray by its permutation sign. The affine convention therefore agrees with [F2] for $k\ge 1$.

For $1\le i\le k$, the face $x_i=0$ has its ordered basis $E_1,\dots ,{\widehat{E}}_i,\dots ,E_k$. At a relative interior point, $-E_i$ points outward, since the interior has $x_i>0$. Moving this vector from the first position to position $i$ gives $(-E_i)\wedge E_1\wedge \cdots \wedge {\widehat{E}}_i\wedge \cdots \wedge E_k=(-1{)}^i\mathrm{\Omega }\mathrm{.}$ Multiplying the face determinant by $(-1{)}^i$ makes its wedge after that outward vector positive. Thus [F4] gives exactly the claimed boundary sign on this face.

On face zero, ${\sum }_j{x}_j=1$, the remaining ordered vertices are $v_1,\dots ,v_k$, with basis $E_2-E_1,\dots ,E_k-E_1$. The vector $E_1$ points outward, since it increases the coordinate sum. Its wedge with this face basis is $\mathrm{\Omega }$, because all terms selecting another $E_1$ vanish by alternation. Hence the ordered face already has the boundary orientation, giving sign $(-1{)}^0=1$. The outward vectors in this calculation need not be perpendicular: their strict transverse directions are exactly what [F4] requires.

For $k=1$, the face bases in steps 2.1–2.2 are empty determinants, namely $1\in {\mathrm{\Lambda }}^0\{0\}=\mathbb{R}$. The outward vectors at $v_0,v_1$ are $-E_1,E_1$, so their induced determinant-line signs are respectively minus and plus. This gives $[v_1]-[v_0]$, despite the unique vertex ordering of each abstract point in [F2]. For $k=0$, the chosen ray is positive and [F1] gives no face maps or negative-dimensional simplex. The simplex is never empty; zero coefficients or degenerate maps into a target do not change this domain orientation. Every vector and sign was specified explicitly, so no choice principle is used.

For $k=1$, $T_1=[0,1]$ is a compact Jordan interval. If $T_{k-1}$ is compact Jordan for $k\ge 2$, then $T_k$ is its solid under the nonnegative continuous function $u\mapsto 1-{\sum }_{j=1}^{k-1}{u}_j$. Applying [F5] inductively proves compactness and Jordan measurability in every positive dimension. This finite induction chooses no family of objects.

The inverse image under $\bar{\sigma }$ of the open domain of $\omega$ is an open neighbourhood of ${\mathrm{\Delta }}^k$, so the restriction used in the definition exists. By [F3] and [F4], $f$ is smooth on an open neighbourhood of $T_k$, hence continuous on $T_k$. Step 1.1 and [F6] give a finite Riemann integral, and [F7] makes its value independent of a bounding rectangle. The coefficient itself need not have compact support on its neighbourhood.

Two extensions agree on the relative interior of ${\mathrm{\Delta }}^k$, an open set in its affine span; their derivatives and hence pullback coefficients agree there. For any $x\in T_k$, the points $(1-t)x+tb$, where $b_j=1\mathrm{/}(k+1)$ and $0<t\le 1$, lie in the interior and converge to $x$ as $t\downarrow 0$. Continuity of both coefficients forces equality at $x$. Thus their integrands are identical on all of $T_k$, proving extension independence, including along every face.

When $k=0$, evaluation needs no derivative or integration theorem in dimension zero. When $M$ is empty there is no simplex to which the definition applies. A zero form has zero coefficient and integral zero. Degenerate maps are allowed; if the derivative has rank less than $k>0$, alternation makes its top-form pullback zero. The affine domain and its faces are retained even for such maps. The definition uses one extension whose existence is part of [F2], and the resulting value is independent of it; it makes no simultaneous selection of extensions and uses no choice axiom.

Suppose $k\ge 1$. Each of $K_a,K_b$ is an invertible affine image of the standard compact Jordan simplex from [F1], hence compact Jordan by [F2]. Put $h=a^{-1}\circ b$. It is an affine diffeomorphism of ${\mathbb{R}}^k$, it maps $K_b$ onto $K_a$, and its constant derivative has determinant $d>0$ because both parametrizations are positive.

For a single smooth extension write $a^{\ast }{\bar{\sigma }}^{\ast }\omega =f(x)d{x}_1\wedge \cdots \wedge d{x}_k$. The coefficient is smooth near $K_a$ and bounded on $K_a$. By [F4], its expression in the $b$ parametrization is $f(h(y))\det Dhd{y}_1\wedge \cdots \wedge d{y}_k$: evaluating the alternating form on the $k$ columns of $Dh$ gives exactly this determinant. Thus the coefficient in $b$ coordinates is $d(f\circ h)$.

Apply [F3] to the open set ${\mathbb{R}}^k$, injective $C^1$ map $h$, compact Jordan set $K_b$ and continuous function $f$ on $h(K_b)=K_a$. Every derivative is invertible and $\mathrm{\mid }\det Dh\mathrm{\mid }=d$. Therefore ${\int }_{K_a}f(x)dx={\int }_{K_b}df(h(y))dy,$ which is precisely equality of the two form integrals for a fixed extension. If two neighbourhood extensions are used, they agree on the relative interior of the affine simplex. Their pullback coefficients therefore agree there; every boundary point is a limit of relative-interior points, so continuity makes the coefficients agree on the whole compact simplex. Their integrals consequently coincide in either coordinate system.

For $k=0$ both parametrizations of the affine point are the unique point map and both definitions are evaluation at $\sigma (v_0)$; no positive-dimensional change-of-variables theorem is used. For $k=1$, step 3.1 includes all positive affine rescalings of the closed interval, with endpoints included in the compact set. Zero coefficients and rank-deficient simplex maps require no division by a form value, so the equality still holds. Empty targets supply no simplex. All maps $h$ and their coefficients are determined by the two given parametrizations; no choice is used.

First let $k\ge 2$. Write $\eta ={\sum }_{i=1}^k(-1{)}^{i-1}{f}_{i}d{x}_1\wedge \cdots \wedge \widehat{d{x}_i}\wedge \cdots \wedge d{x}_k\mathrm{.}$ All $f_i$ are smooth near $T_k$. In [F3], every derivative except ${\mathrm{\partial }}_i{f}_i$ wedges a repeated differential and vanishes; moving $d{x}_i$ past $i-1$ factors cancels the coefficient sign. Hence $d\eta =\left({\sum }_{i=1}^k{\mathrm{\partial }}_i{f}_i\right)d{x}_1\wedge \cdots \wedge d{x}_k\mathrm{.}$

Fix $i$. Let $z$ denote the increasing list of all coordinates except $x_i$, let $D_i=\{z\ge 0:\sum z\le 1\}$ and put $b(z)=1-\sum z$. The $x_i$ section of $T_k$ is $[0,b(z)]$ for $z\in D_i$, and it is empty off $D_i$. Coordinate permutation has absolute determinant one by [F6]. The full integrand ${\mathrm{\partial }}_i{f}_i$ is integrable by [F7], and every nonempty section is continuous on its closed interval. Applying [F5] after that permutation and [F4] on sections with $b(z)>0$ gives ${\int }_{T_k}{\mathrm{\partial }}_i{f}_{i}dx={\int }_{D_i}(f_i(z,x_i=b(z))-f_i(z,x_i=0))dz\mathrm{.}$ When $b(z)=0$, both the section integral and the endpoint difference are zero, so the formula holds on these sections too. No exceptional family is discarded.

Parametrize face zero by $y=(x_2,\dots ,x_k)\in T_{k-1}$, with $x_1=1-{\sum }_{j=2}^k{x}_j$. For $i=1$ the omitted differential wedge pulls back to $dy$. For $i>1$, substitute $d{x}_1=-{\sum }_{j=2}^{k}d{x}_j$; only its $-d{x}_i$ term survives, and moving $d{x}_i$ to its increasing position contributes $(-1{)}^{i-2}$. Thus the omitted wedge pulls back to $(-1{)}^{i-1}dy$. The coefficient sign in step 1.1 cancels it, giving ${\delta }_0^{\ast }\eta =\left({\sum }_{i=1}^k{f}_i{\mid }_{\mathrm{f}\mathrm{a}\mathrm{c}\mathrm{e}0}\right)dy\mathrm{.}$

On face $i\ge 1$, $x_i=0$ and the remaining vertex ordering gives precisely the increasing remaining coordinate basis. All summands of $\eta$ except the one indexed by $i$ pull back to zero, because they contain $d{x}_i$. The signed contribution of this face is therefore $(-1{)}^i\int {\delta }_i^{\ast }\eta =-{\int }_{D_i}{f}_i(z,x_i=0)dz\mathrm{.}$ This matches the lower endpoint term in step 2.1.

For each $i>1$, the map from $y$ to the increasing coordinates $z$ omitting $x_i$ replaces the missing coordinate by $x_1=1-\sum y_j$. Its derivative has determinant $(-1{)}^{i-1}$: expand along the identity rows, leaving the entry $-1$ in the position corresponding to $x_i$. It maps $T_{k-1}$ bijectively onto $D_i$, with inverse obtained by solving $x_i=1-\sum z$. Thus [F6] transforms the upper endpoint integral in step 2.1 into the integral of $f_i$ over the face-zero parametrization, with absolute determinant one. For $i=1$ the map is the identity. Summing over $i$, step 2.2 identifies all upper endpoint terms with $\int {\delta }_0^{\ast }\eta$.

By [F8], sum the identities of step 2.1 and use step 1.1 for the left side, step 3.1 for the lower endpoints and step 3.2 for the upper endpoints. This gives the displayed Stokes identity for $k\ge 2$, with sign $+1$ on face zero and $(-1{)}^i$ on face $i$. All sums are finite.

For $k=1$, $\eta =f$ is a function, and [F3] and [F4] give ${\int }_0^{1}df=f(1)-f(0)$. The face-zero map is the terminal vertex and the face-one map the initial vertex, whose integrals are evaluations by [F1]. This is the same formula. The assertion excludes $k=0$ and does not introduce forms of degree minus one. Zero forms give zero on both sides; all collapsed sections were treated in step 2.1, including intersections of faces. All coordinates, changes and sums are explicit and finite, so the proof uses no choice.

For one smooth simplex $\sigma$, take a neighbourhood extension $\bar{\sigma }$ as required in [F2]. The smooth form $\eta ={\bar{\sigma }}^{\ast }\omega$ is defined on that whole neighbourhood in the affine span, so [F1] applies. By [F4] its derivative is ${\bar{\sigma }}^{\ast }d\omega$. By [F5], its pullback to face $i$ is $(\bar{\sigma }\circ {\delta }_i{)}^{\ast }\omega$, which extends the face simplex smoothly. Definition [F3] consequently gives ${\int }_{\sigma }d\omega ={\sum }_{i=0}^k(-1{)}^i{\int }_{\sigma \circ {\delta }_i}\omega \mathrm{.}$ The values do not depend on the selected extension.

A chain is a finitely supported coefficient function on the supplied simplex set. Define ${\int }_c\omega ={\sum }_{\sigma \in \mathrm{supp}c}c(\sigma ){\int }_{\sigma }\omega$. This is independent of a written expression for $c$: combining repetitions adds their coefficients, and inserting a zero coefficient changes nothing. Finite distributivity gives additivity and real homogeneity in $c$. No basis selection or simultaneous choice of extensions is involved, because [F3] already assigns a unique value to each simplex.

Multiply step 1.1 by $c(\sigma )$ and sum over its finite support. The boundary from [F2] is the same finite double sum of face simplices with coefficients $c(\sigma )(-1{)}^i$. When identical faces occur, step 1.2 combines their coefficients in exactly the same way in its integral. Therefore ${\int }_{c}d\omega ={\sum }_{\sigma ,i}c(\sigma )(-1{)}^i{\int }_{\sigma {\delta }_i}\omega ={\int }_{\mathrm{\partial }c}\omega \mathrm{.}$

For $k=1$, [F1] uses the terminal-minus-initial endpoint evaluations, so the formula includes every smooth path, constant or otherwise. Degenerate higher simplices remain generators, and step 1.1 applies to their smooth extensions without a rank assumption. If $c=0$ or $M=\mathrm{\varnothing }$, the relevant sums are empty and both integrals vanish. A zero form has zero pullback and zero integral. The assertion involves only positive chain degrees and finite sums, so no negative degree or choice assumption is hidden.

Near a fixed boundary-chart point there are finitely many coefficients in a form. Intersect their finitely many extension neighbourhoods and apply [F3] to these extensions on that open set. By [F2], replacing any extension leaves each first derivative on the half-space unchanged. Thus the resulting restricted $(k+1)$-form is well defined and has locally extendible coefficients. The construction is local at each point and selects no extensions over a family of chart points.

On a chart overlap let $g$ be the transition map. Locally extend its coordinate functions and the finitely many target coefficients, shrinking the source extension neighbourhood so that its image lies in the open set of coefficient extensions; continuity at the specified point ensures this. The coordinate identity for the original form is the equality of its source coefficients with those of $g^{\ast }$ of its target coefficients on the half-space. By [F2] their derivatives agree there. Applying [F4] to the Euclidean extensions yields $d(g^{\ast }\eta )=g^{\ast }(d\eta )$ on the half-space. Therefore the local derivatives in step 1.1 obey the form transformation rule and patch to a single form on $M$. This uses local extensions, not a demand that an extended transition map remain inside the half-space.

To compute $d^2$, use the first derivatives of the same coefficient extensions to represent the first derivative form, which is permitted by step 1.1. Equation [F5] then restricts to $d^2=0$ on the half-space. Likewise [F6], applied to simultaneous local extensions of two forms and restricted back, proves real linearity and the signed product rule. All these identities patch by step 2.1. This calculation explicitly includes the vanishing of $d^2$ of each function that occurs when differentiating a wedge of pulled-back coordinate differentials.

At a specified point of $M$, [F9] extends the coordinate representative of $F$ to a Euclidean-open set. Extend a target form's finitely many coefficients near its image and shrink the source as in step 2.1. The Euclidean pullback, derivative and wedge identities of [F4] and [F7] restrict to the corresponding identities on $M$, independently of all extensions by [F2]. This works even if $F$ maps an open set entirely into $\mathrm{\partial }N$: the Euclidean calculation takes place before restriction and does not presume that $F$ carries interior points to interior points. Composition and identity laws follow from the same local formulas.

Step 3.1 puts $\mathrm{im}d\subseteq \ker d$, so the stated vector-space quotient is defined. By step 3.2, a closed form pulls back to a closed form, and a change by $d\eta$ pulls back to a change by $d(F^{\ast }\eta )$; hence the quotient maps are well defined and functorial. On boundaryless charts the construction is exactly [F8]. For dimension zero, all positive-degree forms vanish and $d=0$; the empty manifold has only zero section spaces. At boundary points step 1.1 handles every derivative by [F2], and no orientation or nonempty choice is required.

Definition [F1] gives one uniquely determined value on every smooth $k$-simplex. For each finite chain, distributing its coefficients in the displayed sum shows that this function extends to a real linear functional. Two such functionals agreeing on all simplices agree on every finite chain. By [F2] this defines a unique element $I_M^k(\omega )$ of the cochain space. No choice of a vector-space basis or of simplex extensions is made.

For forms $\omega ,\eta$ of degree $k$ and real $a,b$, alternating evaluation in the definition of pullback gives ${\sigma }^{\ast }(a\omega +b\eta )=a{\sigma }^{\ast }\omega +b{\sigma }^{\ast }\eta$. For $k>0$, the Jordan coefficient integral is linear by [F4]; for $k=0$, evaluation is linear directly. Thus $I_M^k(a\omega +b\eta )(\sigma )=a{I}_M^k(\omega )(\sigma )+b{I}_M^k(\eta )(\sigma )$ on every simplex, and step 1.1 makes $I_M^k$ a real linear map.

For $k=0$ the value at a point simplex is exactly the function value there; for $k=1$ it is the integral of the pulled-back one-form over the closed oriented interval. Degenerate simplices remain in the supplied set and receive their actual integrals, rather than being removed. If $k>\dim M$, [F3] gives zero source and the map is zero, even though the smooth cochain space may be nonzero. Negative degrees are zero on both sides. On an empty manifold there are no simplices and the only cochain is zero. These conventions include the zero form and zero chain and require no choice.

The definition of the cochain differential, followed by integration and [F2], gives $(\delta I_M^k(\omega ))(c)=I_M^k(\omega )(\mathrm{\partial }c)={\int }_{\mathrm{\partial }c}\omega ={\int }_{c}d\omega =I_M^{k+1}(d\omega )(c)\mathrm{.}$ The same coefficients and alternating boundary signs occur in [F2] and [F3], so no sign adjustment is required.

Since step 1.1 holds for every chain, the two linear functionals are equal. Together with the degreewise real linearity in [F1], this is precisely the cochain-map identity. For $k=0$ it is the fundamental-theorem formula for values at the two endpoints of each smooth one-simplex, including constant paths. For $k=\dim M$, the form $d\omega$ is zero, and the same equality proves $\delta I_M^k(\omega )=0$ without assuming there are no higher-dimensional singular simplices.

If $k>\dim M$ or $k<0$, the form and all relevant source differentials are zero, so the identity is an equality of zero cochains; this includes the map out of degree minus one. If $M$ is empty, both complexes are zero. Zero chains and degenerate simplices were included in [F2], so they create no exception to step 1.1. Every evaluation uses a finite chain and a previously well-defined integral; no choice axiom enters.

By [F1], $\delta I_M^k(\omega )=I_M^{k+1}(d\omega )=I_M^{k+1}(0)=0$. Thus the integration cochain is a cocycle and represents a class in [F4]. If ${\omega }^{\mathrm{\prime }}=\omega +d\eta$, real linearity and [F1] give $I_M^k({\omega }^{\mathrm{\prime }})-I_M^k(\omega )=I_M^k(d\eta )=\delta I_M^{k-1}(\eta )\mathrm{.}$ The two cochains therefore represent the same smooth singular cohomology class.

To identify this with the induced-map construction in [F5], reindex the de Rham complex as $C_n={\mathrm{\Omega }}^{-n}(M)$ and the smooth cochain complex as $D_n=C_{\mathrm{\infty }}^{-n}(M;\mathbb{R})$. Keep their differentials unchanged; a differential of cochain degree $+1$ now lowers $n$ by one. Identity [F1] makes $f_n=I_M^{-n}$ a chain map. The cycles and boundaries in chain degree $-k$ are exactly the original cocycles and coboundaries in degree $k$. Consequently [F5] gives the displayed quotient map, agreeing with step 1.1 by its defining property.

On closed representatives, $[a\omega +b\eta ]$ maps to $[a{I}_M(\omega )+b{I}_M(\eta )]$ by the real linearity of [F1]. Thus the induced map is real linear. In degree zero there are no nonzero exact forms from degree minus one, and the same calculation maps a closed function to its point-evaluation cocycle. In degree one, a change by the differential of a function maps to its cochain coboundary, exactly as in step 1.1.

Negative degrees and degrees above $\dim M$ have zero de Rham source; the target above that dimension need not be zero for the induced map to be defined. On an empty manifold the source and target are both zero. Zero representatives map to zero classes, and all degenerate simplices remain part of the target complex from [F4]. No representatives are selected simultaneously: step 1.1 proves independence for arbitrary representatives, and [F5] defines the quotient map. Hence no choice is used.

Let $\sigma$ be a smooth singular $k$-simplex in $M$. By [F2], $F\circ \sigma$ is a smooth simplex in $N$: composing $F$ with one target-valued neighbourhood extension of $\sigma$ supplies its extension. Functoriality in [F3] on that domain gives ${\sigma }^{\ast }(F^{\ast }\omega )=(F\circ \sigma {)}^{\ast }\omega$ along the simplex. Their affine coefficients, and therefore their integrals in [F4], are identical. Hence $I_M^k(F^{\ast }\omega )(\sigma )={\int }_{\sigma }{F}^{\ast }\omega ={\int }_{F\circ \sigma }\omega =I_N^k(\omega )(F_{\mathrm{\#}}\sigma )=(F^{\ast }{I}_N^k(\omega ))(\sigma )\mathrm{.}$

Every chain is a finite linear combination of simplices, so step 1.1 gives equality of the two cochains. If $d\omega =0$, both sides represent cohomology classes by [F1]–[F3]. Passing to those classes yields $I_M([F^{\ast }\omega ])=[F^{\ast }{I}_N^k(\omega )]=F^{\ast }{I}_N([\omega ])\mathrm{.}$ Changing $\omega$ by $d\eta$ changes its pullback by $d{F}^{\ast }\eta$ and its integration cochain by $\delta I_N^{k-1}(\eta )$; precomposition carries the latter to $\delta F^{\ast }{I}_N^{k-1}(\eta )$. Thus the identity is independent of representatives on both routes.

In degree zero step 1.1 is the equality $(\omega \circ F)(\sigma (v_0))=\omega (F(\sigma (v_0)))$. In degree one it equates the pullback integrals on the entire closed parameter interval, with no requirement on distinct endpoints. Constant and degenerate simplices, maps wholly into a boundary, and zero forms satisfy the same coefficient identity. Negative degrees have zero source, and an empty source manifold has zero target cochain groups; an empty target admits such a map only from an empty source. All formulas are defined on each supplied simplex and finite chain, so no choices of representatives or extensions are made simultaneously.

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.

Set $H(x,t)=c+t(x-c)$. Convexity makes this target-valued for $0\le t\le 1$; its polynomial coordinate expression gives all required local extensions. Its endpoint maps are $ip$ and the identity. For a closed form $\omega$ of positive degree, the constant-map pullback is zero because its derivative is zero. Thus [F2] gives $\omega =d(L_H\omega )$. For a closed zero-form $f$, the same identity has $L_{H}f=0$ and $df=0$, so $f-f(c)=0$. Conversely constant functions are closed. Hence de Rham cohomology is zero in positive degrees and is $\mathbb{R}$ in degree zero, with evaluation at $c$ inverse to the constant-function map.

On the point $\{c\}$ there is exactly one simplex $s_j$ in every degree $j\ge 0$. For $j\ge 1$, its boundary is $({\sum }_{a=0}^j(-1{)}^a)s_{j-1}$, equal to $s_{j-1}$ when $j$ is even and zero when $j$ is odd. Therefore the cochain group is $\mathbb{R}$ in each nonnegative degree, with ${\delta }^k=0$ for even $k$ and ${\delta }^k=\mathrm{id}$ for odd $k$. This unnormalized complex has $H^0=\mathbb{R}$ and $H^k=0$ for $k>0$: in positive odd degree the kernel is zero, and in positive even degree the entire kernel is the preceding image.

The unmodified radial homotopy need not extend into a boundary target beyond the time endpoints. Use the time-flattened prism guaranteed by [F3] instead. It has the same endpoint maps and gives a degree-one chain operator $P$ with ${\mathrm{id}}_{\mathrm{\#}}-(ip{)}_{\mathrm{\#}}=\mathrm{\partial }P+P\mathrm{\partial }\mathrm{.}$ For a cochain $\phi$ of degree $k\ge 1$ set $D\phi =\phi P_{k-1}$, and set $D=0$ in degree zero. Direct evaluation gives $\delta D\phi +D\delta \phi =\phi -(ip{)}^{\ast }\phi \mathrm{.}$ In degree zero the first term is zero and the second is $\phi \mathrm{\partial }{P}_0$, so this identity still holds. No dual exactness theorem or selected cochain extension is used.

Since $pi={\mathrm{id}}_{\{c\}}$, [F6] gives $i^{\ast }{p}^{\ast }=\mathrm{id}$ on cochains of the point. Step 2.1 gives $p^{\ast }{i}^{\ast }=\mathrm{id}$ on cohomology of $V$, because the difference on any cocycle is the coboundary $\delta D\phi$. Thus $i^{\ast },p^{\ast }$ are inverse cohomology maps. More explicitly in positive degree, for a cocycle $\phi$ let $\beta =i^{\ast }\phi$. In odd degree $\beta =0$ by step 1.2, so take $\gamma =0$; in positive even degree take the preceding-degree point cochain with the same scalar value as $\beta$, so $\delta \gamma =\beta$. Then $\phi =\delta (D\phi +p^{\ast }\gamma )\mathrm{.}$ This proves positive-degree vanishing without a representative-selection principle. In degree zero, evaluation at $c$ and constant cochains give the inverse identifications with $\mathbb{R}$.

By [F5], integration sends the constant function $a$ to the cochain with value $a$ on every point simplex. Thus the degree-zero map is the identity under the two identifications with $\mathbb{R}$ in steps 1.1 and 3.1. In every positive degree both groups vanish, so their unique linear map is an isomorphism; negative degrees are zero by the complex conventions. A coordinate diffeomorphism and its inverse give inverse pullback maps in both theories, and [F1] transports these conclusions to the coordinate domain.

Nonemptiness is used only to fix one contraction centre; the empty domain instead has zero groups on both sides and still a comparison isomorphism, but not the asserted degree-zero identification with $\mathbb{R}$. For $n=0$ the nonempty domain is a point, already calculated in step 1.2, and all positive-degree forms vanish. Degree one is covered by the zero odd-degree kernel at the point and the explicit primitive formulas. Constant and degenerate simplices are retained throughout. The endpoint flattening in step 2.1 preserves $c$ and $x$, and [F2] handles both endpoints for forms. A single centre and explicit operators suffice; no choices over families of domains or cohomology classes are made.

Under [F3], apply [F2] to the two-member cover to obtain smooth functions ${\rho }_U,{\rho }_V\ge 0$ with sum one and supports contained in $U,V$ respectively. If the construction is presented as a locally finite refinement, group a term into $U$ whenever its closed support lies in $U$, and into $V$ otherwise. A subfamily of a locally finite closed family has closed union: near any point only finitely many members meet a neighbourhood, and the finite union is closed there. Thus each grouped sum is smooth with its support still in the assigned open. This gives the asserted pair in the refinement convention as well. Countable choice is spent only in [F2]'s selection of a countable subordinate chart family, its shrinking data and bumps; none of the subsequent steps selects a partition or primitive for each form.

Restriction commutes with $d$ by [F1], so $r,s$ are real cochain maps. If $r\omega =0$, it vanishes at every point of the cover, so $r$ is injective. Also $sr=0$. If $s(\alpha ,\beta )=0$, the forms agree on $W$ and define one form on $M$ by their values on the two opens. Each point has a neighbourhood where it is one of those smooth forms, including at boundary points. This form restricts to $(\alpha ,\beta )$, proving $\ker s=\mathrm{im}r$.