TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-29

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Hodge star exists uniquely and is given by the complementary-basis formula in an oriented orthonormal basis

Statement

Let $V$ be an oriented finite-dimensional real inner product space of dimension $n$ . For every degree $0 \leq k \leq n$ there is a unique linear map $⋆ : Λ^{k} V \to Λ^{n - k} V$ satisfying

$α \land ⋆ β = ⟨ α, β ⟩ ω for all α, β \in Λ^{k} V,$

where $ω$ is the oriented unit volume form of The oriented unit volume form. If $(e_{1}, \dots, e_{n})$ is a positively oriented orthonormal basis and $I = {i_{1} < \dots < i_{k}}$ has complement $I^{c} = {i_{1}^{c} < \dots < i_{n - k}^{c}}$ , let $ε_{I}$ be the sign of the permutation $(i_{1}, \dots, i_{k}, i_{1}^{c}, \dots, i_{n - k}^{c}) \mapsto (1, \dots, n)$ ; then

$⋆ e_{I} = ε_{I} e_{I^{c}} .$

Facts & Assumptions

Given: An oriented $n$ -dimensional real inner product space $V$ , its unit volume form $ω$ , a degree $k$ , and a positively oriented orthonormal basis $(e_{1}, \dots, e_{n})$ .

[L1]

The Hodge star is characterized by $α \land ⋆ β = ⟨ α, β ⟩ ω$ (The Hodge star on an oriented finite-dimensional real inner-product space).

[L2]

The Gram pairing on the exterior powers is a positive-definite, hence nondegenerate, inner product (The Gram formula gives a well-defined positive-definite inner product on exterior powers, and $∥ v_{1} \land \dots \land v_{k} ∥^{2}$ is the Gram determinant).

[L3]

The unit volume form is $ω = e_{1} \land \dots \land e_{n}$ for the positively oriented orthonormal basis, with $⟨ ω, ω ⟩ = 1$ (The oriented unit volume form).

[L4]

The wedges $e_{I}$ form a basis of $Λ^{k} V$ and the wedges $e_{I^{c}}$ a basis of $Λ^{n - k} V$ (Increasing-index wedges of a basis form a basis of $Λ^{k} V$ ).

Proof

technique · direct

1.1

By [L3] and [L4], the positively oriented orthonormal basis exists and yields the wedge bases $(e_{I})_{I}$ of $Λ^{k} V$ and $(e_{J})_{J}$ of $Λ^{n - k} V$ .

L3L4

2.1

Define a linear map $⋆ : Λ^{k} V \to Λ^{n - k} V$ by $⋆ e_{I} : = ε_{I} e_{I^{c}}$ on the basis of step 1.1.

step 1.1

3.1

For subsets $I, J$ of sizes $k$ and $k$ , one has $e_{J} \land e_{I^{c}} = 0$ unless $J = I$ : if $J \neq I$ some index occurs twice, and if $J = I$ then $e_{I} \land e_{I^{c}} = ε_{I} e_{1} \land \dots \land e_{n} = ε_{I} ω$ by the definition of $ε_{I}$ and [L3]. The Gram pairing of [L2] on the orthonormal basis satisfies $⟨ e_{J}, e_{I} ⟩ = 1$ for $J = I$ and $0$ otherwise, so $e_{J} \land ⋆ e_{I} = ε_{I} e_{J} \land e_{I^{c}} = ⟨ e_{J}, e_{I} ⟩ ω$ for all $I, J$ .

L2L3step 1.1step 2.1

4.1

Both sides of the relation of [L1] are bilinear in $(α, β)$ , so step 3.1 extends from basis wedges to the identity $α \land ⋆ β = ⟨ α, β ⟩ ω$ for all $α, β \in Λ^{k} V$ .

step 3.1algebra

5.1

Uniqueness: if $⋆^{'}$ also satisfies [L1], then $α \land (⋆ β - ⋆^{'} β) = 0$ for all $α$ ; pairing with $ω$ through the Gram inner product of [L2] gives $⟨ α, ⋆ (⋆ β - ⋆^{'} β) ⟩ = 0$ for all $α$ , so nondegeneracy forces $⋆ (⋆ β - ⋆^{'} β) = 0$ ; the map $⋆$ of step 2.1 permutes a basis up to sign, hence is bijective, so $⋆ β = ⋆^{'} β$ .

L1L2step 2.1step 4.1

6.1

Steps 2.1 and 4.1 prove existence with the complementary-basis formula, and step 5.1 proves uniqueness.

step 2.1step 4.1step 5.1∎

Depends on

Used by

Cited to discharge well-definedness by The Hodge star on an oriented finite-dimensional real inner-product space.

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Reyer Sjamaar, Manifolds and Differential Forms, §2.4 (standard reference, not scraped)