ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (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.

Writhe normalization cancels a ribbon kink

Example

Assume the Axiom of Choice. In the ribbon category of $Z / 2$ -graded finite-dimensional vector spaces over a field $k$ of characteristic $\neq 2$ with the sign braiding and the parity twist, let $X$ be the odd one-dimensional object, so $λ = θ_{X} = - 1$ and $d_{X} = {Tr}_{L} (j_{X}) = 1$ . For $β = e \in B_{1}$ and its positive stabilization $σ_{1} \in B_{2}$ , The scalar twist controls the two Markov stabilizations gives $t_{1} (e) = 1$ and $t_{2} (σ_{1}) = (- 1) t_{1} (e) = - 1$ , so the unnormalized values differ by the factor $λ^{- 1} = - 1$ . The exponent sums are $w (e) = 0$ and $w (σ_{1}) = 1$ (Exponent sum and writhe of a braid), so the normalized values

$J_{X} (\hat{e}) = λ^{- 0} t_{1} (e) = 1, J_{X} (\hat{σ_{1}}) = λ^{- 1} t_{2} (σ_{1}) = (- 1)^{- 1} \cdot (- 1) = 1$

agree: the writhe factor cancels the kink and produces the invariant of the unframed unknot predicted by The writhe-normalized ribbon trace is an unframed link invariant. The common value is $1$ here; since $d_{X} = 1$ is a unit, the further normalization $d_{X}^{- 1} J_{X}$ is trivial and also gives $1$ on the unknot.

Facts & Assumptions

Given: AC; the field $k$ with $char k \neq 2$ ; the category of $Z / 2$ -graded finite-dimensional vector spaces with the sign braiding and the parity twist; its odd one-dimensional object $X$ ; the braid $e \in B_{1}$ and its positive stabilization $σ_{1} \in B_{2}$ .

[L1]

The model is a ribbon category with $End (1) = k$ and $X$ absolutely simple, $θ_{X} = λ {id}_{X}$ , so the stabilization lemma gives $t_{n + 1} (ι_{n} (β) σ_{n}^{\pm 1}) = λ^{\pm 1} t_{n} (β)$ ; that lemma is stated under countable choice, which AC supplies here (AC implies DC implies countable choice); in this model $λ = - 1$ and the odd line has $d_{X} = {Tr}_{L} (j_{X}) = 1$ , so $t_{1} (e) = 1$ and $t_{2} (σ_{1}) = - 1$ (The scalar twist controls the two Markov stabilizations, Absolutely simple objects).

[F1]

A ribbon twist satisfies balancing and dual-compatibility (Twist and ribbon structure); the Drinfeld composite and left trace are those of A braided rigid category has a Drinfeld morphism and The categorical trace of a morphism into the double dual.

[F2]

The trivial one-braid closes to the unknot, and stabilization preserves its oriented closure under countable choice (The closure of a geometric braid, Markov moves preserve the oriented closure up to isotopy). AC supplies that choice assumption as recorded in [L1].

[L2]

The exponent sum satisfies $w (σ_{1}) = w (ι_{1} (e) σ_{1}) = w (e) + 1 = 1$ and $w (e) = 0$ (Exponent sum and writhe of a braid); the positive stabilization is $β \mapsto ι_{n} (β) σ_{n}$ (Markov conjugation and stabilization moves).

[L3]

Assume AC: the writhe-normalized trace $J_{X} (\hat{β}) = λ^{- w (β)} t_{n} (β)$ is an invariant of oriented unframed link types of closures (The writhe-normalized ribbon trace is an unframed link invariant, The Axiom of Choice).

Verification

1.1F1givenalgebra

Verify the model and dimension. Even linear maps and graded duals give the rigid $k$ -linear category, with the ordinary evaluation and basis coevaluation satisfying the zig-zags. The sign braiding is natural; its hexagons are $(- 1)^{p (q + r)} = (- 1)^{p q} (- 1)^{p r}$ and the analogous identity in the first variable, and its square is the identity. Parity is natural, multiplicative on tensor products and unchanged on duals, so it is a ribbon twist by [F1]. The odd line has only scalar endomorphisms and twist $- 1$ . For a dual basis $e, e^{\lor}$ , the Drinfeld composite gives $u_{X} (e) = - e^{\lor \lor}$ , hence $j_{X} (e) = e^{\lor \lor}$ ; coevaluation $1 \mapsto e \otimes e^{\lor}$ and evaluation $e^{\lor \lor} \otimes e^{\lor} \mapsto 1$ give $d_{X} = 1$ .

1.2L2given

The writhe exponents. The trivial one-braid has exponent sum $w (e) = 0$ , and its positive stabilization $σ_{1}$ has $w (σ_{1}) = 1$ by [L2].

2.1L1L2F2step 1.1given

The unnormalized values and the kink. By [L1], $t_{1} (e) = 1$ and $t_{2} (σ_{1}) = λ t_{1} (e) = - 1$ . By [F2], the closures both represent the unknot, so the unnormalized evaluation changes by the factor $- 1$ under the positive stabilization, the kink contribution modelled by the scalar twist $λ = - 1$ .

3.1L3step 2.1step 1.2algebra

The normalized values agree. Substituting steps 2.1 and 1.2, $J_{X} (\hat{e}) = λ^{- w (e)} t_{1} (e) = (- 1)^{0} \cdot 1 = 1, J_{X} (\hat{σ_{1}}) = λ^{- w (σ_{1})} t_{2} (σ_{1}) = (- 1)^{- 1} \cdot (- 1) = 1.$ The two normalized values are equal, in accordance with [L3].

4.1step 2.1step 1.2step 3.1∎

Conclusion. The writhe factor $λ^{- w}$ cancels exactly the kink contribution $λ$ contributed by the stabilization, so the normalized evaluation is the same on the closure of $e$ and on its positive stabilization, as the invariant theorem predicts; the common value is $1$ , and the dimension normalization by $d_{X} = 1$ is trivial here. All computations are finite; the Axiom of Choice is assumed through [L3] and supplies the countable-choice input to [L1], as recorded there.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

44 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

P. Etingof, S. Gelaki, D. Nikshych, and V. Ostrik, Tensor Categories (AMS Mathematical Surveys and Monographs 205), author's final version (standard reference, not scraped)