ExampleConstruction: Literature-sourcedVerification: 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.

Normalized comparison maps around a relation loop

Example

Take the braid $v = σ_{1} σ_{2} σ_{1} = σ_{2} σ_{1} σ_{2} \in B_{3}$ and three signed words representing it, for instance $t = (1, 2, 1)$ and $w = (2, 1, 2)$ , together with the word $u = (1, 2, 1, 2, 2^{- 1})$ obtained from $t$ by appending a cancelling pair; the three normalized maps $γ_{t, u}, γ_{u, w}, γ_{t, w}$ form a loop in the expression graph, and the example verifies $γ_{u, w} \circ γ_{t, u} = γ_{t, w}$ by computing the three derived images $c_{t, u}, c_{u, w}, c_{t, w}$ and checking $c_{u, w} c_{t, u} = c_{t, w}$ in ${Hom}_{D^{b}} (R_{π (v)} (- 3), R_{π (v)} (- 3)) = Q \cdot i d$ . Here $π (v) = s_{1} s_{2} s_{1} \in S_{3}$ is the permutation projection and the common internal shift is $(- 3)$ , since every word has signed exponent $3$ . The two comparison composites are displayed and each has its unique normalized degree-zero lift.

Facts & Assumptions

Given: The three signed words $t = (1, 2, 1)$ , $u = (1, 2, 1, 2, 2^{- 1})$ , $w = (2, 1, 2)$ of $B_{3}$ , their word complexes, and the normalized maps $γ$ and derived comparisons $c$ of Derived comparisons give unique normalized homotopy maps and Canonical comparisons between standard graph tensor products.

[F1]

Same braid. $t$ , $u$ and $w$ all represent the braid $v = σ_{1} σ_{2} σ_{1} = σ_{2} σ_{1} σ_{2}$ ; $u$ is obtained from $t$ by adjoining the letters $σ_{2} σ_{2}^{- 1}$ , whose product is the identity, so the product of $u$ is $v$ ; the equality $t = w$ is an Artin relation (The braid group by Artin presentation). The graph word tensors use their permutation projections and the comparison system of Canonical comparisons between standard graph tensor products.

[F2]

Uniqueness and dimension. For any two of these words, the homotopy Hom space is one-dimensional in internal degree $0$ and the homotopy comparison is the unique element lifting the derived map $c$ . (Derived comparisons give unique normalized homotopy maps)

[F3]

Transitivity. $γ_{u, w} γ_{t, u} = γ_{t, w}$ and, in the derived category, $c_{u, w} c_{t, u} = c_{t, w}$ . (Normalized comparison isomorphisms are transitive, Canonical comparisons between standard graph tensor products)

Verification

technique · direct

1.1F1F2

The three words represent the same braid by [F1], so the three maps $γ_{t, u}, γ_{u, w}, γ_{t, w}$ are defined as elements of one-dimensional degree-zero homotopy Hom spaces; their derived images are the comparisons $c_{t, u}, c_{u, w}, c_{t, w}$ , each obtained by composing the multiplication maps from the shifted graph word tensors through $R_{π (v)} (- 3)$ .

2.1F1F2F3step 1.1algebra

Let $M_{t}, M_{u}, M_{w}$ be the three tensor graph models and $μ_{a} : M_{a} \to R_{π (v)} (- 3)$ their iterated multiplication maps, with shifts adding to $(- 3)$ . The cancelling pair in $u$ contributes $R_{s_{2}} (- 1) \otimes_{R} R_{s_{2}} (1) ≅ R$ , by $b \otimes c \mapsto b s_{2} (c)$ , and its inverse sends $1 \mapsto 1 \otimes 1$ . Thus the typed comparisons are $c_{t, u} = μ_{u}^{- 1} μ_{t} : M_{t} \to M_{u}$ , $c_{u, w} = μ_{w}^{- 1} μ_{u} : M_{u} \to M_{w}$ and $c_{t, w} = μ_{w}^{- 1} μ_{t} : M_{t} \to M_{w}$ . In particular $c_{u, w} c_{t, u} = μ_{w}^{- 1} μ_{u} μ_{u}^{- 1} μ_{t} = μ_{w}^{- 1} μ_{t} = c_{t, w}, c_{w, t} c_{t, w} = μ_{t}^{- 1} μ_{w} μ_{w}^{- 1} μ_{t} = 1_{M_{t}} .$ Transporting each comparison by its source and target multiplication maps gives the identity of the common graph model.

3.1F2F3step 2.1∎

Since $c_{u, w} c_{t, u} = c_{t, w}$ by step 2.1 and the derived images of the two sides of the claim are these comparisons, and since the homotopy Hom space is one-dimensional in degree $0$ by [F2], the composite $γ_{u, w} γ_{t, u}$ has the same derived image as $γ_{t, w}$ and therefore coincides with it. The two displayed composites therefore have the asserted unique normalized degree-zero lifts.

Remarks

The loop is nondegenerate: the three words are pairwise distinct, and $u$ differs from $t$ by a cancelling pair rather than being equal to it, so the composites displayed are computed by nontrivial comparisons. The identity obtained after transporting $c_{t, u}$ to the common graph model and the typed equality $c_{u, w} c_{t, u} = c_{t, w}$ are the worked special case of the comparison system's transitivity.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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

Raphaël Rouquier, Categorification of the braid groups, arXiv:math/0409593v1 (30 September 2004), §3 "The 2-braid group" (standard reference, not scraped)