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 distinct lines $U_{0}, U_{1}, U_{2}$ in $F^{2}$ have $\dim_{F} (U_{0} + U_{1} + U_{2}) = 2$ while the inclusion-exclusion analogue of the dimension formula predicts $3$ , so the two-subspace formula does not extend

Statement refuted

False claim: for finite-dimensional linear subspaces $U_{0}, U_{1}, U_{2}$ of a vector space $V$ over $F$ ,

$\dim_{F} (\sum_{j < 3} U_{j}) + \dim_{F} (U_{0} \cap U_{1}) + \dim_{F} (U_{0} \cap U_{2}) + \dim_{F} (U_{1} \cap U_{2}) = \dim_{F} U_{0} + \dim_{F} U_{1} + \dim_{F} U_{2} + \dim_{F} (U_{0} \cap U_{1} \cap U_{2}) .$

This is the inclusion-exclusion analogue of The dimension formula: for finite-dimensional linear subspaces $U$ and $W$ of $V$ , the subspaces $U + W$ and $U \cap W$ are finite-dimensional and $\dim_{F} (U + W) + \dim_{F} (U \cap W) = \dim_{F} U + \dim_{F} W$ , written without subtraction so that both sides are natural numbers; for two subspaces the same rearrangement is exactly that theorem.

Let $F$ be any field, let $F^{2}$ be the function space on $2 = {0, 1}$ (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}$ ) with $e_{0} = (1_{F}, 0_{F})$ , $e_{1} = (0_{F}, 1_{F})$ and $d : = e_{0} + e_{1} = (1_{F}, 1_{F})$ , and put

$U_{0} : = span {e_{0}}, U_{1} : = span {e_{1}}, U_{2} : = span {d} .$

Then $\dim_{F} U_{j} = 1$ for each $j$ , all three pairwise intersections and the triple intersection equal ${0_{V}}$ and so have dimension $0$ , and $\sum_{j < 3} U_{j} = F^{2}$ has dimension $2$ . The left-hand side is $2 + 0 + 0 + 0 = 2$ and the right-hand side is $1 + 1 + 1 + 0 = 3$ , so the claimed identity fails.

The three sets are called lines informally, as on the order-69 examples page; the word carries no separate definition here.

Facts & Assumptions

Given: A field $F$ , the vector space $F^{2}$ , the vectors $e_{0}$ , $e_{1}$ , $d = e_{0} + e_{1}$ , and the linear subspaces $U_{0}, U_{1}, U_{2}$ above.

[L1]

$span {v} = {λ v : λ \in F}$ ; if $v \neq 0_{V}$ then $λ v = 0_{V}$ only for $λ = 0_{F}$ and $span {v} \neq {0_{V}}$ ( $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$ , claims 1 and 3).

[L2]

$e : 2 \to F^{2}$ is an ordered basis with $(\sum_{i < 2} λ_{i} e_{i}) (j) = λ_{j}$ , and $\dim_{F} F^{2} = 2$ (The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ , claims 2, 3 and 4).

[L3]

$\sum_{j < 3} U_{j} = span (⋃_{j < 3} U_{j})$ , and a sum of a family contains each summand ( $\sum_{i < n} U_{i} = span (⋃_{i < n} U_{i})$ , so the sum is the smallest linear subspace containing every $U_{i}$ , The sum $U + W$ of two linear subspaces and the sum $\sum_{i < n} U_{i}$ of a finite family).

[L4]

$span (T)$ is a linear subspace containing $T$ , contained in every linear subspace containing $T$ , and monotone; the intersection of two linear subspaces is a linear subspace, and every linear subspace contains $0_{V}$ (Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ , The span is monotone and idempotent, $span (S) = S$ exactly when $S$ is a linear subspace, and $span (S \cup {0_{V}}) = span (S)$ , The intersection of a nonempty family of linear subspaces of $V$ is a linear subspace of $V$ , Linear subspace of a vector space).

[L5]

$\dim_{F} V = p$ means $V$ has a basis with $p$ elements, and it is well defined; $\dim_{F} {0_{V}} = 0$ ; a basis is a linearly independent spanning subset (Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis, If $V$ has a basis with $n$ elements and a basis with $m$ elements then $n = m$ ; and if $V$ has one finite basis then every basis of $V$ is finite, Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i < n} λ_{i} v_{i} = 0_{V}$ forces every $λ_{i} = 0_{F}$ , and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent, Equinumerous sets, $A \approx B$ and $A ⪯ B$ , Finite, countably infinite, countable, uncountable).

[L6]

In $F^{2}$ : elements are equal exactly when they agree at $0$ and at $1$ ; $(λ x) (j) = λ x (j)$ ; $1_{F} \neq 0_{F}$ ; $λ 0_{F} = 0_{F}$ and $λ 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}$ , Vector space over a field, In any vector space $0_{F} v = 0_{V}$ , $λ 0_{V} = 0_{V}$ , $(- λ) v = - (λ v)$ , $(- 1_{F}) v = - v$ , and $λ v = 0_{V}$ forces $λ = 0_{F}$ or $v = 0_{V}$ , Field, The natural numbers $N$ (von Neumann), On $N$ the order is membership: $m < n ⟺ m \in n$ ).

