Alphabeta Math
TheoremStatement: 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.

The ribbon evaluation is an invariant of framed colored links

Statement

Assume ACω (The Axiom of Countable Choice (ACω)). Let C be a ribbon category and X∈C. If β∈Bn and β′∈Bn′, with n,n′≥1, are braids whose blackboard-framed X-colored closures are isotopic as framed oriented tangles, then

tn(β)=tn′(β′)

in End⁡C(1). More generally, t is an invariant of framed X-colored links: the value tn(β) depends only on the framed isotopy class of the closure of β. Ordinary Markov stabilization is not a framed isotopy: it inserts a curl and is handled only after writhe normalization.

Facts & Assumptions

Given: ACω; a ribbon category C, an object X, braids β∈Bn and β′∈Bn′ whose blackboard-framed X-colored closures are isotopic as framed oriented tangles.

[L1]

The ribbon evaluation equals the evaluation of the blackboard-framed closure: tn(β)=FX(β^fr), and the same for β′; moreover the closure of the stabilized braid ιn(β)σn±1 is the closure of β with one full twist added on a band (The ribbon trace equals the framed-closure evaluation).

[L2]

The tangle evaluation functor assigns equal values to isotopic framed tangles: isotopic framed tangles are equal morphisms of the framed oriented tangle category, and a functor preserves equalities (A ribbon object defines a unique framed-tangle evaluation functor).

Proof

technique · direct
1.1L1L2given

The two evaluations agree. By [L1] tn(β)=FX(β^fr) and tn′(β′)=FX(β′^fr). The closures are isotopic framed oriented tangles by hypothesis, so by [L2] their values under FX are equal. Hence tn(β)=tn′(β′).

1.2L1given

The framing changes under stabilization. By [L1], stabilization inserts one signed full twist. A framing number is the linking number of a component with its normal push-off; a full twist changes that number by ±1 (Turaev, Chapter I §2.1, printed pp. 34--35). The sum of component framing numbers is preserved by framed isotopy, including permutation of components, and changes by ±1 here. Thus stabilization is not a framed isotopy. Its evaluations can nevertheless coincide in a particular category; the functorial invariance alone gives no stabilization identity.

2.1L1L2step 1.1construct

Framed-link invariance. On any closed framed X-colored tangle L, define its evaluation to be FX(L). By [L2] this is a framed-isotopy invariant, and [L1] identifies it with tn(β) whenever L is the blackboard-framed closure of β. On the empty tangle the strict-model evaluator is the identity of the unit, agreeing with t0(e). This constructs the general evaluation without assuming that every framing has a blackboard-braid representative.

3.1step 1.1step 2.1step 1.2∎

Conclusion. Steps 1.1--1.2 give the framed-isotopy invariance of the ribbon evaluation, and step 1.2 records that ordinary Markov stabilization changes the framing and lies outside this statement. The only choice principle used is ACω, consumed through the closure comparison of [L1] and the functor FX of [L2]; the final comparison of the two values is then functoriality of FX applied to equal morphisms.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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