LemmaStatement: 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.

Contraction is independent of the basis formula

Statement

The contraction formula

\sum_{i} T (e^{i}, α_{2}, \dots, α_{r}, e_{i}, v_{2}, \dots, v_{s})

has the same value for every basis $(e_{i})$ and its dual basis $(e^{i})$ .

Facts & Assumptions

Given: A type $(r, s)$ tensor $T$ with $r, s \geq 1$ , fixed arguments $α_{2}, \dots, α_{r}, v_{2}, \dots, v_{s}$ , and two bases $(e_{i})$ and $(b_{j})$ with dual families $(e^{i})$ and $(b^{j})$ .

[F1]

Contraction is given by the displayed dual-basis sum (The contraction of a mixed tensor).

[L1]

Every vector and every covector expand in a basis and its dual family (The dual family $(b^{*})_{b \in B}$ associated to a Hamel basis $B$ , defined by $b^{*} (c) = δ_{b c}$ ).

Proof

technique · direct

1.1

Define the bilinear map $B : V^{*} \times V \to R$ by $B (β, w) = T (β, α_{2}, \dots, α_{r}, w, v_{2}, \dots, v_{s})$ . Then the two contraction sums are $\sum_{i} B (e^{i}, e_{i})$ and $\sum_{j} B (b^{j}, b_{j})$ .

F1givenconstruct

2.1

By [L1], any vector $w$ satisfies $w = \sum_{i} e^{i} (w) e_{i} = \sum_{j} b^{j} (w) b_{j}$ , and any covector $β$ satisfies $β = \sum_{i} β (e_{i}) e^{i} = \sum_{j} β (b_{j}) b^{j}$ . Bilinearity of $B$ therefore gives $\sum_{i} B (e^{i}, e_{i}) = \sum_{i, j} b^{j} (e_{i}) B (e^{i}, b_{j}) = \sum_{j} B (\sum_{i} b^{j} (e_{i}) e^{i}, b_{j}) = \sum_{j} B (b^{j}, b_{j}) .$

L1step 1.1algebra

3.1

The displayed sum is therefore basis-independent, so contraction is intrinsically defined.

step 2.1∎

Depends on

Used by

Tensor product and contraction in a basis Example
Tensor products and contractions of smooth tensor fields are smooth Proposition

Dependency tree · two levels

16 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

Will J. Merry, Differential Geometry (standard reference, not scraped)