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.

Two adjacent noncomposable Gaussian pivots in either finite order

Example

Let $X^{∙}$ be a cochain complex with objects $X^{0} = A, X^{1} = B \oplus C, X^{2} = D_{1} \oplus D_{2} \oplus E, X^{3} = F \oplus G, X^{4} = H, X^{j} = 0 (j \notin {0, 1, 2, 3, 4}),$ differentials $d^{0} = (p; q)$ , $d^{1} = (\begin{array}{cc} ψ & β \\ x & γ \\ y & δ \end{array})$ (rows $D_{1}, D_{2}, E$ , columns $B, C$ ), $d^{2} = (\begin{array}{ccc} z & μ & λ \\ w & ν & φ \end{array})$ (rows $F, G$ , columns $D_{1}, D_{2}, E$ ) and $d^{3} = (r s)$ , with $ψ : B \to D_{1}$ and $φ : E \to G$ isomorphisms and with $d^{1} d^{0} = 0$ , $d^{2} d^{1} = 0$ and $d^{3} d^{2} = 0$ ; this is the Lemma A.2 shape of Clark–Morrison–Walker. The two pivots $ψ$ and $φ$ are adjacent but not composable, so the cancellation order is a genuine choice, and the example computes the reduction in each order.

Facts & Assumptions

Given: The cochain complex $X^{∙}$ displayed above, with the invertible entries $ψ : B \to D_{1}$ of $d^{1}$ and $φ : E \to G$ of $d^{2}$ , and the two cancellation orders: cancel $ψ$ first and then $φ$ in the reduced complex, or cancel $φ$ first and then $ψ$ .

[L1]

At a pivot $φ$ of a block $(\begin{array}{cc} a & b \\ c & φ \end{array})$ in a decomposition $X^{n} = A^{'} \oplus U$ , $X^{n + 1} = B^{'} \oplus V$ , the candidate reduction keeps $X^{j}$ for $j \notin {n, n + 1}$ and the components of the neighbouring differentials along the retained summands $A^{'}$ and $B^{'}$ , and replaces the differential by the Schur complement $a - b φ^{- 1} c$ (An invertible cochain differential block and its candidate reduction, Triangular basis changes diagonalize an invertible differential block).

[L2]

Each single cancellation in its current complex gives cochain maps $p, ı$ and a degree- $(- 1)$ homotopy $h$ with $p ı = 1$ , $1 - ı p = d h + h d$ , $p h = 0$ , $h ı = 0$ , $h^{2} = 0$ (Explicit strong deformation retract from Gaussian cancellation).

[L3]

A finite sequence of cancellations with invertible current pivots composes: the composite data is $p = p_{2} p_{1}$ , $ı = ı_{1} ı_{2}$ , $h = h_{1} + ı_{1} h_{2} p_{1}$ and satisfies the same five identities, and reductions obtained from different valid choices are homotopy equivalent (Finite iteration of current invertible-block cancellations).

Verification

1.1

Complex check. The composite $d^{2} d^{1}$ has $(i, j)$ -entry the sum over $D_{1}, D_{2}, E$ of the products of entries of $d^{2}$ and $d^{1}$ , and each of the three displayed matrix identities $d^{1} d^{0} = 0$ , $d^{2} d^{1} = 0$ , $d^{3} d^{2} = 0$ is exactly the hypothesis that consecutive differentials of $X^{∙}$ vanish; the remaining composites are zero because $X^{- 1} = X^{5} = 0$ .

L1algebra

1.2

Cancelling $ψ$ first. Write $X^{1} = C \oplus B$ and $X^{2} = (D_{2} \oplus E) \oplus D_{1}$ , so that the pivot block of $d^{1}$ is $ψ : B \to D_{1}$ , with $a = (γ; δ) : C \to D_{2} \oplus E$ , $b = (x; y) : B \to D_{2} \oplus E$ and $c = β : C \to D_{1}$ . The Schur complement of the pivot is $a - b ψ^{- 1} c = (γ - x ψ^{- 1} β; δ - y ψ^{- 1} β) : C \to D_{2} \oplus E$ ; the incoming arrow of the reduction is the $C$ -component $q$ of $d^{0}$ , and the outgoing arrow is the restriction of $d^{2}$ to the rows $D_{2}, E$ , namely $(\begin{array}{cc} μ & λ \\ ν & φ \end{array})$ , in which the pivot $φ : E \to G$ still appears unchanged.

