Session-authored (Fable 5 assisted)

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.

✓ 7 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 7 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Matrices and Change of Basis: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-11Open item page →

A matrix represents a map $F^2\to F^3$ by its images of the standard basis vectors

Example

Over a field $F$ , define

$T:F^2\to F^3,\qquad T(x,y)=(x+2y,\,3x-y,\,x+y).$

In the standard ordered bases,

$[T]=\begin{pmatrix}1&2\\3&-1\\1&1\end{pmatrix},$

whose columns are the coordinate columns of $T(1,0)$ and $T(0,1)$ .

Facts & Assumptions

Given: The displayed linear map and the standard ordered bases of $F^2$ and $F^3$ .

[L1]

The $j$ -th column of a linear map's matrix is the coordinate column of the image of the $j$ -th domain basis vector (Coordinate columns $[v]_{\mathcal B}$ and matrices $[T]_{\mathcal B}^{\mathcal C}$ of linear maps relative to ordered bases).

Verification

technique · direct

1.1

One has $T(1,0)=(1,3,1)$ and $T(0,1)=(2,-1,1)$ , so [L1] gives the two displayed columns and hence the displayed $3$ by $2$ matrix.

givenL1

2.1

Multiplication by a general coordinate column gives $\begin{pmatrix}1&2\\3&-1\\1&1\end{pmatrix}\begin{pmatrix}x\\y\end{pmatrix}=\begin{pmatrix}x+2y\\3x-y\\x+y\end{pmatrix}=[T(x,y)]$ , independently verifying that the matrix represents $T$ .

step 1.1L1∎

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

The same operator has two different matrices in two ordered bases

Example

Let $T:F^2\to F^2$ be $T(x,y)=(x,2y)$ . In the standard ordered basis $\mathcal E=(e_0,e_1)$ ,

$[T]_{\mathcal E}^{\mathcal E}=\begin{pmatrix}1&0\\0&2\end{pmatrix}.$

For $\mathcal B=(e_0+e_1,e_1)$ , the same operator has

$[T]_{\mathcal B}^{\mathcal B}=\begin{pmatrix}1&0\\1&2\end{pmatrix}.$

Facts & Assumptions

Given: The displayed operator and ordered bases.

[L1]

A matrix of an operator records the coordinate columns of its basis-vector images, and basis change acts by the two-sided formula (Coordinate columns $[v]_{\mathcal B}$ and matrices $[T]_{\mathcal B}^{\mathcal C}$ of linear maps relative to ordered bases, $[T]_{\mathcal B'}^{\mathcal C'}=P_{\mathcal C'\leftarrow\mathcal C}[T]_{\mathcal B}^{\mathcal C}P_{\mathcal B\leftarrow\mathcal B'}$ ).

Verification

technique · direct

1.1

The standard images are $T(e_0)=e_0$ and $T(e_1)=2e_1$ . The transition matrices are $P_{\mathcal E\leftarrow\mathcal B}=\begin{pmatrix}1&0\\1&1\end{pmatrix}$ and $P_{\mathcal B\leftarrow\mathcal E}=\begin{pmatrix}1&0\\-1&1\end{pmatrix}$ , whose products in either order are $I_2$ .

givenL1

2.1

Directly, $T(e_0+e_1)=e_0+2e_1=(e_0+e_1)+e_1$ and $T(e_1)=2e_1$ , giving the columns $(1,1)$ and $(0,2)$ . Equivalently, $P_{\mathcal B\leftarrow\mathcal E}[T]_{\mathcal E}^{\mathcal E}P_{\mathcal E\leftarrow\mathcal B}=\begin{pmatrix}1&0\\1&2\end{pmatrix}$ .

step 1.1L1∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

The quarter-turn $(x,y)\mapsto(-y,x)$ on $\mathbb R^2$ has matrix $\begin{pmatrix}0&-1\\1&0\end{pmatrix}$ and square $-I_2$

Example

The linear map $Q:\mathbb R^2\to\mathbb R^2$ given by $Q(x,y)=(-y,x)$ is a quarter-turn. In the standard basis,

$[Q]=\begin{pmatrix}0&-1\\1&0\end{pmatrix},\qquad [Q]^2=-I_2.$

Thus $Q^2(x,y)=(-x,-y)$ is the half-turn.

Facts & Assumptions

Given: The real vector space $\mathbb R^2$ with its standard ordered basis and the displayed map $Q$ .

[L1]

