CounterexampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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.

Three lines in $F^{2}$ that meet pairwise only in $0$ and whose sum is $F^{2}$ with decompositions that are not unique, so pairwise trivial intersection does not give a direct sum

Statement refuted

False claim: if $U_0, U_1, U_2$ are linear subspaces of a vector space $V$ with $\sum_{j<3} U_j = V$ and $U_i \cap U_j = \{0_V\}$ for all $i \ne j$ , then $V = \bigoplus_{j<3} U_j$ (Internal direct sum $V = \bigoplus_{i<n} U_i$ : the sum is everything and each summand meets the sum of the others only in $0_V$ ).

Three lines in the plane $F^{2}$ refute it, over any field $F$ . With $e_0, e_1$ the vectors of $F^{2}$ with coordinates $(1_F, 0_F)$ and $(0_F, 1_F)$ (The vector space $F^{X}$ of all functions $X \to F$ with pointwise operations, and $F^{n}$ as the case $X = n = \{0, 1, \dots, n-1\}$ ) and $d := e_0 + e_1$ , put

$U_0 := \operatorname{span}\{e_0\}, \qquad U_1 := \operatorname{span}\{e_1\}, \qquad U_2 := \operatorname{span}\{d\}$

(Linear combination of a finite list, and the span $\operatorname{span}(S)$ as the smallest linear subspace containing $S$ ). Their pairwise intersections are all $\{0_V\}$ and their sum is $F^{2}$ , yet $d$ has two different decompositions, $d = e_0 + e_1 + 0_V$ and $d = 0_V + 0_V + d$ , so condition (D2) fails at $j = 2$ .

The three sets are called lines informally, as elsewhere on this page; no claim is made about their dimension, nor about how many such sets $F^{2}$ contains.

Facts & Assumptions

Given: A field $F$ , the vector space $F^{2}$ over $F$ , the vectors $e_0, e_1$ and $d = e_0 + e_1$ , and the linear subspaces $U_0, U_1, U_2$ as displayed.

[L1]

$F^{2}$ is the vector space of functions $2 \to F$ with $(x+y)_i = x_i + y_i$ and $(\lambda x)_i = \lambda x_i$ , where $2 = \{0,1\}$ , and its zero vector has both coordinates $0_F$ ; the index set of a three-term family is $3 = \{0,1,2\}$ (The vector space $F^{X}$ of all functions $X \to F$ with pointwise operations, and $F^{n}$ as the case $X = n = \{0, 1, \dots, n-1\}$ , Vector space over a field, The natural numbers $\mathbb{N}$ (von Neumann), On $\mathbb{N}$ the order is membership: $m < n \iff m \in n$ ).

[L2]

$\operatorname{span}\{v\} = \{\, \lambda v : \lambda \in F \,\}$ , a span is a linear subspace, and for $v \ne 0_V$ the equation $\lambda v = 0_V$ forces $\lambda = 0_F$ ( $\operatorname{span}\{v\} = \{\, \lambda v : \lambda \in F \,\}$ , which is $\{0_V\}$ when $v = 0_V$ , and when $v \ne 0_V$ contains $0_V$ only as the multiple $0_F v$ , Linear combination of a finite list, and the span $\operatorname{span}(S)$ as the smallest linear subspace containing $S$ ).

[L3]

The elements of $\sum_{i<n} U_i$ are exactly the $\sum_{i<n} u_i$ with $u_i \in U_i$ , and $\sum_{i<3} u_i = (u_0 + u_1) + u_2$ (The sum $U + W$ of two linear subspaces and the sum $\sum_{i<n} U_i$ of a finite family).

[L4]

$V = \bigoplus_{i<n} U_i$ requires (D1) $\sum_{i<n} U_i = V$ and (D2) $U_j \cap \sum_{i \ne j} U_i = \{0_V\}$ for every $j < n$ , where $\sum_{i \ne j} U_i$ is the sum of the family that agrees with $U$ off $j$ and is $\{0_V\}$ at $j$ (Internal direct sum $V = \bigoplus_{i<n} U_i$ : the sum is everything and each summand meets the sum of the others only in $0_V$ ).

[L5]

$V = \bigoplus_{i<n} U_i$ holds if and only if every $v \in V$ has exactly one decomposition $\sum_{i<n} u_i$ with $u_i \in U_i$ ( $V = \bigoplus_{i<n} U_i$ if and only if every $v \in V$ is $\sum_{i<n} u_i$ with $u_i \in U_i$ in exactly one way; equivalently, if and only if the sum is $V$ and $\sum_{i<n} u_i = 0_V$ with $u_i \in U_i$ forces every $u_i = 0_V$ ).

[L6]

In a field: $1_F \ne 0_F$ ; $\lambda 1_F = \lambda$ ; $0_F \lambda = 0_F$ (Multiplication by zero: $0 \cdot a = 0$ ) and multiplication is commutative, so $\lambda 0_F = 0_F$ ; and $0_F$ is the additive identity (Field).

[L7]

A linear subspace contains $0_V$ , by condition (W1) (Linear subspace of a vector space).

[L8]

