Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01
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.

Exterior-power duality pairing

Statement

The canonical pairing

⟨ω,v1∧⋯∧vk⟩:=ω(v1,…,vk)

extends to a nondegenerate bilinear pairing

⋀kV∗×⋀kV→R,

and for decomposable elements one has

⟨α1∧⋯∧αk, v1∧⋯∧vk⟩=det⁡(αi(vj)).

Facts & Assumptions

Given: Covectors α1,…,αk and vectors v1,…,vk in a finite-dimensional real vector space V.

[F1]

A decomposable k-vector is the functional ω↦ω(v1,…,vk) on alternating k-covectors (The finite-dimensional exterior power of vectors).

[F2]

The wedge product is the signed shuffle sum on alternating covectors (The wedge product of alternating covectors).

[L1]

Wedges of a basis and of its dual basis give dual coordinate systems on exterior powers (Wedge monomials in a dual basis form a basis).

Proof

technique · direct
1.1F1F2givenalgebra

By [F2], (α1∧⋯∧αk)(v1,…,vk) is the alternating sum over permutations of ∏iαi(vσ(i)), which is exactly the determinant of the matrix (αi(vj)). By [F1], this is the value of the pairing on the displayed decomposable elements.

2.1L1step 1.1choosealgebra

Choose a basis e1,…,en of V with dual basis e1,…,en. By [L1], the wedges eI form a basis of ⋀kV∗ and the wedges eI form a basis of ⋀kV, and step 1.1 shows ⟨eI,eJ⟩=δIJ. Therefore the pairing matrix in these bases is the identity, so the pairing is nondegenerate.

3.1step 1.1step 2.1∎

Thus the canonical exterior-power pairing is bilinear, has the determinant formula on decomposables, and is nondegenerate.

Depends on

Used by

Dependency tree · two levels

19 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