Riemannian inner product of compactly supported forms

Given: Compactly supported real forms $\alpha ,\beta$ of one fixed degree, and countable choice.

Hodge star is a smooth bundle isomorphism: The Hodge star exists uniquely and is a smooth bundle isomorphism in every degree $0\le k\le n$.

Riemannian volume of a compactly supported smooth density: Assume countable choice. For smooth compactly supported $f$, define ${\int }_{M}f{\mu }_g$ by the intrinsic smooth density integral. More generally every compactly supported signed smooth density $\sigma$ has its existing intrinsic integral, independently of a Riemannian metric. lem-the-riemannian-volume-density-is-coordinate-independent makes $f{\mu }_g$ a smooth compactly supported density. Apply def-integral-of-a-compactly-supported-smooth-density and thm-density-integration-is-defined-without-an-orientation; def-countable-choice is inherited precisely at chart-partition selection. In a chart the summand is the integral of the partition-weighted coefficient $f\sqrt{\det G}$. On a zero-manifold it is the finite sum of scalar density values, and empty support gives zero. No orientation is required.

Positivity of the oriented integral: Let $\omega \in {\mathrm{\Omega }}_c^n(M)$ be nonnegative on the positive determinant ray of an oriented smooth manifold. Then ${\int }_M\omega \ge 0$, and $\omega \mathrm{\ne }0$ implies ${\int }_M\omega >0$.

The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$): The Axiom of Countable Choice, written ${\mathrm{A}\mathrm{C}}_{\omega }$, is the following statement. > For every family $(X_n{)}_{n\in \mathbb{N}}$ of nonempty sets indexed by > $\mathbb{N}$ there is a function $f$ with domain $\mathbb{N}$ such that > $f(n)\in X_n$ for every $n\in \mathbb{N}$. Equivalently, in the vocabulary of def-choice-function: every at most countable family of nonempty sets (def-countable) has a choice function.

Riemannian hodge star: On an oriented Riemannian $n$-manifold, for $0\le k\le n$ the Hodge star is characterized by $\alpha \wedge \ast \beta =⟨\alpha ,\beta {⟩}_g{\mathrm{vol}}_g$ for every pair of $k$-covectors.