ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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 positive crossing factorization complex

Example

Write out the positive crossing complex of The positive and negative Khovanov-Rozansky crossing complexes: with the two resolutions $Γ_{0}$ (two arcs with labels $x_{1}, x_{4}$ and $x_{2}, x_{3}$ ) and $Γ_{1}$ (one wide edge with the same four labels) and the maps $χ_{0}, χ_{1}$ of The wide-edge morphisms chi-zero and chi-one, the positive crossing contributes $0 \to C (Γ_{0}) {0, 2} \overset{χ_{0}}{\to} C (Γ_{1}) \to 0$ with $C (Γ_{1})$ in cohomological degree $0$ , the differential having bidegree $(0, 0)$ on the shifted terms.

Both resolutions carry the potential $a (x_{1} + x_{2} - x_{3} - x_{4})$ . In the standard product bases the four presentation matrices are $P_{0} = (\begin{array}{cc} a & x_{3} - x_{2} \\ a & x_{1} - x_{4} \end{array}), P_{1} = (\begin{array}{cc} x_{1} - x_{4} & x_{2} - x_{3} \\ - a & a \end{array}),$ $Q_{0} = (\begin{array}{cc} a & x_{3} x_{4} - x_{1} x_{2} \\ 0 & x_{1} + x_{2} - x_{3} - x_{4} \end{array}), Q_{1} = (\begin{array}{cc} x_{1} + x_{2} - x_{3} - x_{4} & x_{1} x_{2} - x_{3} x_{4} \\ 0 & a \end{array}),$ the term shifts are $C^{0} (Γ_{0}) = R \oplus R {- 2, 2}$ , $C^{1} (Γ_{0}) = R {- 1, 1} \oplus R {- 1, 1}$ , $C^{0} (Γ_{1}) = R \oplus R {- 2, 4}$ , $C^{1} (Γ_{1}) = R {- 1, 1} \oplus R {- 1, 3}$ , and the two components of $χ_{0}$ are $U_{0}^{0} = (\begin{array}{cc} x_{4} - x_{2} & 0 \\ 0 & 1 \end{array}), U_{0}^{1} = (\begin{array}{cc} x_{4} & - x_{2} \\ - 1 & 1 \end{array}) .$ The negative crossing complex is the analogous two-term complex of $χ_{1}$ with the ${0, - 2}$ shift of The positive and negative Khovanov-Rozansky crossing complexes; written side by side with the positive one, the shift asymmetry is visible: the positive complex shifts the source by ${0, 2}$ and nothing else, while the negative complex applies the overall shift ${0, - 2}$ to both terms.

Caveat: the source's arXiv prose misprints the negative crossing in terms of $χ_{0}$ ; this example uses the corrected $χ_{1}$ complex of The positive and negative Khovanov-Rozansky crossing complexes (Khovanov-Rozansky II, Figure 6 and formula (6); published formula (13)).

Facts & Assumptions

Given: the ring $R = Q [a, x_{1}, x_{2}, x_{3}, x_{4}]$ , the two resolutions $Γ_{0}$ (two arcs) and $Γ_{1}$ (one wide edge), their presentation matrices $P_{0}, P_{1}, Q_{0}, Q_{1}$ with the displayed shifts, and the morphism matrices $U_{0}^{0}, U_{0}^{1}$ of $χ_{0}$ .

[F1]

$C (Γ_{0})$ is the tensor product of the arc rows $(a, x_{1} - x_{4})$ and $(a, x_{2} - x_{3})$ , $C (Γ_{1})$ is the tensor product of the rows $(a, x_{1} + x_{2} - x_{3} - x_{4})$ and $(0, x_{1} x_{2} - x_{3} x_{4})$ , and both have potential $w = a (x_{1} + x_{2} - x_{3} - x_{4})$ (The factorization of a marked MOY graph).

[F2]

$χ_{0}$ is a morphism of factorizations of bidegree $(0, 2)$ ; $χ_{1}$ is a morphism of bidegree $(0, 0)$ ; the positive crossing complex is the cone of $χ_{0}$ with the source shifted by ${0, 2}$ , and the negative crossing complex is the cone of $χ_{1}$ with the overall shift ${0, - 2}$ (The wide-edge morphisms chi-zero and chi-one, The positive and negative Khovanov-Rozansky crossing complexes).

Verification

technique · direct transcription with the two matrix verifications that make each presentation a factorization of potential $w$

1.1F1algebra

The products are factorizations. Multiplying out over $R$ gives $P_{1} P_{0} = (\begin{matrix} a (x_{1} + x_{2} - x_{3} - x_{4}) & 0 \\ 0 & a (x_{1} + x_{2} - x_{3} - x_{4}) \end{matrix}) = w \cdot I_{2}$ and $Q_{1} Q_{0} = (\begin{matrix} w & 0 \\ 0 & w \end{matrix}) = w \cdot I_{2}$ , because the off-diagonal entries $(x_{1} - x_{4}) (x_{3} - x_{2}) + (x_{2} - x_{3}) (x_{1} - x_{4})$ and $(x_{1} + x_{2} - x_{3} - x_{4}) (x_{3} x_{4} - x_{1} x_{2}) + (x_{1} x_{2} - x_{3} x_{4}) (x_{1} + x_{2} - x_{3} - x_{4})$ vanish; hence both presentations are factorizations with potential $w$ , in accordance with [F1].

1.2F2algebra

The morphism and its bidegree. The matrix products $Q_{0} U_{0}^{0} = U_{0}^{1} P_{0}$ and $Q_{1} U_{0}^{1} = U_{0}^{0} P_{1}$ of the definition of $χ_{0}$ show that the displayed $U$ matrices commute with the differentials, and the entries $x_{4}, - x_{2}$ and the shifts $R {- 1, 1} \to R {- 1, 3}$ , $R {- 2, 2} \to R {- 2, 4}$ combine to bidegree $(0, 2)$ ; on the source shifted by ${0, 2}$ the differential has bidegree $(0, 0)$ .

2.1F1F2step 1.2∎

The two complexes side by side. The positive complex has terms $C (Γ_{0}) {0, 2}$ in degree $- 1$ and $C (Γ_{1})$ in degree $0$ with differential $χ_{0}$ , and the negative complex has terms $C (Γ_{1}) {0, - 2}$ in degree $0$ and $C (Γ_{0}) {0, - 2}$ in degree $1$ with differential $χ_{1}$ ; in both cases the differential is a morphism of factorizations of bidegree $(0, 0)$ on the shifted terms by step 1.2 and [F2], so each displayed two-term complex is a complex of objects of ${h m f}_{w}$ . The shift asymmetry is exactly the one recorded in The positive and negative Khovanov-Rozansky crossing complexes: ${0, 2}$ on the positive source versus the overall ${0, - 2}$ normalization on the negative complex.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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.