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 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\Bigl(\sum_{j<3}U_j\Bigr) + \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 := \operatorname{span}\{e_0\}, \qquad U_1 := \operatorname{span}\{e_1\}, \qquad U_2 := \operatorname{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]

$\operatorname{span}\{v\} = \{\, \lambda v : \lambda \in F \,\}$ ; if $v \ne 0_V$ then $\lambda v = 0_V$ only for $\lambda = 0_F$ and $\operatorname{span}\{v\} \ne \{0_V\}$ ( $\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$ , claims 1 and 3).

[L2]

$e : 2 \to F^{2}$ is an ordered basis with $\bigl(\sum_{i<2}\lambda_i e_i\bigr)(j) = \lambda_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 \ne i$ is an ordered basis of $F^{n}$ ; hence $\dim_F F^{n} = n$ , and $F^{0}$ is the zero space with basis $\varnothing$ and dimension $0$ , claims 2, 3 and 4).

[L3]

$\sum_{j<3}U_j = \operatorname{span}\bigl(\bigcup_{j<3}U_j\bigr)$ , and a sum of a family contains each summand ( $\sum_{i<n} U_i = \operatorname{span}\bigl(\bigcup_{i<n} U_i\bigr)$ , 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]

$\operatorname{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 $\operatorname{span}(S)$ as the smallest linear subspace containing $S$ , The span is monotone and idempotent, $\operatorname{span}(S) = S$ exactly when $S$ is a linear subspace, and $\operatorname{span}(S \cup \{0_V\}) = \operatorname{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} \lambda_i v_i = 0_V$ forces every $\lambda_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 \preceq B$ , Finite, countably infinite, countable, uncountable).

[L6]

In $F^{2}$ : elements are equal exactly when they agree at $0$ and at $1$ ; $(\lambda x)(j) = \lambda x(j)$ ; $1_F \ne 0_F$ ; $\lambda 0_F = 0_F$ and $\lambda 1_F = \lambda$ (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$ , $\lambda 0_V = 0_V$ , $(-\lambda)v = -(\lambda v)$ , $(-1_F)v = -v$ , and $\lambda v = 0_V$ forces $\lambda = 0_F$ or $v = 0_V$ , Field, The natural numbers $\mathbb{N}$ (von Neumann), On $\mathbb{N}$ the order is membership: $m < n \iff 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 \cdots 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 \ne 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 $\operatorname{span}\{v\}$ , and it is linearly independent, since an injective list into $\{v\}$ has length $0$ or is the one-term list $v$ , and $\lambda v = 0_V$ forces $\lambda = 0_F$ because $v \ne 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 $\lambda e_0 = \mu e_1$ ; evaluating at $0$ gives $\lambda 1_F = \mu 0_F$ , that is $\lambda = 0_F$ , so the element is $0_F e_0 = 0_V$ . An element of $U_0 \cap U_2$ is $\lambda e_0 = \mu d$ ; evaluating at $1$ gives $0_F = \mu$ , so it is $0_V$ . An element of $U_1 \cap U_2$ is $\lambda e_1 = \mu d$ ; evaluating at $0$ gives $0_F = \mu$ , 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 $\operatorname{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\bigl(\sum_{j<3}U_j\bigr) = \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 \ne 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 = \bigoplus_{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 \ne 0_F$ and the field axioms.

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: 87 results over 27 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

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,U2U_0, U_1, U_2U0​,U1​,U2​ in F2F^{2}F2 have dim⁡F(U0+U1+U2)=2\dim_F(U_0+U_1+U_2) = 2dimF​(U0​+U1​+U2​)=2 while the inclusion-exclusion analogue of the dimension formula predicts 333, so the two-subspace formula does not extend