[proofplan] The Hodge star is defined as the unique linear map $\star: \Lambda^p T_x^* M \to \Lambda^{n-p} T_x^* M$ satisfying $\alpha \wedge \star\beta = (\alpha, \beta)_g \, \omega_g$ for all $\alpha, \beta \in \Lambda^p T_x^* M$, where $(\cdot, \cdot)_g$ is the metric on $\Lambda^p$ induced by $g$ and $\omega_g$ is the Riemannian volume form. We verify the basis formula by substituting the candidate $\star \omega_I = \omega_{I^c}$ (with the sign fixed by the volume-form ordering) into the defining identity, evaluating against every basis multivector $\omega_J$ with $|J| = p$, and using orthonormality of the coframe to compute both sides explicitly. The case $J = I$ produces $\omega_g$ on each side; for $J \neq I$ both sides vanish because the wedge product contains a repeated factor. [/proofplan]

[step:Set up the orthonormal coframe and the basis of $\Lambda^p T_x^* M$] Fix $x \in M$ and an orthonormal coframe $\omega_1, \ldots, \omega_n$ for $T_x^* M$, meaning $(\omega_i, \omega_j)_g = \delta_{ij}$ where $(\cdot, \cdot)_g$ denotes the inner product on $T_x^* M$ induced by $g_x$ (musical isomorphism). The volume form at $x$ is \begin{align*} \omega_g = \omega_1 \wedge \omega_2 \wedge \cdots \wedge \omega_n, \end{align*} oriented so that $(\omega_1, \ldots, \omega_n)$ is positively oriented. For each strictly increasing index set $K = \{k_1 < \cdots < k_p\} \subseteq \{1, \ldots, n\}$, write \begin{align*} \omega_K := \omega_{k_1} \wedge \omega_{k_2} \wedge \cdots \wedge \omega_{k_p} \in \Lambda^p T_x^* M. \end{align*} The collection $\{\omega_K : K \subseteq \{1,\ldots,n\}, |K| = p\}$ is a basis of $\Lambda^p T_x^* M$, and the induced inner product on $\Lambda^p T_x^* M$ — extended from $(\omega_i, \omega_j)_g = \delta_{ij}$ to $\Lambda^p$ via the determinant formula — satisfies \begin{align*} (\omega_K, \omega_L)_g = \det\big[(\omega_{k_a}, \omega_{l_b})_g\big]_{a,b} = \delta_{KL}, \end{align*} where $\delta_{KL} = 1$ if $K = L$ and $0$ otherwise. Hence $\{\omega_K\}$ is an orthonormal basis of $\Lambda^p T_x^* M$. [/step]

[step:State the defining identity for $\star$ as a linear map] The Hodge star is the unique linear map \begin{align*} \star : \Lambda^p T_x^* M &\to \Lambda^{n-p} T_x^* M \end{align*} characterised by the identity \begin{align*} \alpha \wedge \star \beta = (\alpha, \beta)_g \cdot \omega_g \qquad \text{for all } \alpha, \beta \in \Lambda^p T_x^* M. \end{align*} Since $\{\omega_K\}_{|K|=p}$ is a basis, the map $\star$ is determined by its values on each $\omega_K$, and the defining identity for fixed $\beta = \omega_K$ is determined by its values against each basis element $\alpha = \omega_J$, $|J| = p$. Therefore $\star \omega_K$ is the unique $(n-p)$-form $\eta_K$ such that \begin{align*} \omega_J \wedge \eta_K = (\omega_J, \omega_K)_g \cdot \omega_g = \delta_{JK} \cdot \omega_g \qquad \text{for every } J \subseteq \{1,\ldots,n\} \text{ with } |J| = p. \end{align*} Our task is to show that the candidate $\eta_K := \omega_{K^c}$ — where $K^c = \{j_1 < \cdots < j_{n-p}\} = \{1,\ldots,n\} \setminus K$ is the increasing complement — satisfies this identity, after fixing the sign so that $\omega_K \wedge \omega_{K^c} = \omega_g$. [/step]

