Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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.

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

Example

Over a field FF, define

T:F2→F3,T(x,y)=(x+2y, 3x−y, x+y).T:F^2\to F^3,\qquad T(x,y)=(x+2y,\,3x-y,\,x+y).

In the standard ordered bases,

[T]=(123−111),[T]=\begin{pmatrix}1&2\\3&-1\\1&1\end{pmatrix},

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

Facts & Assumptions

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

[L1]

The jj-th column of a linear map's matrix is the coordinate column of the image of the jj-th domain basis vector (Coordinate columns [v]B[v]_{\mathcal B} and matrices [T]BC[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)T(1,0)=(1,3,1) and T(0,1)=(2,−1,1)T(0,1)=(2,-1,1), so [L1] gives the two displayed columns and hence the displayed 33 by 22 matrix.

givenL1
2.1

Multiplication by a general coordinate column gives (123−111)(xy)=(x+2y3x−yx+y)=[T(x,y)]\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 TT.

step 1.1L1∎

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: 23 results over 11 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