ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Decategorifying a generator on the vertex-projective basis

Example

Take $m = 2$ . By The graded Grothendieck group is free on the vertex-projective classes the group $G (A_{2})$ is free over $Z [q, q^{- 1}]$ on the basis $[P_{0}], [P_{1}], [P_{2}]$ . By Decategorification is the unreduced Burau action the operator $[R_{1}]$ acts on coefficient column vectors in the ordered basis $([P_{0}], [P_{1}], [P_{2}])$ by $[R_{1}] = (\begin{array}{ccc} 1 & 0 & 0 \\ - q & - q & - 1 \\ 0 & 0 & 1 \end{array}),$ whose columns are the images of $[P_{0}], [P_{1}], [P_{2}]$ : the first column is $[P_{0}] - q [P_{1}]$ , the second $- q [P_{1}]$ , and the third $[P_{2}] - [P_{1}]$ . The matrix $C = (\begin{array}{ccc} q^{2} & q^{2} & 0 \\ 0 & - q & - q \\ 0 & 0 & 1 \end{array})$ is invertible over $Z [q, q^{- 1}]$ (it is upper triangular with diagonal entries $q^{2}, - q, 1$ , all units) and $C [R_{1}] C^{- 1} = B_{1},$ where $B_{1} = (\begin{array}{ccc} 1 - t & t & 0 \\ 1 & 0 & 0 \\ 0 & 0 & 1 \end{array})$ is the first unreduced Burau matrix at $t = q$ , in the column-vector convention of The unreduced Burau matrices. In the Burau coordinates $z = C v$ , the standard coordinate vectors satisfy $e_{0} \mapsto (1 - q) e_{0} + e_{1}$ , $e_{1} \mapsto q e_{0}$ , and $e_{2} \mapsto e_{2}$ . The displayed vertex-projective formulas describe the original basis before this change of coordinates. The example records the conventions: $q = t$ , matrices act on column vectors, and the generator $σ_{i}$ is the one that moves the vertex classes $i - 1, i, i + 1$ .

Facts & Assumptions

Given: The index $m = 2$ , the free basis $[P_{0}], [P_{1}], [P_{2}]$ of $G (A_{2})$ over $Z [q, q^{- 1}]$ , the operator $[R_{1}]$ of the decategorification proposition, and the unreduced Burau matrix $B_{1}$ with parameter $t$ .

[L1]

$G (A_{2})$ is free on $[P_{0}], [P_{1}], [P_{2}]$ and the class map is additive with $[X {r}] = q^{r} [X]$ (The graded Grothendieck group is free on the vertex-projective classes, The graded Grothendieck group of A_m).

[L2]

$[R_{i}] [P_{i}] = - q [P_{i}]$ , $[R_{i}] [P_{i + 1}] = [P_{i + 1}] - [P_{i}]$ , $[R_{i}] [P_{i - 1}] = [P_{i - 1}] - q [P_{i}]$ and $[R_{i}] [P_{j}] = [P_{j}]$ for $∣ i - j ∣ > 1$ , with terms omitted at the boundary; and $C [R_{i}] C^{- 1} = B_{i} ∣_{t = q}$ with $C_{r, r} = C_{r, r + 1} = (- q)^{m - r}$ , $C_{m, m} = 1$ , for every $i$ (Decategorification is the unreduced Burau action).

[L3]

The unreduced Burau matrix $B_{1}$ has the block $(\begin{array}{cc} 1 - t & t \\ 1 & 0 \end{array})$ at rows and columns $0, 1$ and the identity elsewhere, and acts on column vectors (The unreduced Burau matrices).

Verification

technique · direct

1.1L1L2

The matrix of $[R_{1}]$ for $m = 2$ . By [L2] with $i = 1$ and $m = 2$ : $[R_{1}] [P_{1}] = - q [P_{1}]$ , $[R_{1}] [P_{2}] = [P_{2}] - [P_{1}]$ , and $[R_{1}] [P_{0}] = [P_{0}] - q [P_{1}]$ , there being no $P_{- 1}$ term; no $j \in {0, 1, 2}$ satisfies $∣ 1 - j ∣ > 1$ . Reading these as columns in the basis $[P_{0}], [P_{1}], [P_{2}]$ gives the displayed matrix $[R_{1}]$ with columns $(1, - q, 0)^{T}$ , $(0, - q, 0)^{T}$ and $(0, - 1, 1)^{T}$ .

1.2L2

The change of basis. For $m = 2$ the matrix $C$ of [L2] is $C_{0, 0} = C_{0, 1} = (- q)^{2} = q^{2}$ , $C_{1, 1} = C_{1, 2} = (- q)^{1} = - q$ and $C_{2, 2} = 1$ , which is the displayed matrix; it is upper triangular with diagonal entries $q^{2}, - q, 1$ , all units of $Z [q, q^{- 1}]$ , so it is invertible over $Z [q, q^{- 1}]$ .

2.1step 1.1step 1.2L3

The matrix identity. Multiplying out, $C [R_{1}] =$ the matrix with rows $(q^{2} (1 - q), - q^{3}, - q^{2})$ , $(q^{2}, q^{2}, 0)$ , $(0, 0, 1)$ and $C^{- 1}$ has rows $(q^{- 2}, q^{- 1}, 1)$ , $(0, - q^{- 1}, - 1)$ , $(0, 0, 1)$ ; the product $C [R_{1}] C^{- 1}$ has first row $(1 - q, q, 0)$ , second row $(1, 0, 0)$ and third row $(0, 0, 1)$ , which is exactly $B_{1}$ with $t = q$ as in [L3]. Hence $C [R_{1}] C^{- 1} = B_{1}$ .

3.1step 2.1∎

Conclusion. The three-dimensional instance of the decategorification proposition is the displayed matrix computation: the operator $[R_{1}]$ in the vertex-projective basis is conjugate by the explicit invertible matrix $C$ to the unreduced Burau generator at $t = q$ . No choice principle is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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

Mikhail Khovanov and Paul Seidel, Quivers, Floer Cohomology, and Braid Group Actions, J. Amer. Math. Soc. 15 (2002) 203-271, Section 2e.1 (standard reference, not scraped)