[step:Define the sign $\varepsilon(K)$ and write the candidate $\star \omega_K = \varepsilon(K) \, \omega_{K^c}$]For each increasing $K \subseteq \{1,\ldots,n\}$ with $|K| = p$, the wedge $\omega_K \wedge \omega_{K^c}$ uses each $\omega_i$ exactly once and equals a signed multiple of $\omega_g$: \begin{align*} \omega_K \wedge \omega_{K^c} = \varepsilon(K) \cdot \omega_g, \end{align*} where $\varepsilon(K) \in \{+1, -1\}$ is the sign of the permutation $(k_1, \ldots, k_p, j_1, \ldots, j_{n-p})$ relative to $(1, 2, \ldots, n)$ (the *shuffle sign* of $K$). For the special case $K = \{1, \ldots, p\}$, no shuffles are required and $\varepsilon(K) = +1$, giving $\omega_K \wedge \omega_{K^c} = \omega_g$ directly. We define \begin{align*} \star \omega_K := \varepsilon(K) \cdot \omega_{K^c} \in \Lambda^{n-p} T_x^* M, \end{align*} and extend linearly to all of $\Lambda^p T_x^* M$. We now verify that this $\star \omega_K$ satisfies the defining identity $\omega_J \wedge \star \omega_K = \delta_{JK} \omega_g$.[/step]

[guided]What should $\star \omega_K$ be? The defining identity at $\beta = \omega_K$ requires that $\star \omega_K$ is some $(n-p)$-form whose wedge against each $\omega_J$ ($|J|=p$) equals $\delta_{JK} \omega_g$. In particular, taking $J = K$ gives $\omega_K \wedge \star \omega_K = (\omega_K, \omega_K)_g \omega_g = \omega_g$. So we need an $(n-p)$-form that, wedged with $\omega_K$, produces $\omega_g$. The natural candidate is the basis $(n-p)$-form built from the indices *not* in $K$, namely $\omega_{K^c}$ — this is the unique basis multivector whose wedge with $\omega_K$ uses each $\omega_i$ exactly once and is therefore proportional to $\omega_g$. We compute the proportionality constant. For increasing $K = \{k_1 < \cdots < k_p\}$ with complement $K^c = \{j_1 < \cdots < j_{n-p}\}$, the wedge $\omega_K \wedge \omega_{K^c} = \omega_{k_1} \wedge \cdots \wedge \omega_{k_p} \wedge \omega_{j_1} \wedge \cdots \wedge \omega_{j_{n-p}}$ uses each $\omega_i$ exactly once. To match the canonical order $(1, 2, \ldots, n)$ defining $\omega_g$, we permute, picking up a sign equal to the sign of the permutation $(k_1, \ldots, k_p, j_1, \ldots, j_{n-p})$ relative to $(1, 2, \ldots, n)$. Call this sign $\varepsilon(K) \in \{+1, -1\}$ (the *shuffle sign* of $K$). Then \begin{align*} \omega_K \wedge \omega_{K^c} = \varepsilon(K) \cdot \omega_g. \end{align*} For the special case $K = \{1, \ldots, p\}$, the tuple $(1, \ldots, p, p+1, \ldots, n)$ is already in canonical order, no shuffles are required, and $\varepsilon(K) = +1$, so $\omega_K \wedge \omega_{K^c} = \omega_g$ directly. This forces the sign in the definition of $\star$. Writing $\star \omega_K = c \cdot \omega_{K^c}$ for an unknown scalar $c$, the defining identity at $J = K$ reads $c \cdot \omega_K \wedge \omega_{K^c} = \omega_g$, i.e., $c \cdot \varepsilon(K) \omega_g = \omega_g$, forcing $c = \varepsilon(K)$ (since $\varepsilon(K)^2 = 1$). We therefore *define* \begin{align*} \star \omega_K := \varepsilon(K) \cdot \omega_{K^c} \in \Lambda^{n-p} T_x^* M, \end{align*} and extend linearly to all of $\Lambda^p T_x^* M$. The next two steps verify that this $\star \omega_K$ does satisfy the full defining identity $\omega_J \wedge \star \omega_K = \delta_{JK} \omega_g$ for every $J$, not just $J = K$. The hypothesis stated in the theorem — "$I$ and $I^c$ arranged so that $\omega_{i_1} \wedge \cdots \wedge \omega_{i_p} \wedge \omega_{j_1} \wedge \cdots \wedge \omega_{j_{n-p}} = \omega_g$" — is precisely the assertion $\varepsilon(I) = +1$. Under that hypothesis the formula simplifies to $\star \omega_I = \omega_{I^c}$, with no sign. The case $I = \{1, \ldots, p\}$ in the theorem's first display has $I^c = \{p+1, \ldots, n\}$, $\varepsilon(I) = +1$, and recovers $\star(\omega_1 \wedge \cdots \wedge \omega_p) = \omega_{p+1} \wedge \cdots \wedge \omega_n$ as a special case.[/guided]

