ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck passaudited 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.

A unit pivot forces the minus Schur sign

Example

Work over $Q$ and let $X^{0} = Q^{2}, X^{1} = Q^{2}, d^{0} = (\begin{array}{cc} 1 & 1 \\ 1 & 1 \end{array}), d^{1} = 0, X^{j} = 0 (j \notin {0, 1}) .$ This is a two-term cochain complex, since $d^{1} d^{0} = 0$ . Decompose $X^{0} = A \oplus U$ and $X^{1} = B \oplus V$ with $A, B$ the first coordinates and $U, V$ the second coordinates, so that the four blocks of $d^{0}$ are $a = b = c = φ = 1$ and the lower-right entry of $d^{0}$ is the identity, an invertible pivot.

The example compares the two candidate signs in the Schur complement $a \mp b φ^{- 1} c$ : the correct minus sign gives the reduced differential $1 - 1 \cdot 1^{- 1} \cdot 1 = 0$ on $Q \to Q$ , whose kernel and cokernel are both one-dimensional and agree with those of $d^{0}$ , while the plus sign gives multiplication by $2$ , whose kernel and cokernel both vanish.

Facts & Assumptions

Given: The two-term complex $X^{∙}$ displayed above with the coordinate decomposition at degree $0$ , and the candidate reduction ${\overset{ˉ}{X}}^{∙}$ at the pivot $φ = 1$ .

[L1]

With $L = (\begin{array}{cc} 1 & - b φ^{- 1} \\ 0 & 1 \end{array})$ and $R = (\begin{array}{cc} 1 & 0 \\ - φ^{- 1} c & 1 \end{array})$ one has $L d^{0} R = diag (a - b φ^{- 1} c, φ)$ , $R^{- 1} (p; q) = (p; 0)$ , $(r s) L^{- 1} = (r 0)$ and $\overset{ˉ}{d} p = 0 = r \overset{ˉ}{d}$ ; the candidate reduction is a cochain complex (Triangular basis changes diagonalize an invertible differential block).

[L2]

The candidate reduction keeps $X^{j}$ for $j \notin {0, 1}$ , replaces $X^{0}$ by $A$ and $X^{1}$ by $B$ , and its differentials at degrees $- 1, 0, 1$ are $p$ , $a - b φ^{- 1} c$ and $r$ where $d^{- 1} = (p; q)$ and $d^{1} = (r s)$ (An invertible cochain differential block and its candidate reduction).

[L3]

Over an abelian category the reduction is homotopy equivalent to $X^{∙}$ by a strong deformation retract, and the induced maps on homology objects of the reindexed chain complexes are inverse isomorphisms; in particular isomorphic homology objects in every degree (Gaussian cancellation preserves homotopy type and abelian-category homology).

[L4]

The homology object $H_{n}$ of a chain complex is the cokernel of the boundary-to-cycle map $B_{n} (C) \to Z_{n} (C)$ ; for a two-term complex the homology at the source is the kernel of its outgoing differential, and at the target it is the cokernel of its incoming differential (Homology object of a chain complex).

Verification

1.1

The lower-left $2 \times 2$ block of $d^{0}$ is $(\begin{array}{cc} 1 & 1 \\ 1 & 1 \end{array})$ in the rows $B, V$ and columns $A, U$ , so $a = b = c = φ = 1$ and the pivot is the lower-right identity, invertible with $φ^{- 1} = 1$ .

L2algebra

1.2

The Schur complement is $a - b φ^{- 1} c = 1 - 1 \cdot 1^{- 1} \cdot 1 = 0$ , so by [L1] the reduction has differential ${\overset{ˉ}{d}}^{0} = 0 : Q \to Q$ ; its neighbouring arrows are ${\overset{ˉ}{d}}^{- 1} = p = 0$ and ${\overset{ˉ}{d}}^{1} = r = 0$ , because $d^{- 1} = 0$ and $d^{1} = 0$ have no components into or out of the discarded summands. Hence ${\overset{ˉ}{X}}^{∙}$ is $Q \overset{0}{\to} Q$ in degrees $0, 1$ .

L1L2algebra

1.3

Under the reindexing $C_{n} = X^{- n}$ the two-term complex becomes the chain complex $Q \overset{d^{0}}{\to} Q$ concentrated in degrees $0, - 1$ , so by [L4] its homology is $H_{0} = \ker d^{0}$ and $H_{- 1} = coker d^{0}$ , corresponding to cochain degrees $0$ and $1$ . For the reduction these are $\ker (0) = Q$ and $coker (0) = Q$ ; for $X^{∙}$ they are $\ker d^{0} = Q (1, - 1) ≅ Q$ , since $(\begin{array}{cc} 1 & 1 \\ 1 & 1 \end{array}) (\binom{x}{y}) = (\binom{x + y}{x + y})$ , and $coker d^{0} = Q^{2} / Q (1, 1) ≅ Q$ . The two complexes therefore have isomorphic one-dimensional homology, as [L3] requires.

L1L3L4algebra

2.1

With the plus sign, the candidate differential would be $a + b φ^{- 1} c = 1 + 1 = 2$ , the map $Q \overset{2}{\to} Q$ with $\ker (2) = 0$ and $coker (2) = Q / 2 Q = 0$ ; its homology would vanish in both degrees, whereas $X^{∙}$ has one-dimensional homology in both degrees and is homotopy equivalent to its reduction by [L3]. The plus sign is therefore impossible, and the example exhibits the minus sign in the Schur complement. ∎

L3step 1.2step 1.3algebra

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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)