[proofplan] We argue by contradiction. If $\mathcal{H}^p$ were infinite-dimensional, Gram–Schmidt produces an infinite $L^2$-orthonormal sequence $(e_n) \subset \mathcal{H}^p$. Each $e_n$ is harmonic, so $\Delta e_n = 0$, and $\|e_n\|_g = 1$. The sequence then satisfies the hypotheses of the [Compactness Theorem](/theorems/2748) (uniform $L^2$-bounds on the form and its Laplacian), which produces an $L^2$-Cauchy subsequence. But the orthonormality of $(e_n)$ forces $\|e_n - e_m\|_g^2 = 2$ whenever $n \neq m$, so no subsequence can be $L^2$-Cauchy — contradiction. [/proofplan] [step:Assume $\mathcal{H}^p$ is infinite-dimensional and produce an orthonormal sequence] Let $(M, g)$ be a compact oriented Riemannian manifold without boundary, and let $\mathcal{H}^p := \{\alpha \in \Omega^p(M) : \Delta\alpha = 0\}$ denote the space of harmonic $p$-forms. Equip $\mathcal{H}^p$ with the global $L^2$ inner product \begin{align*} \langle\langle \cdot, \cdot \rangle\rangle_g : \Omega^p(M) \times \Omega^p(M) &\to \mathbb{R}, \\ (\eta, \xi) &\mapsto \int_M (\eta, \xi)_g \, \omega_g, \end{align*} where $(\cdot, \cdot)_g$ is the fibrewise inner product on $\Lambda^p T^*M$ and $\omega_g$ is the Riemannian volume form. Write $\|\eta\|_g := \langle\langle \eta, \eta \rangle\rangle_g^{1/2}$. Suppose, for contradiction, that $\dim \mathcal{H}^p = \infty$. Then $\mathcal{H}^p$ contains a linearly independent sequence $(v_n)_{n \ge 1}$. Apply the Gram–Schmidt orthonormalisation procedure with respect to $\langle\langle \cdot, \cdot \rangle\rangle_g$: define inductively \begin{align*} \tilde e_n &:= v_n - \sum_{k=1}^{n-1} \langle\langle v_n, e_k \rangle\rangle_g \, e_k, \qquad e_n := \tilde e_n / \|\tilde e_n\|_g. \end{align*} The vectors $\tilde e_n$ are non-zero by linear independence of $(v_n)$, so the procedure is well-defined. The resulting sequence $(e_n) \subset \mathcal{H}^p$ satisfies \begin{align*} \langle\langle e_n, e_m \rangle\rangle_g = \delta_{nm}, \qquad \|e_n\|_g = 1 \quad \text{for all } n \ge 1. \end{align*} Each $e_n$ is a finite linear combination of harmonic forms, hence harmonic: $\Delta e_n = 0$. [/step] [step:Verify the hypotheses of the Compactness Theorem with constant $C = 1$] The [Compactness Theorem](/theorems/2748) states: any sequence $(\alpha_n) \subset \Omega^p(M)$ satisfying \begin{align*} \|\alpha_n\|_g \le C, \qquad \|\Delta \alpha_n\|_g \le C \end{align*} for some constant $C > 0$ independent of $n$ admits an $L^2$-Cauchy subsequence. We verify both hypotheses for $(e_n)$ with $C := 1$: (i) $\|e_n\|_g = 1 \le 1$ by construction. (ii) $\|\Delta e_n\|_g = \|0\|_g = 0 \le 1$ since $e_n \in \mathcal{H}^p$. Therefore the [Compactness Theorem](/theorems/2748) applies and produces a subsequence $(e_{n_k})_{k \ge 1}$ that is Cauchy in the $L^2$-norm $\|\cdot\|_g$. [guided] We want to feed our orthonormal sequence $(e_n)$ into the [Compactness Theorem](/theorems/2748) to extract an $L^2$-Cauchy subsequence. To do this we must verify the theorem's hypotheses, which require a single constant $C > 0$ such that \begin{align*} \|\alpha_n\|_g \le C, \qquad \|\Delta \alpha_n\|_g \le C \end{align*} hold uniformly in $n$. Why must we check both, when they look immediate? Because the contradiction we are about to derive collapses if either hypothesis fails — the [Compactness Theorem](/theorems/2748) is the only mechanism producing the Cauchy subsequence, and Gram–Schmidt alone gives us nothing about Laplacians. We claim $C := 1$ works. We verify the two hypotheses in turn. (i) The form bound. By construction in Step 1, the Gram–Schmidt output satisfies $\|e_n\|_g = 1$ for all $n \ge 1$. Hence $\|e_n\|_g \le 1$ trivially. (ii) The Laplacian bound. Each $e_n$ is a finite linear combination of harmonic forms (each $v_k$ lies in $\mathcal{H}^p$, and Gram–Schmidt only takes linear combinations), so $\Delta e_n = 0$ as elements of $\Omega^p(M)$. Therefore $\|\Delta e_n\|_g = \|0\|_g = 0 \le 1$. Both bounds hold with the single constant $C = 1$, independent of $n$, so the [Compactness Theorem](/theorems/2748) applies and yields a subsequence $(e_{n_k})_{k \ge 1}$ that is Cauchy in the $L^2$-norm $\|\cdot\|_g$. A remark on what makes this step work. The [Compactness Theorem](/theorems/2748) is the deep input: it rests on Garding's inequality for the Hodge Laplacian, which produces an $H^1$-bound on $e_n$ from $L^2$-bounds on $e_n$ and $\Delta e_n$, and on the Rellich–Kondrachov compact embedding $H^1 \hookrightarrow\hookrightarrow L^2$. Because $M$ is compact, this embedding is global and yields an $L^2$-Cauchy subsequence of any $H^1$-bounded sequence on $M$. The harmonic hypothesis is what makes the Laplacian bound free; without it, an arbitrary orthonormal sequence in $L^2(\Lambda^p T^*M)$ has no reason to satisfy a uniform Laplacian bound, and indeed the unit ball of $L^2$ is not compact. [/guided] [/step] [step:Derive a contradiction from orthonormality] Compute the squared $L^2$-distance between any two distinct elements of the orthonormal sequence: for $n \neq m$, \begin{align*} \|e_n - e_m\|_g^2 &= \langle\langle e_n - e_m, e_n - e_m \rangle\rangle_g \\ &= \langle\langle e_n, e_n \rangle\rangle_g - 2\langle\langle e_n, e_m \rangle\rangle_g + \langle\langle e_m, e_m \rangle\rangle_g \\ &= 1 - 0 + 1 = 2. \end{align*} In particular, applied to the subsequence $(e_{n_k})$ extracted in the previous step, $\|e_{n_k} - e_{n_\ell}\|_g^2 = 2$ for all $k \neq \ell$. Hence \begin{align*} \|e_{n_k} - e_{n_\ell}\|_g = \sqrt{2} \not\to 0 \qquad \text{as } k, \ell \to \infty, \end{align*} so $(e_{n_k})$ is not Cauchy in $\|\cdot\|_g$. This contradicts the conclusion of Step 2, which produced an $L^2$-Cauchy subsequence. The assumption $\dim \mathcal{H}^p = \infty$ is therefore false, and $\mathcal{H}^p$ is finite-dimensional. [guided] We have a Cauchy subsequence $(e_{n_k})$ from Step 2 — but the orthonormality from Step 1 will turn out to forbid this. The plan is to compute the $L^2$-distance between any two distinct elements of $(e_n)$ and show that it is bounded below by a positive constant; this is then inherited by every subsequence and contradicts the Cauchy property. We compute. For $n \neq m$, expand the squared norm using the bilinearity of $\langle\langle \cdot, \cdot \rangle\rangle_g$: \begin{align*} \|e_n - e_m\|_g^2 &= \langle\langle e_n - e_m, e_n - e_m \rangle\rangle_g \\ &= \langle\langle e_n, e_n \rangle\rangle_g - 2\langle\langle e_n, e_m \rangle\rangle_g + \langle\langle e_m, e_m \rangle\rangle_g. \end{align*} Now we plug in the orthonormality relations from Step 1: $\langle\langle e_n, e_n \rangle\rangle_g = 1$, $\langle\langle e_m, e_m \rangle\rangle_g = 1$, and $\langle\langle e_n, e_m \rangle\rangle_g = 0$. The cross-term vanishes — this is the crucial rigidity, and it is what makes the orthonormal sequence so far apart in $L^2$. We obtain \begin{align*} \|e_n - e_m\|_g^2 = 1 - 0 + 1 = 2. \end{align*} Now apply this to the subsequence $(e_{n_k})$ extracted in Step 2. The indices $n_k$ are pairwise distinct, so for any $k \neq \ell$ we have $n_k \neq n_\ell$, and the computation above gives $\|e_{n_k} - e_{n_\ell}\|_g^2 = 2$. Taking square roots, \begin{align*} \|e_{n_k} - e_{n_\ell}\|_g = \sqrt{2} \qquad \text{for all } k \neq \ell. \end{align*} In particular, $\|e_{n_k} - e_{n_\ell}\|_g \not\to 0$ as $k, \ell \to \infty$ — the difference is the constant $\sqrt{2}$, not a small quantity. But a Cauchy sequence requires that for every $\varepsilon > 0$ there is an index beyond which all pairwise differences have norm less than $\varepsilon$. Choosing $\varepsilon = 1 < \sqrt{2}$ shows this fails: no tail of $(e_{n_k})$ has all pairwise differences bounded by $1$, since they are all exactly $\sqrt{2}$. Hence $(e_{n_k})$ is not Cauchy in $\|\cdot\|_g$, contradicting the conclusion of Step 2 that produced an $L^2$-Cauchy subsequence. The contradiction forces our standing assumption $\dim \mathcal{H}^p = \infty$ to be false. Therefore $\mathcal{H}^p$ is finite-dimensional, completing the proof. This is the standard "infinite-dimensional unit balls are non-compact" obstruction: a Hilbert space is finite-dimensional if and only if its closed unit ball is compact in the norm topology, equivalently if and only if every bounded sequence has a Cauchy subsequence. The [Compactness Theorem](/theorems/2748) tells us that bounded sequences with bounded Laplacians do have Cauchy subsequences in $L^2$, even though the unit ball of $L^2(\Lambda^p T^*M)$ is not compact. Restricting this conclusion to harmonic forms — where the Laplacian condition is automatic — promotes "bounded sequence in $\mathcal{H}^p$" to "has a Cauchy subsequence", forcing the unit ball of $\mathcal{H}^p$ (as a subspace of $L^2$) to be compact and hence $\mathcal{H}^p$ to be finite-dimensional. [/guided] [/step]