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

If $v_{1}, \dots, v_{m} \in R^{n}$ satisfy $⟨ v_{i}, v_{j} ⟩ = t \geq 0$ for $i \neq j$ and $⟨ v_{i}, v_{i} ⟩ > t$ , they are linearly independent

Statement

Let $v_{1}, \dots, v_{m} \in R^{n}$ and let $t \geq 0$ . Suppose

$⟨ v_{i}, v_{j} ⟩ = t (i \neq j), ⟨ v_{i}, v_{i} ⟩ > t (1 \leq i \leq m) .$

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

Facts & Assumptions

Given: vectors $v_{1}, \dots, v_{m} \in R^{n}$ satisfying the displayed hypotheses.

[F1]

The standard inner product is bilinear (The standard formulas $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and $\sum_{k < n} x_{k} \overline{y_{k}}$ on $C^{n}$ are inner products).

[F2]

A sum of nonnegative real numbers is $0$ only when every summand is $0$ (Positive and negative definiteness, the inertia $(p, q, r)$ , rank $p + q$ , and signature $p - q$ of a real symmetric bilinear or quadratic form).

Proof

technique · direct

1.1

Suppose $\sum_{i = 1}^{m} c_{i} v_{i} = 0$ . Taking the inner product of this vector with itself and expanding bilinearly gives $0 = \sum_{i = 1}^{m} c_{i}^{2} ⟨ v_{i}, v_{i} ⟩ + \sum_{i \neq j} c_{i} c_{j} t = \sum_{i = 1}^{m} c_{i}^{2} (⟨ v_{i}, v_{i} ⟩ - t) + t (\sum_{i = 1}^{m} c_{i})^{2} .$

F1assume-contra

2.1

Each summand on the right is nonnegative: $⟨ v_{i}, v_{i} ⟩ - t > 0$ by hypothesis and $t \geq 0$ . Therefore [F2] forces every term $c_{i}^{2} (⟨ v_{i}, v_{i} ⟩ - t)$ to vanish, and hence every $c_{i}$ is $0$ .

F2step 1.1

3.1

So the only linear relation is the trivial one, and the vectors are linearly independent.

step 2.1discharge-contradiction∎

Remarks

This is the one place in the page where the order and positivity of $R$ are load-bearing. That is exactly what fails over $F_{2}$ .

Depends on

Used by

Dependency tree · two levels

30 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

J. Matousek, Thirty-three Miniatures, Miniature 4 (standard reference, not scraped)

If v1,…,vm∈Rnv1​,…,vm​∈Rn satisfy ⟨vi,vj⟩=t≥0⟨vi​,vj​⟩=t≥0 for i≠ji=j and ⟨vi,vi⟩>t⟨vi​,vi​⟩>t, they are linearly independent