The columns of a linear map's matrix are the coordinate columns of its basis-vector images (Coordinate columns $[v]_{\mathcal B}$ and matrices $[T]_{\mathcal B}^{\mathcal C}$ of linear maps relative to ordered bases).

[L2]

The matrix of a composite is the product of the matrices ( $[S\circ T]_{\mathcal B}^{\mathcal D}=[S]_{\mathcal C}^{\mathcal D}[T]_{\mathcal B}^{\mathcal C}$ ).

Verification

technique · direct

1.1

Since $Q(1,0)=(0,1)$ and $Q(0,1)=(-1,0)$ , [L1] gives $[Q]=\begin{pmatrix}0&-1\\1&0\end{pmatrix}$ . Multiplying this matrix by itself gives $\begin{pmatrix}-1&0\\0&-1\end{pmatrix}=-I_2$ .

givenL1

2.1

By [L2], the matrix square is $[Q^2]$ , and direct substitution gives $Q^2(x,y)=Q(-y,x)=(-x,-y)$ , the half-turn.

step 1.1L1L2∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

Two explicit $2$ by $2$ matrices do not commute

Example

In $M_2(F)$ , let

$A=E_{01}=\begin{pmatrix}0&1\\0&0\end{pmatrix},\qquad B=E_{10}=\begin{pmatrix}0&0\\1&0\end{pmatrix}.$

Then $AB\ne BA$ .

Facts & Assumptions

Given: A field $F$ and the displayed matrix units in $M_2(F)$ .

[L1]

Matrix units satisfy $E_{ij}E_{k\ell}=\delta_{jk}E_{i\ell}$ ( $E_{ij}E_{k\ell}=\delta_{jk}E_{i\ell}$ ).

Verification

technique · direct

1.1

By [L1], $AB=E_{00}=\begin{pmatrix}1&0\\0&0\end{pmatrix}$ while $BA=E_{11}=\begin{pmatrix}0&0\\0&1\end{pmatrix}$ .

givenL1

2.1

The products differ at entry $(0,0)$ , since $1\ne0$ in a field, so $A$ and $B$ do not commute.

step 1.1L1∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

A nonzero square-zero matrix is not similar to any diagonal matrix

Example

For every field $F$ , the matrix

$N=E_{01}=\begin{pmatrix}0&1\\0&0\end{pmatrix}\in M_2(F)$

is nonzero and satisfies $N^2=0$ , but it is not similar to any diagonal matrix.

Facts & Assumptions

Given: A field $F$ and the displayed matrix $N$ .

[L1]

Matrix units satisfy $E_{ij}E_{k\ell}=\delta_{jk}E_{i\ell}$ ( $E_{ij}E_{k\ell}=\delta_{jk}E_{i\ell}$ ).

[L2]

Similarity has the form $N=P^{-1}DP$ with $P$ invertible, and every nonzero scalar in a field has an inverse (Similar matrices: $B=P^{-1}AP$ for an invertible $P$ , Field).

Verification

technique · contradiction

1.1

By [L1], $N^2=E_{01}E_{01}=0$ , while the $(0,1)$ -entry of $N$ is $1$ , so $N\ne0$ . Suppose, for contradiction, that $N=P^{-1}DP$ as in [L2], with $D$ diagonal. Then $0=N^2=P^{-1}D^2P$ , so $D^2=0$ .

assume-contraL1L2

2.1

Every diagonal entry $d$ of $D$ satisfies $d^2=0$ . If $d\ne0$ , the inverse from [L2] gives $d=0$ , a contradiction; hence $D=0$ , and then $N=P^{-1}0P=0$ , contradicting step 1.1. Thus $N$ is not similar to a diagonal matrix.

step 1.1L1L2discharge-contradiction∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

Changing both domain and codomain bases of a map $F^2\to F^3$ uses both sides of the formula

Example

Let $T:F^2\to F^3$ be $T(x,y)=(x+2y,3x-y,x+y)$ . Use the standard bases $\mathcal B,\mathcal C$ and the new bases

$\mathcal B'=(e_0+e_1,e_1),\qquad \mathcal C'=(f_0+f_2,f_1,f_2).$

Then

$[T]_{\mathcal B'}^{\mathcal C'}=\begin{pmatrix}3&2\\2&-1\\-1&-1\end{pmatrix}.$

Facts & Assumptions

Given: The displayed map and four ordered bases.

[L1]