The refuted claim: three linear subspaces whose sum is $V$ and whose pairwise intersections are $\{0_V\}$ form an internal direct sum of $V$ .

Counterexample

technique · direct

1.1

In $F^{2}$ the vectors $e_0$ , $e_1$ and $d = e_0 + e_1$ have coordinates $(1_F, 0_F)$ , $(0_F, 1_F)$ and $(1_F + 0_F,\, 0_F + 1_F) = (1_F, 1_F)$ ; and $U_0, U_1, U_2$ are linear subspaces of $F^{2}$ , being spans.

L1L2L6

1.2

The elements of the three subspaces have the coordinates $\lambda e_0 = (\lambda, 0_F)$ , $\lambda e_1 = (0_F, \lambda)$ and $\lambda d = (\lambda, \lambda)$ , for $\lambda \in F$ .

L1L2L6

1.3

$e_0$ , $e_1$ and $d$ are all different from $0_V$ , since each has a coordinate equal to $1_F$ and $1_F \ne 0_F$ .

L1L6

2.1

The pairwise intersections are $\{0_V\}$ . Each contains $0_V$ , every $U_j$ being a linear subspace. Conversely, if $x \in U_0 \cap U_1$ then $x = (\lambda, 0_F) = (0_F, \mu)$ for some $\lambda, \mu$ , so $\lambda = 0_F$ and $x = 0_V$ ; if $x \in U_0 \cap U_2$ then $x = (\lambda, 0_F) = (\mu, \mu)$ , so $\mu = 0_F$ and $\lambda = 0_F$ ; and if $x \in U_1 \cap U_2$ then $x = (0_F, \lambda) = (\mu, \mu)$ , so $\mu = 0_F$ and $\lambda = 0_F$ .

step 1.2L1L7

2.2

$\sum_{j<3} U_j = F^{2}$ . Given $x \in F^{2}$ , the list $(x_0 e_0,\; x_1 e_1,\; 0_V)$ has its $j$ -th entry in $U_j$ , and its sum is $(x_0 e_0 + x_1 e_1) + 0_V$ , whose coordinates are $(x_0 + 0_F,\; 0_F + x_1) = (x_0, x_1)$ , that is $x$ . The reverse inclusion holds because the sum is a subset of $F^{2}$ .

step 1.2L1L3L6L7

2.3

The vector $d$ has two different decompositions with $j$ -th entry in $U_j$ : the list $(e_0, e_1, 0_V)$ sums to $(e_0 + e_1) + 0_V = d$ , and the list $(0_V, 0_V, d)$ sums to $(0_V + 0_V) + d = d$ ; the two lists differ at index $0$ , since $e_0 \ne 0_V$ .

step 1.2step 1.3L1L3L6L7

3.1

Condition (D2) fails at $j = 2$ . The family agreeing with $U$ off $2$ and equal to $\{0_V\}$ at $2$ admits the list $(e_0, e_1, 0_V)$ , which sums to $d$ , so $d \in \sum_{i \ne 2} U_i$ ; also $d = 1_F d \in U_2$ ; and $d \ne 0_V$ . Hence $U_2 \cap \sum_{i \ne 2} U_i$ contains a vector other than $0_V$ .

step 1.3step 2.3L2L4L6

4.1

So $U_0, U_1, U_2$ satisfy both hypotheses of [L8], by steps 2.1 and 2.2, and fail its conclusion, by step 3.1: the claim is false. The failure is visible directly in step 2.3 as the loss of unique decomposition, which by the direct sum criterion is equivalent to the failure of the direct sum.

step 2.1step 2.2step 2.3step 3.1L5L8∎

Remarks

This is why (D2) is stated as it is. For two summands, (D2) and the pairwise condition coincide (Internal direct sum $V = \bigoplus_{i<n} U_i$ : the sum is everything and each summand meets the sum of the others only in $0_V$ ); from three summands on they part company, and the example above is the smallest separation, living in a plane over any field whatever. Over the reals it is the familiar picture of three distinct lines through the origin in the plane, no two of which meet anywhere but the origin.
The failure is exactly one of uniqueness, not of existence. Every vector of $F^{2}$ does decompose, as step 2.2 shows; what fails is that some vector decomposes in more than one way. That is why $V = \bigoplus_{i<n} U_i$ if and only if every $v \in V$ is $\sum_{i<n} u_i$ with $u_i \in U_i$ in exactly one way; equivalently, if and only if the sum is $V$ and $\sum_{i<n} u_i = 0_V$ with $u_i \in U_i$ forces every $u_i = 0_V$ states unique decomposition, and not mere existence, as the equivalent of a direct sum.
Any third line through the origin does the same job. Nothing above is special to $d = e_0 + e_1$ beyond its having both coordinates nonzero; the argument only needs a vector lying in neither $U_0$ nor $U_1$ , and $d$ is the simplest such vector to write down over an arbitrary field.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 59 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Direct sum of modules (Wikipedia) (standard reference, not scraped)
Linear subspace (Wikipedia) (standard reference, not scraped)

Three lines in F2F^{2}F2 that meet pairwise only in 000 and whose sum is F2F^{2}F2 with decompositions that are not unique, so pairwise trivial intersection does not give a direct sum