CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck 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 \neq j$ , then $V = ⨁_{j < 3} U_{j}$ (Internal direct sum $V = ⨁_{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} : = span {e_{0}}, U_{1} : = span {e_{1}}, U_{2} : = span {d}$

(Linear combination of a finite list, and the span $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 $(λ x)_{i} = λ 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 $N$ (von Neumann), On $N$ the order is membership: $m < n ⟺ m \in n$ ).

[L2]

$span {v} = {λ v : λ \in F}$ , a span is a linear subspace, and for $v \neq 0_{V}$ the equation $λ v = 0_{V}$ forces $λ = 0_{F}$ ( $span {v} = {λ v : λ \in F}$ , which is ${0_{V}}$ when $v = 0_{V}$ , and when $v \neq 0_{V}$ contains $0_{V}$ only as the multiple $0_{F} v$ , Linear combination of a finite list, and the span $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 = ⨁_{i < n} U_{i}$ requires (D1) $\sum_{i < n} U_{i} = V$ and (D2) $U_{j} \cap \sum_{i \neq j} U_{i} = {0_{V}}$ for every $j < n$ , where $\sum_{i \neq 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 = ⨁_{i < n} U_{i}$ : the sum is everything and each summand meets the sum of the others only in $0_{V}$ ).

[L5]

$V = ⨁_{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 = ⨁_{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} \neq 0_{F}$ ; $λ 1_{F} = λ$ ; $0_{F} λ = 0_{F}$ (Multiplication by zero: $0 \cdot a = 0$ ) and multiplication is commutative, so $λ 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 $λ e_{0} = (λ, 0_{F})$ , $λ e_{1} = (0_{F}, λ)$ and $λ d = (λ, λ)$ , for $λ \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} \neq 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 = (λ, 0_{F}) = (0_{F}, μ)$ for some $λ, μ$ , so $λ = 0_{F}$ and $x = 0_{V}$ ; if $x \in U_{0} \cap U_{2}$ then $x = (λ, 0_{F}) = (μ, μ)$ , so $μ = 0_{F}$ and $λ = 0_{F}$ ; and if $x \in U_{1} \cap U_{2}$ then $x = (0_{F}, λ) = (μ, μ)$ , so $μ = 0_{F}$ and $λ = 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} \neq 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 \neq 2} U_{i}$ ; also $d = 1_{F} d \in U_{2}$ ; and $d \neq 0_{V}$ . Hence $U_{2} \cap \sum_{i \neq 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 = ⨁_{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 = ⨁_{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 · two levels

40 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

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

Three lines in F2F2 that meet pairwise only in 00 and whose sum is F2F2 with decompositions that are not unique, so pairwise trivial intersection does not give a direct sum