Alphabeta Math
LemmaStatement: Literature-sourcedProof: 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.

Framed oriented tangles have the ribbon generator-and-relation presentation

Statement

Assume ACω (The Axiom of Countable Choice (ACω)). Every morphism of the framed oriented tangle category T of The framed oriented tangle category is a finite composite of tensor products of identities, crossings, cups, caps and full twists.

A complete presentation on this elementary family is Turaev's reduced presentation (3.1.a), (3.2.a)--(3.2.h), together with the expressions (2.5.d)--(2.5.e) and (3.1.b)--(3.1.c) defining its additional orientation variants. Thus two elementary words represent the same framed tangle exactly when these relations and the strict monoidal axioms relate them.

Here the source's Xδ denotes our X+,+δ, its Zδ denotes our X+,−−δ, and its Yδ denotes our X−,+−δ; its Tδ denotes our X−,−δ. The source's positive cup and cap are ∪+ and ∩+, and its φ,φ′ are φ++,φ+−. The reduced generators are therefore X+,+δ, X+,−−δ, φ+±1, ∪+ and ∩+. The other cups, caps and crossings are the expressions above; a twist on a negative strand is obtained by bending the corresponding twisted positive strand with a cup and cap. Turaev's convention that a positive strand points downwards is transported to ours by reversing all strand orientations; this preserves composition, tensor product and framed isotopy. Crossing superscripts in his mixed-orientation pictures are oriented signs, explaining the minus signs in the dictionary.

The reduced relations are Yang--Baxter, the two zig-zags, inverse crossings and twists, curl slide, the bent-crossing inverse relation (3.2.g), and the twist-square relation (3.2.h). For example, the latter has the well-typed form

(φ++)2=(∩+⊗1+)(1−⊗X+,++)(X+,−−⊗1+)(∪+⊗1+).

Facts & Assumptions

Given: ACω and the category T with its fixed framing and crossing conventions.

[L1]

The objects, elementary tangles, composition, tensor product and boundary-relative framed isotopies are those of The framed oriented tangle category.

[F1]

Turaev, Chapter I, Lemma 3.1.1 and formulas (2.5.d)--(2.5.e), (3.1.b)--(3.1.c), printed pp. 40, 49--50, express every elementary orientation variant in the reduced generators (3.1.a). Lemma 3.3, printed p. 51, proves completeness of (3.2.a)--(3.2.h) for that reduced family. Its proof in §§4.1--4.8, printed pp. 57--69, treats diagrams in the strip relative to its boundary: it checks the oriented second and third Reidemeister moves, changes of height position, and insertion/deletion of a positive-negative curl pair. It does not allow deletion of a single curl.

[F2]

Turaev, Chapter I §2.1, printed pp. 34--35, identifies ribbon bands and annuli with homotopy classes of normal framings; Figure 2.3 turns a signed full twist into the corresponding blackboard curl.

Proof

technique · direct
1.1L1F1F2givenconstruct

Match the models. Thicken a framed core to a sufficiently narrow band, choosing the transverse band direction from its oriented tangent and normal framing. Conversely take the oriented core and surface normal of a band. Homotopies of the framing give isotopies of the narrow bands, relative to the collars; taking cores reverses this construction on isotopy classes. The compact tangle lies a positive distance from the side faces, so the thickness can be chosen uniformly small. This is the ribbon/framing correspondence of [F2], with fixed collars at open ends. Reverse all strand orientations to match the source's endpoint convention and use the displayed crossing dictionary. It identifies our model with the single-color, coupon-free case of [F1].

2.1F1step 1.1construct

Generate and remove redundant generators. By [F1], a generic diagram has finitely many crossing and extremum levels. Cutting between them gives a word in elementary tangles; the source's formulas express its orientation variants in the reduced family. Conversely these formulas represent the indicated elementary tangles by boundary-relative band isotopies. Thus every elementary word can be replaced by a reduced word without changing its morphism.

3.1F1F2step 1.1step 2.1∎

Soundness and completeness. The source checks each reduced relation by a band isotopy, and its complete boundary-relative proof in [F1] shows that equal reduced words are related by those relations and the strict monoidal axioms. Apply step 2.1 to any two equal elementary words, apply that completeness theorem to the resulting reduced words, and undo the replacements. This proves completeness for the enlarged family; soundness follows from the same isotopies. The assumed countable choice is available for the generic-position input. No inference from an unframed closed-link move theorem to a framed boundary-relative theorem is required.

Depends on

Used by

Dependency tree · two levels

9 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