[step:Verify the defining identity for $J = K$] For $J = K$, evaluate the wedge: \begin{align*} \omega_K \wedge \star \omega_K = \omega_K \wedge \big[ \varepsilon(K) \cdot \omega_{K^c} \big] = \varepsilon(K) \cdot (\omega_K \wedge \omega_{K^c}) = \varepsilon(K) \cdot \varepsilon(K) \cdot \omega_g = \omega_g, \end{align*} where the last equality uses $\varepsilon(K)^2 = 1$. On the other side, $(\omega_K, \omega_K)_g \cdot \omega_g = 1 \cdot \omega_g = \omega_g$. The two sides agree: \begin{align*} \omega_K \wedge \star \omega_K = (\omega_K, \omega_K)_g \cdot \omega_g. \end{align*} [/step]

[step:Verify the defining identity for $J \neq K$ via repeated factors]Fix increasing $J, K \subseteq \{1, \ldots, n\}$ with $|J| = |K| = p$ and $J \neq K$. We compute \begin{align*} \omega_J \wedge \star \omega_K = \varepsilon(K) \cdot \omega_J \wedge \omega_{K^c}. \end{align*} Since $J \neq K$, the set $J$ is not the increasing complement of $K^c$, so $J \cap K^c \neq \varnothing$: pick any $i \in J \cap K^c$. Then $\omega_i$ appears as a factor in $\omega_J$ and again as a factor in $\omega_{K^c}$. The wedge product of any multivector containing $\omega_i$ twice vanishes by skew-symmetry of $\wedge$: \begin{align*} \omega_J \wedge \omega_{K^c} = 0. \end{align*} (Justification of $J \cap K^c \neq \varnothing$: if $J \cap K^c = \varnothing$, then $J \subseteq K$, and since $|J| = |K|$ this forces $J = K$, contradicting $J \neq K$.) Therefore $\omega_J \wedge \star \omega_K = 0$. On the other side of the defining identity, \begin{align*} (\omega_J, \omega_K)_g \cdot \omega_g = \delta_{JK} \cdot \omega_g = 0 \end{align*} since $J \neq K$. The two sides agree.[/step]

