ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

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.

Neighboring differentials transform with the pivot basis changes

Example

Let $k$ be any field and consider the cochain segment $X^{0} = k \overset{d^{0} = (\binom{1}{- 1})}{\to} X^{1} = k^{2} \overset{d^{1} = (\begin{array}{cc} 1 & 1 \\ 1 & 1 \end{array})}{\to} X^{2} = k^{2} \overset{d^{2} = (1 - 1)}{\to} X^{3} = k, X^{j} = 0 (j \notin {0, 1, 2, 3}) .$ Both neighbouring composites vanish, $d^{1} d^{0} = (0, 0)$ and $d^{2} d^{1} = (0, 0)$ , so this is a cochain complex. Cancel the lower-right identity in degree $1$ , i.e. use the coordinate decomposition $X^{1} = A \oplus U$ , $X^{2} = B \oplus V$ with $A, B$ the first coordinates and $U, V$ the second coordinates; then $a = b = c = φ = 1$ and $φ$ is invertible.

The example computes the basis changes of Triangular basis changes diagonalize an invertible differential block explicitly and shows that the transformed neighbouring arrows are $(1; 0)$ and $(1, 0)$ , with diagonalized pivot $diag (0, 1)$ , so the reduced segment is $k \overset{1}{\to} k \overset{0}{\to} k \overset{1}{\to} k$ .

Facts & Assumptions

Given: The cochain segment $X^{∙}$ displayed above with the coordinate decomposition in degrees $1, 2$ , the pivot $φ = 1$ , the neighbouring components $d^{0} = (p; q)$ and $d^{2} = (r s)$ , and the morphisms $L, R, L^{- 1}, R^{- 1}$ of the lemma.

[L1]

For the decomposition at degree $n = 1$ one has $L = (\begin{array}{cc} 1 & - b φ^{- 1} \\ 0 & 1 \end{array})$ , $L^{- 1} = (\begin{array}{cc} 1 & b φ^{- 1} \\ 0 & 1 \end{array})$ , $R = (\begin{array}{cc} 1 & 0 \\ - φ^{- 1} c & 1 \end{array})$ , $R^{- 1} = (\begin{array}{cc} 1 & 0 \\ φ^{- 1} c & 1 \end{array})$ , and $L d^{1} R = diag (a - b φ^{- 1} c, φ)$ , $R^{- 1} (p; q) = (p; 0)$ , $(r s) L^{- 1} = (r 0)$ (Triangular basis changes diagonalize an invertible differential block).

[L2]

The reduced complex keeps $X^{0}$ and $X^{3}$ , replaces $X^{1}$ by $A$ and $X^{2}$ by $B$ , and has differentials ${\overset{ˉ}{d}}^{0} = p$ , ${\overset{ˉ}{d}}^{1} = a - b φ^{- 1} c$ , ${\overset{ˉ}{d}}^{2} = r$ (An invertible cochain differential block and its candidate reduction).

Verification

1.1

The vanishing composites: $d^{1} d^{0} = (\begin{array}{cc} 1 & 1 \\ 1 & 1 \end{array}) (\binom{1}{- 1}) = (\binom{0}{0})$ and $d^{2} d^{1} = (1 - 1) (\begin{array}{cc} 1 & 1 \\ 1 & 1 \end{array}) = (0 0)$ , so $X^{∙}$ is a cochain complex; the blocks of $d^{1}$ are $a = b = c = φ = 1$ because its lower-right entry is the identity, and the neighbour components are $d^{0} = (p; q) = (1; - 1)$ and $d^{2} = (r s) = (1 - 1)$ .

L2algebra

1.2

The basis changes are $L = (\begin{array}{cc} 1 & - 1 \\ 0 & 1 \end{array})$ with inverse $L^{- 1} = (\begin{array}{cc} 1 & 1 \\ 0 & 1 \end{array})$ , and $R = (\begin{array}{cc} 1 & 0 \\ - 1 & 1 \end{array})$ with inverse $R^{- 1} = (\begin{array}{cc} 1 & 0 \\ 1 & 1 \end{array})$ , all with entries in $k$ and determinant $1$ .

L1algebra

2.1

The transformed incoming arrow is $R^{- 1} (p; q) = (\begin{array}{cc} 1 & 0 \\ 1 & 1 \end{array}) (\binom{1}{- 1}) = (\binom{1}{0})$ ; the transformed outgoing arrow is $(r s) L^{- 1} = (1 - 1) (\begin{array}{cc} 1 & 1 \\ 0 & 1 \end{array}) = (1 0)$ .

L1step 1.1step 1.2algebra

2.2

The diagonalized middle differential is $L d^{1} R$ : first $d^{1} R = (\begin{array}{cc} 1 & 1 \\ 1 & 1 \end{array}) (\begin{array}{cc} 1 & 0 \\ - 1 & 1 \end{array}) = (\begin{array}{cc} 0 & 1 \\ 0 & 1 \end{array})$ , then $L (\begin{array}{cc} 0 & 1 \\ 0 & 1 \end{array}) = (\begin{array}{cc} 1 & - 1 \\ 0 & 1 \end{array}) (\begin{array}{cc} 0 & 1 \\ 0 & 1 \end{array}) = (\begin{array}{cc} 0 & 0 \\ 0 & 1 \end{array}) = diag (a - b φ^{- 1} c, φ)$ with $a - b φ^{- 1} c = 1 - 1 = 0$ .

L1step 1.2algebra

3.1

By [L2] the reduced complex has $X^{0} = k$ , $X^{1} = A = k$ , $X^{2} = B = k$ , $X^{3} = k$ with differentials ${\overset{ˉ}{d}}^{0} = p = 1$ , ${\overset{ˉ}{d}}^{1} = a - b φ^{- 1} c = 0$ and ${\overset{ˉ}{d}}^{2} = r = 1$ , that is the reduced segment $k \overset{1}{\to} k \overset{0}{\to} k \overset{1}{\to} k$ ; its composites are $0 \cdot 1 = 0$ and $1 \cdot 0 = 0$ , so it is a cochain complex, as the lemma guarantees. In the transformed coordinates the discarded components are exactly $φ^{- 1} c p + q = 1 - 1 = 0$ of the incoming arrow and $r b φ^{- 1} + s = 1 - 1 = 0$ of the outgoing arrow, which is why the second entries of the transformed arrows vanish; the entries along the retained summands, namely $p = 1$ and $r = 1$ , pass to the reduction unchanged. ∎

L1L2step 2.1step 2.2algebra

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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

Dror Bar-Natan, Fast Khovanov Homology Computations, section 4 Lemma 4.2 and section 5, printed p. 5 (PDF p. 5) (standard reference, not scraped)
David Clark, Scott Morrison and Kevin Walker, Fixing the Functoriality of Khovanov Homology, Appendix A.1, printed pp. 1562-1563 (standard reference, not scraped)