[L7]

Finite sums of naturals: $\sum_{i < 3} d_{i} = ((0 + d_{0}) + d_{1}) + d_{2}$ (The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity, Addition of natural numbers).

Counterexample

technique · direct

1.1

Each of $e_{0}$ , $e_{1}$ , $d$ is nonzero, since each takes the value $1_{F} \neq 0_{F}$ somewhere, and the three are pairwise distinct: $e_{0}$ and $d$ differ at $1$ , $e_{1}$ and $d$ differ at $0$ , and $e_{0}$ and $e_{1}$ differ at $0$ .

1.2

$\dim_{F} U_{j} = 1$ for each $j < 3$ . Take $v$ to be $e_{0}$ , $e_{1}$ or $d$ ; then ${v}$ spans $span {v}$ , and it is linearly independent, since an injective list into ${v}$ has length $0$ or is the one-term list $v$ , and $λ v = 0_{V}$ forces $λ = 0_{F}$ because $v \neq 0_{V}$ . So ${v}$ is a basis with exactly one element.

L1L4L5L6

1.3

The pairwise intersections are ${0_{V}}$ . An element of $U_{0} \cap U_{1}$ is $λ e_{0} = μ e_{1}$ ; evaluating at $0$ gives $λ 1_{F} = μ 0_{F}$ , that is $λ = 0_{F}$ , so the element is $0_{F} e_{0} = 0_{V}$ . An element of $U_{0} \cap U_{2}$ is $λ e_{0} = μ d$ ; evaluating at $1$ gives $0_{F} = μ$ , so it is $0_{V}$ . An element of $U_{1} \cap U_{2}$ is $λ e_{1} = μ d$ ; evaluating at $0$ gives $0_{F} = μ$ , so it is $0_{V}$ . Each intersection also contains $0_{V}$ , being an intersection of linear subspaces, so all three equal ${0_{V}}$ .

L1L4L6

1.4

$\sum_{j < 3} U_{j} = F^{2}$ . The sum contains each $U_{j}$ , hence contains $e_{0}$ and $e_{1}$ ; being a linear subspace it contains $span {e_{0}, e_{1}} = F^{2}$ , and it is contained in $F^{2}$ .

L2L3L4

2.1

The two sides. The triple intersection $U_{0} \cap U_{1} \cap U_{2}$ is contained in $U_{0} \cap U_{1} = {0_{V}}$ by step 1.3 and contains $0_{V}$ , so it is ${0_{V}}$ ; hence all four intersection terms have dimension $0$ by step 1.3. By step 1.4 and the standard basis, $\dim_{F} (\sum_{j < 3} U_{j}) = \dim_{F} F^{2} = 2$ , and by step 1.2 each $\dim_{F} U_{j} = 1$ . So the left-hand side of the claimed identity is $2 + 0 + 0 + 0 = 2$ and the right-hand side is $1 + 1 + 1 + 0 = 3$ .

step 1.2step 1.3step 1.4L2L4L5L7

3.1

Since $2 \neq 3$ , the claimed identity fails for these three finite-dimensional linear subspaces of $F^{2}$ , so the two-subspace dimension formula has no inclusion-exclusion extension to three subspaces.

step 2.1L5∎

Remarks

Same witness, different failure. The three lines used here are exactly those of 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 on the order-69 examples page. That item shows that pairwise trivial intersections together with $\sum_{j < 3} U_{j} = F^{2}$ do not make the sum direct, condition (D2) of 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}$ failing at the third summand. This item shows something else about the same configuration: that the dimensions do not obey inclusion-exclusion. Neither statement follows from the other, and the shared witness is a coincidence of economy rather than a duplication.
Why the two-subspace formula does not extend. The dimension formula: for finite-dimensional linear subspaces $U$ and $W$ of $V$ , the subspaces $U + W$ and $U \cap W$ are finite-dimensional and $\dim_{F} (U + W) + \dim_{F} (U \cap W) = \dim_{F} U + \dim_{F} W$ is proved by extending a basis of $U \cap W$ to bases of $U$ and of $W$ and showing the union is a basis of $U + W$ . With three subspaces there is no single "common part" to extend from: here every pairwise intersection is trivial, so the naive bookkeeping counts three independent directions in a plane that has only two.
The field is arbitrary and is named. Over the two-element field the three lines are still three distinct sets, each with two elements, and every step above uses only $1_{F} \neq 0_{F}$ and the field axioms.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

62 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

Dimension theorem for vector spaces (Wikipedia) (standard reference, not scraped)
Inclusion-exclusion principle (Wikipedia) (standard reference, not scraped)
UC Berkeley Math 110 notes: Linear algebra (standard reference, not scraped)

Three distinct lines U0,U1,U2U0​,U1​,U2​ in F2F2 have dim⁡F(U0+U1+U2)=2dimF​(U0​+U1​+U2​)=2 while the inclusion-exclusion analogue of the dimension formula predicts 33, so the two-subspace formula does not extend