Finite chart localization gives choice-free integration and compact Stokes

For every $p\in K$, take a chart about $p$ and choose concentric coordinate balls $B_r\subseteq {\bar{B}}_r\subseteq B_R$ whose closed larger ball lies in the chart image. Put $U_p={\varphi }^{-1}(B_r)$; it is connected, and its closure lies in the compact set ${\varphi }^{-1}({\bar{B}}_r)$ by [F1]. Apply the bump lemma in [F1] with prescribed open set $U_p$. Its support is closed, lies in $U_p$, and is therefore a closed subset of the displayed compact chart-ball image, hence compact by the ambient-cover criterion [F3]. Consider the set of all such chart-and-bump tuples and their open sets $V_b=\{b>1\mathrm{/}2\}$. They cover $K$ without selecting a tuple as a function of $p$. By [F3] retain finitely many tuples, with bumps $b_1,\dots ,b_m$. For $K=\mathrm{\varnothing }$ use no tuples. In dimension zero use the singleton chart, whose image and support are compact.

First establish the comparison of chart integrals without a global partition. Suppose a top form $\zeta$ has compact support contained in two connected charts $\varphi ,\psi$. On their overlap let $G=\psi {\varphi }^{-1}$. It is a diffeomorphism between Euclidean-open sets; its inverse is the specified reverse chart transition. If $f_x,f_y$ are the two top coefficients, [F9] gives $f_x=(f_y\circ G)\det DG$. The orientation signs satisfy ${\sigma }_{\varphi }\det DG={\sigma }_{\psi }\mathrm{\mid }\det DG\mathrm{\mid }$ by the signed-frame convention of [F4]. The zero-extended target coefficient has compact support inside $\psi (U\cap V)$, and its transformed zero extension is the source coefficient. Therefore [F5] gives $I_{\varphi }(\zeta )=I_{\psi }(\zeta )$ with precisely these signs. No localization of the transition is necessary on a boundaryless manifold. When $n=0$, a connected chart is one point and both values are the same signed evaluation in [F4].

In the nonempty case put $B={\sum }_i{b}_i$ and $\theta =s(4B-1)$. Since $B>1\mathrm{/}2$ on ${\bigcup }_i{V}_{b_i}$, $\theta =1$ on this neighbourhood of $K$. Define ${\chi }_i=\theta b_i\mathrm{/}B$ on $B>0$ and zero on $B=0$. This is smooth, because $\theta =0$ on $B\le 1\mathrm{/}4$, so the quotient is identically zero on a whole neighbourhood of the potential denominator-zero set. Each ${\chi }_i$ is nonnegative, has support in $\mathrm{supp}{b}_i$, and ${\sum }_i{\chi }_i=\theta$. The supports are closed subsets of the compact supports of the $b_i$, so compact by the ambient-cover criterion [F3]: add the open complement of the smaller closed support to a covering family and then discard it from a finite subcover. This proves the finite localization assertion.

Given two finite localizations $({\chi }_i,{\varphi }_i)$ and $({\tau }_j,{\psi }_j)$ near $\mathrm{supp}\omega$, the identities ${\chi }_i\omega ={\sum }_j{\chi }_i{\tau }_j\omega$ and ${\tau }_j\omega ={\sum }_i{\chi }_i{\tau }_j\omega$ hold globally: on the support both sums of cutoffs equal one, and off it $\omega =0$. Each product has compact support in the intersection of its two chart domains. By step 1.2 its chart integrals agree, so finite linearity [F6] gives ${\sum }_i{I}_{{\varphi }_i}({\chi }_i\omega )={\sum }_{i,j}{I}_{{\varphi }_i}({\chi }_i{\tau }_j\omega )={\sum }_{i,j}{I}_{{\psi }_j}({\chi }_i{\tau }_j\omega )={\sum }_j{I}_{{\psi }_j}({\tau }_j\omega )\mathrm{.}$ In dimension zero the same calculation is finite scalar distributivity. Thus ${\mathcal{I}}_M$ is well defined. In particular, for a chart-supported form its value is its single chart integral: insert a cutoff identically one near its compact support using step 2.1 inside that chart, and compare.

For two forms, their compact supports have compact union by [F3], taking finite subcovers of each and uniting them. Use a single localization near this union; [F6] then proves ${\mathcal{I}}_M(a\omega +b\zeta )=a{\mathcal{I}}_M(\omega )+b{\mathcal{I}}_M(\zeta )$, with step 3.1 removing the temporary localization. If an open $U$ contains the support, make the tuples in step 1.1 lie in $U$. The same finite chart integrals compute the restriction integral on $U$ and the integral on $M$, and step 3.1 proves locality. Compactness of the support in either ambient follows from [F3] and its unchanged subspace topology.

Suppose $n\ge 2$ and $\eta$ has compact support in one chart. Its coordinate form extends smoothly by zero to ${\mathbb{R}}^n$: off the compact coordinate support it vanishes, and that support is contained in the chart image, so the chart image and its complement-of-support open set give agreeing smooth expressions. Write this extension as $\tilde{\eta }={\sum }_{j=1}^n(-1{)}^{j-1}{f}_{j}d{x}_1\wedge \cdots \wedge \widehat{d{x}_j}\wedge \cdots \wedge d{x}_n\mathrm{.}$ By [F9], its derivative coefficient is ${\sum }_j{\mathrm{\partial }}_j{f}_j$. The increasing open cubes cover the finite union of the compact coefficient supports, so [F3] gives a large bounding rectangle with every $f_j$ supported strictly inside it. Its coefficients and derivatives are smooth and therefore integrable there by [F10], as are all their coordinate sections. For fixed other coordinates, [F8] gives $\int {\mathrm{\partial }}_j{f}_{j}d{x}_j=0$, because both endpoint values vanish. Applying [F7] to these sections and summing by [F6] yields ${\int }_{{\mathbb{R}}^n}d\tilde{\eta }=0$. The chart sign in [F4] only multiplies zero, and step 3.1 proves ${\mathcal{I}}_M(d\eta )=0$. For $n=1$ the same calculation is just [F8] for a compactly supported function, so no zero-dimensional Fubini assertion is used.

For an arbitrary compactly supported $(n-1)$-form, use step 2.1 near its support to write $\eta ={\sum }_i{\chi }_i\eta$. Each summand has compact support in one chart, and linearity of $d$ gives $d\eta ={\sum }_{i}d({\chi }_i\eta )$. Each term has integral zero by step 4.2; finite linearity from step 4.1 proves ${\mathcal{I}}_M(d\eta )=0$. The cutoff derivatives cause no omitted terms: differentiating the exact finite identity for $\eta$ includes all of them.

For $n=0$ the singleton cover and [F3] make every compact support finite. Chart integration [F4] then gives precisely the asserted signed sum, independent of its listing. The derivative-zero clause is asserted only for $n\ge 1$; with the zero negative-degree convention it also has a vacuous zero input at $n=0$. Empty support, empty manifold and zero forms give empty sums and value zero. The first derivative calculation includes all rectangle endpoints, and no connectedness, compactness of $M$, or infinite choice was assumed. Only finitely many tuples over one compact support and the explicit normalized cutoffs were used.