The two-sided formula is $[T]_{\mathcal B'}^{\mathcal C'}=P_{\mathcal C'\leftarrow\mathcal C}[T]_{\mathcal B}^{\mathcal C}P_{\mathcal B\leftarrow\mathcal B'}$ ( $[T]_{\mathcal B'}^{\mathcal C'}=P_{\mathcal C'\leftarrow\mathcal C}[T]_{\mathcal B}^{\mathcal C}P_{\mathcal B\leftarrow\mathcal B'}$ ).

Verification

technique · direct

1.1

Here $[T]_{\mathcal B}^{\mathcal C}=\begin{pmatrix}1&2\\3&-1\\1&1\end{pmatrix}$ , $P_{\mathcal B\leftarrow\mathcal B'}=\begin{pmatrix}1&0\\1&1\end{pmatrix}$ , and $P_{\mathcal C'\leftarrow\mathcal C}=\begin{pmatrix}1&0&0\\0&1&0\\-1&0&1\end{pmatrix}$ . Multiplying in the order of [L1] gives $\begin{pmatrix}3&2\\2&-1\\-1&-1\end{pmatrix}$ .

givenL1

2.1

Independently, $T(e_0+e_1)=(3,2,2)=3(f_0+f_2)+2f_1-f_2$ and $T(e_1)=(2,-1,1)=2(f_0+f_2)-f_1-f_2$ , producing the same two coordinate columns.

step 1.1L1∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

A $2$ by $3$ matrix and a $3$ by $2$ matrix give square products of different sizes but equal traces

Example

Over any field $F$ , let

$A=\begin{pmatrix}1&2&0\\0&1&3\end{pmatrix},\qquad B=\begin{pmatrix}1&0\\2&1\\0&1\end{pmatrix}.$

The product $AB$ is $2$ by $2$ , the product $BA$ is $3$ by $3$ , and their traces are equal.

Facts & Assumptions

Given: The displayed rectangular matrices over a field $F$ .

[L1]

For conformable rectangular matrices, $\operatorname{tr}(AB)=\operatorname{tr}(BA)$ (For $A\in M_{m\times n}(F)$ and $B\in M_{n\times m}(F)$ , $\operatorname{tr}(AB)=\operatorname{tr}(BA)$ ).

Verification

technique · direct

1.1

Direct multiplication gives $AB=\begin{pmatrix}5&2\\2&4\end{pmatrix}$ and $BA=\begin{pmatrix}1&2&0\\2&5&3\\0&1&3\end{pmatrix}$ .

givenL1

2.1

Hence $\operatorname{tr}(AB)=5+4=9$ and $\operatorname{tr}(BA)=1+5+3=9$ as elements of $F$ , verifying [L1] for products of different square sizes.

step 1.1L1∎

Sources

Standard references

Recommended treatments; not extraction sources.

Matrices and Change of Basis: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

A matrix represents a map F2→F3F^2\to F^3F2→F3 by its images of the standard basis vectors

Example

Facts & Assumptions

Verification

The same operator has two different matrices in two ordered bases

Example

Facts & Assumptions

Verification

The quarter-turn (x,y)↦(−y,x)(x,y)\mapsto(-y,x)(x,y)↦(−y,x) on R2\mathbb R^2R2 has matrix (0−110)\begin{pmatrix}0&-1\\1&0\end{pmatrix}(01​−10​) and square −I2-I_2−I2​

Example

Facts & Assumptions

Verification

Two explicit 222 by 222 matrices do not commute

Example

Facts & Assumptions

Verification

A nonzero square-zero matrix is not similar to any diagonal matrix

Example

Facts & Assumptions

Verification

Changing both domain and codomain bases of a map F2→F3F^2\to F^3F2→F3 uses both sides of the formula

Example

Facts & Assumptions

Verification

A 222 by 333 matrix and a 333 by 222 matrix give square products of different sizes but equal traces

Example

Facts & Assumptions

Verification

Sources

Standard references

A matrix represents a map $F^2\to F^3$ by its images of the standard basis vectors

The quarter-turn $(x,y)\mapsto(-y,x)$ on $\mathbb R^2$ has matrix $\begin{pmatrix}0&-1\\1&0\end{pmatrix}$ and square $-I_2$

Two explicit $2$ by $2$ matrices do not commute

Changing both domain and codomain bases of a map $F^2\to F^3$ uses both sides of the formula

A $2$ by $3$ matrix and a $3$ by $2$ matrix give square products of different sizes but equal traces