[guided]We need to check that the candidate $\star \omega_K = \varepsilon(K) \omega_{K^c}$ satisfies the defining identity not only at $J = K$ (handled in the previous step) but at *every* $J$ with $|J| = p$. The strategy is to show that both sides of $\omega_J \wedge \star \omega_K = (\omega_J, \omega_K)_g \omega_g$ vanish whenever $J \neq K$ — for the same structural reason on each side. Fix increasing $J, K \subseteq \{1, \ldots, n\}$ with $|J| = |K| = p$ and $J \neq K$. Pulling out the scalar $\varepsilon(K)$, \begin{align*} \omega_J \wedge \star \omega_K = \omega_J \wedge \big[\varepsilon(K) \omega_{K^c}\big] = \varepsilon(K) \cdot \omega_J \wedge \omega_{K^c}. \end{align*} Why does $\omega_J \wedge \omega_{K^c}$ vanish? The wedge is a $p$-fold wedge times an $(n-p)$-fold wedge, so it lives in $\Lambda^n T_x^* M$, a one-dimensional space spanned by $\omega_g$. The wedge equals a non-zero multiple of $\omega_g$ if and only if it uses each coframe element $\omega_i$ exactly once — equivalently, $J \sqcup K^c = \{1, \ldots, n\}$, i.e., $J = K$. Whenever $J \neq K$ some index is repeated, and the wedge vanishes by skew-symmetry. Concretely: if $J \neq K$, then since $|J| = |K|$, $J$ cannot be contained in $K$ (otherwise $J = K$), so $J \cap K^c \neq \varnothing$. Pick any $i \in J \cap K^c$; then $\omega_i$ appears as a factor in $\omega_J$ and again in $\omega_{K^c}$, and \begin{align*} \omega_J \wedge \omega_{K^c} = 0. \end{align*} Therefore $\omega_J \wedge \star \omega_K = 0$. On the right-hand side of the defining identity, the same disjointness condition appears through orthogonality: by the determinant formula for the induced inner product on $\Lambda^p T_x^* M$, $(\omega_J, \omega_K)_g = \det[(\omega_{j_a}, \omega_{k_b})_g]_{a,b} = \delta_{JK}$, since the matrix is a permutation matrix exactly when $J = K$ and otherwise has a zero row. So \begin{align*} (\omega_J, \omega_K)_g \cdot \omega_g = \delta_{JK} \cdot \omega_g = 0 \end{align*} since $J \neq K$. Both sides vanish, and the defining identity holds at $(J, K)$ with $J \neq K$. The structural moral: $\omega_J$ and $\omega_K$ "use up" different subsets of the coframe, and the wedge $\omega_J \wedge \omega_{K^c}$ vanishes precisely because the disjoint union $J \sqcup K^c$ fails to be all of $\{1, \ldots, n\}$ exactly once. The orthogonality $(\omega_J, \omega_K)_g = \delta_{JK}$ reflects exactly the same disjointness condition through the determinant formula — which is why both sides of the defining identity vanish in lockstep.[/guided]

[step:Combine the two cases to conclude] For every $J, K$ with $|J| = |K| = p$, \begin{align*} \omega_J \wedge \star \omega_K = \delta_{JK} \cdot \omega_g = (\omega_J, \omega_K)_g \cdot \omega_g. \end{align*} Both sides of $\alpha \wedge \star \beta = (\alpha, \beta)_g \omega_g$ are bilinear in $(\alpha, \beta)$, and the basis $\{\omega_J\} \times \{\omega_K\}$ generates $\Lambda^p T_x^* M \times \Lambda^p T_x^* M$. Hence the identity extends by bilinearity to all $\alpha, \beta \in \Lambda^p T_x^* M$, and the defined map $\star: \Lambda^p T_x^* M \to \Lambda^{n-p} T_x^* M$ with \begin{align*} \star \omega_K = \varepsilon(K) \cdot \omega_{K^c} \end{align*} satisfies the defining identity for the Hodge star. By uniqueness of $\star$ (the identity $\alpha \wedge \star \beta = (\alpha, \beta)_g \omega_g$ characterises $\star \beta$ for each $\beta$, since the linear functional $\alpha \mapsto (\alpha, \beta)_g \omega_g$ has a unique representative under the perfect pairing $\Lambda^p \otimes \Lambda^{n-p} \to \Lambda^n \cong \mathbb{R}$ provided by $\wedge$), this is the Hodge star. In particular, taking $K = \{1, \ldots, p\}$ gives $\varepsilon(K) = +1$, $K^c = \{p+1, \ldots, n\}$, and \begin{align*} \star(\omega_1 \wedge \cdots \wedge \omega_p) = \omega_{p+1} \wedge \cdots \wedge \omega_n. \end{align*} For general $I = \{i_1 < \cdots < i_p\}$ ordered so that $\omega_{i_1} \wedge \cdots \wedge \omega_{i_p} \wedge \omega_{j_1} \wedge \cdots \wedge \omega_{j_{n-p}} = \omega_g$ — i.e., $\varepsilon(I) = +1$ — the formula reads \begin{align*} \star(\omega_{i_1} \wedge \cdots \wedge \omega_{i_p}) = \omega_{j_1} \wedge \cdots \wedge \omega_{j_{n-p}}, \end{align*} as claimed. This completes the proof. [/step]