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 is an isometry and satisfies on
Statement
On of an oriented -dimensional real inner product space, the Hodge star preserves the Gram pairing,
and satisfies
Facts & Assumptions
Given: An oriented -dimensional real inner product space , a degree , and a positively oriented orthonormal basis .
In a positively oriented orthonormal basis, , where is the sign of the permutation listing followed by its complement (The Hodge star exists uniquely and is given by the complementary-basis formula in an oriented orthonormal basis).
Proof
By [L1], sends the orthonormal wedge basis to the family , which is the complementary orthonormal wedge basis with signs attached; hence , and bilinearity gives the isometry on all of .
For each , apply [L1] twice: , where is the sign of the permutation listing followed by . The two permutations differ by interchanging a block of size with a block of size , whose sign is , so and .
Since the form a basis, step 1.2 gives on .
Depends on
Used by
Dependency tree · two levels
5 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)