ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (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.

A birth followed by a merging saddle

Example

Let $A = Z [X] / (X^{2})$ be the Frobenius algebra with unit $η (1) = 1$ and multiplication $m$ . In the algebraic TQFT, consider the movie that first creates a disjoint circle and then attaches a saddle band merging that circle with one existing circle. The induced local map is

A \overset{{id}_{A} \otimes η}{\to} A \otimes A \overset{m}{\to} A,

and this composite is the identity on $A$ .

The diagram records the two successive surface events; it is only a description of the movie, while the verification below is algebraic.

diagram failed to render:
\begin{tikzcd}
\mathcal A
\arrow[r, "{\operatorname{id}\otimes\eta}"]
& \mathcal A\otimes\mathcal A
\arrow[r, "m"]
& \mathcal A
\end{tikzcd}

Example references

The integral Frobenius algebra and local cobordism maps

Khovanov, A categorification of the Jones polynomial, §7

Bar-Natan, Khovanov's homology for tangles and cobordisms, §§7–8

Kauffman, An Introduction to Khovanov Homology, §5

Facts & Assumptions

Given: The rank-two algebra $A = Z [X] / (X^{2})$ , its unit $η (1) = 1$ , and its merge map $m$ .

[F1]

Khovanov Frobenius algebra and cube of resolutions gives the basis ${1, X}$ , the unit $1 \mapsto 1$ , and multiplication $m (a \otimes 1) = a$ for $a \in A$ .

Proof

1.1F1constructalgebra

On the basis element $1$ , $(id \otimes η) (1) = 1 \otimes 1$ , so $m (id \otimes η) (1) = m (1 \otimes 1) = 1$ . On the basis element $X$ , $(id \otimes η) (X) = X \otimes 1$ , so $m (id \otimes η) (X) = m (X \otimes 1) = X$ .

2.1step 1.1algebra∎

The two basis elements generate $A$ as an abelian group, and both are fixed by the composite in step 1.1. By linearity the composite fixes every element of $A$ , hence equals ${id}_{A}$ .

Depends on

Khovanov Frobenius algebra and cube of resolutions

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

Mikhail Khovanov, A categorification of the Jones polynomial, §7 (standard reference, not scraped)
Dror Bar-Natan, Khovanov's homology for tangles and cobordisms, §§7–8 (standard reference, not scraped)
Louis H. Kauffman, An Introduction to Khovanov Homology, §5 (standard reference, not scraped)