LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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.

Triangular criterion: if $⟨ v_{i}, w_{i} ⟩ \neq 0$ and $⟨ v_{i}, w_{j} ⟩ = 0$ for $j < i$ , then $v_{1}, \dots, v_{m}$ are linearly independent

Statement

Let $F$ be a field, let $V$ be an $F$ -vector space, and let $⟨ \cdot, \cdot ⟩ : V \times V \to F$ be a bilinear form. Suppose vectors $v_{1}, \dots, v_{m}, w_{1}, \dots, w_{m} \in V$ satisfy

$⟨ v_{i}, w_{i} ⟩ \neq 0 and ⟨ v_{i}, w_{j} ⟩ = 0 whenever j < i .$

Then $v_{1}, \dots, v_{m}$ are linearly independent.

Facts & Assumptions

Given: a field $F$ , a vector space $V$ over $F$ , a bilinear form $⟨ \cdot, \cdot ⟩$ on $V$ , and vectors $v_{1}, \dots, v_{m}, w_{1}, \dots, w_{m} \in V$ satisfying the displayed hypotheses.

[F1]

A bilinear form is linear in each variable separately (Bilinear forms, and symmetric, skew-symmetric, and alternating bilinear forms).

[F2]

A field has no zero divisors (Field).

Proof

technique · direct

1.1

Suppose $\sum_{i = 1}^{m} c_{i} v_{i} = 0$ with some coefficient nonzero, and let $i$ be the least index with $c_{i} \neq 0$ .

assume-contra

2.1

Pairing with $w_{i}$ and using [F1] gives $\sum_{j = 1}^{m} c_{j} ⟨ v_{j}, w_{i} ⟩ = 0$ . The terms with $j < i$ vanish by the choice of $i$ , and the terms with $j > i$ vanish by the triangular hypothesis, so only $c_{i} ⟨ v_{i}, w_{i} ⟩$ remains.

F1step 1.1

3.1

Since $⟨ v_{i}, w_{i} ⟩ \neq 0$ and a field has no zero divisors by [F2], this forces $c_{i} = 0$ , contradicting step 1.1. Therefore $v_{1}, \dots, v_{m}$ are linearly independent.

F2step 2.1discharge-contradiction∎

Remarks

The direction of the triangular hypothesis matters. The proof chooses the least nonzero coefficient, so it kills the terms below the diagonal by minimality and the terms above it by hypothesis.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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

L. Babai and P. Frankl, Linear Algebra Methods in Combinatorics, §2.1.4 (standard reference, not scraped)

Triangular criterion: if ⟨vi,wi⟩≠0⟨vi​,wi​⟩=0 and ⟨vi,wj⟩=0⟨vi​,wj​⟩=0 for j<ij<i, then v1,…,vmv1​,…,vm​ are linearly independent