L1L2algebra

1.3

Cancelling $φ$ first. In the decomposition $X^{2} = (D_{1} \oplus D_{2}) \oplus (E)$ and $X^{3} = (F) \oplus (G)$ , the pivot $φ : E \to G$ has complement blocks $z, μ$ (row $F$ ) and $w, ν$ , so the Schur complement is the arrow $D_{1} \oplus D_{2} \to F$ with entries $z - λ φ^{- 1} w$ and $μ - λ φ^{- 1} ν$ ; the incoming arrow is the restriction of $d^{1}$ to the rows $D_{1}, D_{2}$ , namely $(\begin{array}{cc} ψ & β \\ x & γ \end{array})$ , and the outgoing arrow is $r : F \to H$ . Cancelling $ψ$ second gives the middle differential $γ - x ψ^{- 1} β$ on $C \to D_{2}$ , the incoming arrow $q$ and the outgoing arrow $r$ .

L1L2algebra

2.1

Cancelling $φ$ second. In the complex of step 1.2 the pivot $φ : E \to G$ sits in the block of $(\begin{array}{cc} μ & λ \\ ν & φ \end{array})$ with retained summands $D_{2}$ of the degree- $2$ object and $F$ of the degree- $3$ object, so the new middle differential is the Schur complement $μ - λ φ^{- 1} ν : D_{2} \to F$ , while the incoming arrow loses its $E$ -component and becomes $γ - x ψ^{- 1} β : C \to D_{2}$ ; the outgoing arrow is $r : F \to H$ .

L1step 1.2algebra

3.1

Order comparison. By steps 1.2 and 2.1, cancelling $ψ$ then $φ$ leaves the cochain complex $A \overset{q}{\to} C \overset{γ - x ψ^{- 1} β}{\to} D_{2} \overset{μ - λ φ^{- 1} ν}{\to} F \overset{r}{\to} H$ ; by step 1.3, cancelling $φ$ then $ψ$ leaves the same objects and the same four arrows. In each order the composite of the single-cancellation data is by [L3] the strong deformation retract data $p = p_{2} p_{1}$ , $ı = ı_{1} ı_{2}$ , $h = h_{1} + ı_{1} h_{2} p_{1}$ of $X^{∙}$ onto that reduction, satisfying $p ı = 1$ , $1 - ı p = d h + h d$ , $p h = 0$ , $h ı = 0$ and $h^{2} = 0$ ; [L3] also gives that the two reductions are homotopy equivalent.

L3step 2.1step 1.3algebra

4.1

A concrete instance over $Q$ . Take every entry of $d^{1}$ equal to $1$ , so $ψ = β = x = γ = y = δ = 1$ ; take $d^{2} = (\begin{array}{ccc} 1 & 1 & - 2 \\ 1 & - 2 & 1 \end{array})$ , $d^{0} = (1; - 1)$ and $d^{3} = (0 0)$ . Then $d^{1} d^{0} = (1 - 1; 1 - 1; 1 - 1) = 0$ , $d^{2} d^{1} = (\begin{array}{cc} 1 + 1 - 2 & 1 + 1 - 2 \\ 1 - 2 + 1 & 1 - 2 + 1 \end{array}) = 0$ and $d^{3} d^{2} = (0 0)$ , so $X^{∙}$ is a complex. The two reduced middle arrows are $γ - x ψ^{- 1} β = 1 - 1 = 0$ and $μ - λ φ^{- 1} ν = 1 - (- 2) (1)^{- 1} (- 2) = 1 - 4 = - 3$ , and the end arrows are $q = - 1$ and $r = 0$ ; both orders give the reduced complex $Q \overset{- 1}{\to} Q \overset{0}{\to} Q \overset{- 3}{\to} Q \overset{0}{\to} Q$ , whose composites $0 \cdot (- 1) = 0$ and $(- 3) \cdot 0 = 0$ vanish. ∎

L1L3step 3.1algebra

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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

David Clark, Scott Morrison and Kevin Walker, Fixing the Functoriality of Khovanov Homology, Appendix A.1, Lemma A.2, printed pp. 1562-1563 (standard reference, not